Owner HN existence by highest-phase reduction

The strict MDQ construction is iterated on its kernels. A bound on the highest old phase is preserved by the kernel triangles and supplies the upper skewed-phase estimate required at every recursive call.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_lt_of_phiPlus_lt (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {a b ε : ℝ} (hab : a < b) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthin : b - a + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (hwide : 6 * ε ≤ b - a) {E : C} (hE : ¬Limits.IsZero E) (hI : Slicing.intervalProp C σ.slicing a b E) (hplus : Slicing.phiPlus C σ.slicing E hE < b - 4 * ε) : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase E < b - 3 * ε

A φ⁺ < b - 4ε bound forces the midpoint-branch skewed phase below b - 3ε.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_gt_of_strictQuotient_inner (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {a b ε : ℝ} (hab : a < b) [Fact (a < b)] [Fact (b - a ≤ 1)] (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthin : b - a + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) {X B : Slicing.IntervalCat C σ.slicing a b} (hInner : Slicing.intervalProp C σ.slicing (a + 2 * ε) (b - 4 * ε) X.obj) (q : X ⟶ B) (hq : IsStrictEpi q) (hB : ¬Limits.IsZero B.obj) : a + ε < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase B.obj

A nonzero strict quotient of an object in the inner strip has skewed phase above the lower enveloping boundary.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hn_exists_with_phiPlus_reduction (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {a b ε : ℝ} (hab : a < b) [Fact (a < b)] [Fact (b - a ≤ 1)] (hFinite : WeakStabilityCondition.StabilityCondition.Deformation.ThinStrictFiniteLength C σ a b) {L U : ℝ} (hWindow : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Y.obj → L < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase Y.obj ∧ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase Y.obj < U) (hWidth : U - L < 1) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hthin : b - a + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (hL_a : a ≤ L + ε) (hwide : 6 * ε ≤ b - a) (t : ℝ) (ht : a + ε ≤ t) (X : Slicing.IntervalCat C σ.slicing a b) (hX : ¬Limits.IsZero X) (hquot : ∀ (A : Subobject X), A ≠ ⊤ → IsStrictMono A.arrow → t < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase (Limits.cokernel A.arrow).obj) (hplusX : ∀ (hXobj : ¬Limits.IsZero X.obj), Slicing.phiPlus C σ.slicing X.obj hXobj < b - 4 * ε) : have F := WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab; have Psem := fun (ψ : ℝ) (E : C) => F.IsSemistable E ψ; ∃ (G : HNFiltration C Psem X.obj), ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < U

Iterating the owner two-branch MDQ construction produces an HN filtration above the explicit quotient lower bound.