The Theory of Error-Correcting Codes I: The MacWilliams IdentityTextbook
## Motivation
Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.
The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's [*The Theory of Error-Correcting Codes*](https://books.google.com/books?id=nv6WCJgcjxcC). The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.
This development isolates the arbitrary-$q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.
## Setting
Let $F$ be a finite field of cardinality $q$, let $\iota$ be a finite coordinate type, and let a **word** be a function $c:\iota\to F$. A **linear code** $C$ is an $F$-linear subspace of the word space. The standard bilinear form is
$$
\langle c,v\rangle=\sum_{i\in\iota}c_i v_i,
$$
and the **dual code** is
$$
C^\perp=\{v:\iota\to F:\langle c,v\rangle=0\text{ for every }c\in C\}.
$$
The **Hamming weight** $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$, the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial
$$
W_C(X,Y)=\sum_{c\in C}X^{n-\operatorname{wt}(c)}Y^{\operatorname{wt}(c)}.
$$
Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$. The Lean development represents this object symbolically in `MvPolynomial (Fin 2) ℤ`; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.
## Formalization targets
### Character orthogonality over a code
For a primitive complex additive character $\psi$ of $F$, define
$$
S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle).
$$
The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.
### Coordinatewise Hamming transform
For every word $c$ and all $X,Y\in\mathbb C$, the second milestone records the full character-weighted transform of the Hamming monomial:
$$
\sum_{v\in F^\iota}
X^{n-\operatorname{wt}(v)}Y^{\operatorname{wt}(v)}
\psi(\langle c,v\rangle)
=
\bigl(X+(q-1)Y\bigr)^{n-\operatorname{wt}(c)}
(X-Y)^{\operatorname{wt}(c)}.
$$
This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.
### MacWilliams identity
The capstone is the following equality of integer polynomials:
$$
|C|\,W_{C^\perp}(X,Y)
=
W_C\bigl(X+(q-1)Y,\,X-Y\bigr).
$$
This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula
$$
W_{C^\perp}(X,Y)
=
\frac{1}{|C|}W_C\bigl(X+(q-1)Y,\,X-Y\bigr).
$$
## Significance
The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.
The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.
## Difficulty
The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$. The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.
The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.
## Formalization scope
The coordinate type is an arbitrary finite type rather than only `Fin n`; its cardinality plays the role of the code length. A word is `CodingTheory.Word F ι := ι → F`, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.
The polynomial `CodingTheory.hammingWeightEnumeratorPolynomial` has coefficients in $\mathbb Z$ and variables indexed by `Fin 2`. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.
The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$. The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.
## Selected references
- F. J. MacWilliams and N. J. A. Sloane, [*The Theory of Error-Correcting Codes*](https://books.google.com/books?id=nv6WCJgcjxcC), North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). [Publisher chapter record](https://doi.org/10.1016/S0924-6509(08)70530-0).
- Violetta Weger, [*Coding Theory*](https://home.cit.tum.de/~wvi/CT.pdf), Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
- F. J. MacWilliams, [“A Theorem on the Distribution of Weights in a Systematic Code”](https://doi.org/10.1002/j.1538-7305.1963.tb04003.x), *Bell System Technical Journal* 42 (1963), 79--94.
Eilenberg Theorems for Many-Sorted FormationsResearch Paper
## Motivation
Classical Eilenberg correspondence theorems connect algebraic descriptions of finite-state behavior with language-theoretic closure principles. The version developed by Juan Climent Vidal and Enric Cosme Llópez replaces one-sorted monoids by **many-sorted algebras**, so that operations may accept arguments of several prescribed sorts and return a value of another sort. This is the natural algebraic setting for typed term languages: a signature records the permitted input and output sorts of each operation, and a language is a family of sets indexed by sorts. The paper proves that two ways of organizing finite-state behavior—through finite-index congruences and through regular languages—determine the same ordered structure. The source is the final section of [Climent Vidal and Cosme Llópez, *Eilenberg theorems for many-sorted formations*](https://arxiv.org/abs/1604.04792), published in the *Houston Journal of Mathematics* 45(2), 2019.
The companion manuscript *A Kleene theorem for free many-sorted algebras* develops the free-term and recognizability infrastructure used by this formalization. It supplies a concrete Lean representation of sorted signatures, free algebras, homomorphisms, terms, and finite many-sorted carriers. The present mission begins from that reusable core and formalizes the formation-level theorem of the HJM paper, rather than repeating the already completed Kleene development.
## Setting
Fix a finite type of sorts $S$ and an $S$-sorted signature $\Sigma$. For an $S$-sorted set $X$, write $T_\Sigma(X)$ for the free $\Sigma$-algebra on $X$. A **congruence** $\Phi$ on a many-sorted algebra is a family of equivalence relations $\Phi_s$, one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family
$$
(T_\Sigma(X)_s/\Phi_s)_{s\in S}
$$
is finite. A sorted language $L$ is **$\Phi$-saturated** when membership in $L_s$ is constant on every $\Phi_s$-class. The **syntactic congruence** $\Omega(L)$ is the greatest algebra congruence that saturates $L$, and $L$ is regular when $\Omega(L)$ has finite index.
A **finite-index congruence formation** $\mathfrak F$ selects, for every variable family $X$, a nonempty filter $\mathfrak F(X)$ of finite-index congruences on $T_\Sigma(X)$. The selection is closed under intersections, upward inclusion, and pullback along homomorphisms whose composite with the relevant quotient projection is surjective at every sort.
A **regular-language formation** $\mathcal L$ selects regular languages in each $T_\Sigma(X)$. It contains every language saturated by the universal congruence; whenever $L,K\in\mathcal L(X)$ it contains every language saturated by $\Omega(L)\cap\Omega(K)$; and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.
The two constructions are
$$
\mathcal L_{\mathfrak F}(X)
=\{L\mid \text{$L$ is saturated by some }\Phi\in\mathfrak F(X)\},
$$
and
$$
\mathfrak F_{\mathcal L}(X)
=\{\Phi\mid \text{$\Phi$ has finite index and every $\Phi$-saturated language lies in $\mathcal L(X)$}\}.
$$
## Formalization targets
The capstone is the paper's final formation theorem: the ordered sets of finite-index congruence formations and regular-language formations are order-isomorphic, with the isomorphism fixed to be exactly the two displayed constructions.
$$
\operatorname{Form}_{\mathrm{Cgr}_{\mathrm{fi}}}(\Sigma)
\cong
\operatorname{Form}_{\mathrm{Lang}_{r}}(\Sigma).
$$
The milestones establish the universal property of the syntactic congruence, closure of finite-index congruences under the filter operations, the well-definedness of each construction, and the two recovery identities
$$
\mathfrak F_{\mathcal L_{\mathfrak F}}=\mathfrak F,
\qquad
\mathcal L_{\mathfrak F_{\mathcal L}}=\mathcal L.
$$
These identities determine the inverse maps and prevent the goal from being satisfied by an unrelated abstract order equivalence.
## Significance
The theorem packages a family of finite quotients and a family of regular languages as interchangeable data. On the algebraic side, closure is expressed by filters of congruences and quotient-surjective pullbacks. On the language side, the same information is expressed through saturation by syntactic congruences. The result therefore gives a systematic translation between quotient-based and language-based classifications in a typed, many-sorted setting.
Formalizing the theorem adds congruence, quotient-index, saturation, syntactic-congruence, and formation interfaces to the existing free many-sorted algebra library. These components are reusable for future formalizations of recognizability, Myhill–Nerode principles, finite algebra formations, and varieties or pseudovarieties of typed algebras. The mathematical theorem is already proved in the cited 2019 paper; the remaining task is to produce machine-checked Lean proofs of the source-faithful statements.
## Difficulty
The two maps are simple to write down but their inverse laws are not pointwise tautologies. A finite-index congruence must be reconstructed from the family of all languages it saturates, and a language formation must be reconstructed from all selected finite-index congruences. In the many-sorted case, finiteness applies to the entire quotient family, including its support across sorts, and intersections and pullbacks must preserve this global condition. The quotient-surjectivity premise is also essential: replacing it by ordinary surjectivity of the original homomorphism would change the formation axiom.
The syntactic congruence creates a second layer of care. It must be characterized as the greatest compatible sorted equivalence saturating a language, not merely as the kernel of the language's characteristic function, which need not itself respect the algebra operations. Thus an argument that treats saturation as an arbitrary set-theoretic equivalence misses the algebraic compatibility required by the theorem.
## Formalization scope
The Lean development uses the existing `MSKleene` representation of sorted sets, signatures, argument tuples, algebras, homomorphisms, terms, and free algebras. Congruences are sort-indexed setoids with explicit compatibility for every signature operation. Their order is inclusion of relations. Intersection and the universal congruence are concrete constructions, while pullback is defined along an algebra homomorphism.
Finite index is represented by finiteness of the sigma-type of all quotient carriers, matching the paper's finite sorted-set convention; it is not weakened to separate finiteness of each inhabited component. The sort type is assumed finite in the finite-index filter and formation correspondence theorems, as required in the final section of the source. Languages are arbitrary sorted subsets of free term algebras, including empty components. No nonemptiness assumption on variable carriers or algebra sorts is added.
The syntactic congruence is defined internally as the supremum-style least upper bound of all congruences saturating a language, rather than postulated together with its universal property. The formation structures contain only the source closure axioms. In particular, neither correspondence map nor either inverse identity is stored as a structure field; doing so would trivialize the capstone. Contributions are welcome on the foundational universal-property and finite-index lemmas, the two formation constructors, and the recovery identities that assemble into the final order isomorphism.
## Selected references
- Juan Climent Vidal and Enric Cosme Llópez, *Eilenberg theorems for many-sorted formations*, Houston Journal of Mathematics 45(2), 2019, pp. 351–416. [arXiv:1604.04792](https://arxiv.org/abs/1604.04792)
- Samuel Eilenberg, *Automata, Languages, and Machines, Volume B*, Academic Press, 1976.
- Adolfo Ballester-Bolinches, Jean-Éric Pin, and Xaro Soler-Escrivà, *Formations of finite monoids and formal languages: Eilenberg's variety theorem revisited*, Forum Mathematicum 26, 2014, pp. 1737–1761.
Gross–Yellen Graph Theory I: Cayley's Tree FormulaTextbook
## Motivation
Counting the trees on a fixed, labeled vertex set is one of the oldest enumeration
problems in graph theory. Cayley stated the count in 1889 while enumerating isomers of
saturated hydrocarbons — each tree corresponds to a possible carbon skeleton — and the
same number reappears throughout combinatorics as the number of spanning trees of the
complete graph $K_n$, a special case of Kirchhoff's Matrix–Tree Theorem, and as the base
case against which more refined tree-counting results (trees with a prescribed degree
sequence, forests, spanning trees of general graphs) are measured.
Several independent proofs of the count are known — a direct recursive argument, a
determinant computation via the Matrix–Tree Theorem, a double-counting argument on
increasing trees — and each exposes a different piece of structure. This mission
formalizes the proof via **Prüfer sequences**, due to Prüfer (1918): an explicit,
computable bijection between labeled trees and certain finite sequences, presented here
following Gross and Yellen, *Graph Theory and Its Applications*, 3rd ed. (CRC Press,
2018), Section 3.7, pp. 157–162.
## Setting
Fix $n \geq 2$ and take the vertex set to be $\{1, \dots, n\}$ (formalized as `Fin n`).
A **labeled tree** on $n$ vertices is a simple graph $T$ on this vertex set that is
connected and acyclic (Mathlib's `SimpleGraph.IsTree`). Two labeled trees are the same
exactly when their edge sets coincide — the two 4-vertex trees in Figure 3.7.1 of the
source are both paths but are *different* labeled trees, since the labels sit on
different vertices.
A **Prüfer sequence** of length $n - 2$ is any sequence $(s_1, \dots, s_{n-2})$ of
labels drawn from $\{1, \dots, n\}$, repetitions allowed (so there are $n^{n-2}$ of
them, by the rule of product).
The **encoding** of a tree $T$ (Algorithm 3.7.1, p. 157) builds its Prüfer sequence by
repeating, $n-2$ times: find the leaf (degree-one vertex) with the smallest label among
those not yet removed, record the label of *its* neighbor, then delete that leaf. The
**decoding** of a sequence (Algorithm 3.7.3, p. 159) reverses this: it rebuilds the
tree edge by edge, at each step joining the smallest label not yet used and not
appearing later in the sequence to the next label in the sequence, finishing by joining
the two labels left over.
## Formalization targets
### Goal — Cayley's Tree Formula (Theorem 3.7.5, p. 162)
$$
\operatorname{Nat.card}\, \{T : \text{SimpleGraph}(\text{Fin } n) \mid T.\text{IsTree}\} = n^{\,n-2}, \qquad n \geq 2.
$$
This is the weakest stable statement: it is exactly the count Cayley identified, phrased
without reference to any particular proof method, so it is not tied to properties of
Prüfer sequences beyond what is needed to establish the count.
## Significance
The identity itself is foundational: it is the base case of Kirchhoff's Matrix–Tree
Theorem (which computes the analogous count for spanning trees of an arbitrary graph as
a cofactor of its Laplacian) and it appears as an ingredient in random graph theory
(counting spanning trees of $K_n$ bounds the number of ways a random graph process can
build a tree) and in the analysis of algorithms on trees, where the Prüfer encoding
itself is used as a compact serialization of a labeled tree.
The result has been proved by hand for over a century, and its most classical proof (the
one formalized here) has not, to this project's knowledge, appeared as a
machine-checked Lean proof; Mathlib's `Combinatorics.SimpleGraph` library has the tree
and acyclicity infrastructure this mission builds on, but not the Prüfer bijection or
the count itself. Formalizing it here means constructing the encoding and decoding maps
explicitly as computable, total recursive functions, and proving they are mutually
inverse — the mission's four milestones below are exactly the four supporting results
the source uses for this.
## Difficulty
The obvious first attempt is to define the encoding by structural recursion, peeling one
leaf per step, but this immediately runs into a dependent-typing obstacle: after
deleting a vertex, the "remaining graph" naturally lives on a *smaller* vertex type, so
a naive recursive definition changes type at every step and the final sequence's type
(length $n-2$) is not visible to the recursion by construction. The formalization here
sidesteps this by keeping the ambient vertex type fixed at `Fin n` throughout and
tracking the shrinking set of "active" vertices as an ordinary `Finset (Fin n)`
parameter, so the recursion is on a natural number step-counter rather than on the type
itself; the price is that every step's "leaf" and "neighbor" must be picked out by an
explicit `Finset.filter`/`Finset.min` computation whose well-definedness (there is
always a smallest active leaf, and it always has a unique active neighbor) is exactly
the content of Propositions 3.7.1 and 3.7.3 below, rather than something the type system
gives for free. The inverse direction has the dual issue in reverse: decoding recurses
structurally on the sequence while tracking a shrinking *label set*, and showing the two
recursions undo each other (Proposition 3.7.4) requires the same induction run in both
directions simultaneously.
## Formalization scope
Trees are `SimpleGraph (Fin n)` satisfying Mathlib's `SimpleGraph.IsTree`; no alternate,
weaker notion of "tree" is used. Prüfer sequences are functions `Fin (n - 2) → Fin n`
(equivalently, by `Fintype.card_fun`, exactly the $n^{n-2}$ count needed) rather than
`List` or `Vector`, so that the final counting step is immediate once the bijection is
established. The encoding and decoding functions (`pruferEncode`, `pruferDecode`) are
supplied as `noncomputable` definitions in `Definitions.Def_GYGraphTheory` — noncomputable
only because Prop-level decidability of a general `SimpleGraph.Adj` is classical, not
because the algorithm is non-constructive; every step is the literal Prüfer procedure,
junk-valued (defaulting to label `0`) outside its intended domain in exactly the way a
hand proof would say "this step is meaningless once fewer than two active vertices
remain." The four milestones give the precise faithful statements of the source's
Propositions 3.7.1, Corollary 3.7.2, Proposition 3.7.3, and Proposition 3.7.4; the goal
theorem is the immediate corollary once all four are in hand, via `Fintype.card_congr`
and `Fintype.card_fun`. A trivializing formalization is not available here: `IsTree` is
Mathlib's standard, non-vacuous notion, and the milestones pin down `pruferEncode`
and `pruferDecode` to the source's specific algorithm rather than leaving the bijection's
existence as a free black box. Beyond the four milestones, a full development needs:
basic `Finset`/`List` manipulation lemmas relating `pruferPeel`'s step-indexed recursion
to `pruferDecodeAux`'s list-indexed recursion (reusable in any future mission touching
Prüfer-style encodings); and the final cardinality argument tying the bijection to
`n ^ (n - 2)`. Contributions connecting this formula to Mathlib's general Matrix–Tree
machinery (if and when it exists) would be a natural, welcome extension but are out of
scope for this mission.
## Selected references
- A. Cayley, *A theorem on trees*, Quart. J. Math. 23 (1889), 376–378.
- H. Prüfer, *Neuer Beweis eines Satzes über Permutationen*, Archiv der Mathematischen
Physik 27 (1918), 742–744.
- J.L. Gross and J. Yellen, *Graph Theory and Its Applications*, 3rd ed., CRC Press,
2018, Section 3.7 "Counting Labeled Trees: Prüfer Encoding", pp. 157–162.
Hatcher Algebraic Topology III: The Classification of Covering SpacesTextbook
## Motivation
The third mission in the series formalizing Allen Hatcher's *Algebraic Topology* (Cambridge University Press, 2002; [pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)) turns to the second main topic of Chapter 1, **covering spaces** (Section 1.3, pp. 56–78). The first mission used the covering $\mathbb{R}\to S^1$ to compute $\pi_1(S^1)$, and the second proved van Kampen's theorem. This mission develops the general theory of covering spaces of a fixed space $X$: the lifting properties (pp. 60–62), the classification of connected covering spaces by subgroups of $\pi_1(X)$ (pp. 63–68), and deck transformations and group actions (pp. 70–72). Its goal is the **classification theorem** (Theorem 1.38, p. 67), Hatcher's "Galois correspondence" between path-connected covering spaces of $X$ and subgroups of $\pi_1(X,x_0)$, together with its companions Proposition 1.39 (deck groups and normal covers) and Proposition 1.40 (covering space actions and orbit spaces).
All statements live in the Lean namespace `Hatcher` used by the earlier missions.
## Setting
A **covering space** of $X$ (p. 56) is a space $\tilde X$ with a map $p:\tilde X\to X$ such that every $x\in X$ has an open neighborhood $U$ whose preimage is a disjoint union of open sets each mapped homeomorphically onto $U$; $p^{-1}(U)$ may be empty, so $p$ need not be surjective. This is Mathlib's `IsCoveringMap`. For a covering space with basepoints $p:(\tilde X,\tilde x_0)\to(X,x_0)$ we write
$$p_*:\pi_1(\tilde X,\tilde x_0)\to\pi_1(X,x_0),\qquad H=p_*\big(\pi_1(\tilde X,\tilde x_0)\big)\le\pi_1(X,x_0)$$
for the induced homomorphism (`Hatcher.coverHom`) and its image (`Hatcher.coverSubgroup`).
$X$ is **semilocally simply-connected** (p. 63, `Hatcher.IsSemilocallySimplyConnected`) if each $x\in X$ has a neighborhood $U$ such that every loop at $x$ contained in $U$ is null-homotopic in $X$. The bundle `Hatcher_Covering` also fixes: the structure `CoveringSpace X` (a total space $\tilde X$ and a covering map $p$) and its pointed version `PointedCover X x₀` (with $\tilde x_0\in p^{-1}(x_0)$ and associated subgroup `PointedCover.subgroup`); **isomorphism** of covering spaces (p. 67), a homeomorphism $f:\tilde X_1\to\tilde X_2$ with $p_1=p_2f$, with or without preservation of basepoints (`IsIsomorphic`, `IsPointedIsomorphic`); the **deck transformation group** $G(\tilde X)$ (p. 70, `deckGroup`), the self-homeomorphisms of $\tilde X$ commuting with $p$; **normal** covering spaces (p. 70, `IsNormalCover`); Hatcher's condition $(\ast)$ for a **covering space action** of a group $G$ on $Y$ (p. 72, `IsCoveringSpaceAction`); and the **orbit space** $Y/G$ with its quotient map (`OrbitSpace`, `orbitProj`).
## Formalization targets
### Goal (Theorem 1.38, p. 67)
Let $X$ be path-connected, locally path-connected and semilocally simply-connected, with basepoint $x_0$. Then:
1. every subgroup $H\le\pi_1(X,x_0)$ is $p_*\pi_1(\tilde X,\tilde x_0)$ for some path-connected covering space with basepoint;
2. two path-connected covering spaces with basepoints are isomorphic by a basepoint-preserving isomorphism iff their subgroups coincide;
3. two path-connected covering spaces are isomorphic (basepoints ignored) iff their subgroups, at some choice of basepoints over $x_0$, are conjugate in $\pi_1(X,x_0)$.
Together these say that $(\tilde X,\tilde x_0)\mapsto p_*\pi_1(\tilde X,\tilde x_0)$ is a bijection from basepoint-preserving isomorphism classes of path-connected covering spaces to subgroups, inducing a bijection from isomorphism classes to conjugacy classes of subgroups.
### Milestones
1. **Proposition 1.31** (p. 61), first part: $p_*$ is injective.
2. **Proposition 1.31**, second part: $p_*\pi_1(\tilde X,\tilde x_0)$ consists of the classes of loops at $x_0$ whose lifts starting at $\tilde x_0$ are loops.
3. **Proposition 1.32** (p. 61): for $X,\tilde X$ path-connected, the fibre $p^{-1}(x_0)$ is in bijection with the cosets of $H$, so the number of sheets is the index of $H$.
4. **Proposition 1.33** (p. 61), the lifting criterion: for $Y$ path-connected and locally path-connected, $f:(Y,y_0)\to(X,x_0)$ lifts to $(\tilde X,\tilde x_0)$ iff $f_*\pi_1(Y,y_0)\subseteq H$.
5. **Proposition 1.34** (p. 62), unique lifting: two lifts of $f:Y\to X$ agreeing at one point agree everywhere if $Y$ is connected.
6. **Necessity of semilocal simple connectivity** (p. 63): if $X$ has a simply-connected covering space (surjective onto $X$), then $X$ is semilocally simply-connected.
7. **Existence of a simply-connected covering space** (pp. 63–65): if $X$ is path-connected, locally path-connected and semilocally simply-connected, it has a simply-connected covering space (the universal cover).
8. **Proposition 1.36** (p. 66): under the same hypotheses, every subgroup $H\le\pi_1(X,x_0)$ is realized as $p_*\pi_1(X_H,\tilde x_0)$ for a path-connected covering space.
9. **Proposition 1.37** (p. 67): for $X$ path-connected and locally path-connected, two path-connected covering spaces with basepoints are basepoint-preservingly isomorphic iff their subgroups are equal.
10. **Change of basepoint** (pp. 67–68, proof of Theorem 1.38): moving $\tilde x_0$ within $p^{-1}(x_0)$ replaces $H$ by a conjugate, and every conjugate arises this way.
11. **Proposition 1.39(a)** (p. 71): a path-connected covering space of a path-connected, locally path-connected $X$ is normal iff $H$ is a normal subgroup.
12. **Proposition 1.39(b)**: $G(\tilde X)\cong N(H)/H$, given as a surjective homomorphism $N(H)\to G(\tilde X)$ with kernel $H$.
13. **Proposition 1.39, final clause**: for the universal cover, $G(\tilde X)\cong\pi_1(X,x_0)$.
14. **Proposition 1.40(a)** (p. 72): for a covering space action of $G$ on $Y$, the quotient map $Y\to Y/G$ is a normal covering space.
15. **Proposition 1.40(b)**: if moreover $Y$ is path-connected, $G$ is the group of deck transformations of $Y\to Y/G$, via $g\mapsto(y\mapsto gy)$.
16. **Proposition 1.40(c)**: if $Y$ is path-connected and locally path-connected, $G\cong\pi_1(Y/G)/p_*\pi_1(Y)$, given as a surjective homomorphism $\pi_1(Y/G)\to G$ with kernel $p_*\pi_1(Y)$.
## Significance
*The result itself.* The classification theorem is the central structural fact about covering spaces: the connected coverings of $X$ are "the same as" the subgroups of $\pi_1(X)$, with the universal cover corresponding to the trivial subgroup and normal coverings to normal subgroups. Proposition 1.40 is the standard method for computing fundamental groups of orbit spaces ($\pi_1(\mathbb{RP}^n)=\mathbb{Z}/2$, $\pi_1(T^n)=\mathbb{Z}^n$, lens spaces) and is used throughout Hatcher's later chapters.
*Formalizing it.* Mathlib (at this environment's revision) already has the lifting theory for covering maps: path and homotopy lifting (`IsCoveringMap.liftPath`, `liftHomotopy`), the monodromy action (`IsCoveringMap.monodromy`), the injectivity of $p_*$ (`injective_path_homotopic_map`, cited there as Proposition 1.31), the unique-lifting statement (`IsCoveringMap.eq_of_comp_eq`), and the lifting criterion itself (`existsUnique_continuousMap_lifts_of_range_le`, cited as Proposition 1.33). For quotient maps by a free properly discontinuous action it has `IsQuotientCoveringMap`, with the homomorphism $\pi_1(Y/G)\to G^{\mathrm{op}}$ and its kernel and surjectivity. Milestones 1, 4, 5 and 16 are therefore expected to be short reductions to Mathlib, and Mathlib's quotient-covering theory should carry most of milestones 14–15. Mathlib has no notion of semilocal simple connectivity, no construction of the universal cover or of the coverings $X_H$, no classification theorem, and no deck transformation groups or normal coverings; milestones 6–13 and the goal are new.
## Difficulty
The heart of the mission is the construction of the universal cover (pp. 63–65): the points are homotopy classes of paths from $x_0$, the topology is generated by the sets $U_{[\gamma]}$ for $U$ in the basis of path-connected open sets on which $\pi_1$ dies, and one must verify that this is a topology basis, that $p$ is a covering map, and that the result is simply connected. Proposition 1.36 then passes to a quotient by $H$ and checks that the projection remains a covering map. Both are elementary but long, and formalizing them requires a systematic treatment of path homotopy classes as points of a space.
Propositions 1.37 and 1.39 follow from the lifting criterion and unique lifting; the deck-group homomorphism in 1.39(b) sends a loop in $N(H)$ to the deck transformation produced by the lifting criterion, and its kernel is computed by Proposition 1.31. Proposition 1.40(a) needs the quotient topology on $Y/G$ and the evenly covered neighborhoods $p(U)$ from condition $(\ast)$; part (b) is the observation that a deck transformation of a path-connected cover is determined by one value. Milestone 3 is orbit–stabilizer for the monodromy action.
## Formalization scope
* Spaces are arbitrary topological spaces; hypotheses (path-connectedness, local path-connectedness, semilocal simple connectivity, connectedness of the domain in Proposition 1.34) are stated per theorem, exactly where Hatcher assumes them.
* `CoveringSpace X` bundles a total space in the **same universe** as $X$ with a covering map; the classification quantifies over covering spaces in this sense. Since the universal cover and the coverings $X_H$ are constructed from paths in $X$, they live in that universe, so nothing is lost.
* "Isomorphic" is the existence of a homeomorphism over $X$ (Hatcher, p. 67), a proposition on pairs of covering spaces; Theorem 1.38 is stated as the three-part conjunction above rather than as a bijection between quotient sets, which avoids forming the set of isomorphism classes of types while asserting exactly the same content.
* Conjugacy is expressed with Mathlib's `MulAut.conj`; "number of sheets equals the index" is stated as a bijection $p^{-1}(x_0)\simeq\pi_1(X,x_0)/H$ with the coset space.
* The isomorphisms of Propositions 1.39(b) and 1.40(c) are stated as surjective homomorphisms with prescribed kernel, which is how Hatcher proves them and avoids requiring a `Normal` instance in the statement; the final clause of 1.39 and 1.40(b) are stated as the existence of group isomorphisms, the latter with its action on $Y$ prescribed.
* A covering space action includes continuity of each $y\mapsto gy$ (Hatcher's actions are by homeomorphisms). The orbit space is Mathlib's `MulAction.orbitRel.Quotient` with the quotient topology.
* Trivializing readings are excluded: path-connected spaces are nonempty, and a nonempty covering space of a path-connected base is surjective; milestone 6 assumes surjectivity explicitly because its base need not be connected.
Contributions welcome: a reusable construction of the space of path classes with its topology, the covering $X_H$, and the deck-group homomorphism; the short reductions to Mathlib for Propositions 1.31, 1.33 and 1.34 are good first contributions.
## Selected references
- A. Hatcher, *Algebraic Topology*, Cambridge University Press, 2002. Section 1.3, pp. 56–72. [https://pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)
- E. H. Spanier, *Algebraic Topology*, Springer, 1966, Chapter 2 (covering spaces and the classification theorem).
- J. R. Munkres, *Topology*, 2nd ed., Prentice Hall, 2000, Chapter 13 (classification of covering spaces).
- Mathlib, `Mathlib/Topology/Covering/Basic.lean` (covering maps). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.lean)
- Mathlib, `Mathlib/Topology/Homotopy/Lifting.lean` (path and homotopy lifting, monodromy, the lifting criterion). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean)
- Mathlib, `Mathlib/Topology/Covering/Quotient.lean` (quotient covering maps for group actions). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.lean)
Hatcher Algebraic Topology II: The van Kampen TheoremTextbook
## Motivation
Once $\pi_1(S^1)\cong\mathbb{Z}$ is known, the next question in Allen Hatcher's *Algebraic Topology* (Cambridge University Press, 2002; [pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)) is how to compute fundamental groups of spaces built from pieces. Section 1.2 answers this with **van Kampen's theorem** (Theorem 1.20, p. 43): if a space is covered by open sets with a common basepoint and path-connected intersections, its fundamental group is the free product of the fundamental groups of the pieces, modulo relations coming from the intersections. It is the main computational tool of Chapter 1: it gives the fundamental groups of wedges of circles, graphs, surfaces, and every CW complex from its 2-skeleton (Propositions 1.26–1.28), and it underlies the classification of covering spaces in Section 1.3.
This is the second mission in the series formalizing Hatcher's book. The first mission established the covering-space lifting properties and $\pi_1(S^1,1)\cong\mathbb{Z}$ in the Lean namespace `Hatcher`; this one covers the subsection "The van Kampen Theorem" of Section 1.2 (pp. 41–47) together with its warm-up Lemma 1.15 and Proposition 1.14 from Section 1.1 (p. 35).
## Setting
Let $X$ be a topological space with a **basepoint** $x_0$. A **path** is a continuous map $I=[0,1]\to X$, a **loop** at $x_0$ is a path with both endpoints $x_0$, and $\pi_1(X,x_0)$ is the group of homotopy classes of loops at $x_0$ under concatenation. A continuous map $\varphi:X\to Y$ with $\varphi(x_0)=y_0$ **induces** a homomorphism $\varphi_*:\pi_1(X,x_0)\to\pi_1(Y,y_0)$, $[f]\mapsto[\varphi\circ f]$.
Let $(A_\alpha)_{\alpha\in\iota}$ be a family of subsets of $X$, each containing $x_0$, with the subspace topology; write $\pi_1(A_\alpha)$ for $\pi_1(A_\alpha,x_0)$. The inclusions $A_\alpha\hookrightarrow X$ induce
$$j_\alpha:\pi_1(A_\alpha)\to\pi_1(X),$$
which are `Hatcher.inclHom`, and the inclusions $A_\alpha\cap A_\beta\hookrightarrow A_\alpha$ and $A_\alpha\cap A_\beta\hookrightarrow A_\beta$ induce
$$i_{\alpha\beta}:\pi_1(A_\alpha\cap A_\beta)\to\pi_1(A_\alpha),\qquad i_{\beta\alpha}:\pi_1(A_\alpha\cap A_\beta)\to\pi_1(A_\beta),$$
which are `Hatcher.interHomLeft` and `Hatcher.interHomRight`.
The **free product** $\ast_\alpha G_\alpha$ of a family of groups is the group of reduced words in the $G_\alpha$ (Hatcher, pp. 41–42); in Lean it is Mathlib's `Monoid.CoprodI`, here `Hatcher.FreeProd`. Its universal property extends the $j_\alpha$ to a single homomorphism
$$\Phi:\ast_\alpha\pi_1(A_\alpha)\to\pi_1(X),$$
`Hatcher.vanKampenHom`. Since $j_\alpha i_{\alpha\beta}=j_\beta i_{\beta\alpha}$ (both are induced by $A_\alpha\cap A_\beta\hookrightarrow X$), the elements
$$i_{\alpha\beta}(\omega)\,i_{\beta\alpha}(\omega)^{-1},\qquad \omega\in\pi_1(A_\alpha\cap A_\beta),$$
lie in the kernel of $\Phi$. Let $N$ be the **normal subgroup generated** by all of them, `Hatcher.vanKampenNormal`.
## Formalization targets
### Goal (Theorem 1.20)
If $X$ is the union of path-connected open sets $A_\alpha$ each containing $x_0$, each $A_\alpha\cap A_\beta$ is path-connected, and each $A_\alpha\cap A_\beta\cap A_\gamma$ is path-connected, then
$$\Phi \text{ is surjective}\qquad\text{and}\qquad \ker\Phi=N .$$
Hence $\Phi$ induces an isomorphism $\pi_1(X)\cong\ast_\alpha\pi_1(A_\alpha)/N$.
### Milestones
1. **Lemma 1.15** (p. 35). If $X$ is the union of path-connected open sets $A_\alpha$ containing $x_0$ with each $A_\alpha\cap A_\beta$ path-connected, then every loop in $X$ at $x_0$ is homotopic to a product of loops each of which is contained in a single $A_\alpha$.
2. **Proposition 1.14** (p. 35). $\pi_1(S^n)=0$ for $n\ge 2$.
3. **Theorem 1.20, first part** (p. 43). Under the hypotheses of Lemma 1.15, $\Phi$ is surjective.
4. **The kernel contains the relators** (p. 43). $N\le\ker\Phi$, with no hypotheses on the cover.
5. **Theorem 1.20, second part** (p. 43). If moreover every triple intersection is path-connected, $\ker\Phi\le N$.
6. **Induced isomorphism** (p. 43). Under the same hypotheses there is an isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ sending the class of a word to its image under $\Phi$.
## Significance
*The result itself.* Van Kampen's theorem is the gluing law for $\pi_1$. With it Hatcher computes $\pi_1$ of wedge sums (free products), of graphs (free groups), of the closed orientable surfaces (Example 1.26), and shows that attaching $2$-cells kills exactly the attaching loops (Proposition 1.26), so that every group is a fundamental group (Corollary 1.28). The surjectivity half alone gives Proposition 1.14, that spheres of dimension at least two are simply connected, and hence that $\mathbb{R}^2$ is not homeomorphic to $\mathbb{R}^n$ for $n\ne 2$ (Corollary 1.16).
*Formalizing it.* Mathlib has the fundamental groupoid and fundamental group, induced homomorphisms (`FundamentalGroup.map`), free products of groups (`Monoid.CoprodI`) with their universal property, normal closures, and quotient groups. It has no version of van Kampen's theorem for topological spaces (its `CategoryTheory/Limits/VanKampen` concerns colimits in categories, not fundamental groups), and no computation of $\pi_1(S^n)$ for $n\ge 2$; on the platform, however, the theorem `SP4Mission.sphere_simplyConnected` (already proved in this environment) states that the unit sphere of $\mathbb{R}^n$ is simply connected for $n\ge 3$, which is Proposition 1.14 with shifted indexing, so that milestone can be closed by a one-line reduction. The mission supplies the statements in Hatcher's form, on Mathlib's $\pi_1$, so that later missions (covering spaces, cell complexes) can use them directly.
## Difficulty
Surjectivity is a compactness argument: subdivide $I$ so each piece of the loop lies in one $A_\alpha$, then use path-connectedness of the intersections to connect the subdivision points back to $x_0$. The formal difficulty is bookkeeping: producing the subdivision from an open cover of $[0,1]$ (Mathlib's `exists_monotone_Icc_subset_open_cover_unitInterval` is the tool) and showing the reparametrised concatenation is homotopic to the original loop.
The kernel computation is the hard part. Hatcher's proof takes a homotopy $F:I\times I\to X$ between two factorizations, subdivides the square into rectangles each mapped into a single $A_\alpha$, perturbs the grid so at most three rectangles meet at a corner (this is where triple intersections enter), and then shows that moving the loop across one rectangle at a time changes the factorization only by the two elementary moves that hold in $\ast_\alpha\pi_1(A_\alpha)/N$. Every step is elementary, but the induction over the grid is long, and each elementary move requires an explicit path-homotopy in a subspace. The naive idea of proving $\ker\Phi\le N$ by an induction on word length does not work: the relation between two factorizations of the same loop is only visible through a homotopy in $X$, not through the words.
Proposition 1.14 is easy given Lemma 1.15 but requires exhibiting the cover of $S^n$ by two complements of antipodal points, showing each is simply connected (homeomorphic to $\mathbb{R}^n$ via stereographic projection, which Mathlib has as `stereographic`), and showing their intersection is path-connected when $n\ge 2$.
## Formalization scope
* The index set $\iota$ and the space $X$ are arbitrary; the $A_\alpha$ are `Set X` with the subspace topology, and $\pi_1(A_\alpha)$ is Mathlib's `FundamentalGroup ↥(A α) ⟨x₀, _⟩`. Hypotheses are stated explicitly on each theorem: `IsOpen`, `IsPathConnected`, `⋃ α, A α = Set.univ`, and path-connectedness of pairwise (and, where Hatcher requires it, triple) intersections.
* $i_{\alpha\beta}$ and $i_{\beta\alpha}$ are both defined on $\pi_1(A_\alpha\cap A_\beta)$ (rather than on $\pi_1(A_\beta\cap A_\alpha)$ for the second), so no identification of $A_\alpha\cap A_\beta$ with $A_\beta\cap A_\alpha$ is needed; the set of relators ranges over all ordered pairs $(\alpha,\beta)$.
* "Product of loops" in Lemma 1.15 is a finite `List` of loops, each tagged with the index $\alpha$ of the piece it lies in, concatenated right-to-left with the constant loop as empty product (`Hatcher.loopProd`). Any bracketing gives the same homotopy class.
* The goal is stated as the conjunction "surjective and $\ker\Phi=N$"; the isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ is a separate milestone, stated as the existence of a group isomorphism compatible with $\Phi$ on the quotient, which pins it down uniquely.
* $S^n$ is `Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1`, and "$\pi_1(S^n)=0$" is Mathlib's `SimplyConnectedSpace` (path-connected with trivial fundamental group), which is what Hatcher means since $S^n$ is path-connected.
* Trivializing readings are excluded: the cover hypotheses do not force $\iota$ nonempty, but then $X=\bigcup A_\alpha=\varnothing$ contradicts the existence of $x_0$, so the statements are not vacuous in any interesting case, and $\Phi$ is the specific homomorphism induced by the inclusions.
Contributions welcome: the subdivision lemma for loops in an open cover, a reusable treatment of factorizations and their elementary moves, and the two-set special case $\pi_1(X)\cong(\pi_1(A)\ast\pi_1(B))/N$ as a corollary.
## Selected references
- A. Hatcher, *Algebraic Topology*, Cambridge University Press, 2002. Section 1.2, pp. 40–49; Lemma 1.15 and Proposition 1.14, p. 35. [https://pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)
- E. R. van Kampen, *On the connection between the fundamental groups of some related spaces*, American Journal of Mathematics 55 (1933), 261–267. [https://doi.org/10.2307/2371128](https://doi.org/10.2307/2371128)
- H. Seifert, *Konstruktion dreidimensionaler geschlossener Räume*, Berichte Sächs. Akad. Leipzig 83 (1931), 26–66.
- Mathlib, `Mathlib/GroupTheory/CoprodI.lean` (free products of groups). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/GroupTheory/CoprodI.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/GroupTheory/CoprodI.lean)
- Mathlib, `Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean` (fundamental group and induced homomorphisms). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean)
A Kleene Theorem for Free Many-Sorted AlgebrasResearch Paper
## Motivation
**Kleene's theorem** (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the **regular** ones — those built from finite languages by union, concatenation, and the Kleene star. **Mezei and Wright** (1967) lifted recognizability off strings, calling a subset of an arbitrary algebra **recognizable** when it is the preimage of a subset of a *finite* algebra under a homomorphism. Replacing strings by terms — finite trees labelled by operation symbols — gives the theory of **recognizable tree languages** and finite tree automata of **Gécseg and Steinby** (1984), where the Kleene correspondence reappears with a tree concatenation and an iteration operation in the role of the star.
Many computational structures are inherently **many-sorted**: typed lambda calculi, structured programming languages, process calculi, XML schemas — data and operations organized into distinct sorts. In the many-sorted setting a signature assigns to each operation symbol the sorts of its arguments and of its value, variables carry sorts, and a language is a sort-indexed family of term sets. The predecessor of this mission, Climent Vidal–Cosme Llópez 2020 (**CVCL20**), established that recognizability over free many-sorted algebras is preserved — and, where applicable, reflected — by substitution, iteration, quotient, inverse tree-homomorphic image, and direct linear image, via finite-index congruences. What CVCL20 left open is the **regular** side: whether a natural class of many-sorted regular expressions captures exactly the recognizable languages. This mission closes that gap.
## Setting
Fix a finite set of **sorts** $S$. An **$S$-sorted set** $A = (A_s)_{s\in S}$ is a family of sets; it is **finite** when $\coprod_{s\in S} A_s$ is finite. An **$S$-sorted signature** $\Sigma$ assigns to each pair $(\mathbf{s}, s) \in S^\star \times S$ a set $\Sigma_{\mathbf{s},s}$ of operation symbols of **arity** $\mathbf{s}$ and **coarity** $s$. A **$\Sigma$-algebra** $\mathbf{A}$ is an $S$-sorted set $A$ together with, for each $\sigma \in \Sigma_{\mathbf{s},s}$, an operation $\sigma^{\mathbf A}\colon A_{\mathbf s} \to A_s$, where $A_{\mathbf s} = \prod_{j} A_{s_j}$. A **homomorphism** commutes with all operations sortwise.
The **free $\Sigma$-algebra** $\mathbf T_\Sigma(X)$ on an $S$-sorted set $X$ of variables has as its sort-$s$ carrier $\mathrm T_\Sigma(X)_s$ the set of **$(X,s)$-terms**; every $S$-sorted map $X \to A$ extends uniquely to a homomorphism $\mathbf T_\Sigma(X) \to \mathbf A$. Following automata-theoretic tradition, subsets of $\mathrm T_\Sigma(X)$ are called **languages**. For a sort $s$, a language $L \subseteq \mathrm T_\Sigma(X)_s$ is **$s$-recognizable** when there are a finite $\Sigma$-algebra $\mathbf N$, a homomorphism $f\colon \mathbf T_\Sigma(X) \to \mathbf N$, and a subset $M \subseteq N_s$ with $L = f_s^{-1}[M]$. Write $\mathrm{Rec}_s(\mathbf T_\Sigma(X))$ for the set of all such $L$.
Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable $z \in X_u$ and a language $L \subseteq \mathrm T_\Sigma(X)_u$, **$z$-substitution** $\left(\!\begin{smallmatrix}z\\ L\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s$ replaces, in every term of an input language of sort $s$, each occurrence of $z$ independently by a term of $L$. The **$z$-iteration** is $L^{\star z} = \bigcup_{i\in\mathbb N} L^{i\,z}$, where $L^{0\,z} = \{z\}$ and $L^{i+1\,z} = L^{i\,z} \cup \left(\!\begin{smallmatrix}z\\ L^{i\,z}\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s(L)$. For a finite $S$-sorted set $Z$, the **regular signature** $\mathrm{Reg}(S,\Sigma,Z)$ expands $\Sigma$ by an empty constant $\varnothing_s$, a binary sum $+_s$, a unary $z$-iteration $(\cdot)^{\star z}$ for each $z\in Z_s$, and a $z$-substitution operation for each $z\in Z_t$. Its terms are the **regular expressions** over $(S,\Sigma,Z)$; the power algebra $\mathbf T_\Sigma(Z)^\wp$ carries a canonical $\mathrm{Reg}(S,\Sigma,Z)$-algebra structure, and interpreting a regular expression there yields a language $\{R\}^{Z\sharp}_s$. A language $L\subseteq \mathrm T_\Sigma(X)_s$ is **$s$-regular** when $L = \{R\}^{Z\sharp}_s$ for some finite $Z\supseteq X$ and some regular expression $R$ of type $s$; write $\mathrm{Reg}_s(\mathbf T_\Sigma(X))$.
## Formalization targets
### Goal — the many-sorted Kleene theorem
$$\forall\, s\in S,\qquad \mathrm{Rec}_s(\mathbf T_\Sigma(X)) \;=\; \mathrm{Reg}_s(\mathbf T_\Sigma(X)).$$
The statement fixes no automaton model and no normal form for regular expressions: it asserts only that the two classes of languages coincide, at every sort, for every finite $S$, every finite $S$-sorted signature $\Sigma$, and every finite $S$-sorted set $X$. It splits into $\mathrm{Reg}_s \subseteq \mathrm{Rec}_s$ (Corollary 4.8) and $\mathrm{Rec}_s \subseteq \mathrm{Reg}_s$ (Proposition 4.10).
## Significance
The result completes the Kleene–Myhill–Nerode correspondence on the side of universal algebra, uniformly over an arbitrary finite many-sorted signature: it names the exact operations — those of $\Sigma$, plus empty language, union, sortwise substitution, and sortwise iteration — that generate precisely the finite-state behaviours. Over non-free structures the correspondence is known to fail (recognizable but non-rational subsets of a monoid, Eilenberg 1974), which is what makes the free many-sorted algebra the natural home for an exact statement. The forward direction organizes the regular languages into a $\mathrm{Reg}$-algebra and instantiates the closure properties of CVCL20; the converse gives a constructive, syntactic procedure — from a recognizing homomorphism it builds a regular expression denoting the language — generalizing Lemma 2.5.7 of Gécseg–Steinby, itself descended from McNaughton–Yamada.
The paper is new (June 2026) and has no machine-checked proof. This mission produces the first formalization: a reusable Lean development of finite many-sorted universal algebra — signatures, algebras, free term algebras and their universal property, the Artinian subterm order, power algebras, recognizability, and the substitution/iteration calculus — together with the two inclusions and the state-elimination argument. Everything below the §4 headline results is infrastructure of independent value for many-sorted formal language theory.
## Difficulty
The converse inclusion is the substance. The single-sorted proof eliminates automaton states one at a time along a single axis; the naive port to the many-sorted case — fix a linear order on all states and eliminate — loses track of the sort at which each elimination happens and does not terminate cleanly. The argument instead carries a **sortwise budget**: an $S$-sorted family $K \le N$ recording, for each sort $t$, the set $K_t$ of state values still admissible at internal subterms. The induction is on $\lVert\lVert K\rVert\rVert = \sum_{s\in S} k_s$, and each step removes the top state of *one* chosen sort, so the recursion branches over the sorts whose budget is nonzero and the key identity (Equation (E)) is a union over those sorts. The inductive invariant — the family of auxiliary languages $L_u(C,K,l)$ with its budget bookkeeping — is what separates the many-sorted argument from its ancestor; it is also the part Gécseg–Steinby declare "obvious from the construction" and this proof spells out in full (Claims C1–C6).
## Formalization scope
Proposed Lean representation: $S$ a type with `[Fintype S]`; an $S$-sorted set as `S → Type`; a signature as a family `List S → S → Type` with finiteness where the theorems need it; the free algebra as an inductive term type; the power algebra with sort-$s$ carrier `Set (T_Σ Z s)`; $s$-recognizability as the existence of a finite $\Sigma$-algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: $S$ finite throughout; $\Sigma$ finite and $X$ finite for the §4 results (so that only finitely many basic terms exist and the budget induction is well-founded); the regular operations are exactly $\{\varnothing, +, (\cdot)^{\star z}, z\text{-subst}\}$ together with the operations of $\Sigma$ — not an unrestricted Boolean or closure algebra, which would trivialize the statement.
A complete development needs: the many-sorted UA core (sorted sets and maps, signature, algebra, homomorphism, subalgebra, congruence); the free algebra with unique readability (Proposition 3.4) and universal property (Proposition 3.5); the Artinian subterm order (Proposition 3.6); the power algebra; recognizability and $s$-recognizability with the CVCL20 closure results (Propositions 3.29, 3.30, 3.33); the substitution and iteration calculus (Lemmas 3.23, 3.25, 3.28, Corollary 3.17, Lemma 3.18); and the §4 regular-expression layer (Definition 4.1, Proposition 4.3, Corollary 4.4, Definition 4.6). The UA core and the substitution calculus are reusable beyond this mission. Contributions are welcome at every level — the definitions, the closure results, the auxiliary claims C1–C6, and either inclusion.
## Selected references
- L. Gong, R. Ruiz Mora, N. Sanmartín Vich, E. Cosme Llópez, *A Kleene theorem for free many-sorted algebras*, 2026.
- J. Climent Vidal, E. Cosme Llópez, *Congruence-based proofs of the recognizability theorems for free many-sorted algebras*, Journal of Logic and Computation 30(2) (2020), 561–633. https://arxiv.org/abs/1808.08217
- F. Gécseg, M. Steinby, *Tree Automata*, Akadémiai Kiadó, Budapest, 1984.
- R. McNaughton, H. Yamada, *Regular expressions and state graphs for automata*, IRE Transactions on Electronic Computers EC-9 (1960), 39–47.
- S. C. Kleene, *Representation of events in nerve nets and finite automata*, in *Automata Studies*, Princeton University Press, 1956, 3–42.
- J. Mezei, J. Wright, *Algebraic automata and context-free sets*, Information and Control 11 (1967), 3–29.
- S. Eilenberg, *Automata, Languages, and Machines, Vol. A*, Academic Press, New York, 1974.
## Motivation
Searching an unsorted list of $N$ items for a single marked entry takes $\Theta(N)$ queries
classically — there is no way to do better than checking items one at a time. Grover's algorithm
(Grover 1996) shows that a quantum computer solves the same problem in $\Theta(\sqrt N)$ queries,
a quadratic speedup that applies to any problem expressible as unstructured search over a black-box
oracle (this includes brute-forcing NP-complete problems and inverting one-way functions, which is
why post-quantum cryptography doubles key lengths to compensate). Unlike Shor's algorithm, Grover's
algorithm is provably optimal: Bennett–Bernstein–Brassard–Vazirani (1997) showed $\Omega(\sqrt N)$
queries are necessary for any quantum algorithm solving unstructured search, so the quadratic
speedup is the best any quantum algorithm can achieve on this problem.
## Setting
Model an $N$-item database as the standard basis of $E = \mathbb{C}^N$ (`EuclideanSpace ℂ (Fin N)`),
with inner product $\langle x,y\rangle = \sum_i \overline{x_i}\,y_i$. Fix a **marked index**
$w_0 \in \{0,\dots,N-1\}$. The algorithm starts in the **uniform superposition**
$$|s\rangle = \frac{1}{\sqrt N}\sum_{i} |i\rangle,$$
a unit vector assigning equal amplitude to every item. Two reflections drive the search:
* the **oracle** $O = I - 2|w_0\rangle\langle w_0|$, which flips the sign of the amplitude on the
marked item and leaves every other basis state fixed;
* the **diffusion operator** $D = 2|s\rangle\langle s| - I$ ("inversion about the mean"), the
reflection about $|s\rangle$.
One **Grover iterate** is $G = D\,O$. The algorithm applies $G$ some number of times to $|s\rangle$
and measures; a measurement outcome equal to $w_0$ counts as success.
## Formalization targets
### Milestone — the iterate is an isometry $$\|G x\| = \|x\| \quad \text{for every } x \in E$$
$O$ and $D$ are each reflections about a unit vector, hence isometries; their composition $G$ is
therefore norm-preserving on the whole space, not just at $|s\rangle$ — the minimal fact needed for
$G$ to be a legitimate quantum operation.
### Milestone — the rotation formula $$\langle w_0, G^k s\rangle = \sin\bigl((2k+1)\theta\bigr), \qquad \theta := \arcsin\!\left(\tfrac{1}{\sqrt N}\right)$$
The geometric heart of the algorithm (Nielsen & Chuang, *Quantum Computation and Quantum
Information*, Section 6.1.2): restricted to the real two-dimensional subspace spanned by $|w_0\rangle$
and the component of $|s\rangle$ orthogonal to it, $G$ acts as rotation by a fixed angle $2\theta$.
Each iterate therefore advances the amplitude on the marked state along $\sin((2k+1)\theta)$,
exactly as claimed, with $\theta = \arcsin(1/\sqrt N)$ the rotation's initial offset (since
$\langle w_0, s\rangle = 1/\sqrt N$ at $k=0$).
### Goal $$\exists\, k,\quad 1 - \tfrac1N \;\le\; \bigl|\langle w_0, G^k s\rangle\bigr|^2$$
Some number of iterations drives the probability of measuring the marked item above $1-1/N$. The
goal is stated existentially, without fixing $k$ to a specific rounded formula: the rotation angle
$(2k+1)\theta$ can be made to land within $\theta$ of $\pi/2$ by an appropriate integer $k$, and at
that point $\sin^2((2k+1)\theta) \ge \cos^2\theta = 1-\sin^2\theta = 1 - 1/N$. Pinning $k$ down to
an explicit closed form (e.g. the nearest integer to $\pi/(4\theta) - 1/2$) is one valid strategy,
but is not required by the statement — any correct choice of $k$, and any correct proof it works,
closes the goal.
## Significance
Grover's algorithm is the second landmark quantum algorithm after Shor's, and the one with the
widest applicability: because it treats the search space as a black box, it accelerates any
brute-force search — SAT solving, collision finding, and generic key search among them — which is
the concrete reason NIST's post-quantum cryptography standards double symmetric key lengths rather
than replacing them outright. The mathematics itself has been fully settled since 1996, including
matching optimality lower bounds; nothing here is open. What this mission adds is a **machine-
checked** derivation of the amplitude formula and success bound directly from the definitions of
the oracle and diffusion operators as concrete linear operators on `EuclideanSpace ℂ (Fin N)` —
Mathlib has the finite-dimensional inner product space and rank-one operator machinery this needs
(`InnerProductSpace.rankOne`, `EuclideanSpace.single`), but no existing formalization of the
algorithm itself.
## Difficulty
The obvious first attempt tries to track the full $N$-dimensional state vector through $k$
iterations. This is intractable in general: $G$'s action on an arbitrary basis vector depends on
its overlap with both $|w_0\rangle$ and $|s\rangle$. The move that makes the problem tractable is
recognizing that $G$ preserves the two-dimensional real subspace $\mathrm{span}\{|w_0\rangle,
|s\rangle\}$ — everything orthogonal to this plane is fixed by both $O$ and $D$, and inside the
plane $G$ is *exactly* a rotation matrix by angle $2\theta$. Establishing this invariance and then
tracking only the rotation angle (rather than the full vector) is the standard reduction, and the
one this mission's milestones are built around; skipping it and attempting a direct $N$-dimensional
induction does not scale.
## Formalization scope
Works over a general $N:\mathbb N$ together with a marked index $w_0 : \mathrm{Fin}\,N$ — no
assumption that $N$ is a power of two, since the rotation argument is agnostic to how the $N$ basis
states are physically encoded into qubits (that encoding is a separate, unrelated concern from the
search dynamics proved here). Supplying `w0 : Fin N` already forces $N \ge 1$; no separate
nonemptiness hypothesis is added. The oracle and diffusion operators are built directly from
Mathlib's `InnerProductSpace.rankOne` rather than an ad-hoc pointwise definition, so their
reflection structure (and hence unitarity) is visible from the definition itself. A trivializing
formalization is ruled out explicitly: the goal is stated as an existential over $k$ rather than a
fixed closed-form iteration count, so a correct proof must still exhibit a genuine successful $k$
and establish the bound — it cannot be discharged by an unrelated or degenerate choice. Contributions
extending this to multiple marked items, or proving the matching $\Omega(\sqrt N)$ lower bound
(Bennett–Bernstein–Brassard–Vazirani 1997), are welcome as follow-up missions.
## Selected references
- L. K. Grover, *A fast quantum mechanical algorithm for database search*, STOC 1996.
https://arxiv.org/abs/quant-ph/9605043
- M. A. Nielsen and I. L. Chuang, *Quantum Computation and Quantum Information*, Cambridge
University Press, 2000, Section 6.1.
- C. H. Bennett, E. Bernstein, G. Brassard, and U. Vazirani, *Strengths and Weaknesses of Quantum
Computing*, SIAM J. Comput. 26 (1997). https://arxiv.org/abs/quant-ph/9701001
The Power Method for Eigenvalue ComputationResearch Paper
## Motivation
Finding the eigenvalues of a large matrix or linear operator by computing its characteristic
polynomial is numerically unworkable: the roots of a degree-$n$ polynomial are exponentially
sensitive to small coefficient perturbations, and no closed-form root formula exists once
$n\ge5$. The **power method** avoids the polynomial entirely. Introduced in essentially its
modern form by Müntz (1913) and von Mises and Pollaczek-Geiringer (1929), and analyzed
rigorously alongside its shifted and inverse variants throughout the mid-20th century
(Wilkinson, *The Algebraic Eigenvalue Problem*, 1965), it remains, in the guise of one power
iteration per step, the engine inside PageRank, spectral clustering, and the Lanczos/Arnoldi
methods used to find eigenpairs of matrices too large to diagonalize directly.
## Setting
Let $E$ be a finite-dimensional inner product space over $\mathbb{k}\in\{\mathbb{R},\mathbb{C}\}$,
with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $T:E\to E$ be a
**self-adjoint** (symmetric) linear operator: $\langle Tx,y\rangle=\langle x,Ty\rangle$ for all
$x,y\in E$. The spectral theorem for finite-dimensional self-adjoint operators gives an
orthonormal basis $e_0,\dots,e_{n-1}$ of $E$ ($n=\dim E$) consisting of eigenvectors of $T$,
with real eigenvalues $\lambda_0,\dots,\lambda_{n-1}$ satisfying $Te_i=\lambda_ie_i$.
Call $\lambda_{i_0}$ **dominant** if $|\lambda_j|<|\lambda_{i_0}|$ for every $j\neq i_0$ — it is
then the unique eigenvalue of largest magnitude. Given a starting vector $x_0\in E$ with
coordinates $x_0=\sum_ic_ie_i$ in the eigenbasis, the power iterates are $T^kx_0$ for
$k=0,1,2,\dots$, and the **Rayleigh quotient** of $T$ at a nonzero vector $x$ is
$$R_T(x)=\frac{\operatorname{Re}\langle x,Tx\rangle}{\|x\|^2},$$
which recovers $\lambda_i$ exactly when $x$ is the eigenvector $e_i$.
## Formalization targets
### Iterate expansion $$T^kx_0=\sum_i\bigl(c_i\lambda_i^{\,k}\bigr)\,e_i$$
Rewriting the $k$-th power iterate in the eigenbasis: applying $T$ $k$ times raises each
coordinate's eigenvalue factor to the $k$-th power, since $T$ acts diagonally on the
eigenbasis. This is the algebraic core the rest of the argument rescales and takes limits of.
### Rescaled convergence $$\lambda_{i_0}^{-k}\,T^kx_0\;\longrightarrow\;c_{i_0}\,e_{i_0}\quad(k\to\infty)$$
Given a dominant eigenvalue $\lambda_{i_0}\neq0$ and $c_{i_0}\neq0$, dividing the expansion above
by $\lambda_{i_0}^k$ leaves the $i_0$-th term fixed at $c_{i_0}e_{i_0}$ while every other term is
multiplied by $(\lambda_j/\lambda_{i_0})^k\to0$, since $|\lambda_j/\lambda_{i_0}|<1$ for $j\neq
i_0$. This is the precise sense in which the power iterates "align" with the dominant
eigenvector.
### Goal — Rayleigh quotient convergence $$R_T\bigl(T^kx_0\bigr)\;\longrightarrow\;\lambda_{i_0}\quad(k\to\infty)$$
The practical output of the power method: the Rayleigh quotient of the (unrescaled) iterates
converges to the dominant eigenvalue itself, giving a numerically computable estimator that
needs no knowledge of $\lambda_{i_0}$ in advance. This is the weakest statement that captures
"the power method converges to the dominant eigenvalue" without hard-coding a convergence rate,
so it is the mission's goal.
## Significance
The power method is the template every practical large-scale eigenvalue algorithm departs from:
shifted inverse iteration, Rayleigh quotient iteration (with locally cubic convergence), the
QR algorithm, and Krylov subspace methods (Lanczos, Arnoldi) all begin from the same
diagonal-power argument formalized here, then add a trick — a shift, a change of subspace, an
orthogonalization step — to accelerate or extend it. The result itself is classical and
completely settled mathematically; there is no open question in the convergence theory of the
basic power method under the dominant-eigenvalue hypothesis used here. What this mission
contributes is a **machine-checked** version of that classical argument built directly on
Mathlib's existing finite-dimensional spectral theorem
(`LinearMap.IsSymmetric.eigenvalues`/`eigenvectorBasis`) — as of this writing, Mathlib's
InnerProductSpace/Spectrum.lean and Rayleigh.lean files contain the spectral decomposition
itself, and a Rayleigh quotient for `ContinuousLinearMap`, but not this convergence statement.
## Difficulty
The obvious first attempt is to bound $\|T^kx_0-\lambda_{i_0}^kc_{i_0}e_{i_0}\|$ by a naive
sum of norms and take limits termwise; this works for the *rescaled* sequence (Milestone 2) but
does not by itself give the Rayleigh-quotient limit, because $R_T$ is invariant only under
*nonzero* scalar rescaling, not under limits taken carelessly — one has to first establish that
the limit vector $c_{i_0}e_{i_0}$ is nonzero (using $c_{i_0}\neq0$), then invoke continuity of
$R_T$ away from $0$ to transport the `Tendsto` from the rescaled sequence to
$R_T(T^kx_0)=R_T(\lambda_{i_0}^{-k}T^kx_0)$. Getting the degenerate case $n=1$ right is the
other trap: with only one eigenvalue, the dominance hypothesis is vacuous, and if that
eigenvalue is allowed to be $0$ the rescaling $\lambda_{i_0}^{-k}$ divides by zero and the
rescaled-convergence statement becomes false — the formalization must therefore assume
$\lambda_{i_0}\neq0$ explicitly rather than deriving it from dominance alone.
## Formalization scope
The mission works with a general `RCLike 𝕜` field (real or complex $E$), a `LinearMap.IsSymmetric`
operator on a `FiniteDimensional` inner product space, and Mathlib's own `eigenvalues`/
`eigenvectorBasis` (which already fixes the eigenbasis and a specific, decreasing-by-value
ordering of eigenvalues — the formalization does not re-derive the spectral theorem). Dominance
is stated by magnitude (`|\lambda_j| < |\lambda_{i_0}|`), not by position in Mathlib's ordering,
since the dominant eigenvalue need not be the largest by value (it could be the most negative).
The starting vector $x_0$ is arbitrary subject to $c_{i_0}\neq0$; no normalization ($\|x_0\|=1$)
is imposed, since the Rayleigh quotient and the rescaled limit are both scale-invariant/
scale-equivariant. A trivializing formalization is ruled out explicitly: without both
$\lambda_{i_0}\neq0$ and $c_{i_0}\neq0$, the $n=1$, $T=0$ counterexample above makes the
rescaled-convergence statement false, so these are load-bearing hypotheses, not decoration.
Contributions on the two milestones (the algebraic iterate expansion, and the rescaled-limit
argument) are especially welcome, since they are reusable building blocks for any future mission
on shifted/inverse power iteration or Rayleigh quotient iteration.
## Selected references
- R. von Mises and H. Pollaczek-Geiringer, *Praktische Verfahren der Gleichungsauflösung*,
ZAMM, 1929.
- J. H. Wilkinson, *The Algebraic Eigenvalue Problem*, Oxford University Press, 1965.
- L. N. Trefethen and D. Bau III, *Numerical Linear Algebra*, SIAM, 1997 (Lecture 27: the power
method).
## Motivation
How short can a code for a data source be, if the code must still be uniquely decodable — if every string of concatenated codewords can be unambiguously split back into the original symbols? Shannon's 1948 source coding theorem answers this exactly: the entropy of the source is a hard lower bound on the average codeword length of *any* uniquely decodable code, and it is also achievable up to a one-symbol slack. Entropy is not just a measure of "average surprise" — it is the literal, tight answer to a combinatorial question about how densely symbols can be packed into strings without losing decodability. This is the theorem that gives Shannon's entropy its operational meaning, and it underlies every practical lossless compression scheme (Huffman coding, arithmetic coding, Lempel–Ziv) as the benchmark they approach.
**Timeline.**
- 1948 — Claude Shannon, "A Mathematical Theory of Communication" (*Bell System Technical Journal*), introduces entropy and proves the source coding theorem.
- 1949 — Leon Kraft's MIT master's thesis proves the combinatorial inequality (for prefix codes) that makes the theorem's achievability half constructive.
- 1956 — Brockway McMillan extends Kraft's inequality's necessity direction from prefix codes to the strictly larger class of *uniquely decodable* codes, giving the theorem its full generality.
## Setting
A source has a finite alphabet of symbols $\iota$, with at least two symbols, and probability distribution $p:\iota\to\mathbb R$ ($p_i>0$, $\sum_i p_i=1$). A code assigns to each symbol $i$ a codeword $c(i)$, a finite string over a $D$-ary code alphabet $\alpha$ ($D=|\alpha|\ge 2$); the code is *uniquely decodable* if every finite sequence of codewords is determined by its concatenation. The **entropy** of $p$ in base $D$ is
$$H_D(p) = -\sum_i p_i \log_D p_i.$$
The **expected codeword length** of $c$ under $p$ is $L(c) = \sum_i p_i \, |c(i)|$.
## Formalization targets
### Goal — Shannon's source coding theorem
$$\forall \text{ injective, uniquely decodable } c,\quad H_D(p) \le L(c), \qquad \exists \text{ such } c,\quad L(c) < H_D(p) + 1.$$
(For a source with $|\iota| \ge 2$ symbols — see *Formalization scope* for why the single-symbol case must be excluded.)
## Significance
**The result itself.** This theorem is the reason entropy is called entropy in an information-theoretic sense at all: it converts a quantity defined by an abstract formula ($-\sum p_i\log p_i$) into the exact answer to an operational question (minimum achievable expected code length), with a slack no worse than one symbol. It is the founding theorem of lossless source coding and the benchmark every practical compressor is measured against.
**Formalizing it.** Mathlib recently gained genuine information-theoretic coding content: `InformationTheory.UniquelyDecodable` and the *necessity* direction of the Kraft–McMillan inequality (McMillan's 1956 result: a uniquely decodable code's lengths satisfy $\sum_w D^{-|w|}\le 1$) are already proved, via a counting argument on concatenations of $r$ codewords. This mission builds directly on that foundation rather than duplicating it. What Mathlib does **not** have — and what this mission's milestones supply — is Kraft's original 1949 *sufficiency* direction (existence of a uniquely decodable code realizing any length assignment satisfying the Kraft sum bound), any notion of Shannon entropy for a general finite distribution, and the source coding theorem itself.
## Difficulty
The lower bound ($H_D(p)\le L(c)$) is the easier half: it follows from the Kraft–McMillan inequality (already in Mathlib) via Gibbs'/Jensen's inequality applied to the two probability-like sequences $p_i$ and $D^{-\ell_i}/K$ (where $K=\sum_j D^{-\ell_j}\le1$ is the Kraft sum) — a short, self-contained convexity argument.
The achievability half is the genuine construction. Given the ideal (generally non-integer) lengths $-\log_D p_i$, one rounds up to $\ell_i=\lceil -\log_D p_i\rceil$ (Shannon–Fano–Elias lengths); a one-line estimate shows $D^{-\ell_i}\le p_i$, so the Kraft sum of the rounded lengths is still $\le\sum_i p_i=1$, and the bound $\ell_i<-\log_D p_i+1$ gives $L(c)<H_D(p)+1$ immediately once a code with exactly these lengths is shown to exist. Producing that code is Kraft's sufficiency direction, and it needs an explicit construction: order the lengths, and assign to symbol $i$ the first $\ell_i$ digits of the $D$-ary expansion of the cumulative sum $\sum_{j<i} D^{-\ell_j}$. Verifying this assignment is injective, has the prescribed lengths, and is uniquely decodable (indeed prefix-free) is a careful but standard combinatorial argument — the main open piece of this mission.
## Formalization scope
The source alphabet $\iota$ must have at least two symbols ($|\iota|\ge 2$), not merely be nonempty. A single-symbol source forces $p\equiv 1$ and entropy $H_D(p)=0$, so the achievability conjunct would demand a codeword of length $0$ — but a uniquely decodable code can never contain the empty codeword (`InformationTheory.UniquelyDecodable.epsilon_not_mem`, provable from the definition: the empty string decodes ambiguously as zero or two copies of itself), so no admissible code exists and the theorem would be **false**, not merely hard, at $|\iota|=1$. The same defect breaks Kraft's sufficiency direction (Milestone 2) whenever *any* prescribed length is $0$, independent of $|\iota|$; that milestone accordingly requires every length strictly positive. With $|\iota|\ge2$ and full support, every $p_i<1$ strictly, so the Shannon–Fano lengths $\lceil-\log_D p_i\rceil$ are automatically all $\ge1$, and the achievability construction only ever needs Milestone 2 at positive lengths. The code alphabet $\alpha$ is likewise an arbitrary finite type (matching Mathlib's own `Fintype`/`Nonempty` conventions for the Kraft–McMillan file), with $|\alpha|\ge2$ required to keep `Real.logb` non-degenerate. The source distribution is required strictly positive ($p_i>0$) — the standard simplifying assumption (zero-probability symbols can always be dropped without loss). Unique decodability is stated exactly as Mathlib's `InformationTheory.UniquelyDecodable`, not re-derived from a "prefix code" definition, so the mission's results transport directly onto Mathlib's existing Kraft–McMillan file. A trivializing route to rule out: proving only the lower bound (citing Mathlib's inequality) while leaving the existential achievability half unaddressed would not be Shannon's theorem — the sandwich $H_D(p)\le L^*<H_D(p)+1$ is the theorem's actual content, and the lower bound alone (already essentially free from Mathlib) is not a novel contribution on its own.
Reusable output: the Kraft sufficiency construction (Milestone 2) is directly reusable for any future formalization of Huffman coding optimality, arithmetic coding, or the general "Kraft-inequality-achieving code exists" fact used throughout coding theory. Contributions are welcome starting from Milestone 2 (the open construction) or Milestone 3 (the Gibbs'-inequality lower bound, which only needs Milestone 1, already available via Mathlib).
## Selected references
- C. E. Shannon, "A Mathematical Theory of Communication," *The Bell System Technical Journal* 27 (1948), 379–423, 623–656.
- T. M. Cover and J. A. Thomas, *Elements of Information Theory*, 2nd ed., Wiley, 2006, Chapter 5 ("Data Compression"), §5.2 ("Kraft Inequality") and §5.4 ("Bounds on the Optimal Code Length," Theorem 5.4.1).
- L. G. Kraft, *A Device for Quantizing, Grouping, and Coding Amplitude-Modulated Pulses*, M.S. thesis, MIT, 1949.
- B. McMillan, "Two Inequalities Implied by Unique Decipherability," *IRE Transactions on Information Theory* 2:4 (1956), 115–116.
- Mathlib, `Mathlib.InformationTheory.Coding.UniquelyDecodable` and `Mathlib.InformationTheory.Coding.KraftMcMillan` (2026).
Dynamic Programming and Optimal Control IV: LQR and the Riccati EquationTextbook
## Motivation
The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of $(s,S)$ inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.
## Setting
Matrices $A \in \mathbb{R}^{n\times n}$, $B \in \mathbb{R}^{n\times m}$, $Q = C^\top C \succeq 0$, $R \succ 0$. The Riccati operator (`BertsekasRiccatiMap`)
$$F(P) = A^\top\big(P - P B (B^\top P B + R)^{-1} B^\top P\big) A + Q.$$
$(A,B)$ is **controllable** if $[B, AB, \dots, A^{n-1}B]$ has rank $n$ (`BertsekasControllablePair`); $(A,C)$ is **observable** if $(A^\top, C^\top)$ is controllable (`BertsekasObservablePair`). Separately, $g : \mathbb{R} \to \mathbb{R}$ is **$K$-convex** (`BertsekasKConvex`, Def. 4.2.1) if $K + g(z+y) \ge g(y) + \tfrac{z}{b}(g(y) - g(y-b))$ for all $z \ge 0$, $b > 0$, $y$.
## Target
$$\exists\, P \succ 0:\quad F(P) = P,\quad P \text{ unique among } P' \succeq 0,\quad F^{k}(P_0) \to P \ \ \forall P_0 \succeq 0,\quad \rho\big(A + BL\big) < 1,$$
with $L = -(B^\top P B + R)^{-1} B^\top P A$ — `BertsekasDP.riccati_convergence_stability` (goal). Milestones: Lemma 4.2.1(a)–(d) (`kconvex_of_convex`, `kconvex_combination`, `kconvex_expectation`, `kconvex_sS_structure`), culminating in the $(s,S)$ structure theorem for continuous coercive $K$-convex functions.
## Significance
The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of $(s,S)$-policy optimality. All results are classical and proved in the book; the formal work is new.
## Difficulty
The Riccati proof interleaves monotonicity of $F$ on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing $A$ fails: nothing is symmetric about $A + BL$. For Lemma 4.2.1(d), the difficulty is that $g$ is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.
## Formalization scope
Real matrices over `Fin n`; `Matrix.PosSemidef`/`PosDef`; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since $B^\top P B + R \succ 0$ along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via `spectrum ℂ` of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real $K$; note $K \ge 0$ is forced whenever it is satisfiable ($z = 0$), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 4.4.1, Def. 4.1.1, §4.2, Lemma 4.2.1.) http://www.athenasc.com/dpbook.html
- R. E. Kalman, Contributions to the theory of optimal control, *Bol. Soc. Mat. Mexicana* 5 (1960), 102–119.
- H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in *Mathematical Methods in the Social Sciences*, Stanford Univ. Press, 1960.
Capped Base-Stock Policies: A 2.33-ApproximationResearch Paper
## A performance guarantee for a simple replenishment rule
When replenishment takes several periods, an inventory decision commits stock before the demand that will consume it is known. Too much stock incurs holding costs; too little loses sales. An optimal decision can depend on the entire pipeline of outstanding orders. A rule with only two adjustable parameters is easier to implement, but its simplicity alone gives no guarantee on the cost it can incur.
**Capped base-stock policies** combine an inventory-position target with a maximum order quantity. The class was introduced and analyzed by [Xin (2021)](https://doi.org/10.1287/opre.2020.2019). The present target is the finite-lead-time guarantee in Linwei Xin's *Capped Base-Stock Policies: A 2.33-Approximation*, specifically the author-supplied manuscript with source label `thm-main`. A [public listing of the paper](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538) identifies the July 17, 2026 working paper; the supplied text is the authoritative version for this formalization.
## Demand, stock, and delayed orders
Periods are discrete. **Demand** is a sequence of independent, identically distributed nonnegative real random variables $D_t$ with finite, strictly positive mean $\mu$. The deterministic **lead time** is an integer $L\ge1$. Holding and lost-sales rates are $h>0$ and $p>0$.
At the beginning of period $t$, $I_t$ is on-hand inventory and $x_{1,t},\ldots,x_{L,t}$ are outstanding orders, with $x_{1,t}$ due immediately. That arrival is received, an order $q_t\ge0$ is placed, demand is realized, and costs are charged. The new order arrives $L$ periods later. The equations are
$$I_{t+1}=(I_t+x_{1,t}-D_t)^+,\qquad x_{i,t+1}=x_{i+1,t}\ (i<L),\qquad x_{L,t+1}=q_t.$$
Here $u^+=\max\{u,0\}$. Unfilled demand is lost rather than backlogged. With $\ell_t=(D_t-I_t-x_{1,t})^+$, the period cost is $hI_{t+1}+p\ell_t$. Initial inventory and every pipeline coordinate are zero. A **nonanticipative policy** chooses orders using only information available before the current demand; policies may depend on the entire observed past and on independent private randomization.
For a policy $\pi$, its **long-run expected average cost** is
$$C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[hI_{t+1}^\pi+p\ell_t^\pi],\qquad \mathrm{OPT}=\inf_{\pi\in\Pi}C(\pi).$$
The capped rule is $q_t=\min\{(S-I_t-\sum_{i=1}^Lx_{i,t})^+,r\}$ for finite $S,r\ge0$. Write $C^*_{\rm CBS}=\inf_{S,r\ge0}C(\pi_{S,r})$. Ordinary base stock is already included by taking $r=S$; no infinite order cap is required.
## Formalization targets
For $0\le r\le\mu$ and $m\ge1$, set
$$I_r^m=\max_{0\le k\le m}\sum_{i=1}^k(r-D_i),\qquad G_m(r,z)=\mathbb E\left[\left(I_r^m+\sum_{i=1}^m(D_i-r)-z\right)^+\right].$$
Empty sums are zero. The **lower certificate** is
$$\underline C=\inf\{hz+p(\mu-r):0\le r\le\mu,\ z\ge0,\ G_L(r,z)\le L(\mu-r),\ G_{L+1}(r,z)\le(L+1)(\mu-r)\}.$$
The pair $(0,0)$ is feasible. Both horizon constraints are retained. With
$$\kappa_L=1+\frac{4L^2}{(L+1)(3L-1)},$$
the goal is Theorem 1's complete assertion:
$$C^*_{\rm CBS}\le\kappa_L\underline C,\qquad C^*_{\rm CBS}\le\kappa_L\mathrm{OPT}\le\frac73\mathrm{OPT}.$$
The exact rational constant is used; the title's 2.33 is a rounded description. Multiplicative inequalities also make sense when the optimal cost is zero.
Five supporting targets reproduce selected source statements: Proposition 1's lower-certificate bound; Proposition 2's finite-cap cost conclusion; Lemma 2's bound on a consecutive block in the greedy recursion; Proposition 3's ordinary-base-stock cost bound; and Proposition 4's two-branch inequality. The finite-cap and ordinary-base-stock parameters remain exactly $(S,r)=((L+1)r+z,r)$ and $S=(L+1)r+2z$, respectively. Labels accompany the printed numbering so the supplied source is unambiguous.
## What completing the mission establishes
The result gives a uniform cost guarantee for this policy class across all positive holding and penalty rates, every positive integer lead time, and arbitrary nonnegative demand laws with finite positive mean. It bounds the infimum of costs over the policy parameters; it does not by itself provide an algorithm for selecting parameters or assert that the infimum is attained. At $L=1$ the displayed coefficient is 2, while its uniform upper bound is $7/3$.
The manuscript supplies mathematical proofs. This mission asks for checked proofs of their formal statements. Compiling the declarations confirms that they are well formed, not that the claims are proved. A completed development would provide reusable delayed-inventory dynamics, measurable history policies, average-cost optimization objects, finite-horizon demand envelopes, and policy-comparison results.
## Where the formal work lies
The pipeline carries consequences of past decisions across multiple demand periods. Nonanticipativity and independence must be stated precisely before expectation and convexity arguments can be used. Also, existence of a stationary distribution alone does not identify its expected cost with a long-run cost from an empty initial system. The manuscript invokes stationary results from prior inventory work, including [Xin and Goldberg (2016)](https://doi.org/10.1287/opre.2016.1514), and uses stationary CBS quantities in intermediate arguments. Their needed hypotheses and connections to the original objective require proof within a complete development.
The two cost bounds depend on both coordinates of a feasible lower-certificate pair. Losing either horizon constraint changes that certificate. Replacing it with an arbitrary scalar lower bound or assuming the policy comparisons would remove substantive parts of the result.
## Formalization scope and conventions
Stock, orders, and demand take arbitrary nonnegative real values. Time is represented from zero in the operational model, corresponding to period one in the manuscript. The formal representation uses a canonical probability model with independent demand coordinates and an independent uniform private seed; measurable time-dependent decision functions use only preceding demands and that seed. Connecting arbitrary standard-Borel randomized controls to this canonical realization is a representation obligation. The zero-start optimum ranges over these general history policies, not only stationary or capped policies.
Expected nonnegative costs, their upper limits, and cost infima are represented in the extended nonnegative reals. Thus a policy with infinite expected cost does not acquire a fictitious zero value through a totalized real integral. The finite-horizon envelope expectations use the original integrable demand law. The greedy lemma uses integer-indexed sequences so subtraction of earlier times has no natural-number truncation; its blocks are nonempty, as required to define their maximum.
Definitions contain no unproved facts. In particular, stationarity, convergence from the empty initial state, lower bounds, and upper policy comparisons are not fields assumed by the model. Contributions to these intermediate obligations and to any of the five source targets support the central theorem.
## Selected references
- Linwei Xin, *Capped Base-Stock Policies: A 2.33-Approximation*, working paper, 2026. [SSRN listing](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538). Author-supplied LaTeX is authoritative: Theorem 1 (`thm-main`), Proposition 1 (`lemma-lb`), Proposition 2 (`prop-finite-cap-bound`), Lemma 2 (`lem-greedy-window`), Proposition 3 (`prop-base-stock-bound`), Proposition 4 (`lem-two-branch`). Source SHA-256: `f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a`.
- Linwei Xin, *Technical Note—Understanding the Performance of Capped Base-Stock Policies in Lost-Sales Inventory Models*, Operations Research 69(1), 61–70, 2021. [DOI](https://doi.org/10.1287/opre.2020.2019).
- Linwei Xin and David A. Goldberg, *Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models*, Operations Research 64(6), 1556–1565, 2016. [DOI](https://doi.org/10.1287/opre.2016.1514).
Dynamic Programming and Optimal Control VII: Infinite Horizon ProblemsTextbook
## Motivation
Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.
## Setting
States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$; finite nonempty control sets $U(i)$; costs $g(i,u)$; sub-stochastic transitions $p_{ij}(u) \ge 0$, $\sum_j p_{ij}(u) \le 1$, the deficit being the termination probability (`BertsekasSSPModel`). Operators
$$(T_\mu J)(i) = g(i,\mu(i)) + \sum_j p_{ij}(\mu(i)) J(j), \qquad (TJ)(i) = \min_{u \in U(i)}\Big[g(i,u) + \sum_j p_{ij}(u) J(j)\Big]$$
(`BertsekasSSPPolicyOp`, `BertsekasSSPBellmanOp`), $N$-stage costs by backward recursion with policy shift (`BertsekasSSPNCost`), and the survival mass $P\{x_m \ne t\}$ (`BertsekasSSPSurvival`). **Assumption 7.2.1**: for some $m > 0$, every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (`BertsekasDiscounted*`); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (`BertsekasSSPAvoidProb`).
## Target
Under Assumption 7.2.1, there is a vector $J^*$ with
$$T^k J_0 \to J^* \ \ \forall J_0, \qquad J^* = T J^* \text{ uniquely}, \qquad J^*(i) \le J_\pi(i) = \lim_N J^N_\pi(i) \ \ \forall \pi \text{ admissible},$$
and a stationary policy attaining $J^*$ — `BertsekasDP.ssp_main_theorem` (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.
## Significance
These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$-stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.
## Difficulty
$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$-stage contraction, uniformly over the finitely many $m$-stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$-stage costs for *nonstationary* policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$). For the average-cost results the associated-SSP construction (stop on reaching $s$) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.
## Formalization scope
Finite states `Fin n`, finite control type, constraint sets as `Finset`s with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is `Tendsto` in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real `liminf` and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
- D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, *Math. Oper. Res.* 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
- M. L. Puterman, *Markov Decision Processes*, Wiley, 1994. https://doi.org/10.1002/9780470316887
Dynamic Programming and Optimal Control V: LQG and Certainty EquivalenceTextbook
## Motivation
The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.
## Setting
Linear dynamics and measurements
$$x_{k+1} = A_k x_k + B_k u_k + w_k, \qquad z_k = C_k x_k + v_k,$$
with quadratic cost $\mathbb{E}\big[x_N^\top Q_N x_N + \sum_{k<N}(x_k^\top Q_k x_k + u_k^\top R_k u_k)\big]$, $Q_k \succeq 0$, $R_k \succ 0$. The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (`BertsekasLQGModel`, `BertsekasLQGSample`, `BertsekasLQGProb`). A **policy** maps the realized measurement history $(z_0,\dots,z_k)$ to $u_k$; the closed-loop process is `BertsekasLQGTraj`, the expected cost `BertsekasLQGCost`. The estimator $\mathbb{E}[x_k \mid I_k]$ is an explicit conditional average (`BertsekasCondExpVec`, `BertsekasLQGEstimate`); the gains $L_k$ come from the time-varying Riccati recursion (`BertsekasLQGRiccati`, `BertsekasLQGGain`).
## Target
$$\pi^*(I_k) = L_k\, \mathbb{E}[x_k \mid I_k] \ \text{ along its own trajectories} \quad\Longrightarrow\quad J(\pi^*) \le J(\pi)\ \ \forall \pi,$$
— `BertsekasDP.lqg_certainty_equivalence` (goal). Milestone: Lemma 5.2.1 in pointwise form — the error $x_k - \mathbb{E}[x_k \mid I_k]$ is the same under any two policies, outcome by outcome (`lqg_estimation_error_policy_independent`).
## Significance
This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.
## Difficulty
The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.
## Formalization scope
Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of $R_k$ makes every matrix inverse in the gains genuine. Measurement noise covariance is *not* assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (§5.2, Lemma 5.2.1.) http://www.athenasc.com/dpbook.html
- P. D. Joseph, J. T. Tou, On linear control theory, *Trans. AIEE* 80 (1961), 193–196. https://doi.org/10.1109/TAI.1961.6371743
- T. L. Gunckel, G. F. Franklin, A general solution for linear sampled-data control, *J. Basic Eng.* 85 (1963), 197–201. https://doi.org/10.1115/1.3656559
Dynamic Programming and Optimal Control III: The Minimum PrincipleTextbook
## Motivation
The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero — no HJB equation, no adjoint equations, no maximum principle — which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.
## Setting
Minimize, over admissible pairs, the cost
$$h(x(T)) + \int_0^T g(x(t), u(t))\,dt \quad\text{s.t.}\quad \dot x(t) = f(x(t), u(t)),\; x(0) = x_0,\; u(t) \in U \subseteq \mathbb{R}^m,$$
with $f, g, h$ continuously differentiable (`BertsekasCTModel`). Admissible controls are piecewise continuous on $[0,T]$ — formalized as: bounded image and continuous off a finite set (`BertsekasPiecewiseContinuousOn`) — and state trajectories are continuous, satisfying the ODE off a finite set (`BertsekasCTAdmissibleFrom`, parametrized by an arbitrary start $(t_0, \xi)$). The Hamiltonian is $H(x,u,p) = g(x,u) + \langle p, f(x,u)\rangle$ (`BertsekasHamiltonian`).
## Target
For an optimal admissible pair $(u^*, x^*)$: there exist an adjoint $p$ and a constant $c$ with
$$\dot p(t) = -\nabla_x H(x^*(t), u^*(t), p(t)), \quad p(T) = \nabla h(x^*(T)),$$
$$u^*(t) \in \arg\min_{u \in U} H(x^*(t), u, p(t)), \qquad H(x^*(t), u^*(t), p(t)) = c,$$
away from finitely many times — `BertsekasDP.pontryagin_minimum_principle` (goal). Milestones: Prop. 3.2.1 (`hjb_sufficiency_of_continuous`), Lemma 3.3.1 (`envelope_gradient_lemma`), Prop. 3.3.2 (`discrete_minimum_principle`).
The HJB milestone carries the hypotheses that $f$ and $g$ are jointly continuous — the consequence of the §3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is $0$.
## Significance
The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem — the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument — the book's own HJB-based derivation is explicitly informal.
## Difficulty
For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function — neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is *not* a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating $t \mapsto V(t, x(t))$ along a trajectory that satisfies the ODE only off a finite set, then integrating.
## Formalization scope
States and controls in `EuclideanSpace ℝ (Fin n)` / `(Fin m)`; gradients in Mathlib's `gradient`; the ODE and adjoint via `HasDerivAt` off a finite exceptional set; costs via `intervalIntegral`. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable — the junk-value escape (non-integrable integrand ⇒ integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). $U$ is an arbitrary set — no compactness or convexity is assumed in the goal.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Ch. 3.) http://www.athenasc.com/dpbook.html
- L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, *The Mathematical Theory of Optimal Processes*, Interscience, 1962.
- W. H. Fleming, R. W. Rishel, *Deterministic and Stochastic Optimal Control*, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7
## Motivation
Every introductory number theory course opens with the same fact: the integers factor into primes in exactly one way. Euclid's *Elements* (Book IX, Proposition 14) already proves a form of it for the case of two factorizations sharing no further structure, but the theorem is not stated in full generality — with existence *and* uniqueness as a single package — until Gauss's *Disquisitiones Arithmeticae* (1801, Art. 16). Every standard modern treatment restates it as the opening theorem of the subject: Hardy & Wright, *An Introduction to the Theory of Numbers* (Theorem 2), and Apostol, *Introduction to Analytic Number Theory* (1976, Theorems 1.9–1.10), both prove it in the first chapter, before anything else is developed. The reason is structural, not pedagogical convenience: gcd, lcm, multiplicative functions, the notion of "the" prime factorization of an integer, and the entire multiplicative structure of $\mathbb{Z}$ depend on it being true. Mathlib itself packages the general statement as `UniqueFactorizationMonoid`, of which $\mathbb{N}$ is one instance — this mission asks for the classical, elementary argument specific to $\mathbb{N}$, in the two-part shape every textbook gives it.
## Setting
A **prime** $p \in \mathbb{N}$ is a natural number $p \geq 2$ whose only divisors are $1$ and $p$ (Mathlib's `Nat.Prime`). A **factorization** of $n \in \mathbb{N}$ is represented here as a **multiset** $l$ of natural numbers — an unordered collection that tracks multiplicity but not order, so that two factorizations differing only by a reordering of their factors are already identified as the same multiset, with no separate permutation argument needed. Write $l.\mathrm{prod} = \prod_{p \in l} p$ for the product of the elements of $l$ with multiplicity, under the convention that the empty multiset has product $1$. The theorem concerns multisets all of whose elements are prime.
## Formalization targets
### Goal — unique factorization
$$
\forall\, n \neq 0,\quad \exists!\, l : \mathrm{Multiset}\ \mathbb{N},\ \left(\forall p \in l,\ p \text{ prime}\right) \wedge l.\mathrm{prod} = n.
$$
For every nonzero $n$ there is exactly one multiset of primes whose product is $n$. This is the capstone: existence and uniqueness combined into the single statement every textbook eventually asserts.
### Milestone 1 — existence
$$
\forall\, n \neq 0,\quad \exists\, l : \mathrm{Multiset}\ \mathbb{N},\ \left(\forall p \in l,\ p \text{ prime}\right) \wedge l.\mathrm{prod} = n.
$$
Every nonzero natural number is *a* product of primes (Apostol, Theorem 1.9). This alone says nothing about how many such multisets there might be.
### Milestone 2 — uniqueness
$$
\left(\forall p \in l_1,\ p \text{ prime}\right) \wedge \left(\forall p \in l_2,\ p \text{ prime}\right) \wedge l_1.\mathrm{prod} = n = l_2.\mathrm{prod} \ \implies\ l_1 = l_2.
$$
Any two multisets of primes with the same product are equal (Apostol, Theorem 1.10). Combined with Milestone 1, this gives the Goal.
## Significance
**The result itself.** Unique factorization is what makes "the prime factorization of $n$" a well-defined object rather than a choice. Every downstream elementary and analytic number theory construction leans on it: $\gcd(a,b)$ and $\mathrm{lcm}(a,b)$ computed via shared prime exponents, multiplicative arithmetic functions ($\varphi$, $\sigma$, $\mu$) defined by their values on prime powers, the Euler product for $\zeta(s)$, and $p$-adic valuations. Without it, none of these constructions are canonical.
**Formalizing it.** The general statement is already machine-checked in Mathlib as an instance of `UniqueFactorizationMonoid` (and concretely realized for $\mathbb{N}$ via `Nat.factors`/`Nat.factors_unique`), so this is not open mathematics. What this mission asks for is the specific, elementary two-lemma argument — strong induction for existence, Euclid's lemma plus strong induction for uniqueness — spelled out for $\mathbb{N}$ with the `Multiset` representation used here, rather than a one-line appeal to the packaged Mathlib result. A solution that simply repackages `Nat.factors_unique` and its companions is a legitimate route (nothing here is designed to block it), but the more valuable contribution is the self-contained classical proof, since that is what a reader of Apostol or Hardy & Wright expects to see reconstructed.
## Difficulty
For **existence**, ordinary induction on $n$ does not immediately work: if $n$ is composite, $n = ab$ with $1 < a, b < n$, and the inductive hypothesis is needed for *both* $a$ and $b$ at once, neither of which is simply $n - 1$. The fix is strong (well-founded) induction on $n$, splitting into the prime case (trivial single-element multiset) and the composite case (combine the two multisets for $a$ and $b$).
For **uniqueness**, the natural first attempt — "cancel a common prime factor from both sides and recurse" — silently assumes that the *same* prime appears in both multisets, which is exactly what needs to be proved. The step that actually does the work is **Euclid's lemma**: if a prime $p$ divides a product $l_2.\mathrm{prod}$, it divides one of the factors of $l_2$. This is not a restatement of primality (irreducibility, "no nontrivial divisors") but a genuinely separate fact about $\mathbb{N}$ that requires either Bézout's identity or a well-ordering argument to establish; conflating "prime" with "has this divisibility property" is the standard trap for a first attempt at this proof.
## Formalization scope
The statement is specific to $\mathbb{N}$ (not $\mathbb{Z}$ or a general `UniqueFactorizationMonoid`), and factorizations are represented as `Multiset ℕ` rather than `List ℕ` up to permutation — this is a deliberate choice that folds "unique up to reordering" directly into multiset equality. The hypothesis is $n \neq 0$, not $n > 1$: the case $n = 1$ is included, and its unique witness is the *empty* multiset, since the empty product is $1$ and no nonempty multiset of primes (each $\geq 2$) can have product $1$. $n = 0$ is excluded because no multiset of natural numbers has product $0$ under this convention (every prime is $\geq 2$, and the empty product is $1$), so no factorization of $0$ exists to be unique.
No auxiliary platform `Definitions` are required — the statement is expressed entirely in terms of `Nat.Prime` and `Multiset.prod` from Mathlib. Reusable contributions welcome beyond the two milestones: an explicit construction of the canonical *sorted* `List ℕ` factorization (`Nat.factors`-style) connecting this multiset formulation to the more computational list representation, or a generalization of the uniqueness argument to an explicit statement and proof of Euclid's lemma as a standalone milestone.
## Selected references
- C. F. Gauss, *Disquisitiones Arithmeticae*, 1801, Art. 16.
- G. H. Hardy and E. M. Wright, *An Introduction to the Theory of Numbers*, 6th ed., Oxford University Press, 2008, Theorem 2.
- T. M. Apostol, *Introduction to Analytic Number Theory*, Springer, 1976, Theorems 1.9–1.10.
- The Mathlib Community, *Mathlib4*, `Mathlib.RingTheory.UniqueFactorizationDomain`, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/UniqueFactorizationDomain.html
Formalizing an 8-Vertex Candidate Counterexample to the Geodesic-Cycle Assignment Problem (OPG-500)Open Problem
[VM-STATUS-20260908-R05-PROVED]
> **Status update (2026-09-08):** The root theorem `OPG500Counterexample.eight_vertex_counterexample` is now **Proved** by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`. The historical text below describes the mission as it stood before formal closure.
---
## Motivation and historical context
Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.
Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.
The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked `candidate_only`: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.
## Setting
Let $G$ be a finite simple graph. A **positive edge-length assignment** is a function
$$
\ell:E(G)\longrightarrow \mathbb R
$$
such that $\ell(e)>0$ for every edge $e$. The length of a finite path or cycle is the sum of the lengths of its edges.
A simple cycle $C$ is **$\ell$-geodesic** when, for every pair of vertices $x,y$ on $C$, at least one of the two $x$–$y$ arcs of $C$ has length equal to the shortest-path distance between $x$ and $y$ in $G$. Equivalently, there is no $x$–$y$ path in $G$ whose length is strictly smaller than both $x$–$y$ arcs of $C$. The definition concerns vertices of the cycle and permits ties between shortest paths.
A simple cycle is **peripheral** when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.
Fix the graph $H$ on vertices $0,1,\ldots,7$. The vertices $0,1,2,3$ induce $K_4$. For each $i\in\{0,1,2,3\}$, set $y_i=7-i$ and join $y_i$ to exactly the three core vertices other than $i$. The four vertices $y_i$ are pairwise nonadjacent. Thus the frozen edge set is
$$
\{01,02,03,04,05,06,12,13,14,15,17,23,24,26,27,35,36,37\}.
$$
The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.
## Formalization targets
### Main target: the universal eight-vertex obstruction
Formalize the following statement for the fixed graph $H$:
$$
H\text{ is 3-connected}\quad\text{and}\quad
\forall\ell:E(H)\to\mathbb R_{>0},\;
\exists C,\; C\text{ is an $\ell$-geodesic simple cycle of $H$ and is not peripheral}.
$$
The existential cycle may depend on $\ell$. The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.
### Supporting targets
The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of $H$, the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.
## Significance
A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.
A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.
Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.
## Difficulty
The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.
The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.
## Formalization scope
The Lean development will use `Fin 8` for the vertices of $H$ and a `SimpleGraph` representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.
The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.
Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.
## Selected references
- A. Georgakopoulos and P. Sprüssel, *Geodetic topological cycles in locally finite graphs*, Electronic Journal of Combinatorics 16 (2009), R144. Section 3.1, Theorem 3.1; Section 5, Problem 3. https://arxiv.org/abs/0911.3999v1
- Open Problem Garden, *Geodesic cycles and Tutte's Theorem*, problem statement and vertex-based definition. https://www.openproblemgarden.org/op/geodesic_cycles_and_tuttes_theorem
- W. T. Tutte, *How to draw a graph*, Proceedings of the London Mathematical Society 13 (1963), 743–768. Cited as reference [18] by Georgakopoulos and Sprüssel for peripheral-cycle generation.
- Vibe Mathing, frozen OPG-500 candidate repository at commit `a41fe59b4535851ea55f6e868e938b9aaf81e924`. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924
## 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
Coherent Measures of Risk: the axioms, and why Value-at-Risk fails themResearch Paper
## Motivation
In 1999 Artzner, Delbaen, Eber and Heath asked what a *risk measure* ought to satisfy, wrote
down four axioms, and observed that the industry standard of the day -- Value-at-Risk -- fails
one of them. The failing axiom is subadditivity: merging two positions should never require more
capital than holding them apart. VaR can violate it, so under VaR a diversified book can appear
riskier than its parts.
That observation did not stay academic. It is the reason the Basel framework moved its market-risk
capital standard from Value-at-Risk to Expected Shortfall. Few results in mathematical finance
have had a more direct regulatory consequence, and the mathematics is elementary enough to state
completely.
## Setting
A position is a payoff `X : Fin (n+1) -> R` across finitely many equally-weighted states, and a
risk measure `rho` sends it to the capital that must be added to make it acceptable. Following
Definition 2.4 of the paper, `rho` is **coherent** when it is translation-invariant, subadditive,
positively homogeneous and monotone. Nonemptiness of the state space is carried in the index type
so the worst case is always attained; no probability measure is needed for these four axioms,
which is faithful to the paper -- Artzner et al. state T, S, PH and M without reference to one.
Value-at-Risk is defined here at an integer tolerance `k` rather than a probability level, which
keeps the quantile unambiguous on a finite space: `VaR X k` is the least capital leaving at most
`k` states in loss, corresponding to level `k/(n+1)`.
## The goal
The mission's goal theorem is the negative result: **Value-at-Risk is not subadditive.** A witness
is 25 equiprobable states with `X` losing 100 in state 0 alone and `Y` losing 100 in state 1
alone. Each has one losing state in twenty-five, so at tolerance `k = 1` both have `VaR = 0`;
their sum loses in two states, exceeding the tolerance, so `VaR (X+Y) 1 = 100 > 0 + 0`. The
witness was checked numerically before this mission was drafted; what is open is the Lean proof.
The milestones establish the positive contrast on the same footing: worst-case risk, the most
conservative measure, satisfies all four axioms, so the failure is specific to VaR rather than
inherent to risk measurement.
## Source
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, *Coherent Measures of Risk*, Mathematical
Finance **9** (1999) 203-228. Axioms T, S, PH and M are Definition 2.4; the failure of
subadditivity for VaR and the diversification consequence are discussed in Section 3.
Kelly's Criterion: the optimal fraction for an even-money betResearch Paper
## 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](https://en.wikipedia.org/wiki/Bochner%27s_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.
## Motivation: approximating entire continuous functions
An approximation result must specify both the allowed approximants and the error being controlled. Matching finitely many values is different from approximating a function everywhere with one error bound. **Polynomial approximation** on a closed interval provides a model: finitely described functions can approach an arbitrary continuous function uniformly, without assuming that the function has derivatives or a convergent power-series expansion. [Lebl, Theorem 11.7.1](https://www.jirka.org/ra/html/sec_stoneweier.html).
The broader question replaces polynomials with a collection of continuous functions closed under algebraic operations. The relevant issue is which properties of that collection guarantee approximation of every continuous function. This distinguishes a useful approximation family from one that cannot detect some points or cannot approximate nonzero values at a particular point. The six targets follow the real and complex approximation results in §11.7 of Jiří Lebl’s *Basic Analysis*, Volume II. [Source section](https://www.jirka.org/ra/html/sec_stoneweier.html).
## Setting: function algebras and uniform error
A **metric space** is a set $X$ with a nonnegative, symmetric distance $d(x,y)$ that vanishes exactly when $x=y$ and satisfies the triangle inequality. It is **compact** if every cover by open sets has a finite subcover. Let $K$ be either the real numbers $\mathbb R$ or the complex numbers $\mathbb C$, and write $C(X,K)$ for the continuous functions from $X$ to $K$. Products, sums, and scalar multiplication of functions are taken pointwise. The notation $K[t]$ denotes polynomials in one indeterminate $t$ with coefficients in $K$, and $[a,b]=\{x\in\mathbb R:a\le x\le b\}$ for real endpoints $a,b$.
A **non-unital function algebra** $A$ contains the zero function and is closed under these three operations. It need not contain the constant function $1$. It **separates points** if, whenever $x\ne y$, some $g\in A$ satisfies $g(x)\ne g(y)$. It **vanishes nowhere** if, for each $x$, some $g\in A$ satisfies $g(x)\ne0$. The witness may depend on $x$; one everywhere nonzero function is not specified. A complex algebra is **self-adjoint** if it contains the pointwise complex conjugate of every member. These conventions retain the source’s non-unital setting. [Lebl, Definitions 11.7.5, 11.7.7, and 11.7.15](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Uniform convergence** of $f_n$ to $f$ means
$$
\forall\varepsilon>0\;\exists N\in\mathbb N\;\forall n\ge N\;\forall x\in X,
\qquad |f_n(x)-f(x)|<\varepsilon.
$$
Here $|\cdot|$ is real absolute value or complex modulus. On compact $X$, the **closure** $\overline A$ in $C(X,K)$ uses this uniform topology; saying that $A$ is **dense** means $\overline A=C(X,K)$. [Mathlib’s compact-domain convergence interface](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/CompactConvergence.lean).
## Formalization targets
The first four statements supply approximation, normalization, closure, and interpolation results. The final two state density, with the complex result as the goal. No approximation rate or degree bound is prescribed.
**Theorem 11.7.1.** For $K=\mathbb R$ and for $K=\mathbb C$, respectively,
$$
f\in C([a,b],K)\Longrightarrow
\exists(p_n)_{n\in\mathbb N}\subseteq K[t],\qquad
p_n\longrightarrow f\ \text{uniformly on }[a,b].
$$
The real clause requires real coefficients. Complex polynomials are evaluated at the complex embedding of the real argument. [Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Corollary 11.7.4.** For $a\ge0$,
$$
\exists(p_n)\subseteq\mathbb R[t],\qquad
(\forall n,\ p_n(0)=0)\ \land\
p_n\longrightarrow |\cdot|\ \text{uniformly on }[-a,a].
$$
[Source corollary](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Proposition 11.7.6.** For compact metric $X$ and either scalar field,
$$
A\text{ a non-unital algebra in }C(X,K)
\Longrightarrow\overline A\text{ is such an algebra}.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Proposition 11.7.11.** For an arbitrary set $X$, without topology, let $A\subseteq K^X$ be an algebra separating points and vanishing nowhere. Then
$$
\forall x\ne y\;\forall c,d\in K\;\exists f\in A,
\qquad f(x)=c\ \land\ f(y)=d.
$$
Both scalar fields belong to this single target. [Source proposition](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Theorem 11.7.12.** For compact metric $X$,
$$
A\subseteq C(X,\mathbb R)\text{ an algebra separating points and vanishing nowhere}
\Longrightarrow\overline A=C(X,\mathbb R).
$$
[Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Theorem 11.7.16, complex Stone–Weierstrass.** For compact metric $X$,
$$
\begin{gathered}
A\subseteq C(X,\mathbb C)\text{ a self-adjoint algebra},\\
A\text{ separates points and vanishes nowhere}
\end{gathered}
\Longrightarrow\overline A=C(X,\mathbb C).
$$
[Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
## Significance: density without an assumed unit
The density conclusion turns structural conditions on an approximation family into a statement about every continuous target function. Exact interpolation only controls specified values at two points; density controls all points simultaneously to any positive tolerance. The normalized absolute-value result retains a constraint on every approximating polynomial, rather than obtaining normalization only in the limit.
These are established theorems, not open conjectures. Mathlib already has machine-checked polynomial approximation, unital Stone–Weierstrass results, and non-unital algebra infrastructure. The six source-level statements also have standalone proofs checked in the pinned Lean environment. The contribution is an explicit textbook-facing non-unital formulation, with both scalar fields and the source’s normalization and interpolation clauses retained. It is not a claim to the first formalization of Stone–Weierstrass. [Polynomial approximation](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/Weierstrass.lean), [Stone–Weierstrass library](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean).
## Difficulty: local distinctions do not give uniform control
Point separation alone does not say that an algebra can approximate a nonzero value everywhere it is requested. A family may distinguish pairs of points while all its members vanish at one fixed point. Nor does interpolation at a pair of points establish a uniform error bound over an entire compact domain. These are distinct quantifier requirements.
Requiring $1\in A$ would remove the source’s non-unital case instead of resolving it. Likewise, complex scalar multiplication does not itself impose closure under conjugation. The formal difficulty is to preserve all these distinctions while connecting bundled algebras, continuous maps, and uniform closure. A direct use of the library’s unital theorem has an additional hypothesis that is absent here. [Library theorem hypotheses](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean).
## Formalization scope
Namespace `LeblRA` uses `NonUnitalSubalgebra`, `ContinuousMap`, real and complex polynomials, `TendstoUniformly`, and topological `closure`. Domains are arbitrary universe-polymorphic types, with metric and compactness structures only where the source requires them. The interpolation target has neither. Conjugation is the pointwise `star` operation on complex continuous maps.
The conventional algebra structure includes zero, but not an assumed unit. Empty compact spaces are allowed. Polynomial sequence indices start at zero. The interval approximation theorem permits arbitrary endpoints, including a singleton or an empty interval; the absolute-value corollary assumes $a\ge0$ and includes $a=0$. Neither finite-dimensional approximation spaces nor degree bounds are imposed. Replacing density by a finite-domain special case, adding a constant-one hypothesis, or assuming density itself would change the targets.
Reusable infrastructure includes non-unital subalgebras and their closures, polynomial evaluation, compact-domain uniform convergence, and real/complex continuous function spaces. The environment is Lean 4.29.0-rc3 with Mathlib revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Source-faithful alternative proofs and reusable interfaces between these existing structures are welcome; extra alias definitions are unnecessary. [Non-unital algebra structures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean), [topological closures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Algebra/NonUnitalAlgebra.lean).
## Selected references
- Jiří Lebl, *Basic Analysis: Introduction to Real Analysis*, Volume II, author-published open textbook, version 6.3, 2026, §11.7. [Section text](https://www.jirka.org/ra/html/sec_stoneweier.html); [edition information](https://www.jirka.org/ra/).
- The Mathlib community, *Mathlib*, Lean mathematical library, revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`, 2026. [Polynomial approximation](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/Weierstrass.lean), [Stone–Weierstrass and zero-preserving continuous maps](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean), [non-unital algebra closures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Algebra/NonUnitalAlgebra.lean).
## Motivation: limits of families of functions
Analysis often produces a sequence of candidate functions rather than a finished function. A useful existence theorem must say when some candidates approach a single limit everywhere with a common error bound. Ordinary boundedness is insufficient: Lebl gives bounded continuous functions on a closed interval with no uniformly convergent subsequence. The missing condition concerns how consistently the functions respond to nearby inputs. [Examples 11.6.2–11.6.4](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-6).
The Arzelà–Ascoli theorem answers this question for continuous complex-valued functions on a compact metric domain. Its uses include existence questions for differential equations and compactness properties of integral operators, both discussed in the source section. These applications require control of entire functions, not merely convergence at isolated points. [Differential-equation application](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-29), [integral-operator application](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-30).
The four targets follow §11.6 of Jiří Lebl’s *Basic Analysis*, Volume II, a textbook treatment of equicontinuity and compactness for uniform convergence. [Author’s book page](https://www.jirka.org/ra/).
## Setting: pointwise control and uniform control
A **metric space** is a set $X$ with a distance $d(x,y)$ that is nonnegative, symmetric, vanishes exactly when $x=y$, and satisfies the triangle inequality. It is **compact** when every cover by open sets has a finite subcover. Here $\mathbb C$ denotes the complex numbers, $|z|$ their absolute value, and $F_n:X\to\mathbb C$ the function at index $n\in\mathbb N$. Write $C(X,\mathbb C)$ for the continuous functions.
The sequence is **pointwise bounded** if each input has its own bound, and **uniformly bounded** if one bound works for every input and index:
$$
\forall x\in X\;\exists M_x\in\mathbb R\;\forall n\in\mathbb N,
\quad |F_n(x)|\le M_x,
$$
$$
\exists M\in\mathbb R\;\forall n\in\mathbb N\;\forall x\in X,
\quad |F_n(x)|\le M.
$$
It is **uniformly equicontinuous** when
$$
\forall\varepsilon>0\;\exists\delta>0\;\forall x,y\in X\;\forall n\in\mathbb N,
\quad d(x,y)<\delta\Longrightarrow |F_n(x)-F_n(y)|<\varepsilon.
$$
Thus $\delta$ cannot depend on the function index or the points. These are the source’s distinct boundedness and common-continuity conditions. [Definition 11.6.1](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-4), [Definition 11.6.6](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-13).
A **subsequence** has the form $F_{\varphi(n)}$, where $\varphi:\mathbb N\to\mathbb N$ is strictly increasing. **Pointwise convergence** to $f$ means convergence to $f(x)$ separately for every $x$. **Uniform convergence** means that for each $\varepsilon>0$ there is one $N$ such that $|F_n(x)-f(x)|<\varepsilon$ for every $n\ge N$ and every $x$. A subset $D\subseteq X$ is **dense** if its closure $\overline D$ is all of $X$.
## Formalization targets
The supporting targets distinguish countable domains, a necessary continuity condition, and the density property of compact metric spaces. The final target combines the hypotheses into uniform-convergence compactness; no quantitative rate is prescribed.
**Proposition 11.6.5.** For an arbitrary countable set $X$, without any topology or continuity assumption,
$$
F_n\text{ pointwise bounded}
\Longrightarrow
\exists\varphi,f,\quad
\varphi\text{ strictly increasing}\quad\land\quad
\forall x\in X,\ F_{\varphi(n)}(x)\longrightarrow f(x).
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#prop_subsequenceoncountableX).
**Proposition 11.6.7.** For compact metric $X$,
$$
F_n\in C(X,\mathbb C),\quad F_n\longrightarrow f\text{ uniformly}
\Longrightarrow F_n\text{ uniformly equicontinuous}.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-16).
**Proposition 11.6.8.** Every compact metric space satisfies
$$
\exists D\subseteq X,\quad D\text{ countable}\ \land\ \overline D=X.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-18).
**Theorem 11.6.9, Arzelà–Ascoli.** Suppose $X$ is compact metric, $F_n\in C(X,\mathbb C)$, and the sequence is pointwise bounded and uniformly equicontinuous. The complete conclusion is
$$
\left(\exists M\in\mathbb R\;\forall n,x,\ |F_n(x)|\le M\right)
\quad\land\quad
\left(\exists\varphi:\mathbb N\to\mathbb N\;\exists f\in C(X,\mathbb C),\quad
\varphi\text{ strictly increasing},\quad
F_{\varphi(n)}\longrightarrow f\text{ uniformly}\right).
$$
Both the global bound and the subsequence conclusion are required. The limit belongs to $C(X,\mathbb C)$, so its continuity is explicit. [Source theorem](https://www.jirka.org/ra/html/sec_arzelaascoli.html#thm_arzelaascoli).
## Significance: a compactness criterion with explicit hypotheses
The result supplies a uniform limit under hypotheses that concern individual inputs and a shared continuity condition. It therefore identifies a usable replacement for boundedness alone in a space of functions. The distinction matters downstream: retaining only pointwise convergence would not provide a common error bound across the domain, and assuming uniform boundedness in advance would discard one of the theorem’s conclusions. [Lebl, Theorem 11.6.9](https://www.jirka.org/ra/html/sec_arzelaascoli.html#thm_arzelaascoli).
These are established theorems, not open conjectures. Mathlib already contains machine-checked general Arzelà–Ascoli results, compactness and convergent-subsequence infrastructure, and the countable-dense-set interface. The four source-level statements also have ordinary local Lean proofs checked against their exact types. The contribution is a faithful textbook-facing formulation that keeps the distinct hypotheses, quantifier order, arbitrary countable domain, and both capstone conclusions visible. It is not a claim to the first formalization of Arzelà–Ascoli. [Mathlib Ascoli development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/Ascoli.lean), [countable dense subsets](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Bases.lean).
## Difficulty: preserving the quantifier order
Convergence at every point does not automatically mean uniform convergence. A permissible index threshold may depend on the point, and different pointwise limits may require different subsequences. Likewise, separate continuity of every $F_n$ does not give a single $\delta$ valid for all $n$. Replacing these statements with their uniform versions silently changes the problem. Lebl’s bounded sequence $x\mapsto x^n$ on $[0,1]$ already rules out the naive implication from bounded continuous functions to a uniformly convergent subsequence. [Example 11.6.3](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-7).
The formal challenge is to retain these distinctions across the representations of functions, convergence, and compactness. In particular, the countable-domain proposition must not acquire a compactness assumption, while the capstone must not acquire global bounds as an extra premise.
## Formalization scope
The development uses namespace `LeblRA`, arbitrary universe-polymorphic domain types, Lean’s complex numbers, and zero-based natural-number indices. Zero-based indexing only reindexes the source’s sequence starting at one. A strictly increasing map is represented by `StrictMono`; pointwise limits use `Tendsto` at `atTop`, uniform limits use `TendstoUniformly`, and density uses `Dense`. Finite and empty domains remain allowed.
The boundedness and equicontinuity hypotheses are written as explicit quantifiers, not new custom definitions. No claim may be replaced by a finite-domain special case, a vacuous hypothesis, or a statement that assumes its uniform conclusion.
Reusable infrastructure consists of complex norms, metric and compact spaces, continuous maps, uniform convergence, equicontinuity, and sequence compactness. The pinned environment is Lean 4.29.0-rc3 with Mathlib revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Source-faithful alternative proofs and explicit equivalences between the raw conditions and library predicates are welcome; applications beyond the four numbered targets are outside this scope. [Uniform-convergence interface](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/UniformConvergence.lean), [sequence compactness](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Sequences.lean).
## Selected references
- Jiří Lebl, *Basic Analysis: Introduction to Real Analysis*, Volume II, author-published open textbook, version 6.3, 2026, §11.6. [Section text](https://www.jirka.org/ra/html/sec_arzelaascoli.html); [edition information](https://www.jirka.org/ra/).
- The Mathlib community, *Mathlib*, Lean mathematical library, revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`, 2026. [General Ascoli theorems](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/Ascoli.lean), [uniform convergence](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/UniformConvergence.lean), [topological bases and separability](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Bases.lean).
Elementary Number Theory: Primes, Congruences, and Secrets I: Sums of Two SquaresTextbook
## From individual representations to an arithmetic criterion
Writing a positive integer as a sum of two squares is an elementary question with a precise general answer. Some integers have such a representation and others do not; checking a few small inputs does not explain the distinction. A criterion expressed through prime factorization instead decides the question for every positive integer. This project follows Section 5.7 of William Stein's *Elementary Number Theory: Primes, Congruences, and Secrets*, including the section's supporting statements and one subsequent exercise. The selected material connects divisibility, coprimality, algebraic identities, and rational approximation within a single classical topic. The source is the [author-hosted January 2017 text](https://wstein.org/ent/ent.pdf), using its numbering rather than the numbering of earlier drafts.
## Integers, representations, and prime exponents
A **two-square representation** of an integer $n$ consists of integers $x,y$ satisfying $n=x^2+y^2$. Either coordinate may be zero or negative. A representation is **primitive** when the greatest common divisor of its coordinates is one; this restricts representations, not the definition of representability itself. For a positive integer $n$ and a prime $p$, the **prime exponent** $v_p(n)$ is the exponent of $p$ in the prime factorization of $n$. The congruence $p\equiv3\pmod4$ means that division of $p$ by four leaves remainder three.
The approximation statement uses a real number $t$, a positive integer $N$, and a **reduced fraction** $a/b$, where $a$ is an integer, $b$ is a positive integer, and their greatest common divisor is one. These conventions agree with [Stein's section and its definition of primitive representations](https://wstein.org/ent/ent.pdf).
## Formalization targets
The supporting targets retain their complete source statements. Lemma 5.7.4 concerns every positive integer $n$ with a prime divisor $p\equiv3\pmod4$:
$$\nexists x,y\in\mathbb Z:\quad n=x^2+y^2\quad\text{and}\quad\gcd(x,y)=1.$$
Equation (5.7.1) is the integer identity
$$(x_1^2+y_1^2)(x_2^2+y_2^2)=(x_1x_2-y_1y_2)^2+(x_1y_2+x_2y_1)^2.$$
Lemma 5.7.5 states that, for every real $t$ and positive integer $N$, some reduced fraction satisfies
$$0<b\le N,\qquad |t-a/b|\le\frac{1}{b(N+1)}.$$
The capstone, Theorem 5.7.1, is the complete equivalence
$$n=x^2+y^2\text{ for some }x,y\in\mathbb Z
\quad\Longleftrightarrow\quad
\forall\text{ primes }p\mid n,\quad p\equiv3\pmod4\Longrightarrow v_p(n)\text{ is even},$$
for every positive integer $n$. Both implications are required. These four statements are located on printed pages 117–120 of the [source PDF](https://wstein.org/ent/ent.pdf).
Exercise 5.11, on printed page 122, is an optional downstream target:
$$\forall n\in\mathbb Z,\ \exists k\in\{0,1,2,3\}:\quad
\nexists x,y\in\mathbb Z,\ n+k=x^2+y^2.$$
It describes gaps among represented integers and is not a prerequisite milestone for the capstone.
## What the criterion and its formalization provide
The criterion replaces a search for coordinates with a finite condition on the factorization of an input. It applies to composite integers as well as primes and distinguishes the exponent of a prime divisor from the mere presence of that divisor. The primitive obstruction also explains why a claim about coprime coordinates must not be confused with a claim that excludes all representations. The composition identity supplies an explicit statement of multiplicative closure, while the exercise gives a uniform restriction on consecutive runs. These are the consequences and accompanying results presented in [Stein's treatment](https://wstein.org/ent/ent.pdf).
The mathematics is established, not an open research problem. Important formal ingredients already exist in Mathlib: the [sum-of-two-squares development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/NumberTheory/SumTwoSquares.lean) includes the arithmetic criterion and primitive obstruction, and the [Diophantine approximation development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean) supplies the bounded-denominator result. The work here is a source-aligned collection of exact theorem interfaces and independently checked proofs. Reusing those results does not claim a new proof of the classical mathematics or an exact transcription of Stein's argument.
## Why the complete statement matters
A finite list of successful representations cannot establish an assertion about every positive integer. Similarly, a restriction on primitive representations is insufficient to settle general representability, because a nonprimitive pair is still a valid representation. The capstone must account for prime exponents and both directions of the equivalence simultaneously. The approximation result has its own coupled requirements: obtaining a small denominator without the stated error bound, or a good approximation with an uncontrolled denominator, does not meet the target. These distinctions are explicit in the [source statements](https://wstein.org/ent/ent.pdf).
## Formalization scope
The namespace is `SteinENT`. Inputs $n,p,N$ use natural numbers, with positivity hypotheses wherever the source uses positive integers. Coordinates and all subtraction in the composition identity use integers. Prime exponents use `Nat.factorization`; primitivity uses `Int.gcd x y = 1`. Approximation witnesses use Lean's rational type, whose canonical numerator and positive denominator already express a reduced fraction. The error inequality is an inequality of real numbers. The gap exercise allows every integer starting point, including negative ones.
No hypothesis assumes the desired representation or restricts the capstone to a bounded test range. There is no additional definition that hides a proof obligation, and no separate alias item for primitivity. Standard Mathlib arithmetic, rational approximation, and tactic libraries provide reusable infrastructure. Complete alternative proofs are welcome when they preserve these interfaces, including the explicit positive-input boundary and unrestricted integer coordinates.
## Selected references
- William Stein, *Elementary Number Theory: Primes, Congruences, and Secrets*, Undergraduate Texts in Mathematics, Springer, 2008; [author-hosted January 2017 version](https://wstein.org/ent/ent.pdf), Section 5.7 and Exercise 5.11. [Author's book page](https://wstein.org/ent/).
- William Stein, [author's source text at commit c4984c7ddb22258674816f8c000b0d8eb485d694](https://github.com/williamstein/ent/blob/c4984c7ddb22258674816f8c000b0d8eb485d694/body.tex), corresponding section and exercises.
- The Mathlib Community, [Mathlib4 at commit 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e](https://github.com/leanprover-community/mathlib4/tree/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e), Lean 4 library, pinned formalization environment; number-theory modules linked above.
Dynamic Programming and Optimal Control II: Label Correcting MethodsTextbook
## Motivation
Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.
## Setting
A finite directed graph with arc set $\mathcal{A}$, real arc lengths $a_{ij}$, origin $s$ and destination $t \ne s$ (`BertsekasSPGraph`). Walks are nonempty node lists whose consecutive pairs are arcs (`BertsekasIsWalkFrom`), with length the sum of arc lengths (`BertsekasWalkLength`); the shortest distance is the infimum of walk lengths in the extended reals, $+\infty$ if no walk exists (`BertsekasShortestDistance`). The standing assumption of §2.3: **every cycle has nonnegative length** (negative arcs allowed).
The algorithm state (`BertsekasLCState`) carries labels $d_j \in \overline{\mathbb{R}}$, the scalar UPPER, and the candidate list OPEN. Initially $d_s = 0$, all other labels $\infty$, UPPER $= \infty$, OPEN $= \{s\}$. One iteration (`BertsekasLCStep`, nondeterministic): remove any $i$ from OPEN; for each child $j$ of $i$ in any order, if $d_i + a_{ij} < \min\{d_j, \text{UPPER}\}$ set $d_j := d_i + a_{ij}$, and put $j$ in OPEN if $j \ne t$, or update UPPER if $j = t$. The algorithm terminates when OPEN is empty.
## Target
$$\text{OPEN} = \varnothing \implies \text{UPPER} = \operatorname{dist}(s, t) \in \overline{\mathbb{R}},$$
for every execution, **under the nonnegative arc length assumption of §2.3** ($a_{ij} \ge 0$ for every arc) — `BertsekasDP.label_correcting_correctness_of_nonneg_arcs` (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (`label_correcting_terminates`) — and the workhorse invariant that every finite label is the length of an actual walk from $s$, which needs neither (`label_correcting_invariant`).
The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test $d_i + a_{ij} < \min\{d_j, \mathrm{UPPER}\}$, and with a negative arc a longer prefix can still reach $t$ more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-*cycle* assumption of §2.1 and was disproved by the counterexample $s=0$, $t=2$, $a_{02}=1$, $a_{01}=2$, $a_{12}=-2$ (a graph with no cycles at all), where the algorithm terminates with $\mathrm{UPPER}=1$ while the shortest distance is $0$. Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.
## Significance
Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.
## Difficulty
Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.
## Formalization scope
Finite node type with decidable equality; arcs as a `Finset` of ordered pairs; lengths total on $V \times V$ (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in `EReal`, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 2.3.1, §2.3.) http://www.athenasc.com/dpbook.html
- E. W. Dijkstra, A note on two problems in connexion with graphs, *Numer. Math.* 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
- R. Bellman, On a routing problem, *Quart. Appl. Math.* 16 (1958), 87–90. https://doi.org/10.1090/qam/102435
Discrete Mathematics—Lecture Notes I: Capacitated Hall MatchingTextbook
## 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](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html). 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](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch1.S1.html).
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](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html):
$$
\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](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html).
Mathlib already provides finite-family and graph versions of Hall's theorem in its [Hall development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Combinatorics/Hall/Finite.lean) and [graph interface](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Combinatorics/SimpleGraph/Hall.lean). 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](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html); [graph conventions](https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch1.S1.html).
- The mathlib community, *Mathlib 4*, revision 777aaa6, 2026. [Finite-family Hall theorem](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Combinatorics/Hall/Finite.lean); [native graph Hall theorem](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Combinatorics/SimpleGraph/Hall.lean).