Davie–Stothers Fourth-Power Bound: omega < 2.3737Research Paper
## Motivation
The **matrix-multiplication exponent** $\omega$ measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, two $n\times n$ matrices can be multiplied using $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$. It is a central benchmark in algebraic complexity and controls the exponent of many algorithms that use matrix multiplication as a subroutine.
Coppersmith and Winograd's 1990 analysis of the square of their tensor established $\omega<2.375477$. That number remained the record for roughly two decades. Stothers' 2010 thesis first obtained a smaller exponent by analyzing the fourth tensor power, and Davie and Stothers later supplied a self-contained journal treatment. Their Theorem 5.3 and numerical parameters give $\omega<2.373689703$; see [Davie--Stothers](https://www.maths.ed.ac.uk/~sandy/a11164.pdf), printed pp. 367--368. The result is the first historical step below the classical tensor-square barrier and is the natural next capstone after a formal proof of the $2.375477$ bound.
This mission formalizes the Davie--Stothers fourth-power argument at the exact rational endpoint $2.3737$. It concentrates on the new mathematical layer introduced by the fourth power: five non-matrix constituents, their recursive value estimates, and the two-dimensional same-marginal ambiguity in the final distribution count.
## Setting
For a field $K$, an order-three tensor represents a bilinear map. 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. Restrictions apply linear maps to the three tensor legs; degenerations permit polynomial families of maps. A direct sum of matrix-multiplication tensors has disjoint variable blocks and can be converted into an exponent inequality by Schönhage's asymptotic sum inequality.
The **Coppersmith--Winograd tensor** $CW_q$ has border rank at most $q+2$ and a three-class coordinate partition. Its square decomposes into fifteen coarse constituents $\varphi_{ijk}$ with $i+j+k=4$. Davie--Stothers square this decomposition again. The fourth power has forty-five constituents with indices summing to eight, grouped into ten symmetry classes represented by
$$
\varphi_{008},\ \varphi_{017},\ \varphi_{026},\ \varphi_{035},\ \varphi_{044},
\ \varphi_{116},\ \varphi_{125},\ \varphi_{134},\ \varphi_{224},\ \varphi_{233}.
$$
The first five classes are rectangular matrix-multiplication tensors. The last five require recursive value bounds. With $\rho\in[2,3]$, the paper writes
$$
E=(2q)^\rho,\qquad H=(q^2+2)^\rho,\qquad
L=4q^\rho(q^\rho+2),
$$
and states the five lower bounds in Lemma 5.1. The final fourth-power extraction assigns frequencies to the ten symmetry classes. Their coordinate marginals are encoded by the $9\times10$ matrix $Q$ in Equation (5.2); its kernel is the two-dimensional space $Y$ displayed immediately after that equation.
The paper's bounds are limiting exponential rates and may carry subexponential losses in their finite Salem--Spencer extractions. Prove2Me's `HasTauValueAtLeast` predicate instead records a constant-relative finite witness. The source-faithful formal statements therefore assert attainment of every fixed nonnegative base strictly below each displayed limiting rate, rather than unjustified attainment of the limiting endpoint itself. This downward-closed form retains the complete asymptotic conclusion and is exactly what the final strict numerical surplus needs.
## Formalization targets
### Goal: the Davie--Stothers fourth-power bound
For every field $K$,
$$
\operatorname{matMulExp}(K)<\frac{23737}{10000}=2.3737.
$$
The source's computed endpoint $2.373689703$ is strictly smaller, giving slack for an exact rational certificate. The Lean goal has exactly the same field quantification and `matMulExp` definition as the existing Coppersmith--Winograd mission; only the theorem identifier and endpoint change.
### Source-level milestones
The mission records the canonical nine-grading of $CW_6^{\otimes4}$ and the ten symmetry classes of Table 1. It formalizes all five clauses of Lemma 5.1 for $\varphi_{116}$, $\varphi_{125}$, $\varphi_{134}$, $\varphi_{224}$, and $\varphi_{233}$ in every-strict-lower-base form; Equation (5.2) and the stated basis of $\ker Q$; Lemma 5.2's entropy minimization along that kernel; Theorem 5.3's downward-closed fourth-power value inequality; and the Table 2 numerical specialization. The final milestones connect the resulting tau-value surplus to the border-rank budget and transfer the Strassen-preorder exponent bound to `matMulExp`.
## Significance
Mathematically, this theorem is the first improvement obtained by passing from the square to the fourth power of the Coppersmith--Winograd tensor. It establishes the recursive constituent pattern used by the later eighth-, sixteenth-, and higher-power analyses. In particular, the five formulas in Lemma 5.1 are the first complete catalogue of genuinely recursive fourth-power constituents.
For formalization, the mission creates a reusable representation of higher-power CW gradings and their symmetry orbits. It also forces a distinction between a locally chosen joint type and all other types with the same marginals. Lemma 5.2 is the exact finite-dimensional entropy correction needed when the marginal map has nontrivial kernel. That infrastructure can be reused by later refined-laser and complete-split missions.
The result is known mathematically. The open task is a machine-checked reconstruction. Prove2Me already contains the CW tensor, its characteristic-free border-rank degeneration, its canonical square grading and constituent restrictions, the Salem--Spencer layer, direct-sum tau-value witnesses, the asymptotic sum inequality, and the exponent bridge. The exact optimizer identity for the $\varphi_{116}$ profile is also proved. The remaining frontier is to connect the literal fourth-power constituents to finite direct-sum extractions, then assemble all five value estimates and the final kernel-corrected distribution count.
## Difficulty
The fourth power contains 225 ordered products before symmetry grouping. A formal proof must show that each claimed constituent is the literal block of $CW_q^{\otimes4}$ and that its recursive decomposition uses the correct variable spaces. Replacing a sum of overlapping blocks by an external direct sum would make the value bound artificially strong.
The five non-matrix classes have different feasible frequency polytopes. Their optimizer formulas are valid only after the corresponding nonnegativity and normalization conditions are checked. The $\varphi_{233}$ class already has a nontrivial same-marginal family. At the global level the map $Q$ has a two-dimensional kernel, so marginal counts alone do not determine a unique joint distribution. Ignoring that kernel removes the entropy penalty and invalidates Theorem 5.3.
Finally, Table 2 contains decimal witnesses obtained numerically. A formal proof must replace floating-point evaluation by exact rational parameters and certified bounds for logarithms and real powers, while retaining strict slack at $23737/10000$.
## Formalization scope
The development uses environment `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e` and the existing `TensorObj`, `MMObj`, restriction, degeneration, `HasTauValueAtLeast`, `tensorAsymptoticRank`, `matMulExp_strassen`, and `matMulExp` declarations. Top-level theorems quantify over an arbitrary field. Finite block indices and symmetry classes use finite types; frequency vectors and entropy inequalities use real numbers; exact finite profiles use natural numbers before passing to cofinal asymptotics.
The capstone specializes to $q=6$ and the fourth tensor power. Generic grading, orbit, multinomial, entropy, and optimizer lemmas are welcome when they shorten later missions. Every value theorem must ultimately be backed by restrictions or degenerations to direct sums of concrete matrix-multiplication tensors. An opaque value functional, a constituent definition that is an external sum rather than the source block, or a numerical hypothesis that assumes the desired endpoint is outside scope.
Contributions are welcome for the literal nine-grading, symmetry-orbit classification, the five constituent extractions, exact address factorizations, optimizer feasibility, the kernel calculation and Lemma 5.2, exact Table 2 arithmetic, and the final exponent assembly.
## Selected references
- A. M. Davie and A. J. Stothers, *Improved Bound for Complexity of Matrix Multiplication*, Proceedings of the Royal Society of Edinburgh Section A: Mathematics 143(2), 2013, pp. 351--369. [Author PDF](https://www.maths.ed.ac.uk/~sandy/a11164.pdf) and [DOI 10.1017/S0308210511001646](https://doi.org/10.1017/S0308210511001646).
- A. J. Stothers, *On the Complexity of Matrix Multiplication*, PhD thesis, University of Edinburgh, 2010. [Edinburgh Research Archive](https://era.ed.ac.uk/handle/1842/4734).
- Don Coppersmith and Shmuel Winograd, *Matrix Multiplication via Arithmetic Progressions*, Journal of Symbolic Computation 9, 1990, pp. 251--280. [DOI 10.1016/S0747-7171(08)80013-2](https://doi.org/10.1016/S0747-7171(08)80013-2).
- 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).
Algorithmic Game Theory I: Existence of Nash EquilibriumTextbook
## Motivation
The strategic-form game is the basic object of noncooperative game theory, and the **Nash equilibrium** — a profile of randomized strategies from which no player benefits by deviating unilaterally — is its central solution concept. Nash proved in 1951 that every game with finitely many players and finite strategy sets has such an equilibrium ([Nash, *Non-cooperative games*, Ann. Math. 54 (1951)](https://doi.org/10.2307/1969529)); this single existence theorem is the reason the concept organizes the rest of the field, from the computational complexity of finding equilibria to the price of anarchy. The theorem is stated as Theorem 1.8 of Nisan–Roughgarden–Tardos–Vazirani (eds.), *Algorithmic Game Theory* (Cambridge, 2007), the source text of this mission series, whose first chapter (Tardos–Vazirani) also treats the two special cases that admit direct algorithmic proofs: two-person zero-sum games, where equilibria are exactly the optimal solutions of a dual pair of linear programs (von Neumann 1928; Theorem 1.11), and a simple linear market, where equilibrium prices are computed by an ascending tight-set algorithm (Theorem 1.17).
A timeline of the existence theorem: von Neumann (1928) proved the minimax theorem for two-person zero-sum games; Nash (1950, 1951) extended existence to arbitrary finite games, first via Kakutani's fixed-point theorem and then via Brouwer's. All known proofs of the general theorem pass through a fixed-point principle, and this is not an artifact: computing a Nash equilibrium is PPAD-complete (Daskalakis–Goldberg–Papadimitriou 2009; Chen–Deng–Teng 2009), and PPAD is precisely the complexity class of the fixed-point arguments.
## Setting
A **finite strategic-form game** consists of a finite set $\iota$ of players, for each player $i$ a finite nonempty set $S_i$ of **pure strategies**, and for each player a **payoff function** $u_i : \prod_j S_j \to \mathbb{R}$; all players are utility maximizers. A **mixed strategy** for player $i$ is a probability distribution on $S_i$, represented as a weight function $\sigma_i : S_i \to \mathbb{R}$ with $\sigma_i \ge 0$ and $\sum_{s} \sigma_i(s) = 1$ (a **lottery**). Players randomize independently, so a **mixed profile** $\sigma = (\sigma_i)_{i}$ induces the product distribution on pure strategy vectors, and player $i$'s **expected payoff** is
$$U_i(\sigma) \;=\; \sum_{s \in \prod_j S_j} \Big(\prod_j \sigma_j(s_j)\Big)\, u_i(s).$$
A mixed profile $\sigma$ is a **(mixed) Nash equilibrium** if for every player $i$ and every lottery $\tau$ on $S_i$, replacing $\sigma_i$ by $\tau$ does not increase $U_i$.
A **two-person zero-sum game** is given by a matrix $A \in \mathbb{R}^{m \times n}$: the row player picks a row distribution $p$, the column player a column distribution $q$, and the column player pays the row player $p^{\mathsf T} A q$ in expectation.
The market of §1.8.1 of the source has finitely many divisible **goods**, good $a$ in $s_a$ units, and finitely many **buyers**, buyer $j$ bringing budget $m_j > 0$ and interested in a nonempty set of goods; utilities are linear 0/1, so a buyer wants any goods from her interest set and none other. **Market-clearing prices** are positive prices under which each buyer can spend her whole budget on cheapest goods in her interest set while every good sells out exactly.
## Formalization targets
### Goal (capstone) — Theorem 1.8
$$\text{Every finite strategic-form game has a mixed Nash equilibrium.}$$
Stated for an arbitrary finite family of finite nonempty strategy types; no bound on the number of players, no genericity assumptions.
### Supporting — Brouwer fixed-point theorem
$$K \subseteq E \text{ nonempty compact convex},\ E \text{ finite-dimensional},\ f : K \to K \text{ continuous} \implies \exists x,\ f(x) = x.$$
Mathlib currently has no form of Brouwer's theorem; every known proof of Theorem 1.8 needs it (or an equivalent), so it enters the mission as an explicit milestone rather than an assumed library fact.
### Theorem 1.11 — zero-sum games
$$\exists\, p^\ast, q^\ast:\quad \forall p,\ p^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q^\ast, \quad \forall q,\ {p^\ast}^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q, \quad\text{and}\quad (p^\ast, q^\ast) \text{ is a mixed Nash equilibrium}$$
of the explicit two-player game with payoffs $A_{xy}$ to the row player and $-A_{xy}$ to the column player. The source states the result as: optimal solutions of a dual pair of LPs form a Nash equilibrium of the zero-sum game; the first two conjuncts are the saddle point that LP optimality amounts to, and the third states the Nash-equilibrium clause against the mission's own game vocabulary, so "zero-sum" is formal (the two payoffs sum to zero) rather than implicit in the shape of the statement.
### Theorem 1.17 (existence form)
$$\text{The 0/1-utilities linear market admits market-clearing prices and allocations.}$$
The source proves this by an ascending-price algorithm and also bounds its running time; the complexity half has no formal counterpart in this mission.
## Significance
The capstone is the foundation of the whole mission series: correlated equilibria, price-of-anarchy bounds, and mechanism-design characterizations in later missions all quantify over or compare against Nash equilibria, and the series inherits its game vocabulary (`IsLottery`, `IsMixedProfile`, `expectedPayoff`, `IsMixedNash`) from this mission.
Formalizing it produces the first Brouwer fixed-point theorem in this environment — a well-known gap in mathlib with reuse value far beyond game theory (every degree-theoretic and equilibrium-existence argument needs it). The zero-sum milestone yields the minimax theorem, reusable for the learning-dynamics mission that follows. All results here are classical and proved on paper; the work requested is machine-checked proof, not new mathematics.
## Difficulty
The central difficulty is Brouwer. The standard routes are (i) Sperner's lemma plus a limit argument, which needs a formal theory of simplicial subdivisions that does not exist in mathlib; (ii) algebraic topology (no retraction of the ball onto the sphere), for which mathlib has singular homology but not yet the homology of spheres in usable form; (iii) analytic proofs (Milnor–Rogers). None is short; the milestone is deliberately stated for a general nonempty compact convex set in a finite-dimensional normed space so that any route serves, and so the lemma lands in reusable generality.
Given Brouwer, Theorem 1.8 still requires Nash's gain-function construction on the product of simplices and the verification that fixed points are equilibria — bookkeeping-heavy but standard. Theorem 1.11 does not need Brouwer: mathlib's Sion minimax theorem (`Mathlib.Topology.Sion`) applies to the bilinear payoff on the product of standard simplices, or one can argue by LP duality directly. Theorem 1.17 needs the tight-set/max-flow argument of Lemmas 1.15–1.16 or any direct construction of the equilibrium.
## Formalization scope
Games are presented concretely: players form a finite index type, strategies a finite type per player, payoffs are functions into $\mathbb{R}$; mixed strategies are weight functions with a `IsLottery` predicate, not measure-theoretic distributions. Deviations in the equilibrium definition range over all lotteries (not only pure strategies): the pure-deviation reduction is a lemma a solver may prove, not part of the definition. Strategy sets are assumed nonempty in the capstone; the player set need not be. In the zero-sum milestone both dimensions are positive (`Fin (m+1)`, `Fin (n+1)`), payoffs flow from the column player to the row player, `stdSimplex` plays the role of the mixed-strategy space, and the Nash-equilibrium conjunct is stated for the Boolean-indexed two-player game built by `matrixGameStrat`/`zeroSumPayoff`/`matrixGameProfile` from the definitions bundle. In the market milestone all supplies and budgets are positive, every buyer's interest set is nonempty, and every good has an interested buyer, matching the standing assumptions of §1.8.1; allocations are recorded as money spent, so the clearing condition is $\sum_j x_{ja} = p_a s_a$ with no division anywhere.
Trivializing readings are ruled out: the empty simplex has no lotteries, so nonemptiness hypotheses appear exactly where their absence would make an existence claim false (Brouwer on the empty set, games with an empty strategy set, zero-dimensional matrix games).
## Selected references
- J. F. Nash, *Non-cooperative games*, Annals of Mathematics 54 (1951), 286–295. [DOI](https://doi.org/10.2307/1969529)
- J. von Neumann, *Zur Theorie der Gesellschaftsspiele*, Mathematische Annalen 100 (1928), 295–320. [DOI](https://doi.org/10.1007/BF01448847)
- N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), *Algorithmic Game Theory*, Cambridge University Press, 2007, Chapter 1. [DOI](https://doi.org/10.1017/CBO9780511800481)
- C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, *The complexity of computing a Nash equilibrium*, SIAM J. Computing 39 (2009), 195–259. [DOI](https://doi.org/10.1137/070699652)
Zhang–Si–Si: Corrected Resonant Almost-Periodic Poincaré–Treshchev PersistenceResearch Paper
## Motivation
The classical persistence problem asks which invariant tori of an integrable Hamiltonian survive a small perturbation. A resonance makes some internal angular frequencies vanish, and an **almost-periodic perturbation** introduces infinitely many additional forcing frequencies. Zhang, Si, and Si state a Poincaré–Treshchev persistence theorem for this combined regime: most lower-dimensional resonant tori associated with nondegenerate relative equilibria persist as infinite-dimensional invariant tori [in Theorem 2.7](https://doi.org/10.3934/dcds.2026043). The formal mission targets that headline result in corrected form. It retains the paper’s nonresonance, spatial-shell, and averaged-critical-point hypotheses, while making explicit the full frequency twist and reduced-frequency parameter chart used later in the paper but absent from the printed theorem statement.
## Setting
Let $n,m>0$ and $d=n+m$. The internal variables are $x\in\mathbb T^d$ and $y\in G\subset\mathbb R^d$, where $G$ is bounded and closed. The external forcing angles and their conjugate actions are $\theta\in\mathbb T^{\mathbb Z}$ and $J\in\ell^1(\mathbb Z;\mathbb R)$. The **suspended Hamiltonian** is
$$
\mathcal H_\epsilon(\theta,J,x,y)=
\sum_{j\in\mathbb Z}\omega_jJ_j+N(y)+\epsilon P(\theta,x,y,\epsilon).
$$
Here $N$ is real analytic near $G$. A primitive rank-$m$ resonance lattice is represented by an integer matrix $K_0=(K_1,K_2)$ with $\det K_0=1$, where the last $m$ columns generate the lattice. The adapted angles are $(\psi,\phi)=K_0^{\mathsf T}x$, with $\psi\in\mathbb T^n$ and $\phi\in\mathbb T^m$. Writing $\nabla N$ for the actual derivative of $N$, define
$$
O(g,G)=\{y\in G:K_2^{\mathsf T}\nabla N(y)=0\},
\qquad \Omega(y)=K_1^{\mathsf T}\nabla N(y).
$$
The **averaged potential** $h_0(\phi,y)$ is the zero external and zero $\psi$ Fourier coefficient of $P$ at $\epsilon=0$. A pair $(\phi,y)$ is associated and nondegenerate when
$$
\nabla_\phi h_0(\phi,y)=0,
\qquad \det D_\phi^2h_0(\phi,y)\ne0.
$$
Let $O_0$ be the subset of $O(g,G)$ admitting such a $\phi$, let $\Omega_0=\Omega(O_0)$, and trim in reduced-frequency coordinates:
$$
\Omega_\xi=\{\eta\in\Omega_0:\operatorname{dist}(\eta,\partial\Omega_0)\ge\xi\},
\qquad O_\xi=O_0\cap\Omega^{-1}(\Omega_\xi).
$$
The perturbation has the paper’s **spatial-shell Fourier expansion** over finite shells $A$ in a spatial structure $\mathcal S$. With
$[A]=1+\sum_{j\in A}\log^{\varrho}(1+|j|)$ for $\varrho>2$, each shell has a uniform analytic Fourier bound $B_A$, and $\sum_AB_Ae^{s[A]}<\infty$ for some $s>0$. Every nonzero admissible finite external mode $k$ satisfies
$$
|\langle k,\omega\rangle|\ge
\frac{\gamma}{\Delta([[k]])\Delta(|k|_1)},
$$
where $\gamma>0$, $[[k]]$ is the minimum shell weight containing its support, and $\Delta$ is a nondecreasing approximation function with $\Delta(0)=1$, $\log\Delta(t)/t\downarrow0$, and $\int_0^\infty\log\Delta(t)t^{-2}\,dt<\infty$.
## Target
Assume that $O_0$ is nonempty. On every sufficiently small trim $O_\xi$, require compactness and positive $n$-dimensional measure in the $\Omega$ chart, injectivity of $D(\nabla N)(y)$, an analytic lower-Lipschitz diffeomorphism $\Omega:O_\xi\to\Omega_\xi$, and nondegeneracy of every averaged critical point retained by the conclusion. Then, for every $0<\xi\le\xi_*$, there are $0<\epsilon_0\le1$, a rate $c(\epsilon)\to0$ as $\epsilon\downarrow0$, and closed measurable nonempty sets $\Lambda_\epsilon\subset O_\xi$ for $0<\epsilon\le\epsilon_0$ such that
$$
\operatorname{vol}_n\bigl(\Omega(O_\xi\setminus\Lambda_\epsilon)\bigr)
\longrightarrow0\qquad(\epsilon\downarrow0).
$$
For every $y\in\Lambda_\epsilon$ and every associated nondegenerate $\phi$, construct a topological embedding
$$
\iota_{\epsilon,y,\phi}:\mathbb T^{\mathbb Z}\times\mathbb T^n
\longrightarrow
(\mathbb T^{\mathbb Z}\times\ell^1)\times
(\mathbb T^d\times\mathbb R^d)
$$
that is analytic almost periodic with the same shell structure, is the image of the standard resonant torus under a local canonical transformation, is $c(\epsilon)$-close to that torus, and is invariant under $\mathcal H_\epsilon$ with rotation vector $(\omega,\Omega(y))$.
## Significance
The result combines three features that are usually separated: a positive-rank internal resonance, an infinite external frequency vector, and persistence for an asymptotically full-measure parameter set. It identifies the surviving object in the full suspended phase, including the external actions, rather than only in the finite internal fibre. The paper contains a proof of its printed theorem; the mission’s open work is a Lean proof of the corrected target. The correction exposes the parameter twist and chart assumptions on which the reduction and measure assertion depend, so a completed formalization would distinguish the theorem’s stated content from hypotheses needed to make that content mathematically controlled.
## Difficulty
Finite-dimensional Diophantine notation does not control infinitely many external modes: admissibility, support weights, and the decay of $\Delta$ must interact without leaving an empty mode class. Resonance also removes $m$ internal frequencies and replaces the original parameter set by a lower-dimensional surface. Its ambient Euclidean boundary is therefore unsuitable for a positive trim, and ordinary ambient volume is unsuitable for the majority statement. Finally, persistence must be expressed simultaneously as an invariant solution of the actual Hamilton equations, an analytic almost-periodic embedding, and a canonical equivalence in the suspended phase; any one of these conditions alone admits objects that do not express the theorem.
## Formalization scope
The Lean representation uses finitely supported integer external modes, a covering spatial structure, the literal shell-indexed norm, complex-neighborhood coefficient analyticity, and a separate absolute-summability guard for every infinite Fourier sum. Unit modes are provably admissible. The averaged potential, its gradient and Hessian, the internal frequency $\nabla N$, the resonant set, and the reduced-frequency map are transparent definitions. Nonemptiness of $O_0$, positive volume of every allowed $\Omega_\xi$, and nonempty $\Lambda_\epsilon$ rule out empty-set and zero-measure trivializations.
The formal target strengthens the printed assumptions only where the source’s reduction requires missing control: $D(\nabla N)$ is injective on the retained trim, and $\Omega$ is an analytic diffeomorphism there with a uniform lower Lipschitz bound. The boundary distance and excluded volume are both taken in the $n$-dimensional reduced-frequency chart. The word “Cantor” is represented by closedness, measurability, nonemptiness, and asymptotically full measure; perfectness and total disconnectedness are not additional targets.
The torus lives in a genuine $\ell^1$ external-action space. Its action component has one weighted-$\ell^1$-valued shell expansion, and the Hamiltonian pairing and external action velocity carry convergence guards. A local conjugacy is a homeomorphism between open neighborhoods, fixes $\theta$, is differentiable along all $\ell^1$ action directions and finitely supported external-angle directions, and preserves $\sum_jd\theta_j\wedge dJ_j+\sum_i dx_i\wedge dy_i$ on those cylinder directions. Reusable contributions include spatial-shell Fourier classes, approximation functions, reduced-manifold measure interfaces, weighted infinite canonical forms, and coordinatewise Hamiltonian invariance.
## Selected references
- Yuan Zhang, Wen Si, and Jianguo Si, *Poincaré–Treshchev Mechanism in Integrable Hamiltonian Systems Under Almost-Periodic Perturbations*, Discrete and Continuous Dynamical Systems **52** (2026), 32–69. [DOI: 10.3934/dcds.2026043](https://doi.org/10.3934/dcds.2026043). Main result: Theorem 2.7, journal p. 39 (PDF p. 8); spatial and nonresonance definitions: Definitions 2.2–2.4 and equations (5)–(7), journal pp. 35–38 (PDF pp. 4–7); reduction exposing the additional twist and parameter-change requirements: Lemma 3.2, journal pp. 41–43 (PDF pp. 10–12).
Symplectic Modules Free over an Abelian NilradicalResearch Paper
## Motivation
Polynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$ that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of [Chen--Tan](https://doi.org/10.1016/j.jalgebra.2026.02.022).
The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family $\tau(C,\Phi)$ carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.
## Setting
Fix $\ell\ge2$ and the complex symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$. The relevant maximal parabolic subalgebra has an **abelian nilradical** $\mathfrak n$. Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free $U(\mathfrak n)$-module can consequently be modeled on that polynomial ring.
The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar $C\in\mathbb C$ and a polynomial parameter $\Phi$. Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family $\tau(C,\Phi)$ realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.
## Formalization targets
### Common polynomial-module family
Prove that for every $\ell\ge2$ there is one generator presentation and one family
$$
(C,\Phi)\longmapsto \tau(C,\Phi)
$$
of $\mathfrak{sp}_{2\ell}(\mathbb C)$-representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that $\tau(C,\Phi)$ is a weight module exactly when $\Phi$ is constant, and the stated simplicity criterion outside the exceptional arithmetic set
$$
\left\{\frac{\ell+1}{2}-\frac{n}{2}:n\in\mathbb Z_{>0}\right\}.
$$
For exceptional $C$, prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family $\tau$.
## Significance
The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.
Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.
## Difficulty
The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.
The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.
## Formalization scope
The mission works over $\mathbb C$ with natural rank $\ell\ge2$. The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.
The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family $\tau$. Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's `sorry`. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.
## Selected references
- Yang Chen and Haijun Tan, *Simple $\mathfrak{sp}_{2\ell}(\mathbb C)$-modules which are free over an abelian nilradical*, Journal of Algebra 697 (2026), 341--372, Theorems 1.1--1.3 (formal Theorems 3.7, 3.8, 4.7, 4.9, and 5.2). [DOI](https://doi.org/10.1016/j.jalgebra.2026.02.022)
- G. Shen, foundational work on mixed-product constructions for modules over Lie algebras of Cartan type, cited in the source paper for the Shen--Larsson functor.
Orders of Harmonic Maps into Euclidean BuildingsResearch Paper
## Motivation
Harmonic maps into singular nonpositively curved spaces arise in geometric analysis, rigidity theory, and the study of group actions on buildings. Near a point in the domain, their infinitesimal growth is measured by an **order**, obtained from an Almgren-type frequency quotient. For smooth targets that order is tied to familiar Taylor expansion data. Euclidean buildings are instead assembled from Euclidean apartments along reflection walls, so a map can branch through a singular link and a priori might exhibit a much less controlled spectrum of homogeneities. Breiner and Dees prove that, for maps from surfaces, this spectrum is discrete and is governed by the finite rotational Weyl group of the building. The mission formalizes their headline classification theorem, Theorem 1.1 of [Breiner--Dees](https://doi.org/10.1007/s00526-026-03375-5).
The discreteness matters because frequency information is a basic input to stratification and regularity arguments for singular harmonic maps. A finite list of possible denominators prevents homogeneities from accumulating arbitrarily and isolates rank-one behavior. The formal target makes explicit the nonconstant condition used by the source paper's tangent-map reduction. Without it, the usual numerator and denominator of the frequency quotient both vanish for a constant map, so its order is not defined.
## Setting
A **Euclidean Coxeter complex** consists of Euclidean space together with an affine reflection group. Taking the linear parts of its affine isometries produces a finite rotational reflection group $W$. A **Euclidean building of type $W$** is a complete metric space covered by isometric Euclidean apartments whose overlaps are related by elements of the affine Weyl group; the atlas is required to contain the relevant geodesic segments, rays, and lines and to be maximal with these compatibility properties.
The domain is a connected open subset $D$ of a complex one-dimensional manifold, hence a Riemann surface domain. The formalization uses a concrete Korevaar--Schoen-style metric Sobolev energy built from normalized local difference quotients and Lebesgue area in charts. A map $u:D\to X$ is harmonic when it has finite local energy and minimizes that energy against competitors with the same trace. For $x_0\in D$ and small radii $r$, the energy and boundary moment determine a frequency quotient. When its limit exists with positive denominator, that limit is the order $\operatorname{Ord}_u(x_0)$.
## Formalization targets
### Main classification
For a nonconstant energy-minimizing harmonic map $u:D\to X$ and any $x_0\in D$, prove that the order is defined and that there are positive integers $m,k$ such that
$$
\operatorname{Ord}_u(x_0)=\frac{m}{k},
\qquad k\mid |W|.
$$
If the building has rank one, prove the sharper form
$$
\operatorname{Ord}_u(x_0)=\frac{m}{2}
\qquad\text{for some integer }m\ge 2.
$$
The same theorem also records the small-scale energy and positive-boundary-moment facts needed for the order to be meaningful; these are conclusions, not assumptions supplied by a solver.
## Significance
The result identifies a purely algebraic constraint on an analytic singularity invariant: every denominator divides the order of the finite rotational Weyl group. In rank one, where the target is a tree or an $\mathbb R$-tree, it recovers the half-integer spectrum and its lower bound. This converts an apparently continuous local invariant into a discrete one determined by the building type.
Formalizing the theorem requires reusable infrastructure that is largely absent from current Mathlib: concrete Euclidean-building atlases, metric-valued Sobolev energy, trace and boundary-moment constructions, harmonic energy minimization, frequency quotients, and homogeneous tangent-map interfaces. The paper theorem is proved in ordinary mathematics; the open task is to replace the single `sorry` in the target with a machine-checked Lean proof. A completed development would provide components useful for other singular-target harmonic-map and CAT(0) formalizations.
## Difficulty
The target is not a direct consequence of treating the building as a Euclidean vector space. A harmonic map can cross apartment walls, and a single chart need not contain the image of a punctured neighborhood. The local problem must respect both metric energy and Weyl-group compatibility. Moreover, the frequency quotient is defined through limiting analytic quantities, while the conclusion is an exact rational arithmetic classification. Bridging those levels requires controlling tangent maps and the geometry of directions in the building rather than merely proving monotonicity of the frequency.
The rank-one clause is not obtained by substituting $|W|=2$ into the general statement alone: it also asserts $m\ge2$. The formal proof therefore must preserve the nonconstant hypothesis and the positivity information that rules out the degenerate zero-order case.
## Formalization scope
The Lean bundle fixes a complex one-dimensional manifold model for the source, a genuine complete metric target, a finite affine reflection group acting by Euclidean isometries, and an explicit building atlas. The rotational group $W$ is the image of the affine group under taking linear parts, so $|W|$ is not an arbitrary external number. The domain carries a point $x_0$ and is nonempty by construction. The map is required to be nonconstant on the domain; this is the necessary explicit repair of the printed headline, whose later reduction theorem uses the same condition.
Energy, trace, boundary moment, frequency, and order are transparent definitions tied to the supplied geometry. In particular, the caller cannot choose a zero measure or an unrelated predicate to make the target vacuous. The theorem must establish finite small-scale energy, positivity of the boundary moment, existence of the frequency limit, and its classification. Solvers may contribute supporting files for metric Sobolev estimates, tangent-map compactness, homogeneous harmonic-map classification, or finite-reflection-group lemmas, provided they preserve the exact conventions in the definition bundle.
## Selected references
- Christine Breiner and Ben K. Dees, *On the Possible Orders of Harmonic Maps into Euclidean Buildings*, Calculus of Variations and Partial Differential Equations, 2026, Theorem 1.1 and Sections 2--4. [DOI](https://doi.org/10.1007/s00526-026-03375-5)
- Mikhail Gromov and Richard Schoen, *Harmonic Maps into Singular Spaces and p-adic Superrigidity for Lattices in Groups of Rank One*, Publications Mathématiques de l'IHÉS 76 (1992), 165--246. [EuDML](https://eudml.org/doc/104049)
Arbitrary Torsion in Moment-Angle Homology and Loop HomologyResearch Paper
## Motivation
Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial $4$-sphere.
This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.
## Setting
Let $L$ be an abstract simplicial complex on a finite vertex set $[m]$. Its geometric realization $|L|$ is formed from probability vectors whose supports are faces of $L$. The condition that $L$ is a **simplicial $4$-sphere** means that this realization is homeomorphic to the unit sphere $S^4\subset\mathbb R^5$.
For each face $\sigma\in L$, assign a copy of the closed disk $D^2$ at vertices in $\sigma$ and the boundary circle $S^1$ at vertices outside $\sigma$. The associated moment-angle complex is
$$
\mathcal Z_L
=\bigcup_{\sigma\in L}
\prod_{i=1}^{m}Y_i(\sigma),
\qquad
Y_i(\sigma)=
\begin{cases}
D^2,&i\in\sigma,\\
S^1,&i\notin\sigma.
\end{cases}
$$
The all-ones point is a canonical basepoint. Write $\Omega\mathcal Z_L$ for the based loop space with the compact-open topology. For a space $X$, the mission uses total integral singular homology
$$
H_*(X;\mathbb Z)=\bigoplus_{q\ge0}H_q(X;\mathbb Z)
$$
as an additive abelian group. Saying that an abelian group $G$ is a subgroup means that there is an injective additive homomorphism $G\hookrightarrow H_*(X;\mathbb Z)$.
## Formalization targets
### Arbitrary torsion in one moment-angle manifold
For every finitely generated abelian group $G$, prove that there are an integer $m$ and a simplicial complex $L$ on `Fin m` such that $|L|\cong S^4$ and there are injective homomorphisms
$$
G\hookrightarrow H_*(\mathcal Z_L;\mathbb Z),
\qquad
G\hookrightarrow H_*(\Omega\mathcal Z_L;\mathbb Z).
$$
The quantifier order matters: the same $m$ and the same $L$ must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.
## Significance
The theorem gives a universality statement for moment-angle manifolds over simplicial $4$-spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single $L$ connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.
Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.
## Difficulty
The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.
There is also a substantial representation boundary between combinatorics and topology. The face data of $L$, the union of disk-circle products, the homeomorphism $|L|\cong S^4$, and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.
## Formalization scope
Lean represents $L$ using `AbstractSimplicialComplex (Fin m)`. Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit $4$-sphere.
The moment-angle space is a subtype of `(Fin m → ℂ)` defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is `singularHomologyFunctor` with coefficients in $\mathbb Z$, and total homology is a direct sum over all natural degrees.
The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain $G$ as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.
## Selected references
- Yang Han and Keke Li, *Moment Angle Manifolds Corresponding to $S^4$ Whose Homology and Loop Homology May Have Arbitrary Torsion*, International Mathematics Research Notices 2026(4), 1--7, 2026. [DOI](https://doi.org/10.1093/imrn/rnag024)
- A. Bahri, M. Bendersky, F. R. Cohen, and S. Gitler, *The polyhedral product functor: a method of decomposition for moment-angle complexes, arrangements and related spaces*, Advances in Mathematics 225(3), 2010, 1634--1668. [DOI](https://doi.org/10.1016/j.aim.2010.04.009)
Vector Space Methods XIII: Conjugate-Gradient ConvergenceTextbook
## Motivation
The [conjugate-gradient method in Luenberger's Chapter 10](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) is one of the most enduring consequences of Hilbert-space geometry in numerical optimization. For a bounded self-adjoint coercive operator, it solves the quadratic first-order equation `Q x = b` using only operator applications, inner products, and a short recurrence. Luenberger develops the method from steepest descent and conjugate directions, then proves convergence in a general real Hilbert space rather than only for finite matrices. This mission formalizes that full setting. It also repairs a practical omission in the printed recursion: division formulas are undefined after exact convergence, so the formal algorithm explicitly stops and stutters once its search direction is zero.
## Setting
Let `H` be a **complete real inner-product space** and `Q : H →L[ℝ] H` a bounded **self-adjoint operator**. Constants `m` and `M` satisfy `0 < m ≤ M` and
$$
m\lVert x\rVert^2 \le \langle x,Qx\rangle
\le M\lVert x\rVert^2
$$
for every `x`. The first inequality is **coercivity**; together with self-adjointness it supplies the positive `Q`-energy. For a right-hand side `b` and initial point `x₀`, the initial residual and direction are both `b - Q x₀`. A **conjugate-gradient state** records the current iterate, residual, and direction. If the direction is nonzero, the next state uses Luenberger's `alpha` and `beta` ratios. If the direction is zero, `conjugateGradientStep` returns the same state, so every natural-number iterate is total and all denominators occur only on the active branch.
## Formalization targets
The root theorem `VectorSpaceOpt.conjugate_gradient_converges` states that there is a unique `xStar` satisfying `Q xStar = b` and that the iterate component of the guarded conjugate-gradient state tends to `xStar` in norm. Four milestones provide reusable structure. `coercive_selfadjoint_bijective` establishes existence and uniqueness for `Q x = b` from bounded self-adjoint coercivity. `conjugate_directions_converge` formalizes §10.6, Theorem 1: a complete sequence of nonzero pairwise `Q`-orthogonal directions produces residuals orthogonal to every earlier direction and iterates converging to the solution. `cg_directions_conjugate_until_stop` records the §10.8 invariants only before the explicit stopping time. `cg_energy_contraction` captures the uniform energy reduction factor derived from the bounds `m` and `M`.
The total algorithm is represented by `conjugateGradientIterate`, and its error functional is
$$
E(x)=\langle x-x^*,Q(x-x^*)\rangle.
$$
These definitions are proposed as mission-owned reusable objects in the shared `VectorSpaceOpt` namespace.
## Significance
The mission gives a coordinate-free verification target for an algorithm usually presented through arrays and matrices. Its theorem applies directly to finite-dimensional symmetric positive-definite systems but also retains Luenberger's infinite-dimensional perspective. The guarded recursion is suitable for later executable specializations and makes exact termination a first-class semantic event. The coercivity and conjugate-directions milestones can be reused for Galerkin methods, preconditioned variants, and other Krylov algorithms, while the energy estimate provides a natural connection to condition-number convergence rates.
Unlike a matrix-only formalization, the Hilbert-space theorem cleanly separates the geometric reason for convergence from any storage representation. It therefore complements Mathlib's existing operator and orthogonality libraries and can serve as a specification against which finite implementations are later verified.
It also preserves the book's unifying theme: optimization algorithms arise from the geometry of carefully chosen inner products rather than from coordinate manipulation alone.
## Difficulty
The difficulty is medium to high. Algebraic invariants of the three-term recurrence involve several interacting orthogonality relations and require strict control of nonzero denominators. Infinite-dimensional convergence additionally uses density of the closed span of directions and comparison of the `Q`-energy with the ambient norm. The theorem must move between self-adjoint continuous linear maps, scalar inner products, filters on sequences, and function iteration. Exact termination creates a case split that informal accounts routinely ignore; the formal statement must show that the zero-direction branch is stable and already represents the solution.
## Formalization scope
The proposal follows §10.6 and §10.8, pp. 291–296, and uses Chapter 10, Problem 10 on p. 309 for the coercive-invertibility dependency. All assumptions on `Q`, `m`, and `M` that §10.8 inherits from the preceding sections are repeated explicitly. The conjugate-directions milestone explicitly assumes every direction is nonzero and that the closed span of the directions is the whole Hilbert space. The conjugate-gradient invariants are asserted only for iterations before a zero direction occurs. Once it occurs, the state stutters by definition; the proposal never relies on Lean's totalized value for `0 / 0`.
Luenberger's §10.7, Theorem 1 is not included as a literal milestone. As printed, its orthogonalization-of-moments statement omits self-adjointness of the auxiliary operator relative to the `Q` inner product and omits the linear-independence/nonbreakdown conditions needed to keep denominators nonzero. The mission instead isolates the `Q`-conjugacy invariant directly from §10.8. It does not claim finite-dimensional termination within `dim H` steps, floating-point stability, preconditioning, a sharp Chebyshev condition-number rate, or computability of equality tests on arbitrary Hilbert spaces.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 10, §10.6, Theorem 1, pp. 291–292; §10.8, Theorem 1, pp. 294–296; Problem 10, p. 309. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (real inner-product spaces, continuous linear maps, coercivity, closed spans, orthogonality, and filter convergence).
Vector Space Methods XIV: Quadratic Penalty ConvergenceTextbook
## Motivation
[Quadratic exterior penalties in Luenberger's §10.11](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) replace a constrained problem by a sequence of unconstrained minimizations. The method is simple enough to state in a few lines, yet Luenberger's convergence theorem is strikingly general: no convexity, differentiability, or convergence of the full minimizer sequence is required. If penalty weights increase to infinity and a subsequence of exact penalty minimizers converges, lower semicontinuity alone makes its limit feasible and optimal. This mission isolates that robust primal convergence result as a tractable companion to the more analytic conjugate-gradient and optimal-control missions. It offers a clean formalization target with direct relevance to nonlinear programming and approximation schemes.
## Setting
Let `X` be a **topological space**, `f : X → ℝ`, and `G : X → (Fin p → ℝ)`. **Feasibility** means `G x i ≤ 0` for every component. Define the **positive part** componentwise and the **squared violation** by
$$
G_i^+(x)=\max(0,G_i(x)), \qquad
v(x)=\sum_i (G_i^+(x))^2.
$$
For a positive weight `K`, the penalty objective is `f x + K * v x`. A sequence `K n` is positive, nondecreasing, and tends to `+∞`. The constrained problem is assumed to have a minimizer `xStar`, and for each `n` an exact global minimizer `x n` of the corresponding penalty objective is supplied. A limit point is represented explicitly by a strictly increasing index map `phi` for which `x ∘ phi` tends to `x₀`.
## Formalization targets
The root `VectorSpaceOpt.quadratic_penalty_cluster_point_converges` formalizes §10.11, Theorem 1. Assuming lower semicontinuity of `f` and `v`, it concludes that every stated subsequential limit `x₀` is feasible, has the same objective value as `xStar`, and globally minimizes `f` over the feasible set.
Three milestones split the exact source content into reusable statements. `quadratic_penalty_basic_estimates` is §10.11, Lemma 1: the attained penalty values are nondecreasing, are bounded above by `f xStar`, and the stronger weighted violation `K n * v (x n)` tends to zero. `penalty_cluster_point_feasible` combines convergence of violations with lower semicontinuity at a subsequential limit to recover all component inequalities. `penalty_cluster_point_optimal` combines lower semicontinuity of `f`, the uniform upper bound `f (x n) ≤ f xStar`, feasibility of the limit, and optimality of `xStar` to identify the limiting objective value and global constrained optimality.
## Significance
The theorem captures the essential consistency guarantee behind one of the most widely used constraint-handling methods. Its assumptions separate optimization existence from convergence: minimizers of each auxiliary problem and at least one cluster point are assumed, while the theorem identifies what any such cluster point must be. The componentwise positive-part and violation definitions are reusable for augmented Lagrangians, exact penalties, barrier comparisons, and finite inequality systems. The basic-estimates lemma is particularly useful because it requires neither topology nor continuity and exposes a quantitative fact stronger than mere feasibility residual convergence.
Because the proof target is stated over an arbitrary topological space, the mission also clarifies which parts of penalty convergence are genuinely metric and which depend only on order, finite nonnegative sums, and lower semicontinuity. This abstraction is faithful to the source's vector-space viewpoint.
## Difficulty
The mission has moderate difficulty and relatively low infrastructure risk. The main analytic interfaces are lower semicontinuity along a convergent subsequence and real filter convergence to both zero and infinity. The basic estimates require reasoning simultaneously about minimizers for changing objectives, monotonicity of the weights, and the asymptotic product `K n * v (x n)`. The cluster-point theorem must extract componentwise feasibility from a finite sum of nonnegative squares without assuming continuity of `G`. Lean's `IsMinOn` does not itself assert membership in the feasible set, so feasibility of the known constrained minimizer is included separately rather than hidden in prose.
## Formalization scope
The proposal covers the primal part of §10.11: Lemma 1 on p. 305 and Theorem 1 on p. 306. It makes “limit point” precise through a strictly monotone subsequence, avoiding any assumption that the full sequence converges. The weight sequence may have repeated values because the source only needs it to be nondecreasing, but every weight is positive and the sequence tends to `atTop`. Lower semicontinuity is required for `f` and the composite violation `v`, exactly as in the book; continuity or componentwise lower semicontinuity of `G` is not substituted. Existence of `xStar` and of every penalty minimizer is assumed rather than derived from compactness or coercivity.
The mission does not include §10.11, Lemma 2 or Theorem 2 on dual multipliers. Those results add convexity and continuity assumptions and naturally require careful treatment of an extended-real dual functional. It also does not address approximate minimizers, rates, boundedness of the sequence, existence of cluster points, equality constraints beyond their encoding as paired inequalities, or finite exactness. Keeping those extensions separate preserves the unusually weak hypotheses and clear conclusion of the cited primal theorem.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 10, §10.11, Lemma 1 and Theorem 1, pp. 305–306. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (lower semicontinuity, finite sums, `Fin`-indexed vectors, subsequences, global minima on sets, and filter convergence).
Vector Space Methods XII: Pontryagin Minimum PrincipleTextbook
## Motivation
[Pontryagin's principle as presented by Luenberger](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) is the decisive necessary condition in continuous-time optimal control. It converts an optimization over functions into a pointwise comparison of a Hamiltonian, coupled to the original state equation and a backward costate equation. Luenberger derives the minimum-Hamiltonian convention from vector-space multiplier ideas and a first-order comparison principle. Formalization is especially valuable here because the printed theorem contains a standard but consequential regularity oversight: it asserts a condition at every time even though controls are only piecewise continuous and the cost is an integral. This mission preserves the intended theorem while replacing that false pointwise claim by the mathematically canonical almost-everywhere statement.
## Setting
Fix `t₀ < t₁`, a finite-dimensional **Euclidean state space** `OCState n`, a Euclidean control space `OCControl m`, and a permitted-control set `Omega`. A state-control pair `(x,u)` is **admissible** when `x t₀ = xInit`, the state is **absolutely continuous** on the interval, the control is **almost everywhere strongly measurable** and lies in `Omega` almost everywhere, the differential equation `x' = F(x,u)` holds almost everywhere in the interior, and the running cost is interval integrable. An **optimal pair** globally minimizes the interval integral among all admissible pairs.
The dynamics `F` and running cost `ell` are continuous jointly in state and control and continuously differentiable in the state variable. Their state derivatives `Fx` and `ellx` vary continuously. A global Lipschitz estimate controls changes of `F` in both state and control. Because an a.e. measurable control need not be bounded, the optimal control is explicitly assumed to have an a.e. norm bound on the compact interval, matching the boundedness inherited from the source's piecewise-continuous model. The operator-valued paths `Fx (x₀ t) (u₀ t)` and `ellx (x₀ t) (u₀ t)` are also assumed interval integrable along the optimum. Together these hypotheses provide the measure-theoretic regularity needed for the adjoint and state perturbations. The Hamiltonian uses Luenberger's minimum convention,
$$
H(x,u,\lambda)=\langle \lambda,F(x,u)\rangle+\ell(x,u).
$$
## Formalization targets
The root `VectorSpaceOpt.pontryagin_minimum_principle` asserts the existence of an absolutely continuous costate `lambda` with terminal value `lambda t₁ = 0`. Almost everywhere it satisfies the weak inner-product form of
$$
-\dot\lambda(t)=D_xF(x₀(t),u₀(t))^*\lambda(t)+D_x\ell(x₀(t),u₀(t)),
$$
and almost everywhere on the control interval it satisfies
$$
H(x₀(t),u₀(t),\lambda(t))
\le H(x₀(t),v,\lambda(t))
\quad\text{for every }v\in\Omega.
$$
Two milestones capture source dependencies. `control_state_lipschitz_estimate` is the Grönwall stability estimate used on p. 263 to control the state response by the integral distance between controls; it explicitly assumes interval integrability of both the state-difference norm and the control-difference norm, so Mathlib's totalized integral cannot hide a nonintegrable input. `adjoint_lagrangian_comparison` formalizes §9.6, Proposition 1: under an implicit state equation, differentiability in the state, Lipschitz dependence of the state solution, and an adjoint identity, the objective difference agrees with a frozen-state Lagrangian difference up to an explicit filter-level little-o remainder.
## Significance
This is the flagship analytic mission of the continuation. It connects finite-dimensional differential calculus, Bochner integration, absolute continuity, ODE constraints, adjoints, and localized control variations in one reusable theorem. The definitions form a minimal control framework that can support terminal costs, endpoint constraints, and alternative maximum-principle conventions later. The corrected a.e. conclusion also demonstrates a central benefit of formalization: informal conventions about representatives of controls and isolated time values must be resolved before a theorem can be accepted.
The weak inner-product adjoint equation avoids introducing a coordinate transpose and remains invariant under the Euclidean-space representation. That choice makes the result immediately reusable in later vector-space treatments of transversality and endpoint multipliers.
## Difficulty
The difficulty is very high. Mathlib supplies finite-dimensional calculus, interval integration, absolute continuity, measure-theoretic almost-everywhere statements, and Grönwall tools, but not an assembled Pontryagin framework. The mission must coordinate a state-solution stability estimate, state differentiability of the dynamics and cost, existence and regularity of the backward costate, and Hamiltonian comparison against arbitrary admissible values. The control is measurable rather than globally continuous, so every pointwise expression must be placed under an a.e. quantifier where appropriate. The proposition milestone additionally requires a precise little-o interface instead of an unnamed asymptotic remainder.
## Formalization scope
The proposal covers §9.6, Proposition 1 and Theorem 1, with the regularity inherited from the surrounding discussion made explicit. Both the optimal state and the costate are absolutely continuous. Admissible controls are a.e. strongly measurable, which is a broader measure-theoretic proxy for the source's piecewise-continuous controls and is compatible with integral objectives; the root additionally requires the optimal control to be essentially norm bounded on `Icc t₀ t₁`, restoring the compact-interval boundedness used by the source. The maps `F`, `ell`, `Fx`, and `ellx` are jointly continuous; state derivatives are supplied by `HasFDerivAt`; a uniform Lipschitz bound is stated; and both derivative coefficients along the optimal path are interval integrable. The separate Grönwall milestone requires its state and control norm differences to be interval integrable. The interval is required to have positive length.
There is a documented source erratum. The sentence on printed p. 263 states Hamiltonian minimality for every `t`, while the proof on p. 264 chooses a neighborhood on which a purported strict violation persists. That step requires continuity at the selected time. Moreover, changing a piecewise-continuous control at a single isolated time changes neither its a.e. class, the state equation, nor the integral cost. Therefore no condition can be forced at an arbitrary jump value. The Lean root uses an a.e. conclusion on `Icc t₀ t₁`; an alternative source-faithful repair would assert the inequality at every continuity point of `u₀`. The mission does not claim existence of an optimal pair, compactness of `Omega`, endpoint constraints, nonsmooth dynamics, or a sufficiency theorem.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 9, §9.6, Proposition 1 and Theorem 1, pp. 262–264, including the printed all-times wording and its proof context. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (interval integration, absolute continuity, Euclidean spaces, Fréchet derivatives, ODE estimates, and a.e. measurability).
Vector Space Methods XI: Generalized Kuhn–Tucker ConditionsTextbook
## Motivation
[Luenberger's generalized Kuhn–Tucker theorem](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) turns inequality-constrained optimization into an order-theoretic statement on normed vector spaces. Instead of listing scalar inequalities, it lets a convex cone `P` define positivity in a target space `Z`; one condition `G x ≤ₚ 0` can therefore represent finite, infinite, or function-valued families of constraints. At a regular local minimizer, a positive continuous functional on `Z` simultaneously provides stationarity and complementary slackness. This mission is a separate capstone because the cone-separation argument is conceptually independent of the equality-constrained theorem and because Mathlib currently lacks this general cone-valued KKT result.
## Setting
Let `X` and `Z` be **real normed spaces**, `P : ConvexCone ℝ Z`, `f : X → ℝ`, and `G : X → Z`. The **cone order** is `coneLE P z₁ z₂`, meaning `z₂ - z₁ ∈ P`; strict inequality uses the topological interior of the **convex cone** `P`. The cone is assumed to have nonempty interior. At `x₀`, both `f` and `G` possess linear **Gâteaux derivatives** represented by continuous linear maps `f'` and `G'`. The source's **regularity condition** requires feasibility together with a direction `h` for which `G x₀ + G' h` lies strictly below zero in the cone order.
The point `x₀` is a local, not global, minimizer of `f` on `{x | coneLE P (G x) 0}`. The resulting multiplier `z₀ : Z →L[ℝ] ℝ` is positive on `P`. This mission reuses the previously published `VectorSpaceOpt.coneLE` and `VectorSpaceOpt.dualPositive` definitions from the global Lagrange-duality mission; it deliberately does not introduce equivalent duplicate constants.
## Formalization targets
The root theorem is `VectorSpaceOpt.generalized_kuhn_tucker`, corresponding to §9.4, Theorem 1. It produces `z₀` such that
$$
z₀(P) \subseteq [0,\infty), \qquad
f' + z₀ \circ G' = 0, \qquad
z₀(Gx₀)=0.
$$
Three milestones expose the exact logical interfaces of the source theorem. `kkt_no_strict_linearized_descent` says local minimality and feasibility exclude a direction that strictly decreases `f'` while making the linearized constraint strictly feasible. `kkt_linearized_separator` packages the separation step: nonintersection of the strict descent system, cone regularity, and nonempty cone interior yield a positive continuous multiplier with both KKT conclusions. `kkt_complementary_slackness` isolates the algebraic extraction of stationarity and complementarity from the separating inequality valid for every direction. The items use the shared namespace `VectorSpaceOpt` and list dependencies in this order.
## Significance
This mission generalizes the standard finite-dimensional KKT rule without choosing coordinates or reducing cone constraints to components. It provides a reusable basis for semi-infinite optimization, ordered Banach-space problems, and state constraints expressed in function spaces. The multiplier positivity predicate connects directly to the dual cone used in the earlier global duality mission, while complementarity links local differential theory to primal–dual optimality. A successful formalization would also close a conspicuous gap in general-purpose optimization infrastructure: cone-valued KKT conditions are referenced often but rarely available as a theorem with all topological hypotheses exposed.
The statement is also a useful stress test for compositional textbook formalization. It deliberately shares its order and dual-positivity vocabulary with an earlier mission, so subsequent results can consume one stable API instead of translating among locally invented conventions.
## Difficulty
The main challenge is functional-analytic separation. The relevant convex set mixes objective descent and strict cone feasibility, and the separating functional must be normalized so that its objective component is nonzero. Regularity rules out an abnormal separator and nonempty cone interior controls the sign of the `Z` component. The Gâteaux assumptions are directional rather than full Fréchet differentiability, so local contradiction statements must use only the one-dimensional expansions actually supplied. Lean also requires careful sign discipline: feasibility is encoded as `0 - G x ∈ P`, while positivity is evaluated on elements of `P`. Small convention errors would reverse the dual cone or the stationarity equation.
## Formalization scope
The source says that `X` is a vector space, but its definition of Gâteaux differentiation and its local perturbation argument require a norm and topology. The proposal therefore makes both `X` and `Z` normed real spaces and represents derivatives by continuous linear maps. It keeps Luenberger's cone assumptions: convexity and nonempty interior are explicit; pointedness and closedness are not added because the printed separation argument does not need them. The optimality hypothesis is faithfully local through `IsLocalMinOn`. Feasibility is included in `IsConeRegularAt`, and the no-descent milestone states it separately.
This is proposed as “Vector Space Methods XI” and depends on the earlier global Lagrange-duality mission, proposed as “Vector Space Methods IX,” for `coneLE` and `dualPositive`; the missions should be submitted in numerical order. The proposal does not cover equality constraints, second-order KKT conditions, multiplier uniqueness, constraint qualifications other than Luenberger's strict linearized feasibility condition, or sufficient conditions based on convexity. It also does not specialize to a finite list of scalar inequalities. These omissions preserve the exact role and scale of §9.4.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 9, §9.4, regular-point definition and Theorem 1, pp. 248–250. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (convex cones, continuous linear functionals, topological interiors, differential calculus, local extrema, and geometric separation).
Vector Space Methods X: Equality-Constrained Lagrange MultipliersTextbook
## Motivation
Equality-constrained optimization is the point where the geometric language of vector spaces becomes an operational calculus. In finite dimensions, the familiar rule says that the gradient of an objective at a regular constrained optimum is a linear combination of the constraint gradients. [Luenberger's Chapter 9](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) replaces coordinate gradients by continuous linear maps between Banach spaces and identifies the genuinely important hypothesis: the derivative of the constraint map is onto. The resulting theorem covers constraints with infinitely many degrees of freedom and prepares the functional-analytic form of optimal control. This mission formalizes the local theorem rather than a finite-dimensional specialization. It also records the generalized inverse theorem that makes regular level sets locally rich enough to test every tangent direction.
## Setting
Let `X` and `Z` be **real Banach spaces**, `U ⊆ X` an open set, `f : X → ℝ` an objective, and `H : X → Z` an equality-constraint map. The distinguished point `x₀` lies in `U` and satisfies `H x₀ = 0`. Both maps are **continuously Fréchet differentiable** on `U`; their derivatives at `x₀` are named `f'` and `H'`. A **regular point** is one at which `H' : X →L[ℝ] Z` is surjective. Local optimality is expressed relative to the actual feasible set `{x | x ∈ U ∧ H x = 0}`, and may be either a local minimum or a local maximum. Multipliers live in the **continuous dual** `Z →L[ℝ] ℝ`, never in an untopologized algebraic dual.
The mission also treats a map `T : X → Y` between Banach spaces. Surjectivity of its derivative at `x₀` yields local metric surjectivity: sufficiently nearby target points possess preimages in `U`, with displacement controlled linearly by their distance from `T x₀`. This is the Lyusternik–Graves form of the generalized inverse theorem, not the ordinary inverse theorem requiring a bijective derivative.
## Formalization targets
The main target is `VectorSpaceOpt.equality_lagrange_multiplier`, the exact regular equality-multiplier theorem from §9.3. Its conclusion is the existence of a continuous linear functional `z₀` satisfying
$$
f' + z₀ \circ H' = 0.
$$
Three source-aligned milestones organize the mission. First, `generalized_inverse_function` formalizes §9.2, Theorem 1: an onto derivative gives constants `ε > 0` and `K ≥ 0` so every `y` with `dist y (T x₀) < ε` has a preimage `x ∈ U` obeying `T x = y` and `‖x - x₀‖ ≤ K ‖y - T x₀‖`. Second, `constrained_extremum_tangent_stationary` states that `f' h = 0` for every `h` in the kernel of `H'` at a regular local extremum. Third, `abnormal_lagrange_multiplier` records Luenberger's closed-range corollary: without surjectivity there is a nonzero pair `(r₀,z₀)` satisfying `r₀ • f' + z₀ ∘ H' = 0`.
## Significance
This theorem is the Banach-space bridge between unconstrained differentiation and multiplier theory. It isolates the quotient-space geometry behind the multiplier rule and supplies an interface reusable in variational problems, PDE-constrained optimization, and smooth optimal control. The abnormal alternative matters independently: it represents the degeneracy that later appears in Fritz John conditions and endpoint-constrained control. Formalizing the quantitative generalized inverse statement also contributes infrastructure with uses beyond optimization, including nonlinear solvability, metric regularity, and perturbation estimates.
## Difficulty
The mission is mathematically compact but technically demanding. The hard object is local surjectivity from an onto, noninjective derivative. Its natural linear model passes through the Banach quotient by the kernel and the open mapping theorem, while the nonlinear statement must preserve the open domain and a quantitative norm estimate. At the multiplier stage, a functional defined on the range of `H'` must be shown well-defined, bounded, and represented as a continuous functional on `Z`. Lean must also reconcile `ContDiffOn`, pointwise Fréchet derivatives, kernels and ranges of continuous linear maps, and filter-based local extrema. These are substantial analytic interfaces even though the final equation is short.
## Formalization scope
The proposal follows printed pp. 240–244. All domain, completeness, differentiability, feasibility, and locality hypotheses that are inherited implicitly in the prose are explicit in the Lean statements. The primary theorem assumes surjectivity and therefore produces a normalized multiplier with coefficient one on the objective. The abnormal milestone assumes only that `Set.range H'` is closed and explicitly requires the pair `(r₀,z₀)` to be nonzero. No finite-dimensionality, choice of coordinates, second-order condition, constraint qualification weaker than surjectivity, or sufficiency theorem is claimed.
Boundary cases are intentional. The zero constraint space is allowed and reduces the conclusion to ordinary stationarity. A local maximum is covered alongside a local minimum because the tangent argument is symmetric. The generalized inverse target explicitly returns a preimage inside `U`; it does not silently rely on extending `T` outside its domain. The mission does not identify the feasible level set with a manifold or claim uniqueness of a multiplier. Those are natural later developments but are not statements in the cited pages.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 9, §9.2, Theorem 1, pp. 240–242; §9.3, Lemma 1, Theorem 1, and Corollary 1, pp. 242–244. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (Fréchet derivatives, local extrema, continuous linear maps, Banach quotients, and Lagrange multipliers).
Cubic Congruence for the q-Secant Inversion EnumeratorResearch Paper
## Motivation
Alternating permutations are a classical meeting point of enumerative combinatorics, permutation statistics, and special functions. An up--down permutation alternates between rises and falls, and their ordinary counts are the Euler secant and tangent numbers. Refining this count by the inversion statistic produces the $q$-secant polynomial $E_{2n}(q)$. Its values and congruences retain information that disappears after setting $q=1$: they distinguish how the alternating permutations are distributed by inversion number and reveal cancellation at roots such as $q=-1$. Ji-Cai Liu's article isolates the next nontrivial term in the $(1+q)$-adic expansion of this polynomial, strengthening an earlier Andrews--Foata congruence. The mission formalizes the article's main result, Theorem 1.1, as an exact polynomial-divisibility statement.
## Setting
For $n\ge 0$, let $A(2n)$ be the set of permutations $\sigma=(\sigma_1,\ldots,\sigma_{2n})$ of $\{1,\ldots,2n\}$ satisfying
$$
\sigma_1<\sigma_2>\sigma_3<\sigma_4>\cdots<\sigma_{2n}.
$$
The empty permutation is the unique member of $A(0)$. The inversion number is
$$
\operatorname{inv}(\sigma)
=\#\{(i,j):1\le i<j\le 2n,\ \sigma_i>\sigma_j\}.
$$
The $q$-secant inversion enumerator is the integer polynomial
$$
E_{2n}(q)=\sum_{\sigma\in A(2n)}q^{\operatorname{inv}(\sigma)}\in\mathbb Z[q].
$$
Congruence modulo $(1+q)^3$ means divisibility in $\mathbb Z[q]$: two polynomials $F$ and $G$ are congruent precisely when $(1+q)^3$ divides $F-G$. This formulation avoids evaluation at a single number and records the first three orders of behavior at $q=-1$.
In Lean, a permutation is represented as an equivalence of `Fin (2*n)`. The alternating inequalities and inversion number are finite predicates and counts on this zero-based type. The polynomial variable is the canonical indeterminate in `Polynomial ℤ`.
## Formalization targets
### Cubic congruence
For every integer $n\ge0$, prove
$$
E_{2n}(q)\equiv
q^{2n(n-1)}-\binom n2(1+q)^2
\pmod{(1+q)^3}.
$$
Equivalently,
$$
(1+q)^3\mid
E_{2n}(q)-
\left(q^{2n(n-1)}-\binom n2(1+q)^2\right)
\quad\text{in }\mathbb Z[q].
$$
The boundary value $n=0$ is included. With the empty-permutation convention and natural-number truncated subtraction in the exponent, both sides reduce correctly, so the formal target does not hide a separate exceptional case.
## Significance
The theorem identifies the exact quadratic correction to the highest-inversion monomial near $q=-1$. It therefore explains why the prior congruence modulo $(1+q)^2$ does not generally lift unchanged to the cubic modulus. Specializing at $q=1$ also yields the corresponding refinement modulo $8$ for the ordinary secant numbers. More broadly, the statement is a compact test case for formal reasoning that combines finite permutations, order predicates, inversion statistics, generating polynomials, binomial coefficients, and divisibility in a polynomial ring.
A machine-checked proof would contribute reusable infrastructure for permutation enumerators and polynomial congruences. The published article supplies a human proof; the Prove2me goal is the formal reconstruction of its theorem in Lean. The mission does not encode a proof certificate, an orbit count, or the desired divisibility inside a definition. A successful submission must derive the divisibility from the concrete finite definitions.
The result also gives a useful interface between two styles of formal combinatorics. On one side, alternating permutations are finite objects that can be enumerated, mapped, and partitioned. On the other, their aggregate is an algebraic object in $\mathbb Z[q]$ whose divisibility can be studied without referring to individual permutations. Infrastructure connecting these levels can be reused for other $q$-Euler numbers, descent and major-index enumerators, and congruences obtained from finite weighted actions. The mission keeps that infrastructure general-purpose by making the final target an equality in a quotient of the polynomial ring rather than a specialized computational procedure.
## Difficulty
Direct expansion of $E_{2n}(q)$ is factorial in $n$ and gives no uniform explanation of divisibility by a third power. Divisibility by $(1+q)^3$ is stronger than merely checking the value at $q=-1$: it simultaneously constrains the value and the first two formal orders there. A formal solution must control the entire finite family of alternating permutations while preserving exact inversion exponents and polynomial coefficients. Index conventions are also delicate, because the paper numbers positions and values from $1$, whereas Lean uses `Fin` indices from $0$.
The source argument introduces combinatorial structure beyond the bare statement. Formalizers may contribute reusable lemmas about switching consecutive values, invariance of alternation under permitted switches, inversion-number changes, finite group actions, and divisibility of orbit enumerators. Those are natural milestones, but the present root goal deliberately remains the stable polynomial congruence rather than committing to one decomposition.
## Formalization scope
The mission fixes the coefficient ring to $\mathbb Z$ and uses exact polynomial divisibility. It does not replace congruence by coefficientwise arithmetic modulo $8$, evaluation at $q=-1$, or a numerical check for bounded $n$. `UpDown` is defined directly on permutations of `Fin (2*n)`, `invNumber` counts ordered index pairs with the required inequality, and `qSecant` is the finite sum of monomials $q^{\operatorname{inv}(\sigma)}$.
The formal statement quantifies over every natural number. The conventions at $n=0$ and $n=1$ are part of the same theorem and have been audited explicitly. The uploaded definition bundle is transparent and sorry-free; the only admitted declaration is the mission theorem itself. Useful contributions include general lemmas about polynomial divisibility, finite involutions and orbit sums, or bridges between one-based paper notation and Lean's finite types.
## Selected references
- Ji-Cai Liu, *A Combinatorial Proof of a Cubic Congruence for the $q$-Secant Inversion Enumerator*, Electronic Journal of Combinatorics 33(3), P3.10, 2026. [DOI](https://doi.org/10.37236/15666)
Vector Space Methods V: Convex Separation and Distance DualityTextbook
## Motivation
Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's *Optimization by Vector Space Methods* builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional ([Luenberger, §§5.12--5.13, pp. 130--137](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.
## Setting
Let $X$ be a **real normed space** and $K\subseteq X$ a nonempty convex set. Convexity is represented by `Convex ℝ K`, and topological interior, closure, and infimum distance use Mathlib's `interior`, `closure`, and `Metric.infDist`. A **continuous affine separator** is described by a continuous linear functional $f:X\toL[\mathbb R]\mathbb R$ and a scalar level $c$. The inequality $f(k)\le c$ for all $k\in K$ places $K$ in one closed half-space.
When a convex set contains zero in its interior, its **Minkowski gauge** is the functional `gauge K`. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets
$$
\{x:g_K(x)\le 1\}=\overline K,
\qquad
\{x:g_K(x)<1\}=\operatorname{int}K.
$$
These properties are bundled into the first milestone, following Lemma 1 of §5.12 ([pp. 131--132](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
For two convex sets $K_1,K_2$, **Eidelheit separation** means finding nonzero $f$ and $c$ with $f(x)\le c\le f(y)$ for $x\in K_1$ and $y\in K_2$. The source assumes that $K_1$ has nonempty interior and that its interior does not meet $K_2$. The Lean statement records the nonemptiness of $K_2$ explicitly, since otherwise nonzero separation is not forced.
## Formalization targets
### Gauge and geometric Hahn--Banach milestones
Formalize the six gauge properties above. Then, for a convex $K$ with nonempty interior and an affine subspace $V$ disjoint from that interior, produce $f\ne0$ and $c$ such that
$$
f(v)=c\quad(v\in V),
\qquad
f(k)<c\quad(k\in\operatorname{int}K).
$$
This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 ([p. 133](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
### Supporting hyperplanes and convex-set separation
For $x\notin\operatorname{int}K$, formalize a nonzero functional satisfying $f(k)\le f(x)$ for all $k\in K$. Next formalize Eidelheit separation:
$$
f(x)\le c\le f(y)
\quad\text{for all }x\in K_1,\ y\in K_2.
$$
These are Theorems 2 and 3 of §5.12 ([pp. 133--134](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
### Convex minimum-distance duality
Let $x_1$ have positive distance $d$ from $K$. Produce $f$ and a real upper-bound level $c$ with $\|f\|\le1$, $f(k)\le c$ on $K$, and
$$
f(x_1)-c=d.
$$
Every other feasible pair $(g,b)$ must satisfy $g(x_1)-b\le d$. If $x_0\in K$ realizes the distance, require $-f$ to align with $x_0-x_1$. This is the finite real certificate form of §5.13, Theorem 1 ([pp. 136--137](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## Significance
The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair $(g,b)$ yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when $K$ is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.
Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.
## Difficulty
A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level $c$ is unavoidable. The common shorthand $\sup_{k\in K} f(k)$ introduces a second problem: $K$ need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound $c$ and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.
Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion $x_1\notin K$ would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.
## Formalization scope
The mission is restricted to real normed spaces. Sets use `Set X`; affine varieties use `AffineSubspace ℝ X`; separators use `ContinuousLinearMap`. The gauge is Mathlib's existing `gauge`, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.
The Eidelheit theorem includes `K₂.Nonempty`, an assumption used implicitly by the source's separating conclusion. The capstone includes `K.Nonempty` and `0 < Metric.infDist x₁ K`; it does not assume closedness, boundedness, compactness, or attainment. Its pair $(f,c)$ represents a finite support level, and the universal comparison over all feasible $(g,b)$ rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality $\|x_0-x_1\|=d$ and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 5, §§5.11--5.13, pp. 127--137. [Public scan](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf).
Vector Space Methods IX: Global Lagrange DualityTextbook
## Motivation
Many convex programs impose inequalities valued in a vector space: componentwise inequalities, positive-semidefinite constraints, and families of ordered resource constraints are all instances of one cone order. Chapter 8 of David G. Luenberger's [*Optimization by Vector Space Methods*](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods) develops a global theory for this setting. A perturbation of the constraint produces a convex value function, continuous linear functionals positive on the ordering cone become Lagrange multipliers, and a strict-feasibility condition yields an attained dual optimum. This mission formalizes the progression in §§8.2–8.6, culminating in the book's Lagrange Duality Theorem.
## Setting
Let $X$ and $Z$ be real normed spaces, let $\Omega\subseteq X$ be a nonempty convex set, and let $P\subseteq Z$ be a **convex cone**. The cone induces the relation
$$
z_1\le_P z_2\quad\Longleftrightarrow\quad z_2-z_1\in P.
$$
A continuous linear functional $z^*\in Z^*$ is **dual-positive** when $z^*(p)\ge0$ for every $p\in P$. A map $G:X\to Z$ is **cone-convex on $\Omega$** when its value at a convex combination is below the corresponding convex combination of its values in this cone order. The primal program is
$$
\mu=\inf\{f(x):x\in\Omega,\ G(x)\le_P0\},
$$
where $f$ is real-valued and convex on $\Omega$.
For a multiplier $z^*$, the **Lagrangian** and its possibly infinite dual value are
$$
L(x,z^*)=f(x)+z^*(G(x)),\qquad
\phi(z^*)=\inf_{x\in\Omega}L(x,z^*).
$$
The perturbed primal value $\omega(z)$ replaces the zero right-hand side by $G(x)\le_P z$. Lean represents $\omega$ and $\phi$ in `EReal`, so infeasible perturbations have value $+\infty$ and objectives unbounded below can have value $-\infty$ without arbitrary defaults.
## Formalization targets
### Main goal: Lagrange duality
Assume $P$ has nonempty interior, the primal value $\mu$ is finite, and there is a **strictly feasible point** $x_s\in\Omega$ with
$$
-G(x_s)\in\operatorname{int}P.
$$
Prove that a dual-positive $z_0^*$ exists and attains
$$
\mu=\phi(z_0^*)=
\max_{z^*\ \text{dual-positive}}\phi(z^*).
$$
If $x_0$ attains the primal infimum, also prove complementarity $z_0^*(G(x_0))=0$ and that $x_0$ minimizes $L(\,·\,,z_0^*)$ over $\Omega$.
### Milestones
Five source milestones delimit the reusable theory. A closed convex cone is recovered from all dual-positive inequalities (§8.2, Proposition 1). The finite-height epigraph of the extended perturbation value is convex, and that value is antitone in the cone order (§8.3, Propositions 1–2). A Lagrangian saddle point is sufficient for primal feasibility and optimality when the cone is closed (§8.4, Theorem 2). Finally, multipliers for two perturbed right-hand sides bound the change in optimal objective value from both sides (§8.5, Theorem 1). The root then states §8.6, Theorem 1 rather than duplicating the equivalent multiplier theorem from §8.3.
## Significance
The capstone provides both equality of optimal values and an attained multiplier. It applies to a single vector inequality, so finite systems of scalar inequalities and matrix-cone constraints fit the same statement once their ordering cones are supplied. Complementarity and Lagrangian minimization turn a primal optimizer and multiplier into a certificate. The sensitivity milestone additionally gives quantitative information about how the optimum changes when the constraint right-hand side moves.
Formalization produces a reusable cone-order layer independent of coordinate choices. `coneLE`, `dualPositive`, and `ConeConvexOn` can support later Kuhn–Tucker, vector optimization, and conic programming developments. The `EReal` value functions preserve infeasibility and unboundedness, two cases that a real-valued `sInf` encoding would collapse. This is a formalization mission for a classical theorem, not a claim that the underlying duality result is open.
## Difficulty
The theorem's strict-feasibility condition is load-bearing. Feasibility $-G(x)\in P$ cannot replace interior feasibility, and nonempty interior of $P$ alone does not supply a Slater point. Equality constraints also cannot be converted into pairs of inequalities while retaining strict feasibility; Luenberger explicitly warns about this after the theorem.
The cone assumptions differ across milestones. The main strong-duality theorem does not require $P$ to be closed or pointed, whereas the bipolar and saddle-sufficiency statements require closedness. Using Mathlib's stronger `ProperCone` everywhere would silently add both topological and order hypotheses and shrink the theorem. Another tempting simplification is to make both value functions real. That loses the empty feasible set and unbounded dual subproblem, precisely the boundary cases used when comparing perturbations. The saddle inequalities must also have the correct orientation: the multiplier coordinate is maximized and the primal coordinate is minimized.
## Formalization scope
The mission uses `ConvexCone ℝ Z` with a custom induced relation; it deliberately does not assume a lattice order on $Z$. Multipliers are continuous linear maps $Z\to\mathbb R$. The root assumes a real finite optimum through `IsGLB` and a real witness $\mu$, while `lagrangeDualValue` and `perturbationValue` retain `EReal` codomains. The strict condition is written as membership of $-G(x_s)$ in `interior P`, exactly matching $G(x_s)<_P0$.
No finite-dimensionality, reflexivity, completeness, closedness, or pointedness is added to the root. Closedness appears only where the source uses cone separation to recover primal feasibility. The sensitivity item assumes the two candidate points are feasible, their multipliers are dual-positive and complementary, and each point minimizes its shifted Lagrangian; these hypotheses spell out “solutions and corresponding multipliers” without relying on informal terminology.
Contributions may formalize cone separation, perturbation-value geometry, saddle certificates, or strong duality. Finite-dimensional orthant and positive-semidefinite specializations are useful corollaries but do not replace the general goal. Local multiplier rules, equality constraints, differentiable Kuhn–Tucker conditions, and Chapter 9's local theory remain outside this mission.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 8, §§8.2–8.6, pp. 214–225. [Open Library record](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods)
- Stephen Boyd and Lieven Vandenberghe, *Convex Optimization*, Cambridge University Press, 2004, Chapter 5. [Official book page](https://web.stanford.edu/~boyd/cvxbook/)
Asymmetric Hashing Square Bound: omega < 2.3747Research Paper
AI generated, I think it's correct
## Motivation
The **matrix-multiplication exponent** measures the asymptotic arithmetic cost of multiplying square matrices. A bound $\omega<c$ means that, over the field under consideration, $n\times n$ matrices can be multiplied in $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$. Matrix multiplication is a central benchmark in algebraic complexity and a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The Coppersmith--Winograd tensor and the laser method produced the strongest bounds on $\omega$ for several decades. The 1990 tensor-square analysis gave $\omega<2.375477$. Later analyses of larger powers improved the numerical bound, but they organized their recursion through values assigned independently to constituent tensors. Duan, Wu, and Zhou identified a loss in that organization: several fine constituents that can coexist inside one coarse block may be counted as though they had to be selected independently. Their asymmetric-hashing framework partially compensates for this **combination loss**. The paper's full second-power specialization improves the best bound obtainable from the square of the Coppersmith--Winograd tensor to $\omega<2.374631$; see Section 6.3 and its parameter Table 2 in [Duan--Wu--Zhou](https://arxiv.org/abs/2210.10173).
This mission isolates that second-power result. It is smaller than the paper's record-setting eighth-power calculation, but it contains the genuinely new asymmetric-hashing and hole-repair mechanisms in their first complete form. It therefore provides a focused bridge from the existing formalization of the classical $2.375477$ square analysis to later combination-loss methods.
## Setting
For a field $K$, 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, while a degeneration permits polynomial families of such maps and takes their first nonzero coefficient. A degeneration from the diagonal tensor $I_r$ gives a border-rank upper bound of $r$.
The **Coppersmith--Winograd tensor** with parameter $q$ is
$$
CW_q=
\sum_{i=1}^{q}
(x_i y_i z_0+x_i y_0z_i+x_0y_i z_i)
+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 coordinate partition has six supported types, and the square $CW_q^{\otimes2}$ has fifteen coarse constituent types $(i,j,k)$ with $i+j+k=4$. A large tensor power contains many blocks with prescribed joint and marginal type distributions. The **laser method** retains blocks whose variables are disjoint and interprets their direct sum through Schönhage's asymptotic sum inequality.
Duan--Wu--Zhou refine this organization by also retaining a split distribution for the fine indices inside each coarse constituent. Coarse $X$- and $Y$-blocks are made unique, while compatible coarse triples may initially share a $Z$-block. The resulting partially damaged constituent tensors are described as broken copies of a standard-form tensor. The formal target uses $q=6$, the full Section 6 construction, and the paper's released second-power parameters.
## Formalization targets
### Goal: the full second-power asymmetric-hashing bound
For every field $K$,
$$
\operatorname{matMulExp}(K)<\frac{23747}{10000}=2.3747.
$$
The source reports the stronger numerical endpoint $2.374631$, so the displayed rational inequality has strict slack. The Lean declaration has exactly the same field quantification and uses exactly the same `matMulExp` definition as the existing Coppersmith--Winograd $2.376$ mission; only the theorem name and rational endpoint change.
### Source-level milestones
The mission first isolates the available-block shuffling interface extracted from Definitions 5.3--5.5 and Claims 5.8--5.10, then formalizes the finite covering core of the Hole Lemma 5.6. The subsequent tensor realization by zeroing and identification, the multiple-copy Corollary 5.11, the compatibility-rate identity of Lemma 6.7, the probabilistic part of Claim 6.8, and the global restricted-splitting value inequality in Equation (25) remain visible structural leaves rather than being hidden inside scalar assumptions. The numerical milestone instantiates Equation (25) with the exact $q=6$ data of Section 6.3 and Table 2 and checks a strict value surplus at $\tau=23747/30000$. The structural proof must also make explicit the conversion from the paper's six-symmetrized value to a direct `HasTauValueAtLeast` witness for the mode-symmetric CW square. The final bridge applies the existing tau-value/rank machinery and transfers the Strassen-preorder exponent bound to `matMulExp`.
## Significance
The mathematical result gives the first improvement over the classical Coppersmith--Winograd number while continuing to use only the tensor square. It separates improvement of the tensor analysis from improvement obtained merely by moving to a much higher tensor power. The same standard-form and restricted-splitting language is then reused by the paper's higher-power algorithm, which reports $\omega<2.371866$.
For formalization, the mission adds reusable infrastructure for nested tensor partitions. Existing CW-square work records coarse support types and actual matrix-multiplication restrictions. This mission extends that layer with fine split distributions, compatibility between levels, broken-block bookkeeping, and repair of holes without replacing tensor statements by unverified scalar values. Those definitions are prerequisites for later asymmetric-hashing, complete-split, and more-asymmetry analyses.
The bound is known mathematically and was published at FOCS 2023. The open work is a machine-checked reconstruction. The underlying CW tensor, border-rank certificate, canonical tensor-square grading, Salem--Spencer sets, direct-sum tau-value notion, asymptotic sum inequality, and exponent equivalence already exist on Prove2Me. The new frontier is the cross-level combination-loss analysis and its exact numerical specialization.
## Difficulty
The central difficulty is that coarse and fine decompositions cannot be optimized independently. Two coarse triples may share a $Z$-block, and a fine $Z$-block can be useful for one triple, compatible with several, or removed by a collision. Counting all locally valuable fine constituents therefore does not certify a direct sum. Conversely, requiring every coarse $Z$-block to be unique discards precisely the combinations that produce the improvement.
The Hole Lemma must also preserve the actual tensor. A broken copy lacks some fine variable blocks; combining several such copies is useful only when a degeneration covers every required block with controlled loss and does not duplicate monomials. On the numerical side, the same-marginal maximum-entropy term and restricted-splitting values must be bounded with certified real inequalities. Floating-point output from MATLAB is evidence for a witness, not a Lean proof.
## Formalization scope
The mission uses the existing `TensorObj`, `MMObj`, restriction, degeneration, asymptotic-rank, `HasTauValueAtLeast`, `matMulExp_strassen`, and `matMulExp` declarations in environment `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Top-level results quantify over an arbitrary field. Finite supports and block indices are represented by finite types; probability and split distributions are nonnegative real functions of total mass one; entropy and numerical optimization live in the reals.
The formalization is restricted to $CW_6^{\otimes2}$ for the capstone, although generic definitions and source lemmas may quantify over levels and finite index types. A valid proof must connect scalar rate inequalities to witnessed restrictions or degenerations yielding direct sums of concrete matrix-multiplication tensors. A constant-valued surrogate for the restricted-splitting value, a hypothesis that already assumes the desired exponent bound, or a certificate definition containing its own conclusion is outside scope.
Contributions are welcome for standard-form tensor encodings, finite permutation arguments, hole repair, type and split counting, entropy maximization certificates, certified logarithm and power inequalities, and the final tau-value/rank assembly. Statements should identify the corresponding definition, lemma, claim, equation, or table in the source.
## Selected references
- Ran Duan, Hongxun Wu, and Renfei Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*, 64th IEEE Symposium on Foundations of Computer Science (FOCS), 2023. [arXiv:2210.10173](https://arxiv.org/abs/2210.10173) and [released verification code](https://osf.io/dta6p/).
- Don Cop persmith and Shmuel Winograd, *Matrix Multiplication via Arithmetic Progressions*, Journal of Symbolic Computation 9, 1990, pp. 251--280. [DOI 10.1016/S0747-7171(08)80013-2](https://doi.org/10.1016/S0747-7171(08)80013-2).
- 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).
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)
Vector Space Methods VII: Euler–Lagrange EquationsTextbook
## Motivation
The calculus of variations replaces optimization over finitely many coordinates by optimization over paths. Its necessary conditions underlie geodesics, minimum-energy curves, classical mechanics, and many optimal-control models. Chapter 7 of David G. Luenberger's [*Optimization by Vector Space Methods*](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods) presents this transition as an application of differentiation in normed vector spaces: a local extremum first forces every directional derivative to vanish, and the resulting integral identity forces a differential equation along the optimizing path. This mission formalizes the scalar, fixed-endpoint version in §§7.4–7.5. The target is intentionally the theorem actually isolated by the source, not a stronger modern Sobolev-space variant.
## Setting
Fix real numbers $a<b$. A **$C^1$ path on the segment** is represented in Lean by two functions, $x,\dot x:\mathbb R\to\mathbb R$. Both are continuous on $[a,b]$, and $x$ has derivative $\dot x(t)$ at every $t\in(a,b)$. Ordinary two-sided derivatives are not demanded at $a$ or $b$; this makes the formal endpoint convention match the one-sided role of endpoints in a closed interval.
Let $L(y,v,t)$ be a scalar Lagrangian. Along a candidate path, write
$$
L_x(t)=\frac{\partial L}{\partial y}(x(t),\dot x(t),t),\qquad
L_v(t)=\frac{\partial L}{\partial v}(x(t),\dot x(t),t).
$$
The Lean statement records these partial derivatives with `HasDerivAt` and assumes that $L_x$ and $L_v$ are continuous on $[a,b]$. A **fixed-endpoint variation** is another $C^1$ pair $(h,\dot h)$ with $h(a)=h(b)=0$. The first variation already computed from the action is
$$
\delta J(x;h)=\int_a^b\bigl(L_x(t)h(t)+L_v(t)\dot h(t)\bigr)\,dt.
$$
The main theorem begins from the stationarity identity $\delta J(x;h)=0$ for every such variation. It does not claim that the complete passage from a local extremum in Luenberger's $C^1$ norm to this integral formula has already been bundled into the root statement.
## Formalization targets
### Main goal: Euler–Lagrange equation
From the computed first-variation identity, prove that
$$
\frac{d}{dt}L_v(t)=L_x(t)\qquad(t\in(a,b)).
$$
The conclusion is expressed as `HasDerivAt Lv (Lx t) t`, so it asserts both differentiability of $L_v$ and the equality of its derivative with $L_x$. This is equation (2) and the conclusion reached on printed pages 180–181.
### Milestones
The first milestone formalizes §7.4, Theorem 1: a local minimum or maximum of a real functional has zero derivative along every direction whenever that scalar directional derivative exists. The remaining milestones are the three fixed-endpoint fundamental lemmas from §7.5. They respectively show that a continuous coefficient annihilating all variations is zero, that a continuous coefficient annihilating all variation derivatives is constant, and that an identity involving both $h$ and $\dot h$ forces the second coefficient to have derivative equal to the first. These are stated with the same $C^1$ variation class used by the goal.
## Significance
The result turns an infinite family of scalar integral equalities into a pointwise differential equation. Once available, the same interface can support standard variational examples by supplying a concrete $L$, its two partial derivatives, and a stationary path. It also provides the analytic core needed before treating natural boundary conditions, vector-valued paths, higher derivatives, or weak Euler–Lagrange equations.
The formalization adds reusable interval-sensitive infrastructure. In particular, `IsC1OnSegment` separates a path from its chosen continuous derivative and avoids silently imposing derivatives outside the optimization interval. The three fundamental lemmas are useful independently of the named Euler–Lagrange theorem: they are test-function principles for interval integrals and can serve later missions involving integration by parts or weak formulations. The mathematics is classical and proved in the cited text; the open work is a machine-checked Lean development of these exact statements in the pinned Mathlib environment.
## Difficulty
The source argument uses informal phrases such as “arbitrary $C^1$ function vanishing at the endpoints” and treats endpoint differentiation according to standard calculus convention. In Lean, those phrases must determine a precise domain, derivative witness, continuity requirement, and interval-integral orientation. Replacing $C^1$ variations by merely continuous functions would change Lemmas 2 and 3, while requiring `HasDerivAt` at the endpoints would add a hypothesis not present in the book.
Another tempting shortcut is to assume from the outset that $L_v$ is differentiable and then use integration by parts. That would trivialize the central regularity conclusion of Lemma 3: the book derives differentiability of $L_v$ from stationarity and continuity. The root therefore assumes only continuity of the two coefficient functions and concludes a `HasDerivAt` assertion on the open interval. Conversely, constructing the first variation from a local extremum of the action requires a separate differentiation-under-the-integral development and a topology on bundled $C^1$ paths; it is not hidden inside the main goal.
## Formalization scope
The scalar field, path values, time variable, and action values are all real. The interval is nondegenerate through the explicit hypothesis $a<b$. Integrals use Mathlib's oriented interval integral, but all principal statements are made in the forward orientation. Paths and variations are total functions on $\mathbb R$ whose relevant regularity is restricted to $[a,b]$. The Lagrangian is finite-valued. No measurability or integrability premise is omitted: continuity of the coefficient and variation factors on the compact interval supplies the intended finite integrals.
The goal starts from an already computed first-variation identity. Contributions connecting a genuine local extremum of the action in the norm $\max|x|+\max|\dot x|$ to that identity are welcome as a strengthening, but they must not be advertised as part of the present root theorem. Other welcome contributions include reusable continuous test-function constructions and endpoint-aware interval integration lemmas. Sobolev paths, vector-valued state spaces, free endpoints, and weak derivatives are outside this mission and should be proposed separately rather than obtained by weakening the stated hypotheses until the result becomes vacuous.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 7, §§7.4–7.5, pp. 178–181; definition of $D[a,b]$ on p. 23. [Open Library record](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods)
Vector Space Methods VI: Pseudoinverse OperatorsTextbook
## Motivation
Linear equations between Hilbert spaces need not have unique solutions and may not even be exactly solvable for a given right-hand side. Least squares selects a vector with the smallest residual; when several such vectors exist, minimum norm selects one canonical representative. Luenberger packages this two-stage optimization into the **pseudoinverse** of a continuous linear operator with closed range. The construction unifies exact equations, approximation, normal equations, and orthogonal projections, while retaining a bounded linear operator suitable for subsequent optimization methods ([Luenberger, §§6.9--6.11, pp. 159--165](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
This mission continues the series into Chapter 6. Its capstone formalizes the structural identities of the pseudoinverse, including involution, compatibility with adjoints, reflexive inverse laws, self-adjoint projection products, and factorizations through the normal operators. Earlier milestones establish the adjoint facts and minimum-norm characterizations on which that operator calculus depends.
## Setting
Let $G$ and $H$ be **real Hilbert spaces**, represented in Lean by complete real inner-product spaces, and let $A:G\toL[\mathbb R]H$ be a continuous linear map whose range is closed. The **Hilbert adjoint** is written $A^\dagger$ in the Lean statements and is Mathlib's adjoint continuous linear map. It is characterized by the inner-product relation and satisfies $\|A^\dagger\|=\|A\|$ ([Luenberger, §6.5, Theorem 1, p. 151](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)). Closed range gives the range-kernel identity
$$
\operatorname{range}(A^\dagger)=\ker(A)^\perp,
$$
the Hilbert-space specialization of the closed range theorem used in the chapter ([§6.6, Theorem 2, p. 156](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
For $y\in H$, a vector $x\in G$ is a **least-squares solution** when $\|Ax-y\|$ is no larger than $\|Az-y\|$ for every $z$. A least-squares solution is **minimum norm** when its norm is no larger than that of every other least-squares solution. A continuous linear map $B:H\toL[\mathbb R]G$ satisfies `VectorSpaceOpt.IsPseudoinverse A B` when, for every $y$, $By$ has both properties. This predicate is the mission's one lightweight definition, directly encoding the definition in §6.11 ([pp. 163--164](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## Formalization targets
### Adjoint and closed-range milestones
Formalize $\|A^\dagger\|=\|A\|$. Under closed range, formalize
$$
\operatorname{range}(A^\dagger)=\ker(A)^\perp.
$$
These record §6.5, Theorem 1 and the Hilbert form of §6.6, Theorem 2.
### Normal equations and minimum-norm solutions
Formalize the least-squares equivalence
$$
x\text{ minimizes }\|y-Ax\|
\quad\Longleftrightarrow\quad
A^\dagger A x=A^\dagger y,
$$
as in §6.9, Theorem 1 ([p. 160](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)). For solvable $Ax=y$ and closed-range $A$, characterize the minimum-norm solution by $x=A^\dagger z$ with $AA^\dagger z=y$, following §6.10, Theorem 1 ([pp. 161--162](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)). Finally, formalize existence and uniqueness of a continuous linear $B$ satisfying `IsPseudoinverse A B`.
### Pseudoinverse identities
Given such a $B$, formalize that $A$ is the pseudoinverse of $B$, that $B^\dagger$ is the pseudoinverse of $A^\dagger$, and that
$$
BAB=B,\qquad ABA=A,\qquad (BA)^\dagger=BA.
$$
Also produce pseudoinverses $C$ of $A^\dagger A$ and $D$ of $AA^\dagger$ satisfying
$$
B=CA^\dagger,
\qquad
B=A^\dagger D.
$$
Together with the continuous-linear-map type of $B$, these clauses encode all nine items of §6.11, Proposition 1 ([p. 165](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## Significance
The pseudoinverse turns a possibly inconsistent or underdetermined equation into a canonical bounded linear solution operator. The normal equations connect residual minimization with the self-adjoint operator $A^\dagger A$; the minimum-norm theorem selects the component orthogonal to the kernel. The capstone identities show that the construction behaves like an inverse on the effective ranges and that $BA$ is self-adjoint, while the two factorizations reduce pseudoinverse questions to the normal operators.
The underlying results are proved in Luenberger's text. Their Lean formalization supplies a reusable predicate for minimum-norm least squares and an operator-level API linking adjoints, kernels, ranges, composition, and optimization characterizations. This bridges the earlier missions on minimum norm and estimation with later chapters that use normal operators and generalized inverses. It also records explicitly which conclusions require closed range, preventing accidental use of a bounded pseudoinverse where only an unbounded generalized inverse could exist.
## Difficulty
Pointwise existence of a best residual is not enough. The selected minimum-norm solutions must collectively form a linear bounded map, and closed range is the hypothesis that makes this global operator well behaved. Without closed range, least-squares minimizers may fail to exist and the inverse on the effective range need not be bounded. A formulation that chooses an arbitrary minimizer for each target would therefore miss the main analytic content.
Several notationally similar operations must also remain distinct. The book writes a star for the adjoint and a superscript dagger-like symbol for the pseudoinverse; Mathlib's displayed dagger denotes the Hilbert adjoint. The mission consequently names the generalized inverse through `IsPseudoinverse` instead of overloading dagger notation. Orthogonal complements apply to submodules, compositions must retain their source and target spaces, and each factorization involves a different normal operator. These typing constraints expose domain/codomain mistakes that paper notation suppresses.
## Formalization scope
The mission uses real Hilbert spaces only: `NormedAddCommGroup`, `InnerProductSpace ℝ`, and `CompleteSpace`. Operators are `ContinuousLinearMap`, composition is `∘L`, the Hilbert adjoint is Mathlib's `†`, and the closed-range assumption is `IsClosed (A.range : Set H)`. The orthogonal complement in the range theorem is the submodule `A.kerᗮ`.
`IsPseudoinverse A B` requires two pointwise inequalities for every target: `B y` minimizes residual norm among all inputs, then minimizes norm among all residual minimizers. The second clause cannot be dropped or weakened to exact solutions, because it is what makes the choice canonical for inconsistent as well as underdetermined systems. The minimum-norm-solution milestone states `y ∈ A.range` explicitly; the source treats solvability as part of speaking about a solution. The capstone accepts a continuous linear $B$ satisfying the predicate, so linearity and boundedness are represented by its type, corresponding to the first two items of Proposition 1. Contributions may add reusable lemmas about adjoints, orthogonal complements, closed range, normal equations, or uniqueness of optimizers, but must preserve the closed-range and completeness assumptions in the public operator theorems.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 6, especially §§6.5--6.11, pp. 151--165. [Public scan](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf).
## Motivation
The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a $d$-dimensional polytope with $n$ facets is at most $n - d$. Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the **polynomial Hirsch conjecture**: is the diameter bounded by a polynomial in $n$ and $d$?
## Timeline
- **1957.** Hirsch states the conjecture $\mathrm{diam} \le n - d$ in a letter to Dantzig, who publishes it in *Linear Programming and Extensions* (1963).
- **1964–1966.** Klee determines the exact maximum diameter of $3$-polytopes with $n$ facets, $\lfloor 2n/3\rfloor - 1$ — the Hirsch bound holds up to dimension three.
- **1967.** Klee and Walkup ([Acta Math.](https://doi.org/10.1007/BF02392971)) refute the *unbounded-polyhedron* version, prove the bounded conjecture for $n - d \le 5$, and reduce the general case to the **$d$-step conjecture** ($n = 2d$).
- **1970.** Larman ([Proc. LMS](https://doi.org/10.1112/plms/s3-20.2.249)) proves $\mathrm{diam} \le n\,2^{d-3}$ — linear in the number of facets for each fixed dimension, still the best bound of that shape.
- **1989.** Naddef ([Math. Programming](https://doi.org/10.1007/BF01589418)) proves $0/1$-polytopes satisfy the Hirsch bound, with diameter at most $d$.
- **1992.** Kalai and Kleitman ([Bull. AMS](https://arxiv.org/abs/math/9204233)) prove $\mathrm{diam} \le n^{\log_2 d + 2}$ in under a page — the quasi-polynomial barrier every later bound refines. The same year brings subexponential pivot rules (Kalai; Matoušek–Sharir–Welzl), the algorithmic counterpart.
- **2010.** Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR](https://doi.org/10.1287/moor.1100.0470)) show the known upper-bound arguments survive in a purely combinatorial abstraction — which admits almost-quadratic lower bounds, so a polynomial bound must use real geometry. Kalai launches **Polymath 3** on the polynomial version.
- **2010–2012.** Santos ([Annals of Math.](https://arxiv.org/abs/1006.2814)) disproves the Hirsch conjecture: a $43$-dimensional polytope with $86$ facets and diameter at least $44$, via spindles of large width.
- **2014–2019.** Todd ([SIAM J. Discrete Math.](https://arxiv.org/abs/1402.3579)) sharpens Kalai–Kleitman to $(n-d)^{\log_2 d}$; Sukegawa refines further. Matschke, Santos, and Weibel ([Proc. LMS 2015](https://arxiv.org/abs/1202.4701)) shrink the counterexample to dimension $20$ with $40$ facets and diameter $21$. All known violations remain constant-factor; all known bounds remain quasi-polynomial.
## Setting
Work in $\mathbb{R}^d$. An **H-polytope** is a set cut out by finitely many linear inequalities: given vectors $a_1, \dots, a_n \in \mathbb{R}^d$ and reals $b_1, \dots, b_n$, it is
$$P \;=\; \{\, x \in \mathbb{R}^d \mid \langle a_i, x\rangle \le b_i \text{ for } i = 1, \dots, n \,\},$$
where $\langle a_i, x\rangle = \sum_{j=1}^d a_{ij} x_j$ is the standard inner (dot) product — so each condition $\langle a_i, x\rangle \le b_i$ is one linear inequality, with normal vector $a_i$ and offset $b_i$. Throughout, $P$ is assumed nonempty and bounded. The parameter $n$ counts the inequalities in the given description; since every polytope with $f$ facets admits a description by exactly $f$ inequalities, bounds stated in terms of $n$ over all descriptions are equivalent to bounds in terms of facet counts.
A **vertex** of $P$ is an extreme point. Two vertices $u \ne v$ are **adjacent** when the segment $[u, v]$ is an extreme subset of $P$; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that $[u,v]$ is a one-dimensional face — an **edge**. The **combinatorial diameter** of $P$ is the diameter of the graph of vertices and edges. Throughout, "diameter at most $B$" is expressed as: every two vertices are joined by a walk of $B$ steps, each step staying put or crossing an edge — a form that is monotone in $B$ and asserts connectivity of the graph (Balinski's theorem) as part of the claim.
## Formalization targets
### Goal — the polynomial Hirsch conjecture
$$\exists\, c, k \in \mathbb{N}:\ \text{every nonempty bounded } P = \{x \in \mathbb{R}^d \mid \langle a_i, x \rangle \le b_i,\ i \le n\} \text{ has diameter} \le c\,(n + d)^k.$$
Every polynomial in $n$ and $d$ is dominated by some $c(n+d)^k$ and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.
### Milestones — the known ladder
Six classical results over the same definitions: the Hirsch bound $n - d$ in dimension $d \le 3$ (Klee; Klee–Walkup); Larman's bound $n \cdot 2^{d-3}$; Naddef's bound $d$ for $0/1$-polytopes; the Kalai–Kleitman bound $n^{\log_2 d + 2}$; Todd's bound $(n-d)^{\log_2 d}$ for full-dimensional $P$ with $n \ge d \ge 3$; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds $n - d$.
## Significance
A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR 2010](https://doi.org/10.1287/moor.1100.0470)) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.
None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.
## Difficulty
The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving *any* polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters *large* is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.
## Formalization scope
The Lean model commits to: ambient space `EuclideanSpace ℝ (Fin d)`; the polytope as `Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i}` for `a : Fin n → EuclideanSpace ℝ (Fin d)`, `b : Fin n → ℝ`, with nonemptiness and `Bornology.IsBounded` as explicit hypotheses (boundedness is essential: Klee–Walkup's *unbounded* counterexample would otherwise trivialize the Santos milestone); vertices as `Set.extremePoints ℝ`; adjacency as `u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v)`; and diameter bounds as the walk predicate `DiamLE`, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through `Real.logb` and the natural floor. In `larman_bound` and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all $n, d$ in scope. The dimension parameter $d$ is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with `todd_bound` requiring full-dimensionality (`(interior P).Nonempty`) as in its source.
Welcome contributions: any milestone in any order (`dimension_three_bound` for $d \le 1$ cases and structural lemmas about `Adj` and `DiamLE` are natural entry points, and `kalai_kleitman_bound` is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.
## Selected references
- V. Klee, D. Walkup, *The d-step conjecture for polyhedra of dimension d < 6*, Acta Math. 117 (1967). [doi:10.1007/BF02392971](https://doi.org/10.1007/BF02392971)
- D. Larman, *Paths on polytopes*, Proc. London Math. Soc. 20 (1970). [doi:10.1112/plms/s3-20.2.249](https://doi.org/10.1112/plms/s3-20.2.249)
- D. Naddef, *The Hirsch conjecture is true for (0,1)-polytopes*, Math. Programming 45 (1989). [doi:10.1007/BF01589418](https://doi.org/10.1007/BF01589418)
- G. Kalai, D. Kleitman, *A quasi-polynomial bound for the diameter of graphs of polyhedra*, Bull. AMS 26 (1992). [arXiv:math/9204233](https://arxiv.org/abs/math/9204233)
- F. Santos, *A counterexample to the Hirsch conjecture*, Annals of Mathematics 176 (2012). [arXiv:1006.2814](https://arxiv.org/abs/1006.2814)
- M. Todd, *An improved Kalai–Kleitman bound for the diameter of a polyhedron*, SIAM J. Discrete Math. 28 (2014). [arXiv:1402.3579](https://arxiv.org/abs/1402.3579)
- B. Matschke, F. Santos, C. Weibel, *The width of five-dimensional prismatoids*, Proc. London Math. Soc. 110 (2015). [arXiv:1202.4701](https://arxiv.org/abs/1202.4701)
- F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, *Diameter of polyhedra: limits of abstraction*, Math. Oper. Res. 35 (2010). [doi:10.1287/moor.1100.0470](https://doi.org/10.1287/moor.1100.0470)
- F. Santos, *Recent progress on the combinatorial diameter of polytopes and simplicial complexes*, TOP 21 (2013) (survey). [arXiv:1307.5900](https://arxiv.org/abs/1307.5900)
## Motivation
The $k$-server problem was introduced by Manasse, McGeoch, and Sleator ([STOC 1988 / J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) as a common generalization of paging, weighted caching, and related sequential decision problems, and their **$k$-server conjecture** has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on *every* metric space.
## Timeline
- **1985.** Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
- **1988–1990.** Manasse, McGeoch, and Sleator introduce the $k$-server problem ([STOC 1988; J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the **$k$-server conjecture**, in the symmetric finite setting of the paper.
- **1990.** Fiat, Rabani, and Ravid ([FOCS 1990](https://doi.org/10.1109/FSCS.1990.89566)) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space.
- **1991.** Chrobak, Karloff, Payne, and Vishwanathan ([SIAM J. Discrete Math.](https://doi.org/10.1137/0404017)) prove the conjecture on the real line via **Double Coverage**; Chrobak and Larmore ([SIAM J. Comput.](https://doi.org/10.1137/0220008)) extend it to all tree metrics.
- **1995.** Koutsoupias and Papadimitriou ([J. ACM](https://doi.org/10.1145/210118.210128)) prove the **Work Function Algorithm** is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: *for every metric space there is an online algorithm with competitive ratio $k$.*
- **1996.** The same authors verify the conjecture on spaces of $k+2$ points via the dual **2-evader problem** (Inf. Process. Lett. 57).
- **2004.** Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points.
- **2021.** Coester and Koutsoupias ([ICALP](https://arxiv.org/abs/2102.10474)) give a unifying potential for all known WFA analyses and push the frontier to the circle.
- **2023.** Bubeck, Coester, and Rabani ([STOC](https://arxiv.org/abs/2211.05753)) refute the *randomized* analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
## Setting
Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A **configuration** records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the **movement cost** is the total distance traveled,
$$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$
A **request sequence** is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).
A **deterministic online algorithm** $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the **initial configuration**, before any request arrives. Two points about this way of modeling an algorithm:
- *Online and deterministic, by construction.* The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
- *The service constraint.* Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$.
Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its **cost** is the total movement along this trajectory:
$$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$
For comparison, an **offline schedule** for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The **optimal offline cost** $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$.
Finally, $A$ is **$c$-competitive** if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with
$$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$
## Formalization targets
### Goal — the $k$-server conjecture
$$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$
The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.
### Milestones — the known ladder
The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm *itself* — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the *randomized* analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms.
## Significance
A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.
None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem.
## Difficulty
The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server *other than* the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$.
## Formalization scope
The Lean model commits to: configurations as functions `Fin k → M` (**labeled** servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions `List M → (Fin k → M)` with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in `ℝ` via `Metric.dist`; the offline optimum as an `sInf` over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as `∃ a, ∀ σ`.
Two conventions guard against trivialization. The additive constant is quantified *before* the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ *distinct* points (`Finset.card = k + 1`); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.
Three further definitional layers extend the model. The **work function** `workFunction C₀ σ C` is the `sInf` of (schedule cost + final move to `C`) over schedules serving `σ` from `C₀`, and the **Work Function Algorithm** `WFA` is defined on finite spaces with `k ≥ 1` servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A **tree** is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A **randomized algorithm** is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.
Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about `moveCost`, schedules, and work functions published as reusable platform theorems.
## Selected references
- M. Manasse, L. McGeoch, D. Sleator, *Competitive algorithms for server problems*, J. Algorithms 11 (1990). [doi:10.1016/0196-6774(90)90003-W](https://doi.org/10.1016/0196-6774(90)90003-W)
- A. Fiat, Y. Rabani, Y. Ravid, *Competitive k-server algorithms*, FOCS 1990. [doi:10.1109/FSCS.1990.89566](https://doi.org/10.1109/FSCS.1990.89566)
- M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, *New results on server problems*, SIAM J. Discrete Math. 4 (1991). [doi:10.1137/0404017](https://doi.org/10.1137/0404017)
- M. Chrobak, L. Larmore, *An optimal on-line algorithm for k servers on trees*, SIAM J. Comput. 20 (1991). [doi:10.1137/0220008](https://doi.org/10.1137/0220008)
- E. Koutsoupias, C. Papadimitriou, *On the k-server conjecture*, J. ACM 42 (1995). [doi:10.1145/210118.210128](https://doi.org/10.1145/210118.210128)
- E. Koutsoupias, C. Papadimitriou, *The 2-evader problem*, Inf. Process. Lett. 57(5) (1996), 249–252.
- C. Coester, E. Koutsoupias, *Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle*, ICALP 2021. [arXiv:2102.10474](https://arxiv.org/abs/2102.10474)
- S. Bubeck, C. Coester, Y. Rabani, *The randomized k-server conjecture is false!*, STOC 2023. [arXiv:2211.05753](https://arxiv.org/abs/2211.05753)
- E. Koutsoupias, *The k-server problem* (survey), Computer Science Review 3 (2009). [doi:10.1016/j.cosrev.2009.04.002](https://doi.org/10.1016/j.cosrev.2009.04.002)
Vector Space Methods IV: Minimum-Distance DualityTextbook
## Motivation
Best approximation asks how closely a point can be represented by a prescribed linear model. In a Hilbert space, orthogonality turns this into a geometric projection problem. A general normed space has no inner product and may have no nearest point, so the corresponding certificate must live in the continuous dual rather than in the original space. Chapter 5 of Luenberger's *Optimization by Vector Space Methods* develops exactly this passage from geometry to duality: the Hahn--Banach theorem supplies continuous linear functionals that detect norms, separate points from closed subspaces, and certify an infimum distance even when that distance is not attained ([Luenberger, §§5.4--5.8, pp. 111--120](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
This mission continues the book's vector-space formalization series at the point where minimum-norm arguments cease to be specifically Hilbertian. Its capstone identifies the distance from a point to a linear subspace with the largest value at that point among all norm-at-most-one continuous linear functionals annihilating the subspace. The statement is a prototype for dual certificates throughout approximation theory and convex optimization.
## Setting
Let $X$ be a **real normed space** and let $M$ be a linear subspace. In Lean, $M$ is represented by `Submodule ℝ X`; no topological closure assumption is imposed on the capstone. A **continuous linear functional** is an element $f : X \toL[\mathbb R] \mathbb R$, with operator norm $\|f\|$. It **annihilates** $M$ when $f(m)=0$ for every $m\in M$. The set of all such functionals is the annihilator $M^\perp$ in the book's terminology.
For $x\in X$, the **infimum distance** to $M$ is
$$
d(x,M)=\inf_{m\in M}\|x-m\|.
$$
The Lean target uses `Metric.infDist x (M : Set X)`. Since every submodule contains zero, the underlying set is nonempty and this extended geometric notion is an ordinary nonnegative real number here. A functional $f$ is **aligned** with a vector $v$ when $f(v)=\|f\|\,\|v\|$. Alignment is the normed-space replacement for the familiar inner-product equality associated with a projection direction.
Two auxiliary dual notions are also formalized. A norm-preserving Hahn--Banach extension takes a functional on a subspace and extends it to all of $X$ without changing its norm. A **norming functional** for $x$ is a nonzero functional aligned with $x$. Finally, for closed $M$, the preannihilator of its annihilator is exactly $M$: the functionals vanishing on $M$ distinguish every point outside it ([Luenberger, §§5.4 and 5.7, pp. 112--118](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## Formalization targets
### Norm-preserving extension and norming functionals
For a continuous functional $f$ on $M$, formalize an extension $F$ satisfying
$$
F|_M=f,\qquad \|F\|=\|f\|.
$$
For nontrivial $X$ and every $x\in X$, formalize the existence of a nonzero $f$ with $f(x)=\|f\|\,\|x\|$. These are Corollaries 1 and 2 of §5.4 ([pp. 112--113](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
### Closed-subspace double annihilator
For closed $M$, formalize
$$
\{x\in X: \forall f,\ f|_M=0 \Rightarrow f(x)=0\}=M.
$$
This is the concrete set-valued form of Theorem 1 in §5.7 ([p. 118](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
### Minimum-distance duality
For arbitrary $M$ and $x$, produce one functional $f$ with $\|f\|\le 1$, $f|_M=0$, and
$$
f(x)=d(x,M),\qquad
g(x)\le d(x,M)
$$
for every other $g$ of norm at most one annihilating $M$. Thus $f$ realizes the dual maximum. If a best approximant $m_0\in M$ exists, the same certificate also satisfies
$$
f(x-m_0)=\|f\|\,\|x-m_0\|.
$$
This packages both parts of the minimum-distance theorem in §5.8 ([Theorem 1, pp. 119--120](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf)).
## Significance
The capstone gives an exact lower-bound certificate for an infinite-dimensional approximation problem. Every feasible dual functional supplies the inequality $g(x)\le d(x,M)$, while the distinguished functional reaches equality. Consequently, the primal infimum is identified without assuming reflexivity, strict convexity, finite dimension, closedness of $M$, or existence of a nearest point. When a nearest point does exist, alignment records the equality case of the norm estimate and links the dual certificate back to the geometry of the residual.
The source result is classical and proved in the book; the open work here is its machine-checked Lean formalization in the same namespace as the earlier vector-space missions. The reusable output includes norm-controlled extension infrastructure, norming functionals, a concrete double-annihilator theorem, and a certificate form of distance duality suitable for later convex-separation and constrained-optimization missions.
## Difficulty
The obvious Hilbert-space formulation fails because a normed space has no canonical orthogonal complement and a minimizing element of $M$ need not exist. Replacing the minimum by `Metric.infDist` avoids an unjustified attainment assumption, but the desired dual maximizer must still be an actual continuous functional, not merely a limiting family. Norm control is essential: an algebraic separator without continuity cannot serve as a bounded dual certificate.
There are also degenerate cases that informal notation can hide. The distance may be zero even when $x\notin M$ if $M$ is not closed, and then the zero functional is the correct capstone witness. Conversely, the book's assertion that a norming functional is nonzero requires a nontrivial ambient space. The formal statements must handle these cases without silently strengthening the main theorem to closed subspaces or positive distance.
## Formalization scope
All spaces and functionals are real, matching the chapter and avoiding extra complex-scalar conjugation conventions. The ambient object uses Mathlib's `NormedAddCommGroup`, `NormedSpace`, `Submodule`, and `ContinuousLinearMap`; completeness is not assumed because the cited Hahn--Banach consequences do not require it. The distance is exactly `Metric.infDist`, and annihilation is written pointwise rather than by introducing a new annihilator definition. This keeps the capstone self-contained while the double-annihilator milestone states the same construction explicitly as a set.
No claim is made that a best approximant exists. The alignment clause is conditional on an element already satisfying the global minimum property. No closedness assumption may be added to the capstone, since the zero-distance/nonclosed case is part of the source theorem's generality. The norming-functional milestone alone assumes `[Nontrivial X]`; this prevents a vacuous encoding of “nonzero functional” on the zero space. Contributions may establish the four stated theorems and any generally useful lemmas about restrictions, quotient norms, annihilation, or `Metric.infDist`, provided the public statements retain these conventions.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 5, especially §§5.4, 5.7, and 5.8, pp. 111--120. [Public scan](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf).
Vector Space Methods IV: Hahn–Banach and Minimum Norm DualityTextbook
## Motivation
Chapter 5 of Luenberger's *Optimization by Vector Space Methods* (Wiley, 1969) carries the minimum norm theory of Chapter 3 (Mission I of this series) from Hilbert space to arbitrary real normed spaces. The inner product is gone, so orthogonal projection is no longer available; its role is taken over by the **Hahn–Banach theorem**, in two classical forms. The extension form generalizes the projection theorem and yields a duality principle equating a minimum norm problem in a space $X$ with a maximization problem in its dual $X^*$; the geometric form (separating hyperplanes) extends that duality from subspaces to convex sets. These duality theorems are the backbone of the optimization theory in the remainder of the book — conjugate functionals (Ch. 7) and Lagrange duality (Ch. 8) both trace back to them.
## Setting
Throughout, $X$ is a **real normed linear space**. A linear functional $f$ on $X$ is **bounded** if $|f(x)| \le M\|x\|$ for some constant $M$ and all $x$; the least such $M$ is the norm $\|f\|$. The **(normed) dual** $X^*$ is the space of bounded (equivalently, continuous) linear functionals with this norm; $\langle x, x^*\rangle$ denotes $x^*(x)$. A functional $p : X \to \mathbb{R}$ is **sublinear** when $p(x+y) \le p(x) + p(y)$ and $p(\alpha x) = \alpha\, p(x)$ for $\alpha > 0$. Vectors $x \in X$ and $x^* \in X^*$ are **aligned** when $\langle x, x^*\rangle = \|x^*\|\,\|x\|$, and **orthogonal** when $\langle x, x^*\rangle = 0$; for $S \subseteq X$, the complement $S^\perp \subseteq X^*$ consists of the functionals vanishing on $S$, and for $U \subseteq X^*$, ${}^\perp U \subseteq X$ consists of the vectors annihilated by every member of $U$. A **hyperplane** is a maximal proper linear variety; closed hyperplanes are the level sets $\{x : \langle x, x^*\rangle = c\}$ of nonzero bounded functionals. The **support functional** of a convex set $K$ is $h(x^*) = \sup_{k \in K}\, \langle k, x^*\rangle$.
## Formalization targets
The goal is §5.13 Theorem 1 (**Minimum Norm Duality**): if $x_1 \in X$ has distance $d > 0$ from a convex set $K$ with support functional $h$, then
$$d \;=\; \inf_{x \in K} \|x - x_1\| \;=\; \max_{\|x^*\| \le 1}\ \big[\langle x_1, x^*\rangle - h(x^*)\big],$$
the maximum on the right being achieved by some $x_0^*$; and if the infimum is achieved by $x_0 \in K$, then $-x_0^*$ is aligned with $x_0 - x_1$.
The milestones trace the chapter's route there: boundedness $\Leftrightarrow$ continuity (§5.2); the Hahn–Banach theorem in sublinear form (§5.4 Theorem 1) with its norm-preserving extension and norming-functional corollaries; the annihilator identity ${}^\perp(M^\perp) = M$ for closed subspaces (§5.7 Theorem 1); the two subspace duality theorems and the alignment characterization of best approximations (§5.8 — the chapter's principal results); and the geometric form: Mazur's separation theorem, the support theorem, and Eidelheit's separation theorem (§5.12).
## Significance
The §5.8 duality theorems are the exact normed-space analogue of the projection theorem: existence transfers to the dual problem (minimum norm problems should be *formulated in a dual space* to guarantee solutions — the chapter's methodological moral), orthogonality becomes alignment, and infinite-dimensional problems with finitely many constraints reduce to finite-dimensional dual problems. The geometric form underpins all of convex duality.
All results are classical and proved in the source. Mathlib contains the Hahn–Banach extension theorem and point/convex separation theorems, so several milestones are exercises in connecting Luenberger's formulations to existing library lemmas; the two §5.8 duality theorems, the alignment corollary, and the §5.13 convex duality theorem have no direct Mathlib counterpart and are the mission's genuinely new content.
## Difficulty
Degenerate cases are the trap throughout. In §5.8 Corollary 1 the "only if" direction fails literally when $M$ is dense and $x \in M$ (then $M^\perp = \{0\}$ and no nonzero aligned functional exists); the formalization therefore carries the hypothesis $x \notin \overline{M}$. In the separation theorems the strict inequality holds only on the *interior* of the convex set — on the set itself only $\le$ survives — and nonemptiness hypotheses (of the interior, of $K_2$, of the variety) are what make the "nonzero functional" claims true; dropping any of them creates false statements in trivial spaces. In §5.13 the support functional may take the value $+\infty$, so the dual maximum is formalized by two quantified inequalities (the witness achieves $d$; no admissible functional exceeds $d$) rather than by a real-valued supremum. The infimum in the primal problems need not be attained — attainment appears only as a hypothesis in the alignment clauses.
## Formalization scope
Real scalars throughout. The dual space is represented concretely as continuous linear maps `X →L[ℝ] ℝ`, and annihilators are written as explicit quantified conditions rather than named subspaces. Five notions the chapter needs and Mathlib lacks are published as **definitions** and used by the statements rather than inlined: **alignment** ($\langle x, x^*\rangle = \|x^*\|\,\|x\|$), the **support functional** ($h(x^*) = \sup_{k \in K} \langle k, x^*\rangle$, valued in the extended reals since it may be infinite), the **total variation** of a function on an interval, the normalized space **$NBV[a,b]$**, and the **Riemann–Stieltjes integral** (defined relationally, so that no existence claim is built into the definition). The Minkowski functional needed for Mazur's theorem is Mathlib's `gauge`. Minimum distances are infima `⨅` over coerced sets or submodules; in §5.8 Theorem 2 the dual-side supremum is a real `sSup` over $\{\langle x, x^*\rangle : x \in M,\ \|x\| \le 1\}$, which is nonempty and bounded. Sublinearity in §5.4 is hypothesized exactly as in the source (subadditivity plus positive homogeneity plus continuity). Linear varieties are parametrized as $x_0 + M$ with $M$ a `Submodule ℝ X`. No completeness of $X$ is assumed anywhere — the chapter's results are genuinely about normed spaces, and Hahn–Banach needs no completeness. The concrete dual of $C[a,b]$ (§5.5) **is** in scope, and carries most of the mission's new infrastructure: Mathlib has the *property* of bounded variation (`eVariationOn`) but no total-variation norm, no normalized space $NBV[a,b]$, and no Riemann–Stieltjes integral — its `StieltjesFunction` is the different object of a monotone right-continuous function inducing a Borel measure, and its Riesz–Markov–Kakutani development represents positive functionals on $C_c(X)$ by measures, not bounded functionals on $C[a,b]$ by functions of bounded variation. This mission therefore publishes those notions as definitions and states the representation theorem in both directions. §5.3 (the Riesz–Fréchet theorem, i.e. self-duality of Hilbert space) is the one omission: Mathlib's `InnerProductSpace.toDual` already provides it. §5.6 (second dual, reflexivity) is definitional and likewise present in Mathlib.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969. Chapter 5, pp. 103–142. ISBN 0-471-55359-X.
- H. Hahn, *Über lineare Gleichungssysteme in linearen Räumen*, J. Reine Angew. Math. 157 (1927), 214–229; S. Banach, *Sur les fonctionnelles linéaires II*, Studia Math. 1 (1929), 223–239.
- S. Mazur, *Über konvexe Mengen in linearen normierten Räumen*, Studia Math. 4 (1933), 70–84.
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).
## Motivation
The traveling salesman problem — visit $n$ cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The **subtour-elimination relaxation** (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the **integrality gap** of the relaxation: the supremum of $\mathrm{OPT}/\mathrm{LP}$ over metric instances. Explicit instance families push the gap up to $4/3$; the best proven upper bound sits just barely below $3/2$. The **4/3 conjecture** — the gap is exactly $4/3$ — has been the benchmark question of approximation algorithms for four decades.
## Timeline
- **1954.** Dantzig, Fulkerson, and Johnson solve a 49-city instance by hand with the cutting planes that become the subtour-elimination LP.
- **1970–1971.** Held and Karp introduce the 1-tree/Lagrangian bound and show it equals the subtour LP value — since then, "the Held–Karp bound".
- **1976/1978.** Christofides, and independently Serdyukov, give the $3/2$-approximation: minimum spanning tree plus a matching on odd-degree vertices.
- **1980.** Wolsey ([Math. Prog. Study 13](https://doi.org/10.1007/BFb0120913)) shows Christofides' analysis goes through against the LP: $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, so the integrality gap is at most $3/2$. Shmoys and Williamson ([IPL 1990](https://doi.org/10.1016/0020-0190(90)90028-V)) rediscover this via a monotonicity property.
- **1995.** Goemans ([Math. Programming 69](https://doi.org/10.1007/BF01585563)) analyzes the worst-case ratios of TSP relaxations and states the $4/3$ conjecture explicitly; the $4/3$ lower-bound families (three parallel paths) are by then folklore.
- **2011–2014.** For **graph metrics** (shortest-path metrics of unweighted graphs) the barrier breaks: Oveis Gharan–Saberi–Singh and Mömke–Svensson beat $3/2$, and Sebő–Vygen ([Combinatorica 2014](https://arxiv.org/abs/1201.1870)) reach $7/5$ — the conjectured-optimal shape of progress, but only for a special class.
- **2020–2022.** Karlin, Klein, and Oveis Gharan prove a $3/2 - \varepsilon$ approximation for general metric TSP ([STOC 2021](https://arxiv.org/abs/2007.01409)) and then an integrality-gap bound $\gamma \le 3/2 - \varepsilon$ with $\varepsilon > 10^{-36}$ ([FOCS 2022](https://arxiv.org/abs/2105.10043)), via max-entropy sampling of spanning trees and strongly Rayleigh distributions — the first general improvement over Wolsey in forty years, by an astronomically small margin.
- **Today.** The gap between the $4/3$ lower bound and the $3/2 - 10^{-36}$ upper bound is the conjecture. For half-integral LP solutions — where the conjectured extremal instances live — the bound has been pushed to $1.4983$ (Gupta, Lee, Li, Mucha, Newman, and Sarkar, via matroid-based rounding).
## Setting
An **instance** on $n \ge 3$ cities is a cost function $c$ assigning to each ordered pair of cities $u, v$ a real cost $c(u,v)$, required to be a **metric cost**: symmetric ($c(u,v) = c(v,u)$), zero on the diagonal ($c(v,v) = 0$), and satisfying the triangle inequality $c(u,w) \le c(u,v) + c(v,w)$. Nonnegativity follows; distinct cities at distance zero are allowed, as usual for metric TSP.
A **tour** visits every city exactly once and returns to its start. Formally a tour is given by an ordering: a permutation $\pi$ of the cities, traversed as $\pi(0), \pi(1), \dots, \pi(n-1)$ and back to $\pi(0)$; its cost $\mathrm{tourCost}(c, \pi)$ is the sum of the costs of consecutive steps, and $\mathrm{OPT}(c)$ — written `tspOpt c` — is the minimum over all orderings.
The **subtour-elimination (Held–Karp) relaxation** replaces the tour by a fractional edge weight $x(u,v)$ for each pair of cities. A weight vector $x$ is **feasible** (`IsHeldKarp x`) when it is symmetric with zero diagonal, has entries in $[0,1]$, gives every city fractional degree two ($\sum_u x(v,u) = 2$), and crosses every nontrivial cut at least twice: for every set $S$ of cities other than $\emptyset$ and all cities, $\sum_{u \in S} \sum_{v \notin S} x(u,v) \ge 2$. The **Held–Karp bound** `hkValue c` is the infimum of $\frac{1}{2}\sum_u \sum_v c(u,v)\,x(u,v)$ over feasible $x$ (the double sum counts each edge twice, hence the $\frac12$). The incidence vector of any tour is feasible, so $\mathrm{LP} \le \mathrm{OPT}$ always.
## Formalization targets
### Goal — the 4/3 conjecture
$$\mathrm{OPT}(c) \;\le\; \tfrac{4}{3}\,\mathrm{LP}(c) \qquad \text{for every } n \ge 3 \text{ and every metric cost } c.$$
Together with the known lower-bound families this says the integrality gap is exactly $4/3$. The goal carries no algorithm and no constant to improve: it is the terminal statement of the ladder, open in both directions (a proof or a counterexample instance would each settle it).
### Milestones — the known ladder
Five results over the same definitions: the relaxation is valid ($\mathrm{LP} \le \mathrm{OPT}$); instance families force the gap arbitrarily close to $4/3$; tree doubling gives $\mathrm{OPT} \le 2\,\mathrm{LP}$; Wolsey's theorem gives $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, the classical upper bound; and the Karlin–Klein–Oveis Gharan record $\mathrm{OPT} \le (\frac{3}{2} - \varepsilon)\,\mathrm{LP}$ for some $\varepsilon > 10^{-36}$ (FOCS 2022). The last milestone is a statement-level target: its known proof (max-entropy sampling, strongly Rayleigh polynomials) is far beyond current formalization practice, so the mission's usable proving frontier remains Wolsey — the milestone records the state of the art as a formal statement.
## Significance
The 4/3 conjecture is the reference open problem of approximation algorithms: the quality of the subtour LP calibrates every algorithmic advance on TSP, and the conjectured extremal instances guide the search for better rounding schemes. The bound is also what practical solvers actually compute — branch-and-cut on this LP solves instances with tens of thousands of cities — so the conjecture is a statement about the observed tightness of the world's most-used combinatorial lower bound.
Nothing in this circle exists in any proof assistant: Mathlib has no TSP, no LP relaxations, no polyhedral combinatorics of tours. The mission's milestones force the base layer into existence — tours over `Equiv.Perm`, cut constraints over `Finset`, and, for the upper bounds, the parity and tree arguments (spanning trees against the LP, T-joins for the $3/2$ bound) whose infrastructure is reusable for matching theory and network design far beyond TSP.
## Difficulty
The naive plan — round the LP solution to a tour — has no known analysis losing less than $3/2$ in general, and the half-integral extremal instances show the hard cases are structured and simple-looking at once. Christofides' matching argument is provably stuck at $3/2$ against the LP; forty years of work moved the constant by $10^{-36}$, and that advance needed an entirely new probabilistic toolkit. On the other side, no instance family with ratio above $4/3$ has ever been found despite extensive computational search over small instances (Benoit–Boyd and successors). Both directions of the goal are genuinely open territory.
## Formalization scope
The Lean model commits to: cities `Fin n`; costs `c : Fin n → Fin n → ℝ` with `IsMetricCost` (symmetry, zero diagonal, triangle inequality — nonnegativity is derived, and semimetrics are included as in the standard statement of the conjecture); tours as orderings `π : Equiv.Perm (Fin n)` traversed cyclically via `finRotate`, so every permutation denotes a Hamiltonian cycle and every Hamiltonian cycle is denoted; both optimal values as `sInf` over nonempty, bounded-below sets of reals, so they are genuine minima for `n ≥ 3`. The hypothesis `3 ≤ n` is load-bearing: for `n ≤ 2` the degree-2 constraints are infeasible, `sInf ∅ = 0` by convention, and the bounds would be false — every theorem therefore carries it.
Welcome contributions: the milestones in any order — `held_karp_le_opt` is the natural entry point (the tour's incidence vector crosses every cut at least twice); `integrality_gap_lower_bound` needs the three-path instance family and a case analysis on its tours; `tree_doubling_bound` needs spanning trees against the LP; `wolsey_bound` adds the T-join/parity argument and is the summit. Reusable infrastructure — spanning tree polytopes, T-joins, Eulerian traversals, cut lemmas — is welcome as platform theorems. Graph-TSP ($7/5$), path TSP, and asymmetric TSP are deliberately left to future missions; the Karlin–Klein–Oveis Gharan bound is stated as a milestone, but its sampling machinery is expected to arrive, if ever, as shared infrastructure built over many contributions.
## Selected references
- G. Dantzig, R. Fulkerson, S. Johnson, *Solution of a large-scale traveling-salesman problem*, Oper. Res. 2 (1954).
- M. Held, R. Karp, *The traveling-salesman problem and minimum spanning trees*, Oper. Res. 18 (1970); Part II, Math. Programming 1 (1971).
- N. Christofides, *Worst-case analysis of a new heuristic for the travelling salesman problem*, CMU report (1976); A. Serdyukov, Upravlyaemye Sistemy 17 (1978).
- L. Wolsey, *Heuristic analysis, linear programming and branch and bound*, Math. Prog. Study 13 (1980). [doi:10.1007/BFb0120913](https://doi.org/10.1007/BFb0120913)
- D. Shmoys, D. Williamson, *Analyzing the Held-Karp TSP bound: a monotonicity property with application*, Inf. Process. Lett. 35 (1990). [doi:10.1016/0020-0190(90)90028-V](https://doi.org/10.1016/0020-0190(90)90028-V)
- M. Goemans, *Worst-case comparison of valid inequalities for the TSP*, Math. Programming 69 (1995). [doi:10.1007/BF01585563](https://doi.org/10.1007/BF01585563)
- A. Sebő, J. Vygen, *Shorter tours by nicer ears*, Combinatorica 34 (2014). [arXiv:1201.1870](https://arxiv.org/abs/1201.1870)
- A. Karlin, N. Klein, S. Oveis Gharan, *A (slightly) improved approximation algorithm for metric TSP*, STOC 2021. [arXiv:2007.01409](https://arxiv.org/abs/2007.01409)
- A. Karlin, N. Klein, S. Oveis Gharan, *A (slightly) improved bound on the integrality gap of the subtour LP for TSP*, FOCS 2022. [arXiv:2105.10043](https://arxiv.org/abs/2105.10043)
- V. Traub, J. Vygen, *Approximation Algorithms for Traveling Salesman Problems*, Cambridge University Press, 2024. [book page](https://www.or.uni-bonn.de/tspbook/book.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).