Research proof index

Another key property of the recursion: step i+1 is chosen to be “maximal among those with at least its μA-value”, in the sense that no z strictly between step i+1 and step i can have μA (I.left, z) greater-or-equal to μA (I.left, step(i+1)). This is a tie-breaking/optimality condition derived from minimality in the well-founded has_min cho...

Optimality at the last pre-termination step. Let len be the first index such that step len equals I.left. Then at index len-1, no intermediate point y between I.left and (func (len-1)).val yields a strictly larger value of μA (I.left, y). This is used to show that the final candidate satisfies the selection predicate S₁I.

Proposition 3.8 (part 1): totality on StI μ I under comparability/attainment hypotheses. Under convexity and well-foundedness, if either: - the target S is totally ordered, or - all relevant μA infima are attained, then the order on the set of stable breakpoints becomes total. API note: this produces an instance of Std.Total for the subtype `StI μ...

Proposition 3.8 (part 2): decomposition at a stable breakpoint. Under convexity and the comparability/attainment hypothesis, if x ∈ StI μ I and x<y in I, then μA (I.left, y) = μA (x,y). Intuition: once x is chosen as a stable breakpoint, the “best value” up to y is fully determined by the subinterval starting at x.

prop4d1₁ is the core statement behind Proposition 4.1: under the two hypotheses h₁ (a weak “eventual improvement” along strict chains) and h₂ (a weak slope-like alternative towards the top), the best-response value μAstar μ coincides with the global infimum μmin μ TotIntvl.

prop4d11₁ shows that if the global extremal values on TotIntvl coincide, then the best-response inequality μBstar μ ≤ μAstar μ holds.