% Copyright 2026 Arthur Freitas Ramos, David Barros Hulak, % and Ruy J. G. B. de Queiroz. Manuscript source licensed CC BY 4.0. % https://creativecommons.org/licenses/by/4.0/ \documentclass[11pt]{amsart} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[a4paper,margin=29mm]{geometry} \usepackage{amsmath,amssymb,amsthm} \usepackage{microtype} \usepackage{needspace} \usepackage{xurl} \usepackage[hidelinks]{hyperref} \hypersetup{pdftitle={A Finite Coordinate Reduction for Approachability Loss in Lean}, pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz}, pdfsubject={An audited finite loss identity with improper tensor comparators}, pdfkeywords={Blackwell approachability, improper phi regret, finite simplex, Lean 4, formal verification}} \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\R}{\mathbb R} \newcommand{\DeltaI}{\Delta_I} \newcommand{\DeltaJ}{\Delta_J} \newcommand{\X}{\Delta_{I\times J}} \newcommand{\App}{\operatorname{App}} \newcommand{\Reg}{\operatorname{Reg}} \newcommand{\dec}{\operatorname{dec}} \newcommand{\lift}{\operatorname{lift}} \newcommand{\decl}[1]{{\small\nolinkurl{#1}}} \newcommand{\source}[2]{\href{https://github.com/Arthur742Ramos/blackwell-approachability-lean/blob/42b9d7c77e77fc158d44cb31ef320798c3c73492/rate-preserving-reduction/#1}{#2}} \title[Finite coordinate approachability reduction]{A Finite Coordinate Reduction for Approachability Loss in Lean} \author{Arthur Freitas Ramos} \author{David Barros Hulak} \author{Ruy J. G. B. de Queiroz} \thanks{Author ORCID identifiers: Arthur Freitas Ramos, \href{https://orcid.org/0009-0003-3568-0325}{0009-0003-3568-0325}; David Barros Hulak, \href{https://orcid.org/0009-0002-8056-1774}{0009-0002-8056-1774}; Ruy J. G. B. de Queiroz, \href{https://orcid.org/0000-0003-1482-0977}{0000-0003-1482-0977}.} \thanks{Copyright 2026 the authors. Licensed under \href{https://creativecommons.org/licenses/by/4.0/}{Creative Commons Attribution 4.0 International (CC BY 4.0)}.} \date{October 1, 2026} \subjclass[2020]{91A26, 68T05, 68V20} \keywords{Blackwell approachability, finite coordinate constraints, tensor simplex, improper comparators, loss preservation, Lean 4, Mathlib} \begin{document} \begin{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. \end{abstract} \maketitle \raggedbottom \section{Scope and mathematical context} Blackwell's approachability theory concerns repeated games with vector payoffs and target sets \cite{Blackwell1956}. A useful finite-coordinate objective measures the largest accumulated score among a family of bilinear constraints. The connection with online regret minimization is classical; Abernethy, Bartlett, and Hazan give algorithmic reductions between approachability and online linear optimization \cite{AbernethyBartlettHazan2011}. Dann, Mansour, Mohri, Schneider, and Sivan investigate preservation of optimal rates and give a tensor-based construction in Theorem 4 and Appendix G.5 of their COLT 2025 paper \cite{DannEtAl2025}. The present article studies the finite-coordinate algebra of that construction. Our object is the artifact registered as \href{https://palomar-registry.org/entry?id=PALOMAR-2026-09-20-000001\&version=1}{PALOMAR-2026-09-20-000001, version 1} \cite{PalomarReduction}. Its source is the nested project \texttt{rate-preserving-reduction} at commit \nolinkurl{42b9d7c77e77fc158d44cb31ef320798c3c73492} of \texttt{Arthur742Ramos/blackwell-approachability-lean} \cite{ReductionArtifact}. All implementation claims below refer to this immutable snapshot, rather than to the repository's current default branch. Three distinctions determine what the result means. First, a simplex of constraint coefficients can represent the same constraint function more than once. Its tensor coordinates are not automatically an intrinsic tensor product of the set of functions. Second, the checked online strategies on both sides receive the \emph{original} loss vectors; the development does not convert arbitrary strategies between different feedback alphabets. Third, the published paper's Section 2.2 defines its improper class using a fixed point in the action set for every comparator. The mass-two comparators here have no such fixed point. We use ``improper comparator'' to mean that its image escapes the legal action set, without asserting membership in that fixed-point-defined class. These qualifications are part of the mathematical statement, not merely implementation details. The formal result is nevertheless a complete exact identity in its stated model. It works for every finite horizon, every real payoff tensor, and every original loss sequence. It gives explicit causal translations in both directions and preserves their objectives on each individual sequence. No assumption that the instance is approachable is needed for these identities, and no existence of a low-loss strategy is concluded. \section{The finite coordinate model} Let $I$ and $J$ be nonempty finite sets and let $K$ be a finite set, which may be empty. They index constraint coordinates, actions, and loss coordinates, respectively. Fix arbitrary real numbers \[ a=(a_{ijk})_{i\in I,\,j\in J,\,k\in K}. \] For a finite set $E$, write \[ \Delta_E=\left\{p\in\R^E: p_e\geq0\text{ for all }e,\quad \sum_{e\in E}p_e=1\right\}. \] The action space is $\DeltaJ$, and the coefficient space is $\DeltaI$. An original loss is any $\ell\in\R^K$. There is no simplex constraint on $\ell$ and no bounded loss set is specified in the checked theorem. The scores below are bilinear. The published model also permits bi-affine constraints; an extension by homogenizing affine coordinates is not part of the checked development. \subsection{Scores and redundant constraint parameters} The coordinate constraints and their mixtures are \begin{align} u_i(p,\ell)&=\sum_{j\in J}\sum_{k\in K}a_{ijk}p_j\ell_k, \label{eq:coordinate-score}\\ u_w(p,\ell)&=\sum_{i\in I}w_i u_i(p,\ell),\qquad w\in\DeltaI. \label{eq:mixed-score} \end{align} Consequently $w\mapsto u_w$ parametrizes the convex hull of the coordinate functions. The map need not be injective: two rows of $a$ may define the same function, or every row may be zero. We therefore retain $w$ as a coefficient vector throughout. The source type \decl{Payoff} imposes no independence or injectivity condition. This matters when comparing with the published notation $U\otimes P$. In this article the tensor realization is \[ \X=\left\{x\in\R^{I\times J}: x_{ij}\geq0,\quad \sum_i\sum_j x_{ij}=1\right\}, \] the joint simplex of \emph{coefficient and action distributions}. Its convex-hull characterization concerns those coordinates. No isomorphism with a tensor product formed from the literal set of constraint functions is assumed or proved. For example, if all coordinate functions vanish, the coefficient simplex still has its full coordinate structure even though the function family is a singleton. \subsection{Outer products and the canonical marginal} For real vectors $w$ and $p$, define their outer product by $(w\otimes p)_{ij}=w_i p_j$. For a table $x$, define the action marginal \begin{equation} q(x)_j=\sum_{i\in I}x_{ij}. \label{eq:marginal} \end{equation} Both maps are elementary coordinate operations. If $w\in\DeltaI$ and $p\in\DeltaJ$, then $w\otimes p\in\X$. If $x\in\X$, then $q(x)\in\DeltaJ$, and \begin{equation} q(w\otimes p)=p\qquad(w\in\DeltaI). \label{eq:left-inverse} \end{equation} Indeed, nonnegativity is preserved by multiplication and finite summation, and the relevant total masses are $(\sum_i w_i)(\sum_j p_j)=1$ and $\sum_j\sum_i x_{ij}=1$. Equation \eqref{eq:left-inverse} follows by factoring $p_j$ out of the sum. The registered declarations \decl{outer_jointSimplex}, \decl{marginal_simplex}, and \decl{marginal_outer} express these facts. \begin{proposition}[Two finite tensor decompositions]\label{prop:hull} The joint simplex is the convex hull of the product distributions $w\otimes p$ with $w\in\DeltaI$ and $p\in\DeltaJ$. Every $x\in\X$ also has a decomposition \begin{equation} x=\sum_{i\in I}r_i(e_i\otimes p^{(i)}), \label{eq:row-decomposition} \end{equation} where $r\in\DeltaI$, each $p^{(i)}\in\DeltaJ$, and $e_i$ is the point mass at $i$. Thus at most $|I|$ nonzero rank-one terms are required. \end{proposition} \begin{proof} The point mass $e_{(i,j)}$ at a pair is $e_i\otimes e_j$. Every joint distribution has the coordinate decomposition $x=\sum_{i,j}x_{ij}e_{(i,j)}$. The coefficients are nonnegative and sum to one. Conversely, any convex combination of these vertices is a nonnegative table of total mass one; the same is true for convex combinations of arbitrary product distributions. For the sharper statement, put $r_i=\sum_j x_{ij}$. When $r_i>0$, set $p^{(i)}_j=x_{ij}/r_i$. When $r_i=0$, choose any point mass in $\DeltaJ$, which is possible because $J$ is nonempty. Nonnegative entries imply that every entry of a zero-mass row is zero. Thus in both cases $r_i p^{(i)}_j=x_{ij}$, which proves \eqref{eq:row-decomposition}. Conversely, any table of the displayed form has nonnegative entries and total mass $\sum_i r_i=1$. \end{proof} The formal statements separate the coordinate-vertex characterization, \decl{jointSimplex_eq_finiteTensorCombination}, from the row-wise characterization, \decl{jointSimplex_eq_finiteRowRankOneCombination}. The point-mass product identity is also a selected declaration. The decoder $q(x)$ does not choose either decomposition. It is defined directly on the table, so ambiguity among tensor decompositions cannot affect the decoded action. \section{Improper comparators and exact loss equality} \subsection{The reduced loss map} Use the ordinary finite dot product on tables, $\langle x,y\rangle=\sum_{i,j}x_{ij}y_{ij}$. Define a linear map $M:\R^K\to\R^{I\times J}$ by \begin{equation} (M\ell)_{ij}=-\sum_{k\in K}a_{ijk}\ell_k. \label{eq:reduced-loss} \end{equation} The minus sign is essential. If $B(x,\ell)=\langle x,M\ell\rangle$, then \begin{equation} B(w\otimes p,\ell)=-u_w(p,\ell). \label{eq:B-score} \end{equation} In Lean, \decl{reducedLoss} implements $M\ell$, \decl{flatten} changes curried table coordinates to coordinates indexed by pairs, and \decl{pairing} uses Mathlib's \decl{dotProduct}. The definition \decl{score} is $\langle w\otimes p,-M\ell\rangle$, so its expansion is exactly \eqref{eq:mixed-score}. \subsection{The shift and its image} For $w\in\DeltaI$ define a comparator on the ambient table space by \begin{equation} \phi_w(x)=x+w\otimes q(x). \label{eq:shift} \end{equation} For fixed $w$ this is a linear map. On product distributions it satisfies $\phi_w(v\otimes p)=(v+w)\otimes p$, since $q(v\otimes p)=p$. This is the finite-coordinate version of the algebraic comparator in Appendix G.5 of the cited paper. Its codomain is the ambient real table space, not the joint simplex. \begin{proposition}[Mass-two escape]\label{prop:improper} For every $w\in\DeltaI$ and $x\in\X$, the comparator $\phi_w(x)$ is nonnegative and has total mass two. In particular $\phi_w(x)\notin\X$, and $\phi_w$ has no fixed point in $\X$. \end{proposition} \begin{proof} The marginal $q(x)$ is a probability distribution, so $w\otimes q(x)$ has total mass one. Adding it to the mass-one table $x$ gives total mass two. A fixed point would have to have both mass one and mass two. \end{proof} The selected formal improperness theorem checks escape from the action set; the no-fixed-point conclusion above is an immediate mathematical consequence, not an additional registered theorem. It also explains why the construction cannot be identified with the fixed-point-defined improper class in Section 2.2 of the published paper. This observation does not by itself imply failure of sublinear loss on a restricted image loss set $M(L)$; the present theorem proves neither success nor failure of such a learning guarantee. \begin{lemma}[One-step identity]\label{lem:one-step} For any real table $x$, real vector $w$, and loss $\ell\in\R^K$, \begin{equation} \langle x,M\ell\rangle-\langle\phi_w(x),M\ell\rangle =u_w(q(x),\ell). \label{eq:one-step} \end{equation} Here $q$ and $u_w$ are understood by their coordinate formulas, without requiring $x$ or $w$ to be probability distributions. \end{lemma} \begin{proof} Substitute \eqref{eq:shift} and use additivity of the dot product. The left-hand side becomes $-\langle w\otimes q(x),M\ell\rangle$, which is the right-hand side by \eqref{eq:B-score}. No positivity, boundedness, optimization, or limiting argument is involved. \end{proof} \subsection{Finite-horizon objectives} Let $T\geq0$. For an original trajectory $p=(p_t)_{t