Ordinary p-adic L-functions: Mazur–Tate–Teitelbaum interpolationResearch Paper
## Why construct a p-adic L-function?
A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).
The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 ([MTT](https://doi.org/10.1007/BF01388731)); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).
## Modular forms, periods, and measures
Fix a prime $p$, a positive integer $N$, and a weight $k\ge2$. Let $f$ be a normalized cuspidal Hecke eigenform of weight $k$ on $\Gamma_1(N)$ with nebentypus $\epsilon$ and Fourier coefficients $a_n$ (necessarily algebraic). Fix embeddings $\iota_\infty:\overline{\mathbb Q}\hookrightarrow\mathbb C$ and $\iota_p:\overline{\mathbb Q}\hookrightarrow\mathbb C_p$. No condition $p\nmid N$ is imposed. The character $\epsilon$ is extended by zero on nonunits modulo $N$.
The form is **ordinary** when $|\iota_p(a_p)|_p=1$. The **ordinary root** $\alpha$ is the root of
$$X^2-\iota_p(a_p)X+\iota_p(\epsilon(p))p^{k-1}$$
with $|\alpha|_p=1$. This convention also covers the $U_p$ case: if $p\mid N$, then $\epsilon(p)=0$ and the unit root is $\iota_p(a_p)$ ([MTT I.§12](https://doi.org/10.1007/BF01388731)).
A **measure** means a continuous $\mathbb C_p$-linear functional on the continuous functions $C(\mathbb Z_p^\times,\mathbb C_p)$. It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's `AbstractMeasure` on `(PadicInt p)ˣ`.
The two **periods** $\Omega^+$ and $\Omega^-$ normalize the signed modular integrals. Write
$$\Phi_j(r)=2\pi\int_0^\infty f(r+it)(r+it)^j\,dt,$$
and use $(\Phi_j(r)+s(-1)^j\Phi_j(-r))/2$ for sign $s\in\{+1,-1\}$. A period system specifies nonzero periods, algebraic normalized values for $0\le j\le k-2$, and finite generation over $\mathbb Z$ of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in [MTT I.§2](https://doi.org/10.1007/BF01388731); see also the explicit treatment of general eigenforms in [Williams, §11.7](https://warwick.ac.uk/fac/sci/maths/people/staff/cwilliams/lecturenotes/lecture_notes_part_ii.pdf).
## Formalization targets
The goal is to construct an ordinary root, a period system, and a measure $\mu$ with the following interpolation property. Let $\chi$ be a primitive Dirichlet character of conductor $m=p^n$, where $n\ge0$, and let $0\le j\le k-2$. Put $s=\chi(-1)(-1)^j$. With the positive-exponential Gauss sum $\tau(\chi)=\sum_{a\bmod m}\chi(a)e^{2\pi ia/m}$, define the algebraic number $A_{\chi,j}$ by
$$\iota_\infty(A_{\chi,j})=
\frac{m^{j+1}j!}{(-2\pi i)^j\tau(\chi^{-1})\Omega^s}
L(f_{\chi^{-1}},j+1).$$
The required identity is
$$\int_{\mathbb Z_p^\times}\iota_p(\chi(x))x^j\,d\mu(x)
=e_p(\alpha,\chi,j)\,\iota_p(A_{\chi,j}),$$
where all algebraic character values in the following expression are transported by $\iota_p$:
$$e_p(\alpha,\chi,j)=\alpha^{-n}
\left(1-\frac{\iota_p(\chi^{-1}(p)\epsilon(p))p^{k-2-j}}{\alpha}\right)
\left(1-\frac{\iota_p(\chi(p))p^j}{\alpha}\right).$$
This is the scalar period-normalized form of [MTT I.§14](https://doi.org/10.1007/BF01388731). At $n>0$ both character values at $p$ vanish, leaving $\alpha^{-n}$. At $n=0$ the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.
Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.
## What the formalization supplies
The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.
## Where the difficulty lies
Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.
## Formalization scope and conventions
The cusp form is Mathlib's analytic `CuspForm`, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for $f_{\chi^{-1}}$, and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.
The embeddings share the abstract algebraic closure of $\mathbb Q$; there is no asserted continuous map from $\mathbb C$ to $\mathbb C_p$. The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including $2$, are allowed. Natural-number subtractions occur only in theorem contexts with $k\ge2$ and $j\le k-2$.
The signed projections use a factor of $1/2$. Their normalized measures are added, and the period sign is $\chi(-1)(-1)^j$. These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.
## Selected references
- B. Mazur, J. Tate and J. Teitelbaum, *On p-adic analogues of the conjectures of Birch and Swinnerton-Dyer*, Inventiones Mathematicae 84 (1986), 1–48, Chapter I, §§1–4 and 7–14. [DOI](https://doi.org/10.1007/BF01388731); [digitized original](https://gdz.sub.uni-goettingen.de/download/pdf/PPN356556735_0084/LOG_0007.pdf).
- G. Shimura, *On the periods of modular forms*, Mathematische Annalen 229 (1977), 211–221. [DOI](https://doi.org/10.1007/BF01391466).
- C. Williams, *An introduction to p-adic L-functions II: Modular forms*, lecture notes, §§11.6–11.8, particularly Proposition 11.21, for period normalization of general eigenforms. [Author's notes](https://warwick.ac.uk/fac/sci/maths/people/staff/cwilliams/lecturenotes/lecture_notes_part_ii.pdf).
Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper
# Motivation
Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$. Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.
This mission formalizes the paper that started the **probabilistic method** as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$. It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$.
**Timeline.** Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.
# Setting
Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$. A **graph** is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$; here vertices are labeled $0, \dots, N-1$. A subset $s \subseteq V$ of size $k$ is a **clique** if every two distinct vertices of $s$ are adjacent, and an **independent set** if every two distinct vertices of $s$ are non-adjacent. A $k$-set that is either a clique or an independent set is **monochromatic**: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).
The ambient probability space is the uniform distribution over **all** graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$. This space has exactly $2^{\binom{N}{2}}$ elements.
A graph with no monochromatic $k$-set is a graph with neither a $k$-clique nor an independent $k$-set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.
# Formalization targets
### Goal: the probabilistic lower bound
$$R(k) > 2^{k/2}, \qquad k \ge 3$$
i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$-set.
### Stronger: the three steps of the proof, as separate targets
1. **Count estimate.** For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$,
$$\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.$$
2. **Union-bound principle.** In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:
$$\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.$$
3. **Pair-count bound.** Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$-set in $G$ is at most
$$\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.$$
The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.
# Significance
**The result.** The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).
**Formalizing it.** Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$.
# Difficulty
The central difficulty is that the bad events — "the $k$-set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$-sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.
A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$-set ($2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.
# Formalization scope
**Representation.** Graphs are `SimpleGraph (Fin N)`: a relation on $N$ labeled vertices. A candidate set is a `Finset (Fin N)` of cardinality $k$; "monochromatic" is `IsClique ∨ IsIndepSet` on the graph; "no monochromatic $k$-set" is the predicate `NoMonoK`. All counting is cardinality of finite sets; `monoCount N k G` is the number of monochromatic $k$-sets of $G$.
**Conventions.** $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$. The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$, is a natural follow-up contribution).
**Reusability.** The union-bound principle, the monochromatic-$k$-set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining `ramseyNumber` and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.
# Selected references
- Paul Erdős, *Some remarks on the theory of graphs*, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$.
- Noga Alon, Joel H. Spencer, *The Probabilistic Method*, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
- Stanisław Radziszowski, *Small Ramsey Numbers*, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.
## Context: where this sits in the formalization landscape
This mission is **not** a duplicate of existing platform content, and the choice of target is deliberate:
- **Mathlib gap.** The pinned environment (mathlib `0df444a`) contains no Ramsey-number theory at all — nothing in `Combinatorics/SimpleGraph`, no `ramseyNumber`-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
- **Existing Ramsey content is a different quantity.** The platform's fully-proved `Erdos183` mission concerns *multicolour triangle* Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
- **Directly load-bearing for a live open problem.** The public open problem *diagonal_ramsey_asymptotics* (same environment `0df444a`) asks, eventually in $k$, for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$; its upper half is already proved as `ramsey_theory_upper_bound`. The lower half is exactly what this mission's goal supplies: once `ramsey_lower_bound` is proved, closing that open problem reduces to a translation between the graph formulation used here (`SimpleGraph` / `NoMonoK`) and the edge-colouring formulation (`ramseyDiag`) used there, plus the eventual-quantifier wrapper.
- **Formalization convention.** The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$.
## Motivation
Around 1637 Pierre de Fermat wrote, in the margin of his copy of Diophantus' *Arithmetica*, that no $n$-th power with $n > 2$ splits as a sum of two like powers, and that he had a proof the margin was too narrow to hold. The claim resisted every generation of number theorists that attacked it, and the machinery built during those attacks — cyclotomic fields, ideal theory, class numbers, elliptic curves, modular forms, Galois representations — became a large part of modern algebraic number theory. The statement itself is elementary enough to explain to a schoolchild; nothing about its proof is.
**Timeline.** Fermat himself proved the case $n = 4$ by infinite descent, as a corollary of the fact that the area of a right triangle with integer sides is never a perfect square. Euler treated $n = 3$ in his *Vollständige Anleitung zur Algebra* (1770), by a descent in $\mathbb{Z}[\sqrt{-3}]$ that assumed a unique-factorization property later supplied by others. Dirichlet and Legendre settled $n = 5$ between 1825 and 1830, Dirichlet added $n = 14$ in 1832, and Lamé published $n = 7$ in 1839. In 1847 Kummer made the decisive structural step: introducing ideal numbers to repair the failure of unique factorization in $\mathbb{Z}[\zeta_p]$, he proved the theorem for every **regular** prime exponent — those $p$ not dividing the class number of $\mathbb{Q}(\zeta_p)$, a condition he characterized by divisibility of Bernoulli numerators. Irregular primes were left open, and the elementary programme stalled there for over a century.
The route that closed the problem came from a different direction. The **modularity conjecture** of Taniyama (1955), refined by Shimura and given conceptual support by Weil (1967), predicted that every elliptic curve over $\mathbb{Q}$ arises from a modular form. Hellegouarch and then Frey (1985) attached to a hypothetical solution $a^p + b^p = c^p$ the curve $y^2 = x(x - a^p)(x + b^p)$, whose ramification behaviour is too tame for a curve of its conductor. Serre made this precise as the epsilon conjecture, and Ribet proved it in 1986: modularity of semistable elliptic curves over $\mathbb{Q}$ implies Fermat's Last Theorem. Wiles proved that modularity statement, with the key Hecke-algebra input supplied jointly with Taylor, in two 1995 *Annals of Mathematics* papers. Breuil, Conrad, Diamond and Taylor removed the semistability hypothesis in 2001.
## Setting
Fix a natural number $n$ and natural numbers $a, b, c$. A **Fermat triple of exponent $n$** is a triple $(a,b,c)$ of strictly positive naturals with
$$a^n + b^n = c^n.$$
For $n = 1$ such triples are everywhere, and for $n = 2$ they are the Pythagorean triples, parametrized by $(k(u^2-v^2),\, 2kuv,\, k(u^2+v^2))$. The assertion at issue is that from $n = 3$ upward there are none at all: the hypothesis $3 \le n$ and the positivity hypotheses $0 < a$, $0 < b$, $0 < c$ are exactly what is needed, since $n \le 2$ and the degenerate triples with a zero entry both produce solutions.
Two standard reductions organize any attack. First, if $(a,b,c)$ is a triple of exponent $n$ and $m \mid n$, then $(a^{n/m}, b^{n/m}, c^{n/m})$ is a triple of exponent $m$; since every $n \ge 3$ is divisible by $4$ or by an odd prime $p \ge 3$, the general statement follows from the cases $n = 4$ and $n = p$ an odd prime. Second, for a prime exponent $p$ one may assume $\gcd(a,b,c) = 1$, and the classical literature then splits on whether $p \nmid abc$ (case I) or $p \mid abc$ (case II).
## Formalization targets
### Goal
$$\forall\, n \ge 3,\ \forall\, a, b, c \in \mathbb{N}_{>0},\qquad a^n + b^n \ne c^n.$$
This is the mission's single goal, referenced as the published platform theorem `fermat_last_theorem`. It fixes no exponent, no congruence class, and no auxiliary structure: any complete argument, classical or modern, discharges it.
## Significance
*The result itself.* As a Diophantine statement, Fermat's Last Theorem is a closed case; its value now lies in what proving it required. The proof established the modularity of semistable elliptic curves over $\mathbb{Q}$, made modularity lifting ("$R = T$") a standard technique, and turned Galois deformation theory into a working tool. Those consequences — not the non-existence of Fermat triples — are what the surrounding mathematics uses daily; the Fermat statement is the compact certificate that the machinery works.
*Formalizing it.* The theorem is proved but not formally verified end to end, and that gap is the mission. Machine-checked proofs exist for the small exponents and for Kummer's regular-prime case: Mathlib carries the general statement together with the cases $n = 3$ and $n = 4$, and the `flt-regular` project verified the regular-prime theorem in Lean 4. No formal proof of the full theorem exists in any system; Buzzard's ongoing FLT project at Imperial College is building one by reducing the statement to results known to experts by the late 1980s. Contributions here need not follow that route — a complete Lean proof of any single case not yet covered, or of any structural ingredient (level lowering, modularity lifting, the properties of the Frey curve), is a genuine advance, and the platform's sketch mechanism is the natural way to record such a reduction.
## Difficulty
The naive attacks fail for identifiable reasons, and a solver should rule them out before spending time on them. Congruence and descent arguments of the kind that settle $n = 3, 4, 5, 7$ depend on the arithmetic of a specific small ring and do not generalize: the descent step needs unique factorization in $\mathbb{Z}[\zeta_n]$ or a substitute, and unique factorization fails there for all but finitely many $n$. Kummer's ideal-theoretic repair recovers the argument exactly when $p$ is regular, and no argument in that family is known to handle irregular primes; the irregular primes are moreover infinite in number, so no finite computation closes them. Parity, size, and modular-arithmetic obstructions have all been shown insufficient, since the equation has solutions modulo every prime power for suitable triples. The only known complete proof passes through modularity, which means the formal development needs elliptic curves over $\mathbb{Q}$, their Galois representations, modular forms and Hecke algebras, level-lowering, and a modularity lifting theorem — none of which is a shortcut around the difficulty, all of which is where the difficulty actually lives.
## Formalization scope
The target is stated over $\mathbb{N}$, so no truncated subtraction enters the statement and no sign analysis is hidden in it; the equivalent formulations over $\mathbb{Z}$ and over $\mathbb{Q}$ follow by clearing denominators and moving terms, and a solver who prefers to work over $\mathbb{Z}$ must supply that bridge. Exponentiation is `Monoid.npow` on $\mathbb{N}$, and $0^0 = 1$ plays no role because $3 \le n$. The hypotheses $0 < a$, $0 < b$, $0 < c$ are all load-bearing and none of them is vacuous, so the statement admits no trivializing reading: dropping any one makes it false, and every hypothesis is satisfiable, so the conclusion cannot be reached by contradiction from the assumptions alone. Mathlib does not contain Fermat's Last Theorem, so the goal cannot be discharged by citing a library lemma.
A complete development will want: the reduction from general $n$ to $n = 4$ and odd prime exponents; the coprimality normalization; cyclotomic fields, class groups, and the regularity criterion for the Kummer line of attack; and, for the modular route, Weierstrass curves over $\mathbb{Q}$, conductors and minimal models, Galois representations attached to torsion points, modular forms and Hecke operators, and the level-lowering and modularity-lifting statements. Most of that infrastructure is reusable well beyond this mission and is welcome as separate published theorems and definitions. Partial contributions are welcome in either style: a direct proof of a single exponent, or a sketch that reduces the goal to child lemmas with statements that stand on their own.
## Selected references
- Andrew Wiles, *Modular elliptic curves and Fermat's Last Theorem*, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
- Richard Taylor and Andrew Wiles, *Ring-theoretic properties of certain Hecke algebras*, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
- Kenneth A. Ribet, *On modular representations of $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ arising from modular forms*, Inventiones Mathematicae 100 (1990), 431–476. https://doi.org/10.1007/BF01231195
- Christophe Breuil, Brian Conrad, Fred Diamond and Richard Taylor, *On the modularity of elliptic curves over $\mathbb{Q}$: wild 3-adic exercises*, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8
- Ernst Eduard Kummer, *Beweis des Fermat'schen Satzes der Unmöglichkeit von $x^\lambda + y^\lambda = z^\lambda$ für eine unendliche Anzahl Primzahlen $\lambda$*, Monatsberichte der Königlich Preußischen Akademie der Wissenschaften zu Berlin (1847), 132–139.
- Gerhard Frey, *Links between stable elliptic curves and certain Diophantine equations*, Annales Universitatis Saraviensis 1 (1986), 1–40.
- Riccardo Brasca et al., *Fermat's Last Theorem for regular primes* (`flt-regular`), Lean 4 formalization. https://github.com/leanprover-community/flt-regular
- Kevin Buzzard et al., *The Fermat's Last Theorem project*, Lean 4 formalization in progress. https://imperialcollegelondon.github.io/FLT/
Picard groups of semi-local or finite semiringsOpen Problem
# Motivation
Invertible modules over a commutative semiring are Zariski-locally free, so local semirings have trivial Picard group. The source asks whether the ring-theoretic semilocal conclusion survives without subtraction: must every invertible module over a semiring with finitely many maximal ideals be free? If not, is the conclusion at least true for finite semirings?
This mission turns CUHK-Shenzhen AI Math Problem 19, **Picard groups of semi-local or finite semirings**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
The main theorem asserts freeness for every invertible module over a commutative semiring with finite maximal spectrum. A separate milestone states the finite-semiring fallback. Both are positive formulations; a concrete counterexample to either resolves that target negatively and should motivate a corrected classification.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in semirings, Picard groups, invertible modules, finite semirings. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
Ring proofs use subtraction-sensitive k-ideal properties and decompositions into local factors that can fail for semirings. Finite indecomposable semirings need not be local and may have positive Krull dimension. Invertible modules are projective with strong duality, but familiar rank and determinant arguments may not survive additive noncancellation.
## Suggested attack route
Formalize the known local-freeness proof from the evaluation isomorphism and study patching over finitely many principal opens. Identify exactly where partitions of unity require k-ideals. For finite semirings, enumerate idempotent matrices representing projective modules, impose the invertibility constraints, and seek either a reduction to principal rank-one modules or a minimal counterexample. Product decompositions and faithful-action lemmas should be reusable.
## Formalization scope
The Lean targets use Mathlib's commutative semiring, maximal spectrum, module, invertible-module, and free-module notions. 'Semilocal' is encoded only as finiteness of MaximalSpectrum; no unproved decomposition theorem is assumed. The finite fallback assumes the underlying semiring type is finite but does not assume the module itself finite separately. Cardinality-only variants from the source are not the capstone.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
## Milestones
Resolve the finite-semiring statement, computationally or structurally, while developing the local-to-semilocal patching lemmas needed by the main theorem.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on June 24, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original problem](https://rybindmitry.github.io/problems/19.html)
- [Facets of Module Theory over Semirings](https://arxiv.org/abs/2405.18645)
- [MathOverflow discussion](https://mathoverflow.net/questions/511864/picard-group-of-semi-local-or-finite-semirings)
Hatcher Algebraic Topology I: The Fundamental Group of the CircleTextbook
## Motivation
The fundamental group $\pi_1(X, x_0)$ is the first algebraic invariant a student of topology meets, and $\pi_1(S^1)\cong\mathbb{Z}$ is the first computation of it that carries real content. Allen Hatcher's *Algebraic Topology* (Cambridge University Press, 2002; freely available at [pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)) is the standard text on the subject. Its Chapter 1 opens with exactly this computation (Theorem 1.7, p. 29) and immediately draws three classical consequences from it: the Fundamental Theorem of Algebra (Theorem 1.8), the Brouwer fixed point theorem for the disk (Theorem 1.9), and the Borsuk–Ulam theorem for the sphere (Theorem 1.10).
This mission is the opening entry in a series that formalizes Hatcher's book capstone by capstone. It covers the subsection "The Fundamental Group of the Circle" of Section 1.1 (pp. 29–33): the covering-space lifting properties that drive the proof, the theorem itself, and its three applications. Later entries in the series (van Kampen's theorem, the classification of covering spaces, simplicial and singular homology) will build on the declarations introduced here, which all live in the shared Lean namespace `Hatcher`.
## Setting
A **path** in a topological space $X$ is a continuous map $f : I \to X$, where $I = [0,1]$. A **homotopy of paths** is a family $f_t : I \to X$, $0 \le t \le 1$, such that the endpoints $f_t(0) = x_0$ and $f_t(1) = x_1$ are independent of $t$ and the associated map $F : I \times I \to X$, $F(s,t) = f_t(s)$, is continuous. A **loop** at a **basepoint** $x_0$ is a path with $f(0) = f(1) = x_0$. The set of homotopy classes $[f]$ of loops at $x_0$ is the **fundamental group** $\pi_1(X, x_0)$; its product is $[f][g] = [f\cdot g]$, where $f\cdot g$ traverses $f$ and then $g$, each at double speed (Hatcher, Proposition 1.3).
The **circle** $S^1 \subset \mathbb{R}^2$ is realised as the unit circle of $\mathbb{C}$, so the point $(\cos\theta, \sin\theta)$ is $e^{i\theta}$ and the basepoint $(1,0)$ is $1$. Hatcher's map
$$p : \mathbb{R} \to S^1, \qquad p(s) = (\cos 2\pi s, \sin 2\pi s) = e^{2\pi i s}$$
is `Hatcher.circleCover`. The loops
$$\omega_n(s) = (\cos 2\pi n s, \sin 2\pi n s) = p(ns), \qquad n \in \mathbb{Z},$$
based at $(1,0)$ are `Hatcher.omegaLoopN n`, and $\omega = \omega_1$ is `Hatcher.omegaLoop`; its class $[\omega] \in \pi_1(S^1, 1)$ is `Hatcher.omegaClass`.
A **covering space** of $X$ is a space $\tilde X$ together with a map $p : \tilde X \to X$ such that every $x \in X$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets each mapped homeomorphically onto $U$ by $p$ (Hatcher's condition $(\ast)$, p. 29; such a $U$ is **evenly covered**). A **lift** of a map $f : Y \to X$ is a map $\tilde f : Y \to \tilde X$ with $p \circ \tilde f = f$.
## Formalization targets
### Goal (Theorem 1.7)
$\pi_1(S^1, 1)$ is an infinite cyclic group generated by $[\omega]$. In the form stated in Lean:
$$\forall\, g \in \pi_1(S^1, 1)\quad \exists!\, n \in \mathbb{Z}:\quad [\omega]^n = g.$$
Surjectivity of $n \mapsto [\omega]^n$ says $[\omega]$ generates; uniqueness of $n$ says the group is infinite cyclic rather than finite.
### Milestones on the road to the goal
1. $p(s) = e^{2\pi i s}$ is a covering space of $S^1$ (Hatcher, p. 29).
2. Homotopy lifting property (c): for a covering space $p : \tilde X \to X$, a map $F : Y \times I \to X$ and a lift of $F|_{Y \times \{0\}}$ extend uniquely to a lift of $F$ (p. 30).
3. Path lifting property (a): a path $f$ starting at $x_0$ and a point $\tilde x_0 \in p^{-1}(x_0)$ determine a unique lift $\tilde f$ starting at $\tilde x_0$ (p. 29).
4. Lifting homotopies of paths (b): a homotopy of paths $f_t$ starting at $x_0$ lifts uniquely to a homotopy of paths $\tilde f_t$ starting at $\tilde x_0$ (p. 29).
5. Every loop in $S^1$ at $(1,0)$ is homotopic to $\omega_n$ for a unique $n \in \mathbb{Z}$ (the reformulation of Theorem 1.7 that Hatcher actually proves, p. 29).
6. $[\omega]^n = [\omega_n]$ for every $n \in \mathbb{Z}$ (Hatcher's remark after Theorem 1.7, p. 29).
### Applications (Theorems 1.8–1.10)
$$\text{Every nonconstant } f \in \mathbb{C}[z] \text{ has a root in } \mathbb{C}.$$
$$\text{Every continuous } h : D^2 \to D^2 \text{ has a fixed point.}$$
$$\text{Every continuous } f : S^2 \to \mathbb{R}^2 \text{ satisfies } f(x) = f(-x) \text{ for some } x \in S^2.$$
## Significance
*The result itself.* The computation $\pi_1(S^1) \cong \mathbb{Z}$ assigns to every loop in the circle an integer, its winding number, and shows that this integer is the only homotopy invariant of the loop. It is the seed of degree theory, and in Hatcher's text it is the starting point for every later computation of fundamental groups (products, van Kampen, covering spaces). The three applications are the standard demonstration that a single algebraic invariant can settle purely geometric or algebraic existence questions.
*Formalizing it.* Mathlib (revision `0df444a`) already contains the covering-space infrastructure: `IsCoveringMap`, path lifting (`IsCoveringMap.liftPath`, `eq_liftPath_iff'`), homotopy lifting (`IsCoveringMap.liftHomotopy`, `eq_liftHomotopy_iff'`), monodromy, and the fact that `Circle.exp` is a covering map (`Circle.isCoveringMap_exp`). It also has `FundamentalGroup X x` as the endomorphism group of the fundamental groupoid. It does **not** contain the computation $\pi_1(S^1) \cong \mathbb{Z}$, nor the two-dimensional Brouwer and Borsuk–Ulam theorems. The Fundamental Theorem of Algebra is in Mathlib as `Complex.exists_root` (proved by Liouville's theorem rather than by Hatcher's argument); it is kept as a milestone because it is one of the section's stated theorems, and a solver may close it directly from Mathlib. Milestones 2–4 are also within reach of the existing lifting API, but they are the lemmas Hatcher states and uses, and a faithful record of them in the mission's own namespace is what later entries in the series will import.
## Difficulty
The obvious first idea for the goal is to define the winding number of a loop through the complex argument. That fails because $\arg$ is discontinuous on $S^1$; the integer has to be produced by lifting the loop through $p$ and reading off the endpoint of the lift, which is only well defined because of the uniqueness in the path lifting property. The second difficulty is uniqueness of $n$: this needs lifting of homotopies (milestone 4), not just of paths, together with the observation that a lifted homotopy of paths has constant endpoints.
Connecting the concrete loops to Mathlib's abstract $\pi_1$ is its own obstacle. `FundamentalGroup Circle 1` multiplies by composing morphisms of the fundamental groupoid, so identifying $[\omega]^n$ with the class of the explicit loop $\omega_n$ (milestone 6) requires reparametrization arguments for concatenated paths, for negative $n$ as well as positive.
For Theorem 1.9 the difficulty is the construction and continuity of the retraction $r : D^2 \to S^1$ from a fixed-point-free map, and then the non-existence of a retraction, which uses that $\pi_1(S^1) \neq 0$. For Theorem 1.10 Hatcher's proof lifts a loop $g(s) = f(\cos 2\pi s, \sin 2\pi s)/\lvert \cdots \rvert$ through $p$ and shows the lift changes by an odd integer over half a turn; making that parity argument rigorous in Lean is the substance of the milestone.
## Formalization scope
* $S^1$ is `Circle` (the unit circle in $\mathbb{C}$) with basepoint `1`; $D^2$ is `Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1`; $S^2$ is `Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1`, with $-x$ the antipodal point.
* A covering space is Mathlib's `IsCoveringMap p`. This agrees with Hatcher's condition $(\ast)$; neither requires $p$ to be surjective.
* Paths are continuous maps `C(I, X)` or Mathlib `Path`s; for homotopies of paths, the square is written `I × I` with Hatcher's coordinate order $F(s,t) = f_t(s)$: the first coordinate is the path parameter, the second the homotopy parameter. In the general homotopy lifting property the domain is `Y × I` with $Y$ an arbitrary topological space, as in Hatcher.
* $\pi_1(S^1, 1)$ is Mathlib's `FundamentalGroup Circle 1`, and $[\omega]$ is `FundamentalGroup.fromPath ⟦omegaLoop⟧`. Because the goal quantifies over integer powers of a single element, the order of multiplication in `FundamentalGroup` is immaterial to its truth.
* The goal is stated as $\forall g\, \exists! n,\ [\omega]^n = g$ rather than as an abstract isomorphism with $\mathbb{Z}$, so that the generator is pinned to Hatcher's explicit loop; an isomorphism `FundamentalGroup Circle 1 ≃* Multiplicative ℤ` sending $[\omega]$ to $1$ is an immediate corollary and a welcome contribution.
* "Nonconstant polynomial" is `0 < f.degree`, which excludes both the zero polynomial and nonzero constants.
Contributions welcome: proofs of the milestones from Mathlib's lifting API, a degree homomorphism $\pi_1(S^1,1) \to \mathbb{Z}$ packaged for reuse, and any lemma about concatenation and reparametrization of loops in `Circle` that later chapters of the series can import.
## Selected references
- A. Hatcher, *Algebraic Topology*, Cambridge University Press, 2002. Section 1.1, "The Fundamental Group of the Circle", pp. 29–33. [https://pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)
- L. E. J. Brouwer, *Über Abbildung von Mannigfaltigkeiten*, Mathematische Annalen 71 (1911), 97–115. [https://doi.org/10.1007/BF01456931](https://doi.org/10.1007/BF01456931)
- K. Borsuk, *Drei Sätze über die n-dimensionale euklidische Sphäre*, Fundamenta Mathematicae 20 (1933), 177–190. [https://doi.org/10.4064/fm-20-1-177-190](https://doi.org/10.4064/fm-20-1-177-190)
- Mathlib, `Mathlib/Topology/Homotopy/Lifting.lean` (path and homotopy lifting for covering maps). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean)
- Mathlib, `Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean` (the fundamental group). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean)
Transpose symmetry for injectivity over semiringsOpen Problem
# Motivation
For a square matrix A over a commutative semiring, subtraction and determinant arguments are generally unavailable. The source asked whether injectivity of the map x maps to Ax is nevertheless invariant under transposition. The case n=2 was known, with n=3 presented as the first open size.
This mission turns CUHK-Shenzhen AI Math Problem 20, **Transpose symmetry for injectivity over semirings**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
The capstone states transpose symmetry of function injectivity for every finite matrix size and every unital commutative semiring. In the current Prove2Me snapshot both the general theorem and the dimension-two supporting theorem are published and marked Proved. This mission concerns a resolved result, not an open general declaration. The general literature result is due to Gu, Qi and Cheng, [Transpose Symmetry of Injectivity over Commutative Semirings (2026)](https://arxiv.org/abs/2608.16205).
## Significance
The result establishes transpose symmetry without additive inverses or cancellation. The current formal artifacts already record the finite-dimensional statement over arbitrary unital commutative semirings; users should inspect those exact statements and proof records before selecting extensions. The literature status and formal proof status are both resolved for the linked targets.
## Difficulty
Over rings, adjugates, determinants, or duality make transpose symmetry routine. Over semirings, equality of alternating sums cannot be rearranged by subtraction, additive cancellation need not hold, and linear duals do not reflect injectivity. The successful proof must encode parity-separated minors and use injectivity itself to cancel vectors rather than scalars.
## Suggested attack route
This mission is historical and solved in the literature. A Prove2Me solution can reconstruct the paper's proof with independently authored Lean code: isolate the even/odd minor algebra, verify the top separation identity, descend through matrix sizes, and derive coefficient equality. Generalizations to nonunital semirings and the parallel surjectivity theorem are natural follow-up nodes, provided their exact hypotheses match the paper.
## Formalization scope
The capstone quantifies over every unital commutative semiring and every finite square size, using actual function injectivity of Mathlib mulVec, not merely a trivial kernel. The extra sizes zero, one and two do not weaken the original size-at-least-three question. Both linked theorem items are now Proved on Prove2Me. This update does not copy or redistribute any external repository source, and does not change the published Lean statements or proof identities.
## Milestones
The linked dimension-two theorem is Proved. The general goal is also Proved. Any further generalization, such as a nonunital version or a surjectivity statement, would be a separately stated theorem rather than an unfinished part of either existing item.
## Timeline and literature status
The source problem was added July 4, 2026. Sixuan Gu, Wei Qi, and Yaoyu Cheng posted a general proof on August 17, 2026, together with a Lean formalization. The mission records that rapid resolution rather than presenting the theorem as currently unknown.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original problem](https://rybindmitry.github.io/problems/20.html)
- [Resolved 2026 paper](https://arxiv.org/abs/2608.16205)
- [Lean proof repository](https://github.com/wqirocks/transpose-injectivity)
Dynamic Programming and Optimal Control I: The DP AlgorithmTextbook
## Motivation
Dynamic programming is the backbone of stochastic optimal control, operations research, and reinforcement learning. Its cornerstone — that the backward recursion of Bellman computes the optimal cost of a finite-horizon stochastic control problem — is stated as Proposition 1.3.1 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., Athena Scientific, 2005), the standard graduate text on the subject. Every convergence result for value iteration, every performance bound for approximate DP, and every correctness proof for a planning algorithm ultimately leans on this proposition. A machine-checked version of it — over a clean, reusable model of the basic problem — is the natural foundation stone for formalized control theory and RL theory alike.
## Setting
The **basic problem** (§1.2 of the book): a discrete-time system
$$x_{k+1} = f_k(x_k, u_k, w_k), \qquad k = 0, 1, \dots, N-1,$$
with state $x_k \in S$, control $u_k$ constrained to a finite nonempty set $U_k(x_k) \subseteq C$, and disturbance $w_k$ drawn from a finite space $W$ with conditional probabilities $p_k(w \mid x_k, u_k)$. A **policy** is a sequence $\pi = \{\mu_0, \mu_1, \dots\}$ of feedback maps $\mu_k : S \to C$; it is **admissible** if $\mu_k(x) \in U_k(x)$ everywhere. Its expected cost from $x_0$ is
$$J_\pi(x_0) = \mathbb{E}\Big[ g_N(x_N) + \sum_{k=0}^{N-1} g_k(x_k, \mu_k(x_k), w_k) \Big].$$
In the Lean development these are `BertsekasDPModel`, `BertsekasDPPolicyCost` (backward recursion on remaining stages), and the DP recursion `BertsekasDPValue`:
$$J_N = g_N, \qquad J_k(x) = \min_{u \in U_k(x)} \mathbb{E}_w\big[ g_k(x,u,w) + J_{k+1}(f_k(x,u,w)) \big].$$
Section 1.6 of the book develops the **minimax** variant, where the disturbance is chosen antagonistically from a finite membership set $W_k(x,u)$; the mission mirrors it with `BertsekasMinimaxDPModel`, `BertsekasMinimaxPolicyCost`, `BertsekasMinimaxValue`.
## Target
$$J_0(x_0) \;=\; \min_{\pi \text{ admissible}} J_\pi(x_0), \qquad \text{with the minimum attained,}$$
formalized as `BertsekasDP.dp_algorithm_optimality`: the DP value at the horizon is an `IsLeast` of the set of admissible policy costs. Milestones: the min–max interchange Lemma 1.6.1 (`minimax_selection_interchange`) and the minimax DP validity (`minimax_dp_algorithm`).
## Significance
The proposition itself is the license to compute optimal policies stage by stage; downstream, Missions VI and VII of this series (lookahead bounds, infinite-horizon theory) consume exactly this model and recursion. Formalizing it produces the reusable model of the basic problem — the shared vocabulary for the whole series. The result is classical and proved in the book; the contribution here is a machine-checked proof over a model faithful to the book's, with the measurable-selection subtleties deliberately avoided by finiteness (see scope).
## Difficulty
The proof is a backward induction, but the standard informal argument ("interchange expectation and minimization") must be carried out honestly: the induction hypothesis is about all states simultaneously, the minimizing control must be selected as a function of the state (choice over a finite set), and the policy-cost recursion must be related to the value recursion stage by stage. The minimax milestone needs the interchange lemma with its $> -\infty$ proviso — the classic trap is losing that hypothesis and asserting a false unconditioned interchange.
## Formalization scope
Finite disturbance space (`Fintype W`), finite nonempty control-constraint sets (`Finset`, `inf'`), arbitrary (possibly infinite) state space; expectations are finite weighted sums, probabilities are required to be distributions only at admissible controls. Stage data are total functions on $\mathbb{N}$; only stages $0,\dots,N-1$ matter. Policies are deterministic Markov feedback maps — for this class the book's result is exactly recovered. The trivializing risks (empty constraint sets, junk beyond horizon) are ruled out by the nonemptiness field and by evaluating at exactly $N$ remaining stages. Lemma 1.6.1 is stated in the extended reals over arbitrary types with the book's finiteness-of-infimum proviso.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. ISBN 1-886529-26-4. (Prop. 1.3.1, §1.2–1.3, §1.6.) http://www.athenasc.com/dpbook.html
- R. Bellman, *Dynamic Programming*, Princeton University Press, 1957.
## The problem
**(a)** In a tennis match, you are the favorite, and win each point independently with probability $q\in(1/2,1)$. Let $n,m$ be odd positive integers greater than $1$. You have the choice between playing a best-of-$nm$ (i.e., you play $nm$ points and whoever wins the majority of points wins the match), or a best-of-$n$ of best-of-$m$'s (i.e., the match is won by winning the majority of $n$ "sets", and each "set" is won by winning the majority of $m$ points). Prove that your probability of winning the match is strictly greater by playing the best-of-$nm$.
**(b)** We now consider two generalizations: $m_1,\ldots,m_k$ are odd positive integers, while $n$ is any positive integer, with all integers being greater than $1$. You have the choice between playing a best-of-$nm_1\cdots m_k$, or a best-of-$n$ of "sets", which are best-of-$m_1$'s of "games", …, which are best-of-$m_k$'s of "points". In both cases, now that $n$ may be even, it is possible for the players to tie, in which case the match winner is determined by an independent fair coin. Prove again that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.
**(c)** We consider a further generalization where each completed "set" counts toward the match score in an independently random way:
- with probability $a$, the winner gains $1$ in the match score, as usual;
- with probability $b$, the set is ignored and does not count toward the match score;
- with probability $c$, the *loser* gains $1$ in the match score;
with $a+b+c=1$ and $a>c$, so players are still incentivized to win sets (previously we had $a=1$, $b=c=0$). This random scoring rule is applied once per completed set, at the outermost layer only: the games and points inside a set are decided by plain majorities, with no randomness, and only the set's final result is scored. If you choose to play the best-of-$nm_1\cdots m_k$, then each individual point counts as a set and is subject to the same randomness with probabilities $a,b,c$. Prove that your probability of winning the match is still strictly greater by playing the best-of-$nm_1\cdots m_k$ (the fair-coin-on-ties convention continues).
**(d)** Continue from part (c), but change the fair-coin-on-ties convention so that you only win the match if you have a strictly greater match score than your opponent. Assuming $b\ge1/2$, prove that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.
## Source and connection to Dorner–Hardt
Florian E. Dorner and Moritz Hardt, *Don't Label Twice: Quantity Beats Quality when Comparing Binary Classifiers on a Budget*, ICML 2024. [arXiv:2402.02249](https://arxiv.org/abs/2402.02249) (v3, 8 April 2026).
The paper asks how to spend a fixed budget of noisy crowdworker labels when comparing two binary classifiers: one label each for many data points, or several labels per data point aggregated by majority vote. It proves, via Cramér's theorem, that one label each is asymptotically optimal, and states the finite-sample version as an open conjecture (Section 5, Conjecture 1), still open in the April 2026 revision. Its Section 3 displays the finite-sample inequality for the independent, homogeneous-label case and verifies it numerically over about five billion parameter settings.
**Part (d) of this mission with one level of sets is that Section 3 inequality in tennis language.** A point is a single crowdworker label being correct ($q$ is the label accuracy); a set is a data point, whose test label is the majority of its $m$ labels; and the scoring rule is what the two classifiers do with that label. Writing $p$ for the worse classifier's accuracy and $p+\epsilon$ for the better one's, a set is scored to its winner when the better classifier alone matches the test label, ignored when the two classifiers agree, and scored to its loser when the worse classifier alone matches:
$$a=(p+\epsilon)(1-p),\qquad c=p(1-p-\epsilon),\qquad b=1-a-c,$$
so that $a-c=\epsilon>0$, and $b\ge1/2$ always holds because two classifiers of accuracy at least $1/2$ agree on at least half the data. Substituting into the paper's Proposition 1 recovers its gap-indicator probabilities exactly: $\Pr(+1)=q\epsilon+p(1-p-\epsilon)$, $\Pr(-1)=(1-q)\epsilon+p(1-p-\epsilon)$. The paper's inequality also allows $n=1$ and $q=1$, which parts (c)–(d) exclude only because the inequality can fail to be strict at $b=0$ there; for $b\ge1/2$ the same argument covers those edge cases. The paper's Conjecture 1 as literally stated concerns a correlated-error setting (its Section 3.2) and is **not** claimed here.
**Parts (a)–(c) go beyond the paper's setting: arbitrary nesting depth, a fair-coin tie rule, and no constraint on the ignore rate $b$.** The hypothesis $b\ge1/2$ in part (d) cannot be dropped: with one level, $(a,b,c)=(0.9,0.1,0)$, $q=0.6$, $m=3$, $n=1$, the single best-of-3 finishes strictly ahead with probability $0.5832$ while three single points do so with probability $0.5761$.
## Timeline
- **Feb 2024** — arXiv v1; ICML 2024. Asymptotic theorem via Cramér; finite-sample statement conjectured; ~5·10⁹-configuration numerical sweep.
- **Oct 2024** — arXiv v2.
- **Apr 2026** — arXiv v3; conjecture still stated as open.
- **Aug 2026** — private proof of the Section 3 inequality (strict win, $b\ge1/2$, one level) via exponential tilting of the tie probability.
- **Sep 2026** — private proof of the fair-coin version with no constraint on $b$ (Bernstein degree elevation and a hypergeometric parity argument), then of the full four-part statement via a pairing lemma for player-symmetric rules. This mission formalizes that proof.
## Conventions in the formal statement
"Greater than $1$" is read as $n\ge2$ and each $m_i\ge3$ odd; the list of set sizes in (b)–(d) is nonempty. Laws are functions $\mathbb Z\to\mathbb R$ and every probability is a finite sum — no measure theory. The goal theorem is the conjunction of the four parts.
Multiplicative Number Theory I: Siegel–Walfisz and the Three Primes TheoremTextbook
## Primes in progressions, uniformly in the modulus
Applying the circle method to an additive problem about primes requires counting primes
in arithmetic progressions with an error term *uniform in the modulus*: the modulus is
not fixed in advance, it grows with the size of the numbers being represented. The
**Siegel–Walfisz theorem** is the classical statement of that uniformity, valid for every
modulus up to a fixed power of $\log x$, and it is the one analytic ingredient the
standard proof of **Vinogradov's three primes theorem** cannot do without.
The history is a sequence of partial uniformities:
* **1837.** Dirichlet proves that every progression $a \bmod q$ with $(a,q)=1$ contains
infinitely many primes, for each fixed $q$, with no rate
([Dirichlet's theorem](https://en.wikipedia.org/wiki/Dirichlet%27s_theorem_on_arithmetic_progressions)).
* **1896–1899.** De la Vallée Poussin proves the prime number theorem with the error
term $O(x e^{-c\sqrt{\log x}})$, and extends the zero-free region from $\zeta$ to
$L(s,\chi)$, obtaining the prime number theorem in progressions for each *fixed* $q$
([PNT](https://en.wikipedia.org/wiki/Prime_number_theorem)).
* **1918–1935.** Landau and Page isolate the obstruction to uniformity: a single real
zero near $s=1$, attached to a quadratic character. Landau shows at most one of two
distinct real primitive characters can have such a zero; Page shows at most one
modulus below a given bound can, yielding unconditional uniformity for $q$ up to a
bounded power of $\log x$
([Page's theorem](https://encyclopediaofmath.org/wiki/Page_theorem)).
* **1935.** Siegel proves $L(1,\chi) \gg_\varepsilon q^{-\varepsilon}$ for real
primitive $\chi$, at the price of an ineffective constant
([Siegel](https://eudml.org/doc/205054)).
* **1936.** Walfisz combines Siegel's bound with the de la Vallée Poussin machinery and
obtains uniformity for every fixed power $q \le (\log x)^A$
([Walfisz](https://doi.org/10.1007/BF01218882)).
* **1937.** Vinogradov proves that every sufficiently large odd integer is a sum of
three primes ([Vinogradov's theorem](https://en.wikipedia.org/wiki/Vinogradov%27s_theorem)).
* **2013.** Helfgott removes the "sufficiently large", settling ternary Goldbach for all
odd $n > 5$ ([arXiv:1312.7748](https://arxiv.org/abs/1312.7748)).
## Setting
The **von Mangoldt function** $\Lambda(n)$ equals $\log p$ if $n = p^m$ is a prime power
and $0$ otherwise. The **Chebyshev function** $\psi(x) = \sum_{n \le x} \Lambda(n)$
counts primes with weights; the prime number theorem is the assertion $\psi(x) \sim x$.
A **Dirichlet character** modulo $q$ is a multiplicative function
$\chi : \mathbb{Z}/q\mathbb{Z} \to \mathbb{C}$, supported on the units and taking root-of-unity
values there. The **principal character** $\chi = 1$ is the indicator of the units; a
character is **quadratic** (real) if $\chi^2 = 1$ and $\chi \neq 1$, and **primitive** if
it is not induced by a character of a proper divisor of $q$. The **Dirichlet
$L$-function** $L(s,\chi) = \sum_{n\ge 1}\chi(n)n^{-s}$, defined for
$\operatorname{Re} s > 1$, extends meromorphically to $\mathbb{C}$, entire except for a
simple pole at $s = 1$ when $\chi$ is principal.
The two counting functions of the mission are the **twisted von Mangoldt sum** and the
**progression sum**
$$\psi(N,\chi) = \sum_{n < N} \Lambda(n)\chi(n), \qquad
\psi(N;q,a) = \sum_{\substack{n < N \\ n \equiv a\ (q)}} \Lambda(n),$$
related by finite character orthogonality. Write $\delta_\chi = 1$ for $\chi$ principal
and $\delta_\chi = 0$ otherwise. A zero $\beta \in (0,1)$ of $L(s,\chi)$ lying inside the
classical zero-free region is an **exceptional zero** (a Siegel zero); the set of such
zeros for a given $\chi$ is the **exceptional set** $E$, which the results below
constrain to have at most one element.
## Formalization targets
The attack path follows Davenport, *Multiplicative Number Theory*, 3rd ed., §§14, 18,
20, 21, 22.
**(1) `zero_free_region` (§14, pp. 88–96).** There is an absolute $c>0$ such that for
every $q \ge 1$ and every $\chi \bmod q$,
$$L(s,\chi) \neq 0 \quad\text{for } s \neq 1,\ \operatorname{Re} s \ \ge\ 1 -
\frac{c}{\log\big(q(|\operatorname{Im} s| + 2)\big)},$$
with at most one exception, which is real, lies in $(0,1)$, is a simple zero, and can
occur only for quadratic non-principal $\chi$.
**(2) `pnt_dlvp` (§18, pp. 111–114).** For some $c > 0$ and all $x \ge 2$,
$$\psi(x) = x + O\!\left(x\,e^{-c\sqrt{\log x}}\right).$$
**(3) `psi_char_of_region` (§20, pp. 121–125).** For a region constant $c>0$ there are
$c_1, c_2 > 0$ such that, whenever $E$ is an exceptional set for $\chi \bmod q$ with
respect to $c$ and $q \le \exp(c_2\sqrt{\log N})$,
$$\psi(N,\chi) = \delta_\chi N - \sum_{\beta \in E} \frac{N^\beta}{\beta}
+ O\!\left(N e^{-c_1\sqrt{\log N}}\right).$$
**(4) `siegel` (§21, pp. 126–131).** For every $\varepsilon > 0$ there is
$C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,
$$L(1,\chi) > C(\varepsilon)\, q^{-\varepsilon}.$$
**(5) `siegel_zero` (§21, second form).** For every $\varepsilon > 0$ there is
$C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,
$$L(\sigma,\chi) \neq 0 \quad \text{for all real } \sigma > 1 - C(\varepsilon)q^{-\varepsilon}.$$
**(6) `siegelWalfisz` (§22, pp. 132–134).** For every $A > 0$ there are $C, c > 0$ such
that for all $q \ge 1$, all $\chi \bmod q$, and all $N \ge 2$ with $q \le (\log N)^A$,
$$\big\lVert \psi(N,\chi) - \delta_\chi N \big\rVert \le C N e^{-c\sqrt{\log N}}.$$
This is literally the platform proposition `ThreePrimes.SiegelWalfisz`.
A corollary, not a milestone, records the progression form `siegel_walfisz_ap`: for
$(a,q)=1$ and $q \le (\log N)^A$,
$$\psi(N;q,a) = \frac{N}{\varphi(q)} + O_A\!\left(N e^{-c\sqrt{\log N}}\right).$$
**Goal (`three_primes`, §26).** There is $N_0$ such that every odd $n \ge N_0$ is a sum
of three primes. It follows from milestone (6) by the existing platform theorem
deducing `ThreePrimes.ThreePrimesExistence` from `ThreePrimes.SiegelWalfisz`. The goal
leaves $N_0$ unspecified rather than hard-coding a numeric threshold, so it is not
invalidated by later improvements to that threshold.
## What the result gives, and what remains to be formalized
Siegel–Walfisz is the standard uniform input downstream of which sit the circle method
for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without
it, the three primes theorem's major-arc analysis has no main term.
Platform status is the reason this mission exists. A complete, machine-checked
formalization of the three primes theorem already exists in the namespace `ThreePrimes`
(by user `tabbott`), following Vaughan, *The Hardy–Littlewood Method*, Ch. 3, and
Davenport §26. It is **conditional**: it takes Siegel–Walfisz as an explicit hypothesis
`ThreePrimes.SiegelWalfisz`. Discharging that hypothesis makes the three primes theorem
unconditional, and is the whole content of this mission.
Mathlib contains the analytic continuation of $L(s,\chi)$
([`DirichletCharacter.LFunction`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LSeries/DirichletContinuation.html)),
its functional equation, the non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$,
Dirichlet's theorem, and the Chebyshev function. It does **not** contain the zero-free
region for $L(s,\chi)$, the explicit formula for $\psi(x,\chi)$, Siegel's theorem, or
Siegel–Walfisz. The platform additionally hosts the
[PNT+ project](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) contour
machinery for $\zeta$ — Borel–Carathéodory, the $3 + 4\cos\theta + \cos 2\theta$
inequality, a zero-free rectangle, and `MediumPNT`,
$\psi(x) = x + O(x\exp(-c(\log x)^{1/10}))$. That is a template for the $L(s,\chi)$
analogues, not a proof of them, and its error term is weaker than the de la Vallée
Poussin form milestone (2) asks for.
## Where the obvious argument fails
The first idea is to run the $\zeta$ argument character by character. It works for
complex $\chi$ and breaks for real ones. The positivity device that pushes zeros off
$\operatorname{Re} s = 1$ compares $\chi$, $\chi^2$ and the trivial character at nearby
points; when $\chi$ is quadratic, $\chi^2$ is principal and contributes the pole of
$L(s,\chi_0)$ at $s = 1$ at exactly the height where the putative zero sits, so the
inequality degrades from "no zeros" to "at most one zero" and stops there. Every later
step inherits that unexcluded zero: milestone (3) can only be stated with the
$N^\beta/\beta$ term present, and milestone (6) is exactly the assertion that for
$q \le (\log N)^A$ this term is small — which Siegel's ineffective bound supplies and
nothing effective is known to.
A second shortcut, deducing uniformity from Mathlib's non-vanishing of $L(s,\chi)$ on
$\operatorname{Re} s \ge 1$ together with Dirichlet's theorem, also fails: those results
are qualitative, carry no rate, and are not uniform in $q$.
## Formalization scope
Sums run over $n < N$ with $N \in \mathbb{N}$, matching `Vino.vmSumChar` and
`ThreePrimes.SiegelWalfisz`; Davenport sums over $n \le x$. The two differ by the single
term $\Lambda(N) \le \log N$, negligible against every error term above. Milestone (2)
alone uses a real argument, via Mathlib's `Chebyshev.psi`. $L(s,\chi)$ is Mathlib's
`DirichletCharacter.LFunction`, so no continuation is reconstructed.
The zero-free region is `Davenport.InRegion c q s`, namely
$\operatorname{Re} s \ge 1 - c/\log(q(|\operatorname{Im} s| + 2))$; the exceptional zero
is packaged as `IsExceptionalSet c χ E`: $E$ is a subsingleton, every element is a real
zero of $L(\cdot,\chi)$ in $(0,1)$ and can exist only for quadratic non-principal $\chi$,
and $L(s,\chi) \neq 0$ at every $s \neq 1$ of the region outside $E$. Milestone (1) adds
simplicity as $L'(\beta,\chi) \neq 0$ for $\beta \in E$.
Milestone (3) takes the region constant $c > 0$ as a *parameter* rather than importing it
from milestone (1), so the milestones can be attempted in any order. For large $c$ the
hypothesis `IsExceptionalSet c χ E` may be unsatisfiable for some $\chi$, making the
statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing
reading: milestone (1) produces a definite small $c > 0$ with a witness $E$ for *every*
$\chi$, so instantiating milestone (3) at that $c$ discharges the hypothesis rather than
voiding it.
Siegel's theorem is stated for `χ.IsQuadratic`, `χ ≠ 1`, `χ.IsPrimitive` characters, with
the conclusion a lower bound on $\operatorname{Re} L(1,\chi)$; since $L(1,\chi)$ is real
for real $\chi$, this is the value itself, not a weakening. The constants in milestones
(4), (5) and (6) are **ineffective**; the statements are plain existentials, so
ineffectivity is invisible to Lean, but no numeric constant can be extracted from
anything downstream of them.
The principal character is included in the character-form statements, with main term $N$
(`if χ = 1 then (N : ℂ) else 0`); milestones (3) and (6) therefore contain the prime
number theorem itself and cannot be proved by restricting to non-principal $\chi$.
Milestone (6) requires $c > 0$ strictly, which is what makes $Ne^{-c\sqrt{\log N}}$ a
genuine saving over the trivial $\psi(N,\chi) \ll N$; with $c = 0$ allowed it would be
empty.
Beyond the six milestones, a complete development needs Hadamard factorization for
$L(s,\chi)$ as an entire function of order $1$, the zero-counting estimate $N(T,\chi)$
(§16, pp. 101–103), the truncated explicit formula for $\psi(x,\chi)$ (§19, pp. 115–120),
Perron-type contour truncation, and the imprimitive-to-primitive reduction
$|\psi(N,\chi) - \psi(N,\chi^{*})| \ll (\log q)(\log N)$. All of it is reusable well
beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's
theorem, and effective Chebotarev. Contributions of these supporting results, of
alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the
$\pi(x;q,a)$ versions, and of sharper constants are welcome.
## Selected references
- H. Davenport, *Multiplicative Number Theory*, 3rd ed., revised by H. L. Montgomery,
GTM 74, Springer, 2000. §§14, 18, 20, 21, 22, 26.
[doi:10.1007/978-1-4757-5927-3](https://doi.org/10.1007/978-1-4757-5927-3)
- H. L. Montgomery and R. C. Vaughan, *Multiplicative Number Theory I: Classical
Theory*, Cambridge University Press, 2007. Ch. 11–12 (Theorems 11.3, 11.14, 11.16,
12.10; Corollaries 11.10, 11.12, 11.17, 11.19).
[doi:10.1017/CBO9780511618314](https://doi.org/10.1017/CBO9780511618314)
- R. C. Vaughan, *The Hardy–Littlewood Method*, 2nd ed., Cambridge University Press,
1997. Ch. 3. [doi:10.1017/CBO9780511470929](https://doi.org/10.1017/CBO9780511470929)
- C. L. Siegel, *Über die Classenzahl quadratischer Zahlkörper*, Acta Arithmetica 1
(1935), 83–86. [eudml:205054](https://eudml.org/doc/205054)
- A. Walfisz, *Zur additiven Zahlentheorie II*, Mathematische Zeitschrift 40 (1936),
592–607. [doi:10.1007/BF01218882](https://doi.org/10.1007/BF01218882)
- I. M. Vinogradov, *Representation of an odd number as a sum of three primes*, Doklady
Akad. Nauk SSSR 15 (1937), 291–294.
[Vinogradov's theorem](https://en.wikipedia.org/wiki/Vinogradov%27s_theorem)
- H. A. Helfgott, *The ternary Goldbach conjecture is true*, 2013.
[arXiv:1312.7748](https://arxiv.org/abs/1312.7748)
- *Siegel–Walfisz theorem*, Wikipedia.
[link](https://en.wikipedia.org/wiki/Siegel%E2%80%93Walfisz_theorem)
- *Page theorem*, Encyclopedia of Mathematics.
[link](https://encyclopediaofmath.org/wiki/Page_theorem)
- A. Kontorovich et al., *PrimeNumberTheoremAnd* (PNT+), Lean formalization project.
[github](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd)
- Mathlib, `Mathlib.NumberTheory.LSeries.DirichletContinuation`.
[docs](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LSeries/DirichletContinuation.html)
The Hardy-Littlewood Method I: Weyl's InequalityTextbook
## Motivation
The Hardy--Littlewood circle method is the principal analytic tool for counting solutions to additive equations in integers. Introduced by Hardy and Ramanujan for the partition function and developed by Hardy and Littlewood in their *Partitio Numerorum* series (1920--1928), it produces asymptotic formulae for the number of representations of a large integer $n$ as a sum of $s$ terms drawn from a prescribed set — $k$-th powers, primes, values of a polynomial.
Its engine is an estimate for **exponential sums**. If a sum $\sum_{x<N} e(\alpha x^k)$, where $e(\theta)=\exp(2\pi i\theta)$, exhibits cancellation for every $\alpha$ not well approximable by a rational with small denominator, the method delivers an asymptotic formula; if it does not, the method stalls. Weyl's inequality (Weyl 1916) was the first such estimate and remains the standard one for moderate $k$.
A short timeline of the estimate this mission targets. Weyl (1916) proved the inequality below with the exponent $2^{1-k}$, in the course of his work on uniform distribution. Hardy and Littlewood (1920--1928) built the circle method on it, obtaining $G(k)\le (k-2)2^{k-1}+5$ for Waring's problem. Vinogradov (1935) replaced Weyl differencing by his mean value theorem, superior for large $k$, reducing the bound to $O(k\log k)$; Wooley's efficient congruencing (2012) and the Bourgain--Demeter--Guth decoupling theorem (2016) settled the main conjecture of Vinogradov's mean value theorem. For small $k$ — and as the entry point to the subject — Weyl's inequality is still the right tool, and it is the natural first capstone for a formalization of the method.
## Setting
For a real number $\theta$ write
$$e(\theta) \;=\; \exp(2\pi i \theta),$$
the standard additive character of $\mathbb{R}/\mathbb{Z}$: it satisfies $e(x+y)=e(x)e(y)$, $|e(x)|=1$, and $e(x)=1$ exactly when $x\in\mathbb{Z}$.
For a real number $\theta$ write $\|\theta\|$ for the distance from $\theta$ to the nearest integer. It is periodic with period $1$, vanishes exactly on $\mathbb{Z}$, satisfies the triangle inequality, and is at most $\tfrac12$.
Given a finite set $A\subseteq\mathbb{Z}$, its generating function is $f_A(\theta)=\sum_{a\in A}e(a\theta)$. The basic identity of the subject is
$$\int_0^1 f_A(\theta)^s\,e(-n\theta)\,d\theta \;=\; \#\{(a_1,\dots,a_s)\in A^s : a_1+\cdots+a_s=n\},$$
a consequence of the orthogonality relation $\int_0^1 e(m\theta)\,d\theta=[\,m=0\,]$.
A **Weyl sum** of degree $k$ is $\sum_{0\le x<N} e(\alpha x^k)$. The whole difficulty is to bound it for $\alpha$ in the *minor arcs* — those $\alpha$ admitting no rational approximation $a/q$ with $q$ small.
## Target
Fix $k\ge 2$. For every $\varepsilon>0$ there is a constant $C=C(k,\varepsilon)$ such that whenever $(a,q)=1$, $q\ge 1$, and $\left|\alpha-\frac{a}{q}\right|\le \frac{1}{q^2}$,
$$\left|\sum_{0\le x<N} e(\alpha x^{k})\right| \;\le\; C\,N^{1+\varepsilon}\left(\frac{1}{q}+\frac{1}{N}+\frac{q}{N^{k}}\right)^{2^{1-k}}.$$
The intermediate targets, weakest first, are the milestone list: the counting identity, the Weyl differencing (squaring) step, the Farey covering with coprime numerator, the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, Hua's fourth-moment inequality for $k=2$, and the degree-two case of the inequality itself.
## Significance
*The result itself.* Weyl's inequality is what makes the minor arcs negligible. Applied with $q$ in the range $N^{\delta}\le q\le N^{k-\delta}$ it gives a power saving over the trivial bound $N$, and integrating that saving over the minor arcs shows their contribution is smaller than the main term produced by the major arcs. Every classical application of the circle method — the asymptotic formula in Waring's problem, Vinogradov's three primes theorem, the Birch--Davenport theory of forms in many variables — passes through an estimate of this shape. Without it the method produces an identity, not a theorem.
*Formalizing it.* Mathlib currently contains the analytic prerequisites — Fourier characters on `AddCircle`, Dirichlet's approximation theorem, Abel summation, Gauss sums — but no circle-method apparatus whatsoever: no Weyl sums, no arc dissection, no singular series, no mean value estimates. This mission supplies the first layer. The foundational tier is already machine-checked: **53 theorems** covering the character $e$, the norm $\|\cdot\|$, the geometric sum bound $\left|\sum_{x<N}e(x\theta)\right|\le\min\!\left(N,\frac{1}{2\|\theta\|}\right)$, both orthogonality relations, both forms of Dirichlet's theorem, and the basic theory of $f_A$, are published on the platform with verified proofs and may be imported freely. What remains open is the combinatorial and analytic core listed in the milestones. None of the milestone statements is currently formalized anywhere, to the best of our knowledge.
## Difficulty
The obvious approach fails immediately. One would like to sum $\left|\sum_{x<N}e(\alpha x^k)\right|$ by comparing it to the linear case, where the geometric series gives $\min(N,\frac{1}{2\|\alpha\|})$ outright. But for $k\ge2$ the summand is not a geometric progression and there is no closed form.
Weyl's device is to square and difference: $\left|\sum_x e(\phi(x))\right|^2=\sum_{x,y}e(\phi(x)-\phi(y))$, and the substitution $y=x+h$ turns the inner polynomial into one of degree $k-1$ in $x$. Iterating $k-1$ times reduces to a linear sum, at the cost of raising the estimate to the power $2^{1-k}$ — which is why the saving is so weak for large $k$, and why Vinogradov's method eventually supersedes it.
The genuine obstacles in a formalization are: (i) bookkeeping the shifted ranges produced by each differencing step, which are not $[0,N)$ and must be handled uniformly; (ii) the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, needed to count the $h$ for which the resulting linear coefficient is close to an integer, and which is not currently in Mathlib in this form; (iii) tracking the $\varepsilon$-dependent constants through $k-1$ iterations without the informal $\ll$ notation.
## Formalization scope
Statements are given over the Prove2Me default environment (Lean `v4.30.0`, Mathlib `c5ea003`), in the shared namespace `CircleMethod`, and build on two published definitions: `CircleMethod_char` (the character `e` and the norm `nrm`) and `CircleMethod_genfun` (the generating function `f`).
Conventions this mission commits to:
- $\|\theta\|$ is `nrm θ = |θ - round θ|`. Mathlib's `round` breaks ties upwards, so `round` is *not* an odd function; the characterisation to use is minimality, `nrm θ ≤ |θ - n|` for every integer `n`, which is published as `CircleMethod.nrm_le`.
- Sums run over `Finset.range N`, that is $0\le x<N$, and $N$ is a natural number. Hypotheses `0 < N` and `0 < q` are stated explicitly rather than left implicit.
- Asymptotic notation is eliminated in favour of explicit existential constants: $X\ll_\varepsilon Y$ is rendered as `∀ ε > 0, ∃ C > 0, ∀ …, X ≤ C * Y`, with the constant quantified *outside* the parameters it may depend on and *inside* nothing else. Solvers should not weaken this by allowing $C$ to depend on $N$, $q$ or $\alpha$.
- Exponents such as $N^{1+\varepsilon}$ and $2^{1-k}$ are real powers (`Real.rpow`), not natural powers.
- Coprimality is `Nat.Coprime a.natAbs q`, which is the correct notion for a possibly negative numerator.
One trivialising formalization to rule out: the goal must not be read with $C$ permitted to depend on $N$, since then $C=N$ makes it vacuous. The quantifier order in the Lean statement already forbids this, and solvers should preserve it exactly.
Contributions welcome on any milestone independently; the divisor bound and the Farey covering are self-contained and need no other milestone. Both are reusable well beyond this mission.
## Selected references
- H. Weyl, *Über die Gleichverteilung von Zahlen mod. Eins*, Mathematische Annalen 77 (1916), 313--352. [DOI:10.1007/BF01475864](https://doi.org/10.1007/BF01475864)
- G. H. Hardy and J. E. Littlewood, *Some problems of 'Partitio Numerorum' I--VI*, 1920--1928.
- R. C. Vaughan, *The Hardy--Littlewood Method*, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997. (Weyl's inequality is Lemma 2.4; the geometric sum bound is Lemma 2.1.)
- I. M. Vinogradov, *New estimates for Weyl sums*, Doklady Akademii Nauk SSSR 8 (1935), 195--198.
- T. D. Wooley, *Vinogradov's mean value theorem via efficient congruencing*, Annals of Mathematics 175 (2012), 1575--1627. [DOI:10.4007/annals.2012.175.3.12](https://doi.org/10.4007/annals.2012.175.3.12)
- J. Bourgain, C. Demeter and L. Guth, *Proof of the main conjecture in Vinogradov's mean value theorem for degrees higher than three*, Annals of Mathematics 184 (2016), 633--682. [DOI:10.4007/annals.2016.184.2.7](https://doi.org/10.4007/annals.2016.184.2.7)
Markov Entanglement: Index Policies for Restless Bandits are Asymptotically SeparableResearch Paper
Restless multi-armed bandits are the standard model for allocating a scarce resource across many independently-evolving agents: N arms, each a small Markov chain, and a budget that lets you activate only a fixed fraction of them at each step. The joint problem is PSPACE-hard, so practice runs on *index policies* — score each arm by a priority index computed from its own local state, then activate the top ones until the budget runs out — and evaluates them by *value decomposition*: approximate the joint Q-function by a sum of per-arm local Q-functions, each computed from a single arm's chain. The decomposition is used everywhere from Whittle-index heuristics to modern multi-agent RL, and it is used without an error bound.
Chen and Peng (arXiv:2506.02385) supply one. Their companion mission established the general principle: the value decomposition error of a multi-agent chain is controlled by its *measure of Markov entanglement*, the distance from the chain's transition matrix to the nearest separable one. This mission carries that principle to the restless-bandit setting and proves that index policies are asymptotically separable — their entanglement decays like 1/sqrt(N), so the decomposition error is sublinear in N while the joint Q-function itself is of order N. The relative error vanishes as the system grows, which is exactly why the practice works.
The argument runs through the mean-field limit. Because the arms are homogeneous, the only thing that matters about a joint state is its *configuration*: the fraction of arms in each local state. Under an index policy the configuration evolves by a map that does not depend on N at all, and under two standard technical conditions — a uniform global attractor property and non-degeneracy — that map has a unique attracting fixed point m*. The chain of reasoning is: policy entanglement is bounded by how far the realised policy sits from the mean-field limiting policy (Proposition 1); that distance is bounded by the configuration's deviation from m* (Lemma 2/8); and the deviation concentrates at rate 1/sqrt(N) by a concentration-plus-local-stability argument adapted from Gast, Gaujal and Yan. The concentration and stability inputs (Lemmas 9, 10, 11) are results of Gast et al. and are formalized here as well, so the mission stands on its own.
The mission also formalizes the mean-field map on the whole simplex and checks it against the N-agent characterisation, which is what makes the piecewise-affine and stability analysis expressible at all.
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)
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).