The slope drops strictly on the quotient by the maximal destabilizing subobject

This is the step that makes Harder–Narasimhan recursion work, and it carries two consequences at once: the slopes of successive factors strictly decrease, and the recursion terminates.

The statement

If B is maximal destabilizing in F, then every nonzero subobject of F / B has slope strictly below that of B. In particular the maximal slope of F / B is strictly below that of B, which is StrictAnti for the filtration, and F / B has no nonzero subobject of slope ⊤, so F / B is pure and its own maximal destabilizing subobject has positive multiplicity.

The proof, and why it needs both halves of maximality

Take a nonzero C ⊆ F / B and pull it back to pb ⊆ F, which contains B. The correspondence supplies the short exact sequence 0 ⟶ B ⟶ pb ⟶ C ⟶ 0. Suppose the slope of C were at least that of B. The see-saw inequality then puts the slope of pb at least that of B, while maximality of the slope puts it at most; so they are equal, and pb attains the maximal slope while strictly containing B. That contradicts the second clause of IsMaximalDestabilizing — maximality in the subobject order among the subobjects attaining the slope. The first clause alone is not enough, which is why that clause is carried.

Termination

Because F / B is pure, the maximal destabilizing subobject of F / B has positive multiplicity, and multiplicity is additive, so the multiplicity of the next quotient is strictly smaller. That is the measure the recursion descends on; the chain condition of MuHNInput is what makes the first step available at all, not what makes the recursion stop.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.not_isZero_of_le {X : Scheme} {F : Coh X} {B C : CategoryTheory.Subobject F} (hBC : B ≤ C) (hB : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj B)) : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj C)

A subobject containing a nonzero subobject is itself nonzero.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.topSlope_lt_of_maximalDestabilizing {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {F : Coh X} {B : CategoryTheory.Subobject F} (hB : IsMaximalDestabilizing h F B) (C : CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)) (hC : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj C)) : (P.weakSlopeData h).topSlope (CategoryTheory.Subobject.underlying.obj C) < (P.weakSlopeData h).topSlope (CategoryTheory.Subobject.underlying.obj B)

The slope drops strictly past the maximal destabilizing subobject.

Every nonzero subobject of the quotient has slope strictly below that of B. See the module docstring: the proof uses the see-saw inequality together with both clauses of IsMaximalDestabilizing.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.multiplicity_pos_of_maximalDestabilizing {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {F : Coh X} {B : CategoryTheory.Subobject F} (hB : IsMaximalDestabilizing h F B) (C : CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)) (hC : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj C)) : 0 < P.multiplicity (CategoryTheory.Subobject.underlying.obj C)

The quotient by the maximal destabilizing subobject is pure.

A nonzero subobject of multiplicity zero would have slope ⊤, which topSlope_lt_of_maximalDestabilizing forbids. This is what makes the recursion terminate: the maximal destabilizing subobject of the quotient then has positive multiplicity, so by additivity the next quotient has strictly smaller multiplicity.