Introduction to Linear Optimization X: Max-Flow Min-CutTextbook
How much flow can be sent from a source $s$ to a sink $t$ through a network with arc capacities $u_{ij}\in(0,\infty]$ — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination $\mathbf{f}=\sum_i a_i\mathbf{f}^i$ of simple circulations with only forward arcs, with integer $a_i$ when $\mathbf{f}$ is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ($\max b_s$ s.t. $\mathbf{A}\mathbf{f}=\mathbf{b}$, $b_t=-b_s$, $b_i=0$ for $i\ne s,t$, $0\le\mathbf{f}\le\mathbf{u}$), defines augmenting paths (Definition 7.2: $f_{ij}<u_{ij}$ on forward arcs, $f_{ij}>0$ on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:
(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;
(b) the value of the maximum flow equals the minimum cut capacity $$C(S)=\sum_{\{(i,j)\in\mathcal{A}\mid i\in S,\,j\notin S\}}u_{ij}$$ — the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).
Matrix Completion has No Spurious Local MinimumResearch Paper
Matrix completion — recovering a low-rank matrix $M = ZZ^\top$ from a small random subset of its entries — powers recommender systems and collaborative filtering. In practice it is solved by running (stochastic) gradient descent on the non-convex objective $$f(X)=\min_X\frac12\|P_\Omega(M-XX^\top)\|_F^2+\lambda R(X)$$
where $\Omega=\{(i,j)|M_{i,j} \text{ is observed}\}$ and $R(X)$ is a certain regularizer. from a random starting point, and it just works.
Ge, Lee and Ma (NeurIPS 2016 Best student paper award) explained why: the regularized objective has *no spurious local minima* — every local minimum is global and exactly recovers $M$. This mission formalizes that landmark theorem in Lean 4, in its strongest known form and along its simplest known proof: the unified landscape analysis of Ge–Jin–Zheng (ICML 2017) and an improved sampling bound in Chen–Li (JMLR 2019). Conditional on an explicit good-sample predicate (which holds with high probability under Bernoulli sampling), every local minimum $X$ of $f$ satisfies $XX^\top = ZZ^\top$.
Bandit Algorithms XIII: Pure Exploration and Best-Arm IdentificationTextbook
Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time $\tau$ and a recommendation must be *sound* (wrong with probability at most $\delta$) while minimizing $\mathbb{E}[\tau]$. The information-theoretic complexity is $c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')$: every sound strategy needs $\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}$, and the Track-and-Stop algorithm — the goal theorem — achieves $\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)$ exactly. The mission also covers the fixed-budget counterpart, sequential halving.
Vector Space Methods VIII: Fenchel DualityTextbook
## Motivation
Convex duality converts an optimization problem over points into one over linear functionals. It supplies lower bounds, certificates of optimality, and alternative formulations whose geometry can be simpler than the primal problem. In §§7.8–7.12 of David G. Luenberger's [*Optimization by Vector Space Methods*](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods), this theory is developed for finite-valued convex and concave functions on convex subsets of a real normed space. The capstone is Fenchel duality with restricted domains and an attained continuous-linear-functional dual optimum. This mission preserves that functional-analytic setting rather than reducing the theorem to Euclidean space or silently extending the functions to the whole space.
## Setting
Let $X$ be a real normed space, let $C,D\subseteq X$ be nonempty convex sets, let $f:X\to\mathbb R$ be convex on $C$, and let $g:X\to\mathbb R$ be concave on $D$. For a continuous linear functional $\ell\in X^*$, the **restricted convex conjugate** and **restricted concave conjugate** are
$$
f_C^*(\ell)=\sup_{x\in C}\bigl(\ell(x)-f(x)\bigr),\qquad
g_D^*(\ell)=\inf_{x\in D}\bigl(\ell(x)-g(x)\bigr).
$$
The convex conjugate is admitted into $C^*$ only when its defining set is bounded above; the concave conjugate is admitted into $D^*$ only when its defining set is bounded below. Because $C$ and $D$ are nonempty and the functions are real-valued, these predicates exactly exclude the unwanted infinite endpoint. The Lean definitions use real `sSup` and `sInf`, with boundedness carried explicitly by theorem hypotheses.
The **restricted epigraph** of $(f,C)$ is the set of $(x,r)$ satisfying $x\in C$ and $f(x)\le r$; the restricted hypograph of $(g,D)$ reverses the scalar inequality. Luenberger's qualification requires a common point of the relative interiors of $C$ and $D$, represented by Mathlib's `intrinsicInterior`, and also requires ordinary nonempty interior of at least one of these two graph sets.
## Formalization targets
### Main goal: Fenchel duality
Assume the finite primal value $\mu$ is the greatest lower bound of
$$
\{f(x)-g(x):x\in C\cap D\}.
$$
Prove that some $\ell_0\in C^*\cap D^*$ attains
$$
\mu=g_D^*(\ell_0)-f_C^*(\ell_0)
=\max_{\ell\in C^*\cap D^*}
\bigl(g_D^*(\ell)-f_C^*(\ell)\bigr).
$$
If $x_0$ attains the primal infimum, also prove that $x_0$ attains both conjugate extrema at $\ell_0$: $f_C^*(\ell_0)=\ell_0(x_0)-f(x_0)$ and $g_D^*(\ell_0)=\ell_0(x_0)-g(x_0)$.
### Milestones
The mission records four source milestones. A local minimum of a convex function on its convex domain is global (§7.8, Proposition 1). Convexity of a restricted function is equivalent to convexity of its restricted epigraph (§7.8, Proposition 2). The finite-conjugate domain and the convex conjugate are convex (§7.10, Proposition 1). Finally, a closed restricted epigraph agrees pointwise on $C$ with the continuous-linear biconjugate (§7.10, Proposition 2). Together these statements expose the geometric and conjugacy interfaces on which the capstone depends without turning every paragraph of the chapter into a separate item.
## Significance
The theorem gives an attained dual certificate in an arbitrary real normed space. Equality of primal and dual values eliminates a duality gap, while attainment produces a specific functional that can certify an optimal primal point through simultaneous conjugate equality. The biconjugate milestone is independently useful: it expresses a closed convex function as a supremum of continuous affine minorants on its domain.
Formalizing this material adds a restricted-domain conjugacy API that is not supplied by the existing project artifact named `fenchelConjugate`. That artifact accepts finite-valued functions on a Euclidean space and has no independent convex domain or concave conjugate. Reusing it here would erase hypotheses that are central to Luenberger's theorem. The new definitions remain small, but their exact boundedness contracts make them reusable for later separation, minimax, and Lagrange-duality missions. The theorem is classical; the mission asks for a checked development faithful to the 1969 source and the current Mathlib representation of continuous dual spaces.
## Difficulty
The qualification is not the usual finite-dimensional slogan that relative interiors merely intersect. The source additionally demands that either the restricted epigraph or restricted hypograph have nonempty ordinary interior. Dropping that condition changes the theorem in infinite-dimensional spaces. Replacing `intrinsicInterior` by topological `interior` would also make valid lower-dimensional domains appear empty.
Extended values create another boundary. Real `sSup` and `sInf` are meaningful here only together with nonempty domains and the respective boundedness hypotheses. Treating their default values outside those hypotheses as genuine conjugates would admit false dual candidates. A finite-dimensional conjugate definition avoids neither issue and would prove only a special case. The biconjugate target must quantify over continuous linear functionals, not all algebraic linear maps, because closed epigraph separation is topological. Finally, the dual statement must include actual attainment; proving only equality with a supremum would omit a principal assertion of §7.12.
## Formalization scope
All primal functions are finite-valued real functions. Infinite conjugate values are represented by domain predicates—`BddAbove` for $f_C^*$ and `BddBelow` for $g_D^*$—rather than by changing the public conjugate codomain. The primal finiteness assumption is encoded by a real number $\mu$ together with `IsGLB`, which simultaneously rules out an empty feasible intersection and an infimum of $-\infty$. Epigraph pairs are ordered as $(x,r)$ to match Mathlib conventions, although Luenberger prints the scalar coordinate first.
The ambient space is normed but is not assumed finite-dimensional, reflexive, or complete. Both $C$ and $D$ are explicitly nonempty. The main theorem keeps the common intrinsic-interior condition and the disjunctive ordinary-interior condition verbatim. Contributions may develop separation lemmas, boundedness facts for restricted conjugates, or direct proofs of the milestone statements. A whole-space Euclidean specialization is welcome only as a corollary, not as a replacement for the root. The minimax theorem of §7.13 and extended-real lower-semicontinuous variants are outside this mission.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 7, §§7.8–7.12, pp. 191–202. [Open Library record](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods)
- R. Tyrrell Rockafellar, *Convex Analysis*, Princeton University Press, 1970. [DOI: 10.1515/9781400873173](https://doi.org/10.1515/9781400873173)
Coppersmith–Winograd Bound: omega < 2.376Research Paper
AI generated but i think correct. I think the milestones make it really annoying but the central theorem looks correct.
## Motivation
The **matrix-multiplication exponent** measures the asymptotic number of field operations needed to multiply two square matrices. A bound $\omega<c$ means that, for every $\varepsilon>0$, two $n\times n$ matrices can be multiplied using $O(n^{c+\varepsilon})$ arithmetic operations. Matrix multiplication is a central benchmark in algebraic complexity and a primitive for many algorithms in linear algebra, graph theory, and symbolic computation.
After Strassen showed that $\omega<3$, a sequence of tensor constructions reduced the exponent further. Schönhage's asymptotic sum inequality made it possible to exploit simultaneous matrix products rather than a single square product. In 1990, [Don Coppersmith and Shmuel Winograd](https://www.sciencedirect.com/science/article/pii/S0747717108800132) combined an explicit low-border-rank tensor with a block extraction argument based on Salem--Spencer sets. Their basic analysis gave $\omega<2.38719$; coupling the random weights in the tensor square sharpened this to $\omega<2.375477$, hence the exact rational consequence $\omega<2.376$.
This mission formalizes that historical Coppersmith--Winograd result. It follows the source tensor and its actual block restrictions, while excluding placeholder “laser values” that are not backed by extracted direct sums of matrix-multiplication tensors.
## Setting
For a field $K$, an order-three tensor is represented by three finite-dimensional $K$-vector spaces and an element of their tensor product. The matrix-multiplication tensor
$$
\langle a,b,c\rangle_K
=\sum_{i<a}\sum_{j<b}\sum_{k<c}
x_{ij}\otimes y_{jk}\otimes z_{ki}
$$
encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A **restriction** applies one linear map to each tensor leg. A **degeneration** permits those maps to depend polynomially on a formal parameter and selects their first nonzero coefficient. Thus a degeneration from the diagonal tensor $I_r$ is a border-rank certificate $\underline R(T)\le r$.
The **Coppersmith--Winograd tensor** with parameter $q$ is
$$
T_q=
\sum_{i=1}^{q}
(x_0y_i z_i+x_i y_0z_i+x_i y_i z_0)
+x_0y_0z_{q+1}+x_0y_{q+1}z_0+x_{q+1}y_0z_0.
$$
It has border rank at most $q+2$. Its coordinates carry three classes, indexed by $0,1,2$, and its six nonzero block types are
$$
(0,1,1),\ (1,0,1),\ (1,1,0),\ (0,0,2),\ (0,2,0),\ (2,0,0).
$$
The first three blocks are matrix-multiplication tensors with dimensions $(1,1,q)$, $(q,1,1)$, and $(1,q,1)$; the other three are scalar products. Tensor powers therefore contain many typed rectangular matrix products. The **laser method** selects a large family with disjoint coordinate blocks and applies Schönhage's asymptotic sum inequality to all surviving products simultaneously.
## Formalization targets
### Goal: the 1990 Coppersmith--Winograd bound
For every field $K$,
$$
\operatorname{matMulExp}(K)<\frac{297}{125}=2.376.
$$
The Lean goal has the same quantified proposition and the same `matMulExp` definition as the existing Schönhage-bound mission; only the theorem identifier and rational endpoint change.
### Tensor and block foundations
The development records the characteristic-free order-three degeneration
$$
T_q\unlhd I_{q+2}
$$
and the exact matrix-product dimensions associated with every supported type sequence in $T_q^{\otimes N}$. These statements identify the algebraic input before any asymptotic counting is used.
### Coupled-weight extraction
For $q=6$, the tensor-square grading and the coupled-weight pruning must produce the direct sums and asymptotic inequality stated in Section 8 and in the coupled-constituent lemma on journal pp. 270--272. The final numerical milestone certifies the rational endpoint $297/125$ from exact inequalities, rather than treating the decimal $2.375477$ as a proof object.
## Significance
The result was the strongest matrix-multiplication bound for roughly two decades and introduced the tensor family that underlies the classical laser-method line of work. A formal proof supplies a checked bridge from an explicit border-rank identity to an exponent bound whose combinatorial extraction is substantially more delicate than the earlier Schönhage examples.
The formalization also produces reusable infrastructure. The order-three CW degeneration is an explicit polynomial-family test case over arbitrary fields. The six block identifications and type-count formulas can be reused in analyses of tensor powers. A faithful extraction predicate, stated through actual restrictions to direct sums of `MMObj` tensors, separates sound laser arguments from formulas that count incompatible or coordinate-sharing blocks as independent.
The mathematical bound is known. The open work is its machine-checked reconstruction in Lean. The border-rank theorem, per-type matrix-product restriction layer, tensor-square support invariant, balanced block calculation, Salem--Spencer set theorem, and exact $q=6$ numerical endpoint are already proved. The unrestricted value/rank bridge, the coupled-constituent extraction, and the full Section 8 auxiliary inequality remain the substantive frontier.
## Difficulty
The main difficulty is not expanding $T_q$ or evaluating a decimal logarithm. A tensor power contains exponentially many typed terms, but most share variables. They cannot all be placed in a direct sum, and counting all joint type sequences overestimates the usable matrix products. The source hashes coordinate blocks into a large progression-free set and prunes collisions so that the surviving blocks are genuinely independent.
The $2.376$ improvement adds a second layer. It begins with $T_q^{\otimes2}$, regroups variables into five classes, couples weights that were independent in the simpler analysis, and estimates a nontrivial central block by a further extraction. A formal proof must track the direction of every restriction, the exact multiplicities of all block types, and the loss introduced by pruning. Replacing exponential surviving-block counts by a polynomial number of blocks, or using joint entropy without the marginal compatibility constraints, changes the mathematical claim and is outside the mission.
## Formalization scope
The mission uses the existing `TensorObj`, `MMObj`, `TensorObj.Restrict`, `Degenerates`, `tensorAsymptoticRank`, `matMulExp`, and `matMulExp_strassen` declarations in the Mathlib environment pinned by the earlier matrix-multiplication mission. Tensor dimensions and type counts are natural numbers; exponent and optimization inequalities are real-valued. All top-level bounds quantify over an arbitrary field, matching the integral polynomial identities used by the construction.
Laser statements must exhibit, directly or through a faithful reusable predicate, restrictions from a tensor power to a finite direct sum of concrete matrix-multiplication tensors. The number and dimensions of the summands remain part of the witness. A constant-valued “laser functional,” a vacuous witness hypothesis, or a capacity definition that discards the exponential number of surviving blocks does not satisfy the mission.
Welcome contributions include restriction composition lemmas, tensor-power block equivalences, multinomial and entropy estimates with all marginal constraints, formal Salem--Spencer pruning, exact real-inequality certificates, and the coupled central-block value lemma. Every milestone should cite the corresponding equation, table, or lemma in the primary paper.
## Selected references
- Don Coppersmith and Shmuel Winograd, *Matrix Multiplication via Arithmetic Progressions*, Journal of Symbolic Computation 9, 1990, pp. 251--280. [ScienceDirect](https://www.sciencedirect.com/science/article/pii/S0747717108800132).
- Arnold Schönhage, *Partial and Total Matrix Multiplication*, SIAM Journal on Computing 10(3), 1981, pp. 434--455. [DOI 10.1137/0210032](https://doi.org/10.1137/0210032).
- Avi Wigderson and Jeroen Zuiddam, *Asymptotic Spectra: Theory, Applications and Extensions*, 2023, for the tensor restriction and asymptotic-rank framework used by the Lean development. [Author manuscript](https://www.math.ias.edu/~avi/PUBLICATIONS/WigdersonZu_Final_Draft_Oct2023.pdf).
Schönhage–Pan–Winograd Bound: omega < 2.522Research Paper
## Motivation
The **matrix-multiplication exponent** measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, $N\times N$ matrices can be multiplied using $O(N^{c+\varepsilon})$ arithmetic operations for every $\varepsilon>0$. Improvements to $\omega$ are a central benchmark in algebraic complexity because matrix multiplication is also a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The existing Prove2Me mission formalizes Schönhage's bound $\omega<2.55$ from a concrete two-summand tensor degeneration. The present mission advances the same formal development to the next clean historical construction. Pan and Winograd found a simultaneous approximate algorithm for three matrix products; [Romani recorded its tensor form and the parameter choice $n=11$, $k=5$](https://iris.cnr.it/retrieve/7f08fe3e-3ef4-42b1-b84f-82ba5e09c61a/prod_421763-doc_149822.pdf), which gives $\omega\le 2.5218127\ldots$. [Schönhage's 1981 paper](https://doi.org/10.1137/0210032) reports the equivalent bound $3\log 52/\log 110$ in the arbitrary-field setting. The exact formal target here is the slightly weaker rational inequality $\omega<1261/500=2.522$.
## Setting
For a field $K$, the **matrix-multiplication tensor** $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix:
$$
\langle a,b,c\rangle_K
=\sum_{i<a}\sum_{j<b}\sum_{\ell<c}
e_{ij}\otimes e_{j\ell}\otimes e_{\ell i}.
$$
A direct sum places several such tensors in disjoint coordinate blocks. A tensor $T$ has border rank at most $r$ when it is a polynomial degeneration of the diagonal tensor $I_r=\sum_{s<r}e_s\otimes e_s\otimes e_s$. In the Lean development this relation is `Degenerates T (TensorObj.diagObj K 3 r)`. The argument order matters: the first tensor is the target and the diagonal tensor is the source.
The platform already defines ordinary tensor rank, asymptotic tensor rank, the tensor-rank exponent `matMulExp K`, the equivalent Strassen-preorder exponent `matMulExp_strassen K`, and Schönhage's asymptotic sum inequality. This mission reuses those declarations. No alternative definition of $\omega$ is introduced.
## Formalization targets
The goal has exactly the same quantified proposition as the existing $2.55$ mission, with only the rational endpoint changed:
$$
\forall K\;[\mathrm{Field}(K)],\qquad
\operatorname{matMulExp}(K)<\frac{1261}{500}.
$$
The source construction to be formalized is
$$
\underline R\!\left(
\langle1,5,22\rangle_K\oplus
\langle11,2,5\rangle_K\oplus
\langle10,11,1\rangle_K
\right)\le156.
$$
Each summand has volume $110$:
$$
1\cdot5\cdot22=11\cdot2\cdot5=10\cdot11\cdot1=110.
$$
The milestone chain records the degeneration, its asymptotic-rank consequence, the exact numerical implication
$$
3\cdot110^{\omega^{\mathrm{Str}}_K/3}\le156
\quad\Longrightarrow\quad
\omega^{\mathrm{Str}}_K<\frac{1261}{500},
$$
and the resulting Strassen-form exponent bound. The public goal then transfers the bound to `matMulExp K` through the already established equality of the two exponent definitions.
## Significance
Mathematically, this construction improves the concrete exponent certified by the existing mission from $2.55$ to $2.522$ without changing the surrounding theory. It isolates the first genuinely new ingredient after the accepted Schönhage example: a larger simultaneous tensor degeneration rather than a sharper numerical estimate for the old witness.
For formalization, the mission tests whether the current polynomial-degeneration API can express a historically important trilinear aggregation at realistic scale. Once the explicit witness is available, the remaining declarations form a reusable template for later bounds: a source tensor degeneration, an asymptotic-rank bound, a specialization of the asymptotic sum inequality, and a final exponent transfer. This creates a trustworthy stepping stone toward the Coppersmith--Winograd tensor and later laser-method analyses.
The $2.522$ theorem is known mathematically; the open work is its machine-checked Lean formalization. The exact numerical endpoint and every downstream bridge from the degeneration have already been checked locally. The explicit Pan--Winograd degeneration remains the substantive open milestone.
## Difficulty
The central difficulty is not the logarithmic comparison. It is constructing and verifying the polynomial family whose leading nonzero coefficient is exactly the tagged direct sum of the three matrix-multiplication tensors and whose earlier coefficients vanish. The family has $156$ diagonal source slots and many indexed target coordinates. A proof must account for all mixed-coordinate terms and all cancellations uniformly over an arbitrary field.
[Romani's published summary](https://iris.cnr.it/retrieve/7f08fe3e-3ef4-42b1-b84f-82ba5e09c61a/prod_421763-doc_149822.pdf) states the approximate-rank inequality but does not spell out a Lean-ready map between its trilinear forms and the platform's `TensorObj.bigAdd` coordinate spaces. A solver must therefore recover the source indexing carefully and prove that the resulting modewise linear maps have the required coefficients. Reversing the degeneration direction, conflating tensor rank with asymptotic rank, or silently assuming a characteristic-zero scalar identity would invalidate the result.
## Formalization scope
All theorems quantify over an arbitrary type $K$ with `[Field K]`, matching the existing Schönhage goal and the arbitrary-field statement of the source bound. Tensor spaces are finite-dimensional function spaces already packaged by `MMObj`; the three products are combined with `TensorObj.bigAdd`. Border rank is represented by the existing finitely supported polynomial-family predicate `Degenerates`. Because the source summary specifies approximate rank but not a leading order, the main degeneration milestone existentially quantifies that order instead of hard-coding one.
The mission includes no placeholder laser-value definition and makes no claim about the later $2.376$ analysis. It also excludes Schönhage's additional microscopic symmetrization improvement beyond $3\log52/\log110$. A valid solution must construct the stated degeneration itself; a vacuous hypothesis or a redefinition of `matMulExp` is outside scope.
Reusable contributions include coefficient lemmas for polynomial tensor families, finite-index equivalences for direct sums, and generic aggregation identities that specialize to the $n=11$, $k=5$ witness. Contributions that merely restate the target under stronger field hypotheses do not close the arbitrary-field milestone.
## Selected references
- A. Schönhage, *Partial and Total Matrix Multiplication*, SIAM Journal on Computing 10(3), 1981, pp. 434--455. [DOI 10.1137/0210032](https://doi.org/10.1137/0210032).
- Francesco Romani, *Some Properties of Disjoint Sums of Tensors Related to Matrix Multiplication*, CNR Nota Interna B80-4, February 1980, printed p. 6; journal version, SIAM Journal on Computing 11(2), 1982. [Archived preprint](https://iris.cnr.it/retrieve/7f08fe3e-3ef4-42b1-b84f-82ba5e09c61a/prod_421763-doc_149822.pdf) and [DOI 10.1137/0211020](https://doi.org/10.1137/0211020).
- Avi Wigderson and Jeroen Zuiddam, *Asymptotic Spectra: Theory, Applications and Extensions*, 2023, for the tensor-preorder and asymptotic-rank framework reused by the Lean development. [Author manuscript](https://www.math.ias.edu/~avi/PUBLICATIONS/WigdersonZu_Final_Draft_Oct2023.pdf).
Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$-fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,
$$x_0 + \tfrac{1}{n}\,(\mathcal{E} - x_0) \;\subseteq\; C \;\subseteq\; \mathcal{E},$$
and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$, exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ($\sum_i \lambda_i x_i x_i^{T} = I$, $\sum_i \lambda_i x_i = 0$, $\sum_i \lambda_i = n$), the convex-combination step that produces the $1/n$ ball, and affine invariance.
Introduction to Linear Optimization XIII: Lagrangean Duality and Integer ProgrammingTextbook
Linear programming has a complete duality theory; integer programming does not — and the Lagrangean dual measures exactly how far duality reaches. This mission formalizes the duality theory of integer programming from Section 11.4 of Bertsimas–Tsitsiklis, built on the general linear programming duality of Section 4.10. For the integer program $$Z_{IP} = \min\{c'x : Ax \ge b,\ Dx \ge d,\ x \text{ integer}\}$$ with integer data, the complicating constraints $Ax \ge b$ are dualized with multipliers $p \ge 0$ over the tractable set $X = \{x \text{ integer} \mid Dx \ge d\}$: the dual function is $$Z(p) = \min_{x \in X}\big(c'x + p'(b - Ax)\big)$$ and the Lagrangean dual is $Z_D = \max_{p \ge 0} Z(p)$. Weak duality $Z_D \le Z_{IP}$ (Theorem 11.2) always holds, but strong duality can fail. The convex hull $CH(X)$ of the integer points of a polyhedron with integer data is itself a polyhedron (Theorem 11.3, Meyer's theorem), and the capstone — Theorem 11.4, the central result of Section 11.4 — identifies the Lagrangean dual exactly: $Z_D$ equals the optimal cost of the linear program $$\min\{c'x : Ax \ge b,\ x \in CH(X)\}$$. This is the geometric explanation of the strength of Lagrangean relaxation, yields the bound ordering $Z_{LP} \le Z_D \le Z_{IP}$, and Corollary 11.1 characterizes exactly when the bounds collapse. The polyhedral engine is the general weak/strong duality pair (Theorems 4.17/4.18) over a primal $\min c'x$ s.t. $Ax \ge b$, $x \in P = \{x \mid Dx \ge d\}$, and the formulation-strength comparison $P_{sub} \subseteq P_{cut}$ of Theorem 10.1 supplies the motivating principle that tighter relaxations of the same integer set give sharper bounds.
Parallel repetition for quantum gamesResearch Paper
# Parallel repetition for quantum games
## Nonlocal games
A **nonlocal game** is played between a classical referee and two or more cooperating players who are not allowed to communicate during the game. In the two-player, one-round setting, the referee samples a pair of questions $(x,y)$ from a distribution $\mu$, sends $x$ to Alice and $y$ to Bob, and receives answers $a$ and $b$. The players win when a predicate $V(x,y,a,b)$ accepts. Before the game begins they may agree on a strategy and share a resource, but after receiving their questions they are isolated from one another.
Nonlocal games occupy a useful interface between complexity theory and quantum information. From the perspective of complexity theory, they are the basic objects underlying multiprover interactive proofs: a verifier delegates a computation to separated provers and uses the consistency of their answers to distinguish valid from invalid claims. Classical two-prover games play a central role in the PCP theorem, hardness of approximation, and soundness amplification. Allowing the provers to share entanglement leads to the class $\mathrm{MIP}^*$ and to a substantially richer theory. The theorem $\mathrm{MIP}^*=\mathrm{RE}$ shows how dramatically entanglement changes this landscape: even estimating the entangled value of a nonlocal game can encode undecidable computation [Ji--Natarajan--Vidick--Wright--Yuen 2020](https://arxiv.org/abs/2001.04383).
From the perspective of quantum information, nonlocal games are operational formulations of Bell experiments. A separation between classical and entangled values witnesses correlations that cannot be explained by a local hidden-variable model. The same framework supports **self-testing**, in which near-optimal behavior certifies the underlying state and measurements up to local equivalence, and **device-independent cryptography**, in which security or randomness is certified from observed input-output statistics rather than a trusted description of the devices. Representative references include [Cleve--Høyer--Toner--Watrous 2004](https://arxiv.org/abs/quant-ph/0404076), [Reichardt--Unger--Vazirani 2013](https://doi.org/10.1038/nature12035), and [Pironio et al. 2010](https://doi.org/10.1038/nature09008). The survey of [Palazuelos--Vidick 2016](https://arxiv.org/abs/1512.00419) describes further connections among nonlocal games, Bell inequalities, operator spaces, and quantum information.
Thus the value of a nonlocal game is simultaneously a complexity-theoretic soundness parameter and a quantitative measure of the power of nonclassical correlations. Understanding how this value changes under natural operations on games is important in both subjects.
## Entangled strategies and value
We take the finite answer alphabets to be nonempty. In a classical strategy, Alice's answer depends only on $x$, Bob's answer depends only on $y$, and the players may coordinate using shared randomness. In a finite-dimensional entangled strategy, the players share a bipartite state $\rho$ and use POVM measurement operators
$$
\{A_a^x\}_{a\in A}
\qquad\text{and}\qquad
\{B_b^y\}_{b\in B}
$$
for their respective questions. The probability of producing answers $(a,b)$ on questions $(x,y)$ is
$$
\operatorname{Re}\operatorname{Tr}\!\left(\rho\,(A_a^x\otimes B_b^y)\right).
$$
The supremum of the winning probability over all such finite-dimensional strategies is the **entangled value** $\omega^*(G)$. This optimization ranges over arbitrary local dimensions, shared states, and local measurements, which is one reason even apparently elementary questions about nonlocal games can be difficult.
## Parallel repetition
For a positive integer $n$, the repeated game $G^n$ consists of $n$ independently sampled copies of $G$ played simultaneously. Alice receives $(x_1,\ldots,x_n)$, Bob receives $(y_1,\ldots,y_n)$, and they answer with tuples $(a_1,\ldots,a_n)$ and $(b_1,\ldots,b_n)$. They win only if
$$
V(x_i,y_i,a_i,b_i)=1
$$
for every coordinate $i$.
Parallel repetition is a basic method of **soundness amplification**. Starting from a game that dishonest players cannot win with certainty, the verifier repeats the test in the hope of driving the optimal success probability rapidly toward zero. The difficulty is that independence in the verifier's sampling does not force independence in the players' strategy. Alice may choose her entire answer tuple as a function of all her questions, Bob may do the same, and an entangled strategy may use a single state and joint measurements spanning all coordinates. In particular, one cannot obtain an upper bound on $\omega^*(G^n)$ merely by analyzing the strategy that plays each coordinate independently.
For classical games, Raz's parallel repetition theorem gives exponential decay whenever the one-shot value is below one [Raz 1998](https://doi.org/10.1137/S0097539795280895). Establishing the corresponding behavior for entangled games has been a long-running problem. A general polynomial bound was proved in [Yuen 2016](https://arxiv.org/abs/1604.04340), implying for the first time that $\omega^*(G^n)$ tends to zero for every finite two-player entangled game with $\omega^*(G)<1$.
The full exponential-decay theorem was recently settled by OpenAI. In Chapter 6 of [*Ten Advances in Mathematics and Theoretical Computer Science*](https://cdn.openai.com/pdf/ten-proofs-oai.pdf), OpenAI proves that for every finite two-player entangled game $G$ with $\omega^*(G)<1$, there is a constant $c_G>0$ such that
$$
\omega^*(G^n)\le e^{-c_G n}
$$
for every positive $n$. OpenAI also released a [Lean certificate](https://github.com/openai/ten-proofs/blob/main/QuantumParallelRepetition.lean) for the result. This resolves the general quantum parallel-repetition conjecture, but it does not end the study of the problem. The proof introduces quantitative losses and a substantial technical apparatus, and there remains considerable value in finding alternative arguments, isolating the essential mechanism, improving the dependence on the one-shot gap and answer size, and producing shorter or more conceptual formal proofs.
## A hierarchy of formalization targets
This mission develops a reusable Lean framework for parallel repetition rather than formalizing only one paper. Its targets are organized by the strength of the asserted decay.
### Qualitative decay
The main mission theorem is the fundamental asymptotic statement:
$$
\omega^*(G)<1
\quad\Longrightarrow\quad
\lim_{n\to\infty}\omega^*(G^n)=0.
$$
Equivalently, for every $\delta>0$, all sufficiently large $n$ satisfy $\omega^*(G^n)<\delta$. This statement deliberately specifies no rate. It is a stable top-level theorem that can be recovered from any sufficiently strong quantitative bound.
### Polynomial decay
A stronger target asks for game-dependent constants $C>0$ and $\alpha>0$ such that
$$
\omega^*(G^n)\le Cn^{-\alpha}.
$$
The abstract formulation avoids fixing a particular exponent or logarithmic correction. More refined formalizations can record explicit dependence on the gap $1-\omega^*(G)$, the answer alphabet, or other game parameters. Yuen's 2016 theorem is one important result at this level.
### Exponential decay
The exponential target asks for game-dependent constants $C,c>0$ such that
$$
\omega^*(G^n)\le C e^{-cn}.
$$
Following OpenAI's recent resolution, this target is now a theorem rather than an open conjecture. Within this mission it remains a central milestone: contributors may formalize the released argument in the mission's common interface, construct an independent proof, seek a more elegant or modular proof, or establish sharper quantitative variants.
These levels do not exhaust the project. The same framework can accommodate explicit finite-$n$ inequalities, stretched-exponential estimates, bounds for structured classes of games, improved parameter dependence, and reductions showing that one decay statement implies another.
## Formalization scope
The foundational Lean development represents a game by finite question sets $X,Y$, finite answer sets $A,B$, a nonnegative normalized question distribution $\mu(x,y)$, and a Boolean verification predicate $V(x,y,a,b)$. The parallel-repetition theorems explicitly assume that $A$ and $B$ are nonempty. The development defines finite-dimensional entangled strategies using density matrices and POVM measurement operators, defines the repeated game on tuples, and takes the entangled value as a supremum over all finite-dimensional strategies. Repeated strategies are indexed by complete question tuples and are not required to factor coordinatewise.
A complete development will draw on formal libraries for finite probability, tensor products, positive semidefinite matrices, density matrices, POVMs, trace norms, fidelity, entropy, mutual information, and correlated sampling. These components should be formulated for reuse and should expose the dependence of each bound on the relevant game parameters.
The goal is both to verify parallel-repetition theorems and to build a dependable language for nonlocal games in Lean. Formalization forces distinctions that are easy to suppress on paper: whether constants depend on the game, whether a bound holds for all $n$ or only asymptotically, which strategy model is optimized over, and which hypotheses are needed for a particular rate. The mission welcomes reconstructions of known proofs as well as new, shorter, or conceptually different proofs.
## Selected references
- R. Cleve, P. Høyer, B. Toner, and J. Watrous, [*Consequences and limits of nonlocal strategies*](https://arxiv.org/abs/quant-ph/0404076), CCC 2004.
- R. Raz, [*A parallel repetition theorem*](https://doi.org/10.1137/S0097539795280895), SIAM Journal on Computing 27(3), 1998.
- H. Yuen, [*A parallel repetition theorem for all entangled games*](https://arxiv.org/abs/1604.04340), ICALP 2016.
- Z. Ji, A. Natarajan, T. Vidick, J. Wright, and H. Yuen, [$\mathrm{MIP}^*=\mathrm{RE}$](https://arxiv.org/abs/2001.04383), Communications of the ACM 64(11), 2021.
- OpenAI, [*Ten Advances in Mathematics and Theoretical Computer Science*](https://cdn.openai.com/pdf/ten-proofs-oai.pdf), Chapter 6, 2026; accompanying [Lean formalization](https://github.com/openai/ten-proofs/blob/main/QuantumParallelRepetition.lean).
Markov Entanglement: Value Decomposition Error in Multi-agent MDPsResearch Paper
Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not *entangled* — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.
Introduction to Linear Optimization XII: Interior Point Methods and Path FollowingTextbook
Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For $\mu > 0$ the logarithmic barrier $$B_\mu(\mathbf{x}) = \mathbf{c}'\mathbf{x} - \mu\sum_{j=1}^n \log x_j$$ replaces the constraint $\mathbf{x} \ge \mathbf{0}$; the minimizers $\mathbf{x}(\mu)$ of $B_\mu$ over $\{A\mathbf{x} = \mathbf{b}\}$ trace the central path, characterized by the KKT conditions (9.17): $A\mathbf{x} = \mathbf{b}$, $\mathbf{x} \ge \mathbf{0}$, $A'\mathbf{p} + \mathbf{s} = \mathbf{c}$, $\mathbf{s} \ge \mathbf{0}$, $XS\mathbf{e} = \mu\mathbf{e}$ (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink $\mu^{k+1} = \alpha\mu^k$, maintaining the proximity invariant $$\|\frac{1}{\mu}XS\mathbf{e} - \mathbf{e}\| \le \beta$$. The goal theorem is Theorem 9.7: with $\alpha = 1 - \frac{\sqrt{\beta}-\beta}{\sqrt{\beta}+\sqrt{n}}$ and a $\beta$-close start, after $K = \Big\lceil \frac{\sqrt{\beta}+\sqrt{n}}{\sqrt{\beta}-\beta}\,\log\frac{(\mathbf{s}^0)'\mathbf{x}^0(1+\beta)}{\varepsilon(1-\beta)} \Big\rceil$ iterations the algorithm reaches primal and dual feasible solutions with duality gap $(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon$ — the explicit form of the celebrated $O(\sqrt{n}\log(1/\varepsilon))$ iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting $G(\mathbf{x},\mathbf{s}) = q\log\mathbf{s}'\mathbf{x} - \sum_j \log x_j - \sum_j \log s_j$ by $\delta$ per step reaches gap $\varepsilon$ within an explicit $K$.
Introduction to Linear Optimization XI: The Ellipsoid MethodTextbook
Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is $$E(\mathbf{z}, D) = \{\mathbf{x} \in \mathbb{R}^n \mid (\mathbf{x}-\mathbf{z})'D^{-1}(\mathbf{x}-\mathbf{z}) \le 1\}$$ with $D$ symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid $E \cap \{\mathbf{x} \mid \mathbf{a}'\mathbf{x} \ge \mathbf{a}'\mathbf{z}\}$ is contained in the explicitly constructed ellipsoid $E' = E(\bar{\mathbf{z}}, \bar{D})$, $$\bar{\mathbf{z}} = \mathbf{z} + \frac{1}{n+1}\frac{D\mathbf{a}}{\sqrt{\mathbf{a}'D\mathbf{a}}},$$ $$\bar{D} = \frac{n^2}{n^2-1}\big(D - \frac{2}{n+1}\frac{D\mathbf{a}\mathbf{a}'D}{\mathbf{a}'D\mathbf{a}}\big),$$ and the volume contracts: $$\mathrm{Vol}(E') < e^{-1/(2(n+1))}\,\mathrm{Vol}(E)$$. Two integer-data estimates make the contraction decisive: every extreme point of $P = \{\mathbf{x} \mid A\mathbf{x} \ge \mathbf{b}\}$ with entries bounded by $U$ has coordinates in $[-(nU)^n, (nU)^n]$ (Lemma 8.2), and a full-dimensional bounded such polyhedron has $\mathrm{Vol}(P) > n^{-n}(nU)^{-n^2(n+1)}$ (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball $E(\mathbf{x}_0, r^2 I)$ of volume at most $V$ containing $P$, with $v$ a lower bound on $\mathrm{Vol}(P)$ when $P$ is nonempty, the ellipsoid method correctly decides whether $P$ is empty within $t^* = \lceil 2(n+1)\log(V/v) \rceil$ iterations — the explicit iteration count behind the polynomial-time headline.
Introduction to Linear Optimization IX: Network Flow IntegralityTextbook
Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph $G=(\mathcal{N},\mathcal{A})$ with external supplies $b_i$, arc costs $c_{ij}$, and the node-arc incidence matrix $\mathbf{A}$ — an $n\times m$ matrix in which every column has exactly one $+1$ (start node) and one $-1$ (end node) — so that flow conservation reads $\mathbf{A}\mathbf{f}=\mathbf{b}$, forcing the standing assumption $\sum_{i\in\mathcal{N}} b_i=0$. Because the rows of $\mathbf{A}$ sum to zero, the book works with the truncated matrix $\tilde{\mathbf{A}}$ of the first $n-1$ rows. The combinatorial heart is the correspondence between algebra and graph structure: a set $T$ of $n-1$ arcs forming a tree determines a unique tree solution of $\tilde{\mathbf{A}}\mathbf{f}=\tilde{\mathbf{b}}$, $f_{ij}=0$ off $T$ (Theorem 7.3); connectedness makes $\tilde{\mathbf{A}}$ full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix $\mathbf{B}$ has an integer inverse $\mathbf{B}^{-1}$ (its determinant is $\pm 1$ by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.
Introduction to Linear Optimization VIII: Sensitivity Analysis and Subgradients of the Optimal CostTextbook
How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem $\min\{c'x \mid Ax = b,\ x \ge 0\}$ (rows of $A$ linearly independent) as the requirement vector $b$ and the cost vector $c$ vary. On the convex set $S = \{b \mid P(b) \neq \emptyset\}$ of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost $F(b)$ is finite and convex (Theorem 5.1) — indeed $F(b) = \max_{i} (p^i)'b$ over the extreme points $p^1, \dots, p^N$ of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of $F$: if the primal at $b^*$ is feasible with finite optimal cost, then $p$ is an optimal solution of the dual if and only if $p$ is a subgradient of $F$ at $b^*$ (Definition 5.1: $F(b^*) + p'(b - b^*) \le F(b)$ for all $b \in S$) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set $T$ of cost vectors with finite optimal cost is convex, the optimal cost $G(c)$ is concave on $T$, and near any $c$ with a unique primal optimum $x^*$, $G$ is linear with gradient $x^*$. Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.
Introduction to Linear Optimization VII: Cones, Extreme Rays, and the Resolution TheoremTextbook
How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones $\{d \mid Ad \ge 0\}$ and their rays, extreme rays (defined, like basic solutions, by $n-1$ linearly independent active constraints), the pointedness criterion (Theorem 4.12: $0$ is an extreme point of a polyhedral cone iff the cone contains no line iff $n$ of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is $-\infty$ iff some extreme ray $d$ has $c'd < 0$). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron $P$ with at least one extreme point equals $Q = \{\sum_i \lambda_i x^i + \sum_j \theta_j w^j \mid \lambda_i \ge 0, \theta_j \ge 0, \sum_i \lambda_i = 1\}$ — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.
Introduction to Linear Optimization IV: The Simplex MethodTextbook
How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem $\min c'x$ subject to $Ax = b$, $x \ge 0$ has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs $$\bar{c}_j = c_j - c_B'B^{-1}A_j$$ measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ($\bar{c} \ge 0$ implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction $d$ satisfying $Ad = 0$, $d \ge 0$, $c'd < 0$ certifying optimal cost $-\infty$. The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.
Introduction to Linear Optimization I: Polyhedra and Basic Feasible SolutionsTextbook
Every linear programming problem asks to minimize a linear cost $c'x$ over a polyhedron — a set of the form $P = \{x \in \mathbb{R}^n \mid Ax \ge b\}$, or in standard form $\{x \mid Ax = b,\ x \ge 0\}$. Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the *extreme point* — a point of $P$ that cannot be written as a convex combination of two other points of $P$ (purely geometric, representation-independent); the *vertex* — the unique minimizer of some linear cost $c'y$ over $P$ (geometric, via supporting hyperplanes); and the *basic feasible solution* — a feasible point at which $n$ linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by $n$ linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.
Bandit Algorithms XVI: Markov Decision Processes and UCRL2Textbook
The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with $S$ states, $A$ actions and rewards in $[0,1]$. The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an *extended* MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability $1-\delta$, $\hat R_n < C\,D(M)\,S\sqrt{An\log(nSA/\delta)}$, where $D(M)$ is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound $\mathbb{E}[\hat R_n] \ge C'\sqrt{DSAn}$ brackets the true complexity of tabular reinforcement learning up to $\sqrt{DS}$.
A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.
In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.
That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.
Bandit Algorithms IV: Bernoulli Bandits and KL-UCBTextbook
When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of $[0,1]$, and the correct exponential rate is governed by the binary relative entropy $d(p,q) = p\log\frac{p}{q} + (1-p)\log\frac{1-p}{1-q}$ rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of $d$. The goal theorem shows KL-UCB attains $$\limsup_{n\to\infty} R_n/\log n = \sum_{i:\Delta_i>0} \Delta_i/d(\mu_i, \mu^*)$$ — asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.
Randomness appears to enlarge efficient computation, but the Sipser–Gács–Lautemann theorem places every bounded-error probabilistic polynomial-time language at the second level of the polynomial hierarchy, giving one of complexity theory’s foundational limits on the power of randomization.
Bandit Algorithms I: Concentration of MeasureTextbook
How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's *Bandit Algorithms*: a random variable $X$ is $\sigma$-subgaussian when $\mathbb{E}[e^{\lambda X}] \le e^{\lambda^2\sigma^2/2}$ for all $\lambda$, and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail $\mathbb{P}(X \ge \varepsilon) \le e^{-\varepsilon^2/(2\sigma^2)}$. The goal theorem is the Hoeffding-type bound: the sample mean of $n$ independent $\sigma$-subgaussian deviations exceeds the true mean by $\varepsilon$ with probability at most $\exp(-n\varepsilon^2/(2\sigma^2))$, together with its confidence form $\mathbb{P}\big(\hat\mu + \sqrt{2\sigma^2\log(1/\delta)/n} \le \mu\big) \le \delta$ — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.
Markov Entanglement: Decomposition Error via Agent-wise TV DistanceResearch Paper
Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a *Markov entanglement* measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.
Buying to Bundle: Asymptotic Optimality of Surrogate BundlingResearch Paper
A platform sourcing items from monopolistic sellers with private quality cannot tractably maximize its true profit: the bundle revenue $Rev(v_S)$ is neither monotone, submodular, supermodular, subadditive, nor superadditive. Theorem 4.6 of *Buying to Bundle: Optimal Sourcing from Monopolistic Sellers* shows that the simple surrogate threshold mechanism — maximize the linearized objective $\varpi(x)=N\,E[x(\mu)(\mu-\varphi(\mu))]$ — is profit-optimal up to a $1+O(N^{-1/3})$ factor in large markets. Prove it: Bernoulli concentration for the bundle quality plus sub-exponential control of the dispersion gap $|Rev(v)-E[v]|$ (Lemma 4.5).