Research proof index

Helper lemma: consecutive elements in a RelSeries are strictly increasing. This extracts the < witness from the step relation, rewriting indices so it can be used with toFun and standard arithmetic on ℕ.

Helper lemma: the “next” consecutive inequality, shifted by one. Together with relSeries_step_lt, this is used to express the slope comparison condition in terms of toFun indices i, i+1, i+2.

Remark 2.5 (part 2): idempotence of μmax. The statement μmax μ I = μmax (μmax μ) I says that applying μmax twice does not change the result. Convexity is used to relate the two suprema.

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