A Finite Coordinate Reduction for Approachability Loss in Lean

Scope and mathematical context

Blackwell’s approachability theory concerns repeated games with vector payoffs and target sets [2]. 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 [1]. 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 [3]. The present article studies the finite-coordinate algebra of that construction.

Our object is the artifact registered as PALOMAR-2026-09-20-000001, version 1 [4]. Its source is the nested project rate-preserving-reduction at commit 42b9d7c77e77fc158d44cb31ef320798c3c73492 of Arthur742Ramos/blackwell-approachability-lean [6]. 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 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

2020 Mathematics Subject Classification. 91A26, 68T05, 68V20.

Key words and phrases. Blackwell approachability, finite coordinate constraints, tensor simplex, improper comparators, loss preservation, Lean 4, Mathlib.

Author ORCID identifiers: Arthur Freitas Ramos, 0009-0003-3568-0325; David Barros Hulak, 0009-0002-8056-1774; Ruy J. G. B. de Queiroz, 0000-0003-1482-0977.

Copyright 2026 the authors. Licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). 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.

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

For a finite set $E$, write

The action space is $\Delta_J$, and the coefficient space is $\Delta_I$. An original loss is any $\ell\in\mathbb{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.

Scores and redundant constraint parameters

The coordinate constraints and their mixtures are

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 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

the joint simplex of 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.

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

Both maps are elementary coordinate operations. If $w \in\Delta_I$ and $p \in\Delta_J$, then $w \otimes p \in\Delta_{I \times J}$. If $x \in\Delta_{I \times J}$, then $q(x) \in\Delta_J$, and

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_i\sum_j x_{ij}=1$. (4) follows by factoring $p_j$ out of the sum. The registered declarations outer_jointSimplex, marginal_simplex, and marginal_outer express these facts.

Proposition 2.1 (Two finite tensor decompositions). The joint simplex is the convex hull of the product distributions $w \otimes p$ with $w \in\Delta_I$ and $p \in\Delta_J$. Every $x \in\Delta_{I \times J}$ also has a decomposition

where $r \in\Delta_I$, each $p^{(i)} \in\Delta_J$, and $e_i$ is the point mass at $i$. Thus at most $|I|$ nonzero rank-one terms are required.

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_j^{(i)}=x_{ij}/r_i$. When $r_i=0$, choose any point mass in $\Delta_J$, 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_j^{(i)}=x_{ij}$, which proves (5). Conversely, any table of the displayed form has nonnegative entries and total mass $\sum_i r_i=1$. $\square$

The formal statements separate the coordinate-vertex characterization, jointSimplex_eq_finiteTensorCombination, from the row-wise characterization, 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.

Improper comparators and exact loss equality

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:\mathbb{R}^K \to\mathbb{R}^{I \times J}$ by

The minus sign is essential. If $B(x,\ell)=\langle x,M\ell\rangle$, then

In Lean, reducedLoss implements $M\ell$, flatten changes curried table coordinates to coordinates indexed by pairs, and pairing uses Mathlib’s dotProduct. The definition score is $\langle w \otimes p,-M\ell\rangle$, so its expansion is exactly (2).

The shift and its image

For $w \in\Delta_I$ define a comparator on the ambient table space by

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.

Proposition 3.1 (Mass-two escape). For every $w \in\Delta_I$ and $x \in\Delta_{I \times J}$, the comparator $\phi_w(x)$ is nonnegative and has total mass two. In particular $\phi_w(x)\notin\Delta_{I \times J}$, and $\phi_w$ has no fixed point in $\Delta_{I \times J}$.

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. $\square$

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.

Lemma 3.2 (One-step identity). For any real table $x$, real vector $w$, and loss $\ell\in\mathbb{R}^{K}$,

Here $q$ and $u_{w}$ are understood by their coordinate formulas, without requiring $x$ or $w$ to be probability distributions.

Proof. Substitute (8) 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 (7). No positivity, boundedness, optimization, or limiting argument is involved. $\square$

Finite-horizon objectives

Let $T \ge0$. For an original trajectory $p=(p_{t})_{t<T}$ in $\Delta_{J}$ and a loss trajectory $\ell=(\ell_{t})_{t<T}$ in $\mathbb{R}^{K}$, define

For a joint trajectory $x=(x_{t})_{t<T}$ in $\Delta_{I\times J}$, define

One fixed comparator parameter $w$ is used across the entire horizon. These are raw signed objectives. There is no positive-part operation, normalization by $T$, or claim that they equal a distance to a target set.

Theorem 3.3 (Finite trajectory preservation). For every legal joint trajectory and every loss trajectory,

where $q$ is applied at each round. Fix any anchor $b\in\Delta_{I}$ and put $\operatorname{lift}_{b}(p)=b\otimes p$. Then for every original trajectory,

Proof. Summing (9) gives $R_{w}(x,\ell)=A_{w}(q(x),\ell)$ for each $w$. The two sets of objective values indexed by $w$ are therefore identical, and their suprema are equal. For the anchored direction, use $q(\operatorname{lift}_{b}(p_{t}))=p_{t}$ at each round. $\square$

The two maps are a section and a retraction: $q\circ\operatorname{lift}_{b}=\mathrm{id}$. The composition $\operatorname{lift}_{b}\circ q$ need not be the identity on $\Delta_{I\times J}$. Reconstructing correlations in a joint table is unnecessary because (9) depends only on its action marginal. “Tightness” in the named Lean predicates means these two exact objective-preserving translations; it does not assert a bijection of trajectories.

Remark 3.4 (Real suprema and signed values). For a fixed original trajectory, put $c_i=\sum_{t<T}u_i(p_t,\ell_t)$. Then $A_w(p,\ell)=\sum_i w_i c_i$. Since $I$ is finite and nonempty, its supremum is the finite maximum $\max_i c_i$, attained at a point mass. This proves, in ordinary mathematics, that the real supremum is taken over a nonempty bounded set. The registered proof of regretLoss_eq_approachLoss does not formalize this maximizer or boundedness result: it proves equality of ranges and applies equality congruence to Lean’s real sSup. These distinct facts should not be conflated. The maximum can be negative; if $I,J,K$ are singletons, $a=-1$, $T=1$, and $\ell=1$, both objectives are $-1$. If $T=0$, or if $K$ is empty, all scores and both objectives are zero.

Causal translations in a common information model

A deterministic online strategy with action space $E$ is modeled as a function $F:(\mathbb{R}^{K})^{*}\to E$ from finite lists of prior original losses. Given a list $(\ell_0,\ldots,\ell_{T-1})$, its action at round $t$ is $F(\ell_0,\ldots,\ell_{t-1})$. In particular it cannot see the current or a future loss through this argument. Dependence on time is possible through the length of the list.

For an original strategy $F:(\mathbb{R}^{K})^{*}\to\Delta_J$ and a joint strategy $G:(\mathbb{R}^{K})^{*}\to\Delta_{I\times J}$, define

Each translation uses precisely the same input history as the strategy being translated. The anchor is fixed once, and is retained explicitly in the theorem’s conclusion.

Theorem 4.1 (Common-history strategy preservation). For every finite original loss list $\ell$,

The notation $F(\ell)$ or $G(\ell)$ in these equations denotes the trajectory generated from the successive prefixes of the list.

Proof. The run of $\mathcal{L}_b(F)$ is the pointwise lift of the run of $F$; the run of $\mathcal{D}(G)$ is the pointwise decode of the run of $G$. Substitute these identities into Theorem 3.3. □

This is the content of the registered endpoint algorithmicFiniteTensorTightReduction_of_anchor. Its strategy type is List(Distd) → A; Distd means $d\to\mathbb{R}$, not a probability distribution on $d$. The argument is entirely deterministic. Mixed actions are returned as vectors in a simplex; the development does not specify a random seed, sampled action, probability law, or expected regret. The source uses noncomputable sections; its strategy types and equalities do not certify executable implementations or running-time bounds.

The feedback boundary

The reduced pairing loss at a round is $M\ell_t$, but the checked strategy still observes histories of $\ell_t$. Thus the theorem does not state that an arbitrary original strategy can be run using only the transformed losses $(M\ell_s)_{s<t}$. No injectivity of $M$, inverse map, measurable selection, or loss-history lifting is provided. When $M$ discards coordinates, two different original histories can give the same transformed history, and an arbitrary strategy may choose different actions on them.

One can, externally, restrict strategies to depend only on $M\ell$, or supply an information-preserving encoding of losses. Such choices would require additional definitions and proofs before claiming a standard reduction between instances with different feedback spaces. They are not part of the registered artifact. The exact identities here are instead statements in a shared original-loss information model.

For any chosen set of allowed original loss sequences, the same pointwise equalities transfer every uniform finite-horizon upper or lower bound through the two maps. For example, a guarantee $\operatorname{App}(F(\ell),\ell)\le r(T)$ on those sequences gives the identical bound for $\mathcal{L}_b(F)$, and the converse holds via $\mathcal{D}$. This elementary consequence explains the loss-preservation content. It is not a checked theorem about worst-case suprema over an unbounded loss alphabet, minimax optimization over strategies, convergence rates, or the asymptotic rate definition of the published paper.

A concrete two-by-two example

The registered examples use $I = J = \{0,1\}$ and one loss coordinate, with $a_{ij} = 1$ if $i = j$ and $a_{ij} = -1$ otherwise. Hence

The Lean file RateReductionExamples.lean instantiates both preservation predicates with the uniform anchor and checks comparator escape. It serves as a validation instance, not a new learning-theory theorem.

For an explanatory calculation, take

Then

The shifted table has total mass two. Its pairing with $M\ell$ is $-\ell$, just as the pairing of $x$ with $M\ell$ is $-\ell$; their difference is zero. The original score $u_{0}(q(x),\ell)$ is also zero. The uniform anchored lift of $q(x)$ is the all-1/4 table, different from $x$, but it has the same decoded action and the same regret increment. This illustrates both exactness and the absence of a two-sided inverse on joint actions. The displayed numerical calculation is an exposition of the formulas, rather than a claim that these exact numerals constitute a separate selected Lean declaration.

Proof architecture and the registered statement surface

The implementation is in RateReduction.lean. The statement file RateReductionChallenge.lean imports only Mathlib and restates the finite model in the namespace Blackwell.RateReduction.Palomar. Its twelve intentional proof holes specify the comparison targets. The corresponding RateReductionSolution.lean imports the implementation and proves the matching endpoints by adapters. Definitions on the two surfaces use the same coordinate formulas. The comparison configuration selects the following declarations; all names in this list have the preceding namespace prefix.

1. marginal_simplex proves that the decoder preserves legality.

2. outer_jointSimplex proves legality of product distributions.

3. elementaryTensor_eq_outer_pointMass identifies coordinate vertices with products of point masses.

4. jointSimplex_eq_finiteTensorCombination checks the coordinate convex-hull characterization.

5. jointSimplex_eq_finiteRowRankOneCombination checks the row-supported rank-one characterization.

6. marginal_outer supplies the left-inverse identity.

7. pairing_shift_sub_pairing_eq_score is the one-step algebraic identity.

8. regretSum_eq_approachSum sums it for a fixed mixed constraint.

9. regretLoss_eq_approachLoss transports it to the real-supremum objectives.

10. shift_is_improper checks universal escape from the joint simplex, together with nonemptiness witnesses.

11. finiteTensorTightReduction_of_anchor packages the two finite-trajectory translations for the supplied anchor.

12. algorithmicFiniteTensorTightReduction_of_anchor packages the two causal common-history strategy translations.

The proof follows the mathematical dependency order rather than invoking a general approachability theorem. Finite sums establish mass identities; coordinate point masses give the first hull theorem. For the row theorem, the private definition conditionalRow divides a positive row by its total mass and uses a chosen point mass for a zero row. A single-entry-versus-row-sum inequality proves that a nonnegative zero-mass row vanishes. This is the only choice needed for that decomposition; the decoder and supplied-anchor lift remain explicit coordinate maps.

The one-step proof uses additivity and negation of the finite dot product, followed by additive algebra. Finite summation then proves the fixed-$w$ horizon identity. At the optimization layer, equality of the two ranges is proved using the same witness $w$ in each direction, and congrArgsSup gives the objective equality. It does not appeal to compactness or a selected maximizer. Finally, the run-trajectory identities for strategy lifting and decoding are definitional equalities. The algorithmic packaging is therefore a short consequence of the trajectory equalities.

The central objective, improperness, and reduction signatures require finite nonempty constraint and action index types. In addition, the headline reduction predicates and shiftImproper include $\operatorname{Nonempty} m \land\operatorname{Nonempty} n$ in their conclusions. This makes the scope nonvacuous: the proof is not a universal statement over an empty action simplex or an empty comparator family. The loss-coordinate type requires finiteness but no nonemptiness assumption.

Verification provenance and reproducibility

The historical mechanical record

The immutable Palomar record reports mechanical verification on September 20, 2026, at 01:11:27 UTC, and registration at 01:32:50 UTC [4]. The official workflow is Actions run 35480464336, attempt 1, whose recorded conclusion is success [5]. The record specifies Lean leanprover/lean4:v4.33.0, Mathlib revision db584cd6d46c92f209a44c0f1c829460d327499d, and twelve selected declarations. The project configuration enables NanoDa and permits propext, Quot.sound, and Classical.choice. This allowlist describes the permitted logical dependencies; it is not a statement that each theorem needs every permitted axiom.

For precise identification, the record pins Comparator at 575674928e239f5bc452aab72d1dd7b0f1326494, Lean4Export at 15f6055e299ad5b89345e533cc2192f4cc00f659, NanoDa at 68d5ca9db226849b41a6fff59d796ff19d0a8840, and Landrun at 811cfff51ceaf3d9843708aa6d22e9b84ccac8b4. The mechanical report SHA-256 is 1d4cb886ff3f33b52e007120e146c2dbe426b047d6da0105f62e64a9841949f2. The public JSON record supplies the durable evidence path and preservation receipt, as well as the source and tool pins.

The statement file is recorded as 328 lines and 14,451 bytes, with SHA-256 913b9ab7a1c7963515b60c7aafef700ea5d3d4505d03b2afee2257077bfbe05. The solution file SHA-256 is 25e7e13e22f1e323e720e7b432c5090cae4e115dd36b5bd9ddf08e40a706269d. The registry’s trust field is high; it also records that the Challenge exceeds the preferred audit surface. Its review outcome is neutral, with no listed warnings. Neither a successful machine check nor these labels are a human mathematical referee report, and they do not settle correspondence with every convention in the source paper.

Checks for this exposition

During manuscript preparation, the pinned source and public record were inspected and the local statement and solution bytes were checked against the two recorded SHA-256 hashes. The mathematical exposition was independently checked against the source definitions and the published paper, and the manuscript was compiled and visually inspected. These are manuscript and source-consistency checks. No fresh Lean build, Comparator replay, or NanoDa replay is claimed here. The proof-checking evidence described above is historical evidence from the registered snapshot.

A reader wishing to repeat the project gate can obtain the pinned repository, enter rate-preserving-reduction, and run bash scripts/verify-palomar.sh. The script includes source-shape and metadata gates, a Lake build, a renderer audit, the named axiom audit, and the example check. Its separate Comparator script describes the pinned external checking tools. Running these commands is a reproducibility procedure, not an assertion that they were executed for this manuscript.

This nested project is distinct from the earlier irreducibility entry PALOMAR-2026-09-10-000003, version 1. The registry identifies the two projects as independent: this reduction has its own Challenge, Solution, and configuration and no proof dependency on that earlier artifact. The present exposition does not import or re-prove the earlier irreducibility results.

Licensing and AI assistance

The registered Lean repository snapshot is licensed BSD-3-Clause. This manuscript and its TeX and BibTeX sources are licensed CC BY 4.0; that manuscript license does not relicense the Lean artifact, its dependencies, or the cited papers.

GPT-6.1 assisted with drafting, source cross-checking, and typesetting this manuscript. The pinned artifact’s metadata separately reports GPT-5 Codex assistance for historical proof engineering. Manuscript assistance is not an attribution of the original Lean proof work to GPT-6.1. AI-assisted source review is not a claim of independent human refereeing.

Conclusion

The registered artifact supplies a finite-coordinate joint-simplex model, a decomposition-independent marginal, a universally escaping linear comparator, and exact finite loss equalities. Anchored lifting and marginal decoding extend those equalities to deterministic causal strategies in the same original-loss information model. Its row-wise decomposition also makes the coordinate tensor hull explicit with at most one rank-one term per constraint index.

The scope is an algebraic specialization inspired by the published tensor construction. It does not identify the coefficient representation with a possibly redundant function-family tensor product, implement arbitrary strategies with reduced-loss-only feedback, or establish the published fixed-point-defined improper class. It also proves no general bounded-convex theorem, randomized strategy theorem, computational complexity guarantee, approachability criterion, or asymptotic minimax rate result. Retaining these boundaries makes the source of the exact identity and the meaning of the verified statements directly inspectable.

References