Research proof index

Remark 2.5 (part 3): invariance of μA under replacing μ by μmax μ. Together with rmk2d5₂, this shows that the outer optimization μA is stable under the μmax closure.

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