The weak cutoff bounds the object's own slope, not only its factors' slopes

hnTors W μ₀ and hnFree W μ₀ are defined by the Harder--Narasimhan extrema μ⁻ and μ⁺. Every consumer that wants to read a cutoff against a charge needs the object's own slope instead, and the step between them is that W.slope E lies between μ⁻ and μ⁺.

This is CutoffPhase.lean for the weak, slope-indexed theory.

Why this is not the strict proof

CutoffPhase.lean gets the strict statement from HNPolygon.lean's phase_le_first and last_le_phase, which read the HN filtration as a convex polygonal path in ℂ and cite ComplexPolygonalPath.arg_last_sub_zero_le_arg_first. That apparatus is arg-geometry on semiClosedUpperHalfPlane and does not survive the weakening: the charges here may be 0, where arg says nothing.

The weak statement instead falls straight out of the see-saw of WeakSlopeGeometry.lean, by induction along the chain. Each step adds one factor charge to the running total, and the see-saw traps the new slope between the factor's slope and the old total's — so μ⁺ is never exceeded above and the current factor's slope is never dropped below. No polygon, and no convexity argument.

One thing makes this easier than the strict case rather than harder: 0 ∈ closedUpperHalfPlane, so charge_mem_closedUpperHalfPlane holds for every object including the zero one, and the induction carries no nonvanishing side conditions. In the strict theory that membership fails at 0 and the bookkeeping is real.

The payoff

lt_slope_of_mem_hnTors and slope_le_of_mem_hnFree are what a charge comparison consumes, and unlike their strict counterparts they carry no positive-rank hypothesis: a rank-zero object has slope ⊤, which is above every finite cutoff, so it needs no separate treatment. On the strict side that object has to be routed around through mem_hnTors_of_rank_zero instead.

theorem CategoryTheory.Triangulated.chargeSlope_add_mem_uIcc {z w : ℂ} (hz : z ∈ closedUpperHalfPlane) (hw : w ∈ closedUpperHalfPlane) : min (chargeSlope z) (chargeSlope w) ≤ chargeSlope (z + w) ∧ chargeSlope (z + w) ≤ max (chargeSlope z) (chargeSlope w)

The slope of a sum lies between the slopes of its summands. The two see-saws combined by le_total, in the form an induction over a filtration consumes.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.charge_mem_closedUpperHalfPlane {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) (E : A) : W.charge E ∈ closedUpperHalfPlane

Every object's charge lies in the closed upper half-plane, the zero object included: its charge is 0, which the closed half-plane contains and the semi-closed one does not. This is the hypothesis-free membership the strict theory cannot have.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.charge_chain_succ {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (j : Fin F.n) : W.charge (Subobject.underlying.obj (F.chain j.succ)) = W.charge (Subobject.underlying.obj (F.chain j.castSucc)) + W.charge (F.factor j)

Each chain step is a short exact sequence with the corresponding factor as its cokernel, so the charges add.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μ_le_slope_chain_and_le_μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hk : 0 < k) (hkn : k ≤ F.n) : F.μ ⟨k - 1, ⋯⟩ ≤ W.slope (Subobject.underlying.obj (F.chain ⟨k, ⋯⟩)) ∧ W.slope (Subobject.underlying.obj (F.chain ⟨k, ⋯⟩)) ≤ F.μPlus

The running total of an HN filtration stays inside the slope range.

Induction along the chain. At k = 1 the term is the maximal destabilizing subobject, whose slope is μ⁺ exactly. Each further step adds the next factor, whose slope is below everything already accumulated, so the see-saw puts the new total between that factor's slope and the old total's.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.slope_le_μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : W.slope E ≤ F.μPlus

The object's own slope does not exceed the highest HN slope.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μMinus_le_slope {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : F.μMinus ≤ W.slope E

The lowest HN slope does not exceed the object's own slope.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.lt_slope_of_mem_hnTors {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} (hHN : W.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (h : E ∈ W.hnTors μ₀) : μ₀ < W.slope E

An object of the torsion class has slope strictly above the cutoff.

hnTors says every HN slope exceeds μ₀; this says the object's own does. The zero object is excluded because it has no filtration — hnTors admits it separately.

Unlike SlopeData.slopeOfPhase_lt_of_mem_hnTors, there is no positive-rank hypothesis: a rank-zero object has slope ⊤, above every finite cutoff, and is covered by the same statement.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_le_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} (hHN : W.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (h : E ∈ W.hnFree μ₀) : W.slope E ≤ μ₀

An object of the torsion-free class has slope at most the cutoff.