The cutoff bounds the object's own phase, not only its factors' phases

hnTors Z β and hnFree Z β are defined by the Harder–Narasimhan extrema φ⁻ and φ⁺. Every consumer that wants to read a cutoff against a charge needs the object's own phase instead, and the step between them is the statement that Z.phase E lies between φ⁻ and φ⁺.

That statement is already proved. HNPolygon.lean has it as AbelianHNFiltration.phase_le_first and AbelianHNFiltration.last_le_phase, stated with the extremal indices written out rather than as φ⁺ and φ⁻ — the HN polygon's first and last edges — which is why it does not surface when one greps HarderNarasimhan.lean for a bound on Z.phase E. This file names them in the φ± vocabulary and draws the two cutoff corollaries.

Why this matters for Bridgeland's Lemma 6.2

Cases 1--3 of #740 conclude Im Z(β,ω) > 0 from an object being in the torsion class at the cutoff. Im Z is a statement about the object, so "all HN phases exceed β" has to become "this object's phase exceeds β" first. lt_phase_of_mem_hnTors is that step, and it is the whole categorical content of it — what remains after this is the translation from a phase inequality to a slope inequality, which is Slope.lean's phase_le_iff_slope_le and is not here.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.phiMinus_le_phase {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) : F.phiMinus ≤ Z.phase E

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

last_le_phase with the extremal index named. The two statements are the same term: phiMinus is by definition the phase at index n - 1.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.phase_le_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) : Z.phase E ≤ F.phiPlus

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

theorem CategoryTheory.Triangulated.StabilityFunction.lt_phase_of_mem_hnTors {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} (hHN : Z.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (h : E ∈ Z.hnTors β) : β < Z.phase E

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

hnTors says every HN phase exceeds β; this says the object's own phase does. The zero object is excluded because it has no phase to speak of — hnTors admits it separately.

theorem CategoryTheory.Triangulated.StabilityFunction.phase_le_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} (hHN : Z.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (h : E ∈ Z.hnFree β) : Z.phase E ≤ β

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

theorem CategoryTheory.Triangulated.SlopeData.slopeOfPhase_lt_of_mem_hnTors {A : Type u} [Category.{v, u} A] [Abelian A] (D : SlopeData A) (hHN : D.toStabilityFunction.HasHNProperty) {E : A} (hE : 0 < D.rank E) {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) (h : E ∈ D.toStabilityFunction.hnTors β) : slopeOfPhase β < D.slope E

The torsion class at a phase cutoff, read as a slope bound.

The composite of lt_phase_of_mem_hnTors with lt_phase_iff_slopeOfPhase_lt, and the statement cases 1--3 of Bridgeland's Lemma 6.2 actually consume: an object of the torsion class, of positive rank, has slope strictly above the cutoff's slope. From there Mukai.im_expCharge_pos puts the charge in the open upper half plane.

Rank zero is excluded here and handled by mem_hnTors_of_rank_zero instead — a rank-zero object has phase one and no slope, so it belongs to every T β for arithmetic reasons rather than by any comparison.

theorem CategoryTheory.Triangulated.SlopeData.slope_le_slopeOfPhase_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] (D : SlopeData A) (hHN : D.toStabilityFunction.HasHNProperty) {E : A} (hE : 0 < D.rank E) {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) (h : E ∈ D.toStabilityFunction.hnFree β) : D.slope E ≤ slopeOfPhase β

The torsion-free class, dually.