Research proof index

prop4d3₁ is the dual form of Proposition 4.1: under hypotheses h₁ and h₂ phrased for strict anti-chains and bottom-anchored alternatives, the best-response value μBstar μ coincides with the global supremum μmax μ TotIntvl. The proof reduces to prop4d1₁ on the order dual, and then translates the result back via the duality lemmas.

Proposition 4.8 (implementation form): μQuotient r d is slope-like. Assumptions: - Additivity of d and r along composable intervals: for x<y<z, we have d(x,z) = d(x,y) + d(y,z) and r(x,z) = r(x,y) + r(y,z). - Positivity condition: if r(x,y) = 0 then d(x,y) > 0. Conclusion: - The quotient construction μQuotient r d satisfies the slope-lik...

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.