Research proof index

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.

Strict decrease condition on consecutive μA-slopes for HNFil. This is the analogue of “HN slopes are strictly decreasing”, phrased as the non-comparability statement ¬ μA(i,i+1) ≤ μA(i+1,i+2). The proof is an application of the internal obstruction lemma prop3d7₂.