The phase-one left endpoint through the six-term cohomology sequence

This file owns the analytically expensive step of the subadditivity chain: the comparison for a distinguished triangle whose left endpoint lies in P(1). The argument runs the six-term H⁰ sequence, first at the level of the shifted homological functor and then transported along the canonical heartCoh identifications, and reduces a bounded-amplitude object to that window.

It is isolated because its elaboration cost dominates the module; consumers that need only the final inequalities import Consequences.

theorem CategoryTheory.Triangulated.stabilityMass_H0FunctorShift_negOne_zero_triangle_le_of_obj₁_phase_one {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : σ.slicing.P 1 T.obj₁) : (stabilityMass σ (((Tilting.originalHeartCohFunctor (Slicing.toTStructure C σ.slicing) 0).shift (-1)).obj T.obj₂).obj).toReal + (stabilityMass σ (((Tilting.originalHeartCohFunctor (Slicing.toTStructure C σ.slicing) 0).shift 0).obj T.obj₂).obj).toReal ≤ (stabilityMass σ T.obj₁).toReal + ((stabilityMass σ (((Tilting.originalHeartCohFunctor (Slicing.toTStructure C σ.slicing) 0).shift (-1)).obj T.obj₃).obj).toReal + (stabilityMass σ (((Tilting.originalHeartCohFunctor (Slicing.toTStructure C σ.slicing) 0).shift 0).obj T.obj₃).obj).toReal)

The six-term comparison at the level of the shifted homological functor. Keeping this categorical construction separate from the canonical heartCoh identifications substantially reduces elaboration cost for the public cohomology comparison below.

theorem CategoryTheory.Triangulated.stabilityMass_heartCoh_negOne_zero_triangle_le_of_obj₁_phase_one {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : σ.slicing.P 1 T.obj₁) : (stabilityMass σ (Tilting.originalHeartCoh (Slicing.toTStructure C σ.slicing) (-1) T.obj₂).obj).toReal + (stabilityMass σ (Tilting.originalHeartCoh (Slicing.toTStructure C σ.slicing) 0 T.obj₂).obj).toReal ≤ (stabilityMass σ T.obj₁).toReal + ((stabilityMass σ (Tilting.originalHeartCoh (Slicing.toTStructure C σ.slicing) (-1) T.obj₃).obj).toReal + (stabilityMass σ (Tilting.originalHeartCoh (Slicing.toTStructure C σ.slicing) 0 T.obj₃).obj).toReal)

The six-term cohomology comparison for a phase-one source. This is the homological core of the semistable-left argument, stated before the ambient objects are reassembled from their two nonzero cohomology degrees.

theorem CategoryTheory.Triangulated.stabilityMass_triangle_le_of_obj₁_phase_one_of_amplitude {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : σ.slicing.P 1 T.obj₁) (hEgt : Slicing.gtProp C σ.slicing 0 T.obj₂) (hEle : Slicing.leProp C σ.slicing 2 T.obj₂) (hFgt : Slicing.gtProp C σ.slicing 0 T.obj₃) (hFle : Slicing.leProp C σ.slicing 2 T.obj₃) : (stabilityMass σ T.obj₂).toReal ≤ (stabilityMass σ T.obj₁).toReal + (stabilityMass σ T.obj₃).toReal

The semistable-left comparison on the two-cohomology window (0, 2]. After rotating the semistable source to phase one, the unconditional homological H⁰ functor gives the six-term exact sequence

0 ⟶ H⁻¹(E) ⟶ H⁻¹(F) ⟶ H⁰(A) ⟶ H⁰(E) ⟶ H⁰(F) ⟶ 0.

Its image factorisations give short exact sequences with the common phase-one kernel/image decomposition of H⁰(A). The negative-degree sequence is controlled by the boundary-heart polygon inequality, the degree-zero sequence by the phase-one extension comparison, and exact same-ray additivity reassembles the source mass.