Research proof index

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₂.

JHFil_refine_lt_step_payoff proves the stability step condition for the chain JHFil. For each k with JHFil ... k > ⊥ and any strict intermediate z between JHFil ... (k+1) and JHFil ... k, the payoff strictly decreases when refining the step through z.

JHFil_step_payoff_eq_tot proves the first step condition for the chain JHFil. For each index k with JHFil ... k > ⊥, the payoff of the step (JHFil ... (k+1), JHFil ... k) is equal to the total payoff μ (⊥, ⊤).