Motivation

The Fourier series of a periodic function decomposes it into sinusoidal components, but the partial sums of that series need not converge to the function even when the function is continuous: du Bois-Reymond exhibited in 1873 a continuous $2\pi$-periodic function whose Fourier partial sums diverge at a point. Fejér's 1904 theorem repairs this failure by replacing the partial sums with their Cesàro (arithmetic) averages: for every continuous periodic function, these averages converge to the function, uniformly, with no smoothness hypothesis beyond continuity. This was the first universally valid summation method for Fourier series, and its underlying technique — averaging against a kernel whose mass concentrates at the origin — became the template for what is now called a good kernel or approximate identity, the basic device used throughout harmonic analysis (heat-kernel smoothing, Poisson summation, Fourier-inversion arguments) [Stein & Shakarchi, 2003].

Timeline.

• 1873 — du Bois-Reymond constructs a continuous $2\pi$-periodic function whose Fourier series diverges at a point, showing continuity alone cannot guarantee convergence of the partial sums themselves.
• 1904 — Fejér proves that the Cesàro means of the Fourier series of any continuous periodic function converge to it uniformly (Fejér, 1904).
• The good-kernel method Fejér introduced was later systematized as the general framework for approximate identities in harmonic analysis (Stein & Shakarchi, 2003, Ch. 2, §5).

Setting

Let $f : \mathbb{R} \to \mathbb{C}$ be continuous and $2\pi$-periodic, i.e. $f(x + 2\pi) = f(x)$ for every $x \in \mathbb{R}$. Its $n$-th Fourier coefficient, for $n \in \mathbb{Z}$, is

$$\hat f(n) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta)\, e^{-in\theta}\, d\theta.$$

Its $N$-th partial sum is $S_N(f)(\theta) = \sum_{n=-N}^{N} \hat f(n)\, e^{in\theta}$, and its $N$-th Cesàro (Fejér) mean is the arithmetic average of the first $N+1$ partial sums,

$$\sigma_N(f)(\theta) = \frac{1}{N+1}\sum_{k=0}^{N} S_k(f)(\theta).$$

Formalization targets

Fejér's theorem

$$\sigma_N(f) \longrightarrow f \quad \text{uniformly on } \mathbb{R} \text{ as } N \to \infty.$$

This is the full 1904 statement: no restriction to pointwise convergence, and no extra regularity assumed on $f$ beyond continuity.

Significance

The result itself. Fejér's theorem gives the first universally valid summation method for the Fourier series of a continuous function, closing the gap left open by pointwise convergence tests that need extra regularity. It also yields, essentially for free, a proof of the Weierstrass approximation theorem on the circle — the trigonometric polynomials $\sigma_N(f)$ are dense in the continuous $2\pi$-periodic functions under the uniform norm — and it is the historical prototype of the good-kernel/approximate-identity method underlying Poisson summation, heat-kernel smoothing, and $L^1$ Fourier-inversion arguments.

Formalizing it. Mathlib currently has no infrastructure for this at all. Mathlib.Analysis.Fourier.AddCircle defines Fourier coefficients on the circle and proves $L^2$ convergence (Parseval's identity, via the orthonormal Fourier basis), but it has no notion of a partial sum, no Dirichlet or Fejér kernel, and no pointwise or uniform convergence result for Fourier series of any kind. This mission builds that classical convergence theory — the Fejér kernel, its closed form and positivity, the good-kernel estimates, and the uniform convergence theorem itself — from first principles.

Difficulty

The obvious first attempt is to bound $|\sigma_N(f)(\theta) - f(\theta)|$ termwise from the individual Fourier coefficients. This fails outright: a continuous function's Fourier coefficients need not be absolutely summable, which is exactly the mechanism behind du Bois-Reymond's divergence example. The real difficulty is representing $\sigma_N(f)$ as a convolution,

$$\sigma_N(f)(\theta) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta - \varphi)\, F_N(\varphi)\, d\varphi,$$

against the Fejér kernel $F_N$, and then proving $F_N$ is a good kernel: nonnegative, integrating to $1$ over one period, and — the genuinely quantitative step — with its mass outside any fixed neighborhood of $0$ vanishing as $N \to \infty$. That last estimate needs the closed form

