Research proof index

stable_of_step_cond₂ upgrades the previous lemma from semistability to stability. Under the same strict step condition, each restricted slope on a step interval is not only semistable but satisfies the strict inequality required for Stable.

step_cond₂_of_stable is the converse direction: stability implies the strict step condition. If each restricted slope on the step intervals is stable, then for every strict intermediate z one has the strict inequality comparing μ (filtration (i+1), z) with the step value.

subseqIdx_find_ne_of_plateau is a technical combinatorial lemma about the index where f (subseqIdx ...) hits ⊥. It shows that this index cannot coincide with a specified k under a mild “plateau” hypothesis (∃ N, N+1 ≤ k ∧ f N = f (N+1)). The proof uses a finite-cardinality argument on the image set {f t | t ≤ k}.

subseqIdx_inherit_step_predicate transports a stepwise predicate from the original chain to the values selected by subseqIdx. Given a predicate P on strict steps of f (assumed for each i < Nat.find atf), the lemma produces the corresponding fact for each strict step of the selected values before they reach ⊥.

Monotonicity of support under enlarging the submodule being quotiented out. If N₁ ≤ N₂, then the support of N₃ / N₂ is contained in the support of N₃ / N₁. This is a standard “support shrinks under quotients” statement.

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