Research proof index

Uniqueness of the canonical Harder–Narasimhan filtration (theorem3d10). Given any function f : ℕ → ℒ that: * starts at ⊥ and eventually becomes constantly ⊤, * is strictly increasing up to its finite length, * has semistable successive restrictions, and * has strictly decreasing μA-slopes, then f agrees pointwise with the canonical constructio...

μ_bot_JH_eq_μ_tot is an invariance statement along a Jordan–Hölder filtration. For every index i before the terminal length, the payoff μ (⊥, JH.filtration i) equals the total payoff μ (⊥, ⊤). The proof is by induction on i using the first step condition.

For the associated-prime slope, μmax is definitionally redundant. The definition of μ R M already yields an element that is greatest among the subinterval values, so the μmax operation returns the same value.