math.OC — Optimization and Control
A Finite Coordinate Reduction for Approachability Loss in Lean
We explain a Lean 4 development of a finite-coordinate loss-preserving construction motivated by Theorem 4 of Dann, Mansour, Mohri, Schneider, and Sivan. Nonempty finite constraint and action index sets give a joint probability simplex with a canonical action marginal. For each mixed constraint, a linear comparator adds its outer product with that marginal. The comparator has mass two and leaves the legal action set. A one-step pairing identity yields exact equality of finite-horizon approachability and comparator-regret objectives, with explicit anchored lifts and marginal decoders. The development also proves a row-wise decomposition with at most one rank-one term per constraint index. We describe the twelve declarations registered in Palomar and their historical verification provenance. The scope is deliberately narrow: the constraint simplex parametrizes coordinate functions, both causal strategy translations observe original loss histories, and the comparators have no fixed point in the joint simplex. Thus the checked statements establish finite algebraic loss preservation; they do not certify the full published reduction, its fixed-point-defined improper class, reduced-loss-only feedback, or asymptotic rate theory. No mathematical novelty or formalization priority is claimed.