$$F_N(\theta) = \frac{1}{N+1}\left(\frac{\sin((N+1)\theta/2)}{\sin(\theta/2)}\right)^2,$$

which carries a removable singularity at $\theta = 0$ that must be handled carefully, together with a genuine decay estimate — via a lower bound on $|\sin(\theta/2)|$ — valid uniformly outside any fixed $\delta$-neighborhood of the origin.

Formalization scope

$f$ is complex-valued, and only continuity together with exact $2\pi$-periodicity is assumed — no differentiability, no bounded variation, no realness. Uniform convergence is stated with Mathlib's TendstoUniformly. The period is fixed at $2\pi$, matching the classical circle-group convention, rather than a general $T > 0$; the $T$-periodic statement is a routine rescaling of this one and is not separately targeted here. One route to a trivializing formalization is worth ruling out explicitly: assuming any extra regularity on $f$ (differentiability, bounded variation, Lipschitz continuity) would let the uniform-convergence conclusion follow from the much easier Dirichlet-kernel estimates, and would no longer be Fejér's theorem — the entire content of the result is that continuity alone suffices.

The needed infrastructure is the four definitions above (Fourier coefficient, partial sum, Cesàro mean, Fejér kernel) and the milestone lemmas below, culminating in the goal. The Fejér kernel's closed form, positivity, and good-kernel estimates are reusable well beyond this mission: directly for a Lean proof of the Weierstrass approximation theorem on the circle, and for any future development that needs an explicit approximate identity on the circle group. Contributions are welcome at every milestone; the concentration estimate is the analytic heart of the mission and a natural place to start.

Selected references

• L. Fejér, "Untersuchungen über Fouriersche Reihen," Mathematische Annalen 58 (1904), 51–69.
• E. M. Stein and R. Shakarchi, Fourier Analysis: An Introduction, Princeton Lectures in Analysis I, Princeton University Press, 2003, Chapter 2, §5 ("Good Kernels") and Theorem 5.2.
• Wikipedia, "Fejér's theorem." https://en.wikipedia.org/wiki/Fej%C3%A9r%27s_theorem

Motivation

In 1956 Kelly answered a question that looks like gambling and is really about information: if a channel gives you a noisy advance signal about a sequence of bets, how much is that signal worth? His answer was that the maximum exponential rate of growth of a gambler's capital equals the rate of transmission over the channel -- so information rate and capital growth rate are the same quantity in different units. The betting fraction that achieves it is now called the Kelly criterion, and it is the basis of a large practical literature on position sizing.

The result is short, entirely explicit, and has no analytic subtleties -- which makes it a good formalization target and a surprising gap: the platform currently has fifteen missions on bandit algorithms and none on optimal growth.

Setting

This mission formalizes the simplest case of Kelly's Section 4: an even-money bet with no track take, won independently with probability p and lost with probability q = 1 - p. A gambler stakes a fixed fraction l of current wealth on each bet, so wealth is multiplied by 1 + l on a win and 1 - l on a loss. The exponential rate of growth is

$$G(l) = p \log(1+l) + q \log(1-l).$$

Kelly shows this is maximised at l = p - q, with maximum value 1 + p log p + q log q in bits. We state G in nats (natural logarithm), so the maximum carries an additive log 2; dividing by log 2 recovers Kelly's bit-valued form, which is exactly 1 - H(p) for the binary entropy H. The maximiser is unaffected by the choice of base.

What is being asked

