{"id":"hexagon/2610.00002","pdf":"https://hexagonmath.org/pdf/2610.00002v1","url":"https://hexagonmath.org/abs/2610.00002v1","tags":["cs.LO","msc:91A26","msc:68T05","msc:68V20"],"score":0,"title":"A Finite Coordinate Reduction for Approachability Loss in Lean","domain":"math.OC","origin":"ai-generated","source":"hexagon","authors":["Arthur","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.OC","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"ai_models":["ChatGPT","Codex"],"discussed":0,"published":"2026-10-01","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":true,"formalizations":["https://palomar-registry.org/entry?id=PALOMAR-2026-09-20-000001&version=1"],"human_understanding":"some"}