Research proof index

rmk4d10₁ rewrites the inequality μBstar μ ≤ μAstar μ as an explicit family of inequalities comparing the extremal values on bottom- and top-anchored intervals. This is a convenient “unfolded” form for later arguments.

rmk4d4 is a well-ordering / ranking-function criterion that produces the strict-anti-chain hypothesis needed in prop4d3₁. Given a monotone rank function r : ℒ → ℝ whose range is well-ordered, any strict descending chain must eventually stabilise in rank; the hypothesis h then forces the required inequality by turning equal ranks into a μ = ⊤ sta...

Equivalence between the global typeclass Semistable μ and interval-local semistability on the total interval. This lemma is an API bridge: it lets one freely move between the class-based semistability used in later modules and the predicate semistableI μ TotIntvl defined via StI.

semistable_of_step_cond₂ turns a strict step condition into semistability on each step. Assuming that for every intermediate z strictly between consecutive values filtration (i+1) < z < filtration i the slope strictly improves, the restricted slope Resμ ⟨(filtration (i+1), filtration i), _⟩ μ is semistable.

Semistability of a restriction vs. semistability on the quotient lattice. This lemma is the key “translation” step for coprimary filtrations: * restricting the slope μ R M to an interval (N₁, N₂) corresponds to * the induced slope on the submodule lattice of the quotient module N₂ / N₁. The statement is phrased as an equivalence between `Semistable...

Transport semistability along restriction. This theorem relates: - semistableI μ I, i.e. semistability of the interval I with respect to μ, and - Semistable (Resμ I μ), i.e. global semistability of the restricted function on the interval subtype. API note: this is a key adapter used whenever proofs switch between the “ambient interval” viewpoint a...