The goal theorem is that l = 2p - 1 maximises G over the admissible range (-1, 1) when the bet is favourable (p > 1/2). Milestones supply the maximum value (Kelly's information-rate identity), the admissibility of the maximiser, and the concavity that makes the first-order condition sufficient.

Source

J. L. Kelly Jr., A New Interpretation of Information Rate, Bell System Technical Journal 35 (1956) 917-926, Section 4 ("the simplest case"). The growth-rate expression and the maximiser l = p - q are stated there; the maximum value in bits is Kelly's eq. for G_max.

The identity and maximiser were checked numerically before drafting: for p = 0.55, 0.6, 0.7, 0.9 the claimed maximum matches log 2 + p log p + q log q to six decimals, and a grid search over (-1, 1) at 1e-5 resolution returns 2p - 1 in every case.

Motivation

Positive-definite functions sit at a crossroads of harmonic analysis, probability, and machine learning. A function $f:\mathbb R\to\mathbb C$ is positive-definite if, for every finite family of points $x_1,\dots,x_n$ and complex coefficients $c_1,\dots,c_n$, the Hermitian quadratic form $\sum_{i,j}\overline{c_i}c_j f(x_i-x_j)$ is real and nonnegative. This single algebraic condition is exactly what makes $f$ realizable as: the covariance kernel of a stationary stochastic process; the characteristic function of a random variable (up to normalization); a valid Mercer/RBF kernel in machine learning; or a valid random-features/spectral density in random-feature kernel approximation methods.

Bochner's theorem (1932) is the structural reason all of these examples work: it says positive-definiteness is not merely a necessary condition for such a representation, but exactly characterizes it. A continuous, normalized ($f(0)=1$) function is positive-definite if and only if it is the Fourier–Stieltjes transform of some probability measure $\nu$ on $\mathbb R$ — i.e. $f$ is the characteristic function of a random variable. This mission asks for a machine-checked proof of that theorem, together with its most useful corollary: the case where $f$ is additionally Lebesgue-integrable, so that $\nu$ has an explicit continuous density given directly by the ordinary Fourier transform of $f$.

Setting

Fix IsPositiveDefinite f as above, for $f:\mathbb R\to\mathbb C$ (not restricted to real-valued kernels — the standard, fully general statement). A positive-definite function is automatically Hermitian-symmetric, $f(-x)=\overline{f(x)}$ (IsPositiveDefinite.conj_neg), which is exactly what makes a representation by a genuine (positive) probability measure possible, rather than a signed or complex one. The theorem works with f continuous and normalized. No further hypothesis (in particular, no integrability of f) is assumed for the general representation theorem: the representing measure $\nu$ need not be absolutely continuous (e.g. for a periodic $f$, $\nu$ is a discrete measure supported on the harmonics of the period — this is Herglotz's 1911 theorem, the periodic special case). Under the extra hypothesis that f is Lebesgue-integrable, the representing measure becomes absolutely continuous with a continuous density: this density is fourierTransform f, the (real part of the) Fourier transform of f — automatically real-valued, again by Hermitian symmetry — and Fourier inversion recovers f from it.

Formalization targets

Goal — Bochner's theorem, general case

$$f \text{ continuous, positive-definite, } f(0)=1 \;\Longrightarrow\; \exists\, \nu \text{ a probability measure on } \mathbb R,\; \forall x,\; f(x) = \int_{\mathbb R} e^{i2\pi\xi x}\,d\nu(\xi).$$

The central representation theorem: no integrability hypothesis on $f$, so $\nu$ may be any probability measure, not necessarily a density.

Milestone — Bochner's theorem, L¹ (density) case

$$f \text{ continuous, integrable, positive-definite, } f(0)=1 \;\Longrightarrow\; \tau:=\text{fourierTransform } f \text{ is continuous}, \;\tau \ge 0,\; \int \tau = 1, \text{ and } f(x) = \int e^{i2\pi\xi x}\tau(\xi)\,d\xi.$$

The special case where the representing measure of the goal theorem is absolutely continuous with an explicit density — the form most directly usable in applications. Provable independently of the general goal theorem via classical Fourier-inversion machinery, so it is a natural, self-contained first target.

Significance

Bochner's theorem is one of the load-bearing structural results of 20th-century harmonic analysis: it underlies Bochner–Minlos-type theorems for random fields, the entire theory of stationary Gaussian processes, kernel methods in statistics and machine learning, and (via its periodic specialization, Herglotz's theorem) the spectral theory of stationary time series. Formalizing it gives the platform a reusable, general-purpose characterization of positive-definite functions that any future mission on kernel methods, random features, or characteristic functions can build on directly.

Difficulty

The general representation theorem is the harder target: the standard proof (see the Wikipedia article linked below) constructs, from f, a strongly continuous unitary representation of $\mathbb R$ on a Hilbert space via a GNS-type construction, then invokes Stone's theorem and the spectral theorem to extract the representing measure — a substantial functional-analytic argument, since f need not be integrable and $\nu$ need not have a density. The L¹ milestone is comparatively more tractable: it can be attacked directly via Mathlib's existing Fourier-transform and Fourier-inversion machinery for integrable functions, plus the elementary fact (already available for reuse: IsPositiveDefinite.conj_neg) that a positive-definite function is Hermitian-symmetric.

Formalization scope

IsPositiveDefinite is formalized exactly as the finite Hermitian-form condition above, over Fin n → ℝ point families and Fin n → ℂ coefficients, matching the standard convention in the literature, with f : ℝ → ℂ — the fully general, complex-valued statement, not restricted to real-valued kernels. fourierTransform f ξ is defined as the real part of ∫ Complex.exp(-i2πξ x) * f(x) dx; this is provably the exact (not merely real-part-of) Fourier transform once f is positive-definite, since Hermitian symmetry forces the integral to be real already.

Selected references

• Bochner's theorem, Wikipedia — states the general locally-compact-abelian-group form and sketches the unitary-representation proof; a good map of the territory before diving into either target.
• Salomon Bochner, Vorlesungen über Fouriersche Integrale, Akademische Verlagsgesellschaft, 1932.
• Gustav Herglotz, Über Potenzreihen mit positivem, reellem Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.
• Walter Rudin, Fourier Analysis on Groups, Interscience, 1962, Chapter 1.

Assigning distinct resources under compatibility constraints

A finite allocation problem begins with a list of permitted choices. Each recipient may use some resources but not others, and a resource may be assigned at most once. Knowing that every recipient has an available resource is insufficient: several recipients may all depend on the same small pool. A useful theorem must decide whether the compatibility pattern permits all requirements to be met simultaneously.

This mission develops the matching results in the chapter on systems of distinct representatives in D. Yogeshwaran's Discrete Mathematics—Lecture Notes, §6.1. Its endpoint allows different recipients to require different numbers of resources. The classical one-resource problem, the regular-graph case, and the case in which a bounded number of assignments may remain unfilled are retained as separate source-numbered results. The project concerns established theorems, not a new conjecture about the existence of matchings.

Graphs, matchings, and demands

A finite simple graph consists of a finite set of vertices and unordered pairs of distinct vertices called edges. A bipartition is a pair of disjoint sets $L,R$ whose union is the vertex set, such that every edge joins a vertex in $L$ to a vertex in $R$. The left vertices represent recipients and the right vertices represent resources. An edge records that the resource is permitted for that recipient. These graph conventions follow Definition 1.1 of the notes.

For a vertex $x$, the neighbor set $N_G(x)$ contains the vertices joined to $x$. For a set $S$ of vertices, write $N_G(S)=\bigcup_{x\in S}N_G(x)$. A matching is an edge set in which no vertex is used twice. It is complete on $L$ if every left vertex is used, and perfect if every vertex is used. A subgraph may retain selected edges of the original graph. Its degree $\deg_H(x)$ counts the retained neighbors of $x$.

A demand is a natural number $d_x$ attached to each $x\in L$. Unlike a complete ordinary matching, the capstone may assign more than one resource to a recipient. Resources still have capacity one, and a demand may be zero.

Formalization targets

The ordinary matching criterion is Theorem 6.2:

$$\exists\text{ a complete matching on }L \quad\Longleftrightarrow\quad \forall S\subseteq L,\quad |S|\le |N_G(S)|.$$

The development also includes Exercise 6.3, asserting that a $k$-regular bipartite graph has a perfect matching when $k>0$. Proposition 6.4 states the quantitative deficit version:

$$\bigl(\forall S\subseteq L,\ |S|-d\le |N_G(S)|\bigr) \quad\Longrightarrow\quad \exists M\text{ matching},\quad |L|-d\le |E(M)|, \qquad d\ge1.$$

The capstone is the prescribed-degree equivalence of Exercise 6.5:

$$\begin{split} &\exists H\subseteq G: \bigl(\forall x\in L,\ \deg_H(x)=d_x\bigr) \land \bigl(\forall y\in R,\ \deg_H(y)\le1\bigr)\\ &\qquad\Longleftrightarrow\quad \forall S\subseteq L,\quad \sum_{x\in S}d_x\le |N_G(S)|. \end{split}$$

This statement retains the entire demand function and does not fix a uniform demand, restrict demands to positive values, or replace integral selections by real weights.

The set-theoretic interface is Corollary 6.9. A finite family of arbitrary sets $(A_i)_{i\in I}$ has a system of distinct representatives, meaning an injective choice $f(i)\in A_i$, exactly when

$$\forall J\subseteq I,\qquad |J|\le \left|\bigcup_{i\in J}A_i\right|.$$

Only the index family is finite; the sets themselves may be infinite.

What the development provides

The demand criterion characterizes feasibility entirely in terms of the original compatibility graph and the requested multiplicities. Its necessity identifies an obstruction to any assignment, while its sufficiency asserts that no other obstruction exists. The deficit theorem gives a quantitative statement when complete coverage is unavailable. The regular case gives a distinct consequence for graphs described through their degrees, rather than through a separately supplied collection of neighborhood inequalities. These are the respective contents of Exercises 6.3 and 6.5 and Proposition 6.4.

Mathlib already provides finite-family and graph versions of Hall's theorem in its Hall development and graph interface. The source-aligned development therefore reuses established infrastructure. Its additional work consists of connecting exact graph degrees and edge counts to the source statements, retaining the deficit and zero-demand cases, and supplying an arbitrary-set representatives interface. Local proofs of the five theorem statements have been checked in Lean 4.29.0-rc3 with Mathlib 777aaa6.

Where exact formalization is delicate

Independent local choices do not guarantee a matching: different choices can collide at one resource. Replacing distinct selections by nonnegative real allocations would change the conclusion. Counting total demand alone also misses obstructions carried by proper subsets of recipients.

Several representation issues matter even after the mathematics is known. A left-saturating matching need not be perfect. A subgraph's vertex set may omit isolated ambient vertices. Cardinality conventions for infinite sets can turn a superficially plausible formula into a different assertion. Finally, a theorem that assumes all neighborhood inequalities has not established those inequalities merely because a graph is regular. The individual interfaces must distinguish these obligations rather than hide them inside a definition.

Formalization scope

The graph results use finite vertex types and native SimpleGraph and Subgraph objects. Both disjointness and coverage of the bipartition are explicit. Local-finiteness instances supply finite neighbor enumerations; they impose no further restriction on finite graphs. The complete-matching predicate combines the native matching condition with inclusion of the prescribed vertex set.

Degrees in the capstone are cardinalities of finite subgraph neighbor sets. The deficit conclusion counts unordered subgraph edges. Natural subtraction is truncated at zero, an equivalent convention for these nonnegative cardinality lower bounds. Empty graphs, empty index families, and zero demands remain admissible. In the representatives theorem, arbitrary sets are measured by extended cardinality; infinity is never replaced by zero.

The reusable outputs are the source-aligned graph statements, the complete-matching interface, the prescribed-degree equivalence, and the arbitrary-set representatives criterion. Equivalent proofs and clearer reusable interfaces are within scope. Placeholder conclusions, extra assumptions that exclude the difficult cases, and fractional substitutes for the integral capstone are not.

Selected references

• D. Yogeshwaran, Discrete Mathematics—Lecture Notes, Indian Statistical Institute Bangalore, HTML edition generated 2025. Chapter 6.1; graph conventions.
• The mathlib community, Mathlib 4, revision 777aaa6, 2026. Finite-family Hall theorem; native graph Hall theorem.

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/

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

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
• Resolved 2026 paper
• Lean proof repository

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.

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.

Motivation

The conjugate-gradient method in Luenberger's Chapter 10 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).

Motivation

Quadratic exterior penalties in Luenberger's §10.11 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).

Motivation

Luenberger's generalized Kuhn–Tucker theorem 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).

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

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

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

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

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

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

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

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.