Research proof index

Any coprimary filtration underlies a Harder–Narasimhan filtration. We reuse the same filtration function and verify the Harder–Narasimhan axioms: piecewise semistability (via rmk4d14₂ and semistable_res_iff_semistable_quot) and strict decrease of the minimal associated primes.

h₁_dual_of_h₁ transports the “descending-chain” hypothesis h₁ on ℒ to the corresponding “ascending-chain” hypothesis on the order dual ℒᵒᵈ.

Construct a HarderNarasimhanFiltration from a RelSeries. Assuming F1 starts at ⊥, ends at ⊤, and satisfies the strict slope decrease condition expressed using relSeries_step_lt/relSeries_succ_step_lt, we build a HarderNarasimhanFiltration μ whose underlying function agrees with F1.toFun up to F1.length. This is a bridge lemma used when...

Strict monotonicity of HNFil on the active range. If i < j ≤ HNlen μ, then HNFil μ i < HNFil μ j.

Characterization of “not yet terminated” via HNlen. This is the expected property of Nat.find: HNFil μ n ≠ ⊤ iff n < HNlen μ.

Each successive interval of HNFil is semistable. This is exactly the piecewise_semistable axiom of a Harder–Narasimhan filtration, proved using the semistability statement for stable breakpoints (prop3d7₁) and the translation lemma semistableI_iff.