HEXAGONbeta

A Finite Coordinate Reduction for Approachability Loss in Lean

Primarily AI-generated textHuman understanding: some partsmath.OC — Optimization and Controlcs.LO — Logic in Computer Science

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

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.

Provenance statement

The manuscript names Arthur Freitas Ramos (submitting contributor; ORCID 0009-0003-3568-0325), David Barros Hulak (0009-0002-8056-1774), and Ruy J. G. B. de Queiroz (0000-0003-1482-0977). The submitting contributor reports understanding some parts, but not all, of the work. OpenAI GPT-6.1 assisted with manuscript drafting, inspection of registered source, organization, bibliography, and consistency checks. Historical formal-artifact proof assistance by GPT-5 via Codex is separate from manuscript assistance. The Palomar registration reports Lean, Comparator, and NanoDa acceptance for the pinned source revision; no fresh Lean, Comparator, or NanoDa execution is claimed here. Exact registered artifact: https://palomar-registry.org/entry?id=PALOMAR-2026-09-20-000001&version=1 . The manuscript is deliberately limited to finite-coordinate algebraic loss preservation: both strategy translations observe original loss histories, and the mass-two comparators leave the joint simplex and have no fixed point there. It does 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.
FormalizationsPalomar

Tools used

OpenAI
ChatGPTVersion GPT 6.1 (manuscript)
OpenAI
CodexVersion GPT-5 (historical proof assistance)
Lean
LeanVersion 4.33.0 (registered artifact)

References

  1. Abernethy, Jacob; Bartlett, Peter L.; Hazan, Elad. Blackwell Approachability and No-Regret Learning are Equivalent. Proceedings of the 24th Annual Conference on Learning Theory, vol. 19, pp. 27–46. 2011. \urlhttps://proceedings.mlr.press/v19/abernethy11b.htmllink
  2. Blackwell, David. An analog of the minimax theorem for vector payoffs. Pacific Journal of Mathematics, vol. 6, no. 1, pp. 1–8. 1956. \urlhttps://msp.org/pjm/1956/6-1/pjm-v6-n1-p01-s.pdflink
  3. Dann, Christoph; Mansour, Yishay; Mohri, Mehryar; Schneider, Jon; Sivan, Balasubramanian. Rate-Preserving Reductions for Blackwell Approachability. Proceedings of Thirty Eighth Conference on Learning Theory, vol. 291, pp. 1380–1414. 2025. Theorem 4 and Appendix G.5; fixed-point convention in Section 2.2. \urlhttps://proceedings.mlr.press/v291/dann25a.htmllink
  4. Palomar Registry. Finite tight Blackwell approachability-to-improper phi-regret reduction in Lean. 2026. PALOMAR-2026-09-20-000001, version 1; registered September 20, 2026. Immutable record inspected October 1, 2026. \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-20-000001&version=1link
  5. Palomar Registry. Verify submission geavw0mtiip5. 2026. Historical successful verification workflow of September 20, 2026. \urlhttps://github.com/PalomarRegistry/PalomarSubmission/actions/runs/35480464336link
  6. Ramos, Arthur Freitas; de Queiroz, Ruy Jose Guerra Barretto; Hulak, David Barros. Finite tight approachability-to-improper-regret reduction. 2026. Registered commit 42b9d7c77e77fc158d44cb31ef320798c3c73492; manuscript source inspection on October 1, 2026. \urlhttps://github.com/Arthur742Ramos/blackwell-approachability-lean/tree/42b9d7c77e77fc158d44cb31ef320798c3c73492/rate-preserving-reductionlink

Version history

  1. v1Initial depositCurrentOct 01, 2026