Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns (experimental)
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Is every odd number a sum of k primes? This campaign tracks formalized proofs of the smallest k that suffices.
Schnirelmann (1930) showed some finite k works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved k=5 unconditionally. Helfgott (2013) proved that every odd number greater than 5 is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: 27 is neither prime nor 2 + prime.
Schoolbook matrix multiplication takes n3 operations. The exponent ω is the infimum of all τ such that two n×n matrices can be multiplied in O(nτ) arithmetic operations; trivially ω≥2, and ω=2 is conjectured but open.
Strassen gave the first nontrivial bound, ω<2.81, in 1969, and introduced the laser method in 1986 to reach ω<2.48. Coppersmith and Winograd's 1990 bound of 2.376 stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached ω<2.371339 in 2025, and the current record is ω<2.371177, from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Esquisse d'un Programme I: Dessins d'Enfants and the Faithfulness of the Galois ActionResearch Paper
## Motivation
In *Esquisse d'un Programme* (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a **dessin d'enfant**, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above $0$, $1$ and $\infty$, and that curve and map are defined over the field $\overline{\mathbb{Q}}$ of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group $\Gamma = \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function $f(z) = P(z)/Q(z)$, the action of $\gamma \in \Gamma$ is obtained simply by applying $\gamma$ to the coefficients of $P$ and $Q$. Grothendieck states in §2 (p. 9) that the resulting outer action of $\Gamma$ on the profinite fundamental group $\hat{\pi}_{0,3}$ of $\mathbb{P}^1 \smallsetminus \{0,1,\infty\}$ is **faithful**, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.
Timeline of the results this mission formalizes. Belyi (1979, *On Galois extensions of a maximal cyclotomic field*, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over $\mathbb{C}$ is defined over a number field if and only if it admits a map to $\mathbb{P}^1$ unramified outside $\{0,1,\infty\}$; the "only if" half is an explicit construction with polynomials over $\mathbb{Q}$. Grothendieck (1984) drew the consequence that $\Gamma$ acts on dessins and asserted faithfulness of the action on $\hat{\pi}_{0,3}$. Lenstra, in an appendix to L. Schneps (ed.), *The Grothendieck Theory of Dessins d'Enfants* (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of **plane trees**, equivalently on **Shabat polynomials**. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.
## Setting
Work over $\overline{\mathbb{Q}}$, realized as the algebraic closure of $\mathbb{Q}$, and write $\Gamma$ for its group of field automorphisms fixing $\mathbb{Q}$ pointwise.
A nonconstant polynomial $P$ over a field $K$ is a **Belyi polynomial** (classically a *Shabat polynomial*) when every critical value of $P$ lies in $\{0,1\}$: for every $z \in K$ with $P'(z) = 0$ one has $P(z) = 0$ or $P(z) = 1$. Over an algebraically closed field of characteristic zero this says exactly that $P$, viewed as a degree-$n$ map $\mathbb{P}^1 \to \mathbb{P}^1$, is unramified outside the fibres over $0$, $1$ and $\infty$. The associated dessin is the preimage $P^{-1}([0,1])$, a plane tree with $n$ edges whose vertices are the points above $0$ and $1$, with vertex orders equal to the multiplicities of the corresponding roots of $P$ and of $P - 1$.
Two Belyi polynomials define the same dessin exactly when they are **affinely equivalent**: $Q = P(aX + b)$ for some $a \neq 0$ and some $b$. The target coordinate is already rigidified by the normalisation of the critical values to $\{0,1\}$; only the source coordinate remains free.
The group $\Gamma$ acts coefficientwise: $P^{\gamma}$ is the polynomial obtained from $P$ by applying $\gamma$ to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.
## Formalization targets
### Goal — faithfulness of the Galois action on plane trees
$$\forall\, \gamma \in \Gamma,\quad \gamma \neq 1 \ \Longrightarrow\ \exists\, P \in \overline{\mathbb{Q}}[X] \text{ a Belyi polynomial with } P \not\sim_{\mathrm{aff}} P^{\gamma}.$$
Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.
### Supporting targets
- **Belyi's theorem, polynomial form.** For every finite set $S \subseteq \overline{\mathbb{Q}}$ there is a Belyi polynomial $f \in \mathbb{Q}[X]$ with $f(S) \subseteq \{0,1\}$.
- **Descent to $\overline{\mathbb{Q}}$.** Every Belyi polynomial over $\mathbb{C}$ is affinely equivalent to one whose coefficients are algebraic over $\mathbb{Q}$.
- **Galois equivariance and invariants.** $P^{\gamma}$ is again a Belyi polynomial of the same degree, and the multiplicity of $z$ as a root of $P - c$ equals the multiplicity of $\gamma(z)$ as a root of $P^{\gamma} - \gamma(c)$: the dessin's vertex and face orders are Galois invariants.
- **Finiteness of the orbit.** The set of Galois conjugates of a fixed polynomial over $\overline{\mathbb{Q}}$ is finite — the "visibly finite number of conjugates" of §3.
- **Finiteness in a fixed degree.** For each $n$ there are only finitely many monic Belyi polynomials of degree $n$ over $\overline{\mathbb{Q}}$ with vanishing subleading coefficient.
- **Separation.** For every $\alpha \in \overline{\mathbb{Q}}$ there is a Belyi polynomial $P$ such that every $\gamma$ fixing the class of $P$ fixes $\alpha$. The goal follows from this by taking $\alpha$ with $\gamma(\alpha) \neq \alpha$.
## Significance
The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of $\Gamma$: every nontrivial automorphism of $\overline{\mathbb{Q}}$ is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that $\Gamma$ embeds into the outer automorphism group of $\hat{\pi}_{0,3}$.
Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over $\overline{\mathbb{Q}}$ and $\mathbb{C}$, so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.
## Difficulty
The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all $\gamma \neq 1$, and $\Gamma$ has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number $\alpha$, a tree whose isomorphism class remembers $\alpha$; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over $\mathbb{C}$ is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.
## Formalization scope
Conventions fixed in the Lean development, and not to be re-litigated by solvers:
- $\overline{\mathbb{Q}}$ is `AlgebraicClosure ℚ`, and $\Gamma$ is its group of $\mathbb{Q}$-algebra automorphisms.
- "Belyi polynomial" means: positive degree, and every root of the formal derivative is sent to $0$ or $1$. Critical values are required to lie *in* $\{0,1\}$, not to be exactly $\{0,1\}$; degenerate cases such as $X^n$ (one finite critical value) are therefore included.
- Being a Belyi polynomial is stated over an arbitrary field but is only intended over algebraically closed fields ($\overline{\mathbb{Q}}$, $\mathbb{C}$), where quantifying over the field's own elements captures all critical points.
- Dessin isomorphism is modelled as affine equivalence of the source variable only; conjugating by an affine map of the target is excluded, since the target is rigidified by $\{0,1\}$.
- The Galois action is coefficientwise application of $\gamma$.
Trivialization is ruled out as follows: the goal asserts the *existence* of a moved Belyi polynomial for each nontrivial $\gamma$, with the nondegeneracy `0 < deg P` built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ($\gamma \neq 1$ is satisfiable).
A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over $\mathbb{C}$ as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.
## Selected references
- A. Grothendieck, *Esquisse d'un Programme* (1984), published in L. Schneps and P. Lochak (eds.), *Geometric Galois Actions 1*, LMS Lecture Note Series 242, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511758874
- G. V. Belyi, *On Galois extensions of a maximal cyclotomic field*, Izv. Akad. Nauk SSSR Ser. Mat. 43 (1979), 267–276. English translation: Math. USSR-Izv. 14 (1980), 247–256. https://doi.org/10.1070/IM1980v014n02ABEH001096
- L. Schneps (ed.), *The Grothendieck Theory of Dessins d'Enfants*, LMS Lecture Note Series 200, Cambridge University Press, 1994. https://doi.org/10.1017/CBO9780511569302
- S. K. Lando and A. K. Zvonkin, *Graphs on Surfaces and Their Applications*, Encyclopaedia of Mathematical Sciences 141, Springer, 2004. https://doi.org/10.1007/978-3-540-38361-1
Faithfulness of the Burau representation of B4Research Paper
## Motivation
In 1935 Werner Burau attached to every braid on $n$ strands a matrix over the ring of Laurent polynomials $\mathbb{Z}[t,t^{-1}]$. The resulting homomorphism $\rho_n : B_n \to \mathrm{GL}_n(\mathbb{Z}[t,t^{-1}])$ is the oldest and most studied linear representation of the braid group, and whether it is *faithful* — whether a nontrivial braid can act as the identity matrix — became one of the best known questions about braid groups.
The history is short and sharp:
* **1969** — Magnus and Peluso prove that $\rho_3$ is faithful, by a direct algebraic computation.
* **1991** — Moody proves $\rho_n$ is **not** faithful for $n \ge 9$.
* **1993** — Long and Paton improve this to $n \ge 6$.
* **1999** — Bigelow settles $n = 5$: $\rho_5$ is not faithful.
* This left exactly one open case, $n = 4$, which appears as Question 3.1 in Margalit's problem list for mapping class groups.
* **2026** — Bharathram, Birman and Brendle prove that $\rho_4$ **is** faithful ([arXiv:2607.05283](https://arxiv.org/abs/2607.05283)), closing the last case.
## Setting
Let $n \ge 1$. The braid group $B_n$ is taken here in Artin's presentation: generators $\sigma_1,\dots,\sigma_{n-1}$ subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1}.$$
Let $R = \mathbb{Z}[t,t^{-1}]$. The **unreduced Burau representation** is the homomorphism
$$\rho_n : B_n \longrightarrow \mathrm{GL}_n(R), \qquad \sigma_i \longmapsto I_{i-1} \oplus \begin{pmatrix} 1-t & t \\ 1 & 0\end{pmatrix} \oplus I_{n-i-1},$$
i.e. the identity matrix altered only in the two rows and columns $i$, $i+1$. That these matrices satisfy the two families of braid relations — so that $\rho_n$ is well defined — is proved in the mission's definition file, together with the invertibility of each generator matrix (its inverse is the identity altered by the block $\begin{pmatrix} 0 & 1 \\ t^{-1} & 1-t^{-1}\end{pmatrix}$).
Equivalently, $\rho_n$ is the action of the mapping class group of the $n$-punctured disk $D_n$ on the relative homology $H_1(\widetilde{D_n}, \{\tilde p_*\})$ of the infinite cyclic cover determined by total winding number; this is the description used throughout the source paper.
A representation is **faithful** when it is injective.
## Target
The goal of the mission is the Main Theorem of the paper:
$$\rho_4 : B_4 \longrightarrow \mathrm{GL}_4(\mathbb{Z}[t,t^{-1}]) \ \text{ is injective.}$$
The milestones are three supporting results, each of which can be attacked independently:
1. **Theorem 4.1 (Magnus–Peluso).** $\rho_3$ is injective. The paper gives a new topological proof of this classical statement, and the same argument is the model for the four-strand case.
2. **Observation 2.1.** If a braid $\Phi \in B_n$ satisfies $\rho_n(\Phi) = I$, then its image under the standard inclusion $B_n \hookrightarrow B_{n+1}$ (add one unbraided strand) satisfies $\rho_{n+1}(\iota(\Phi)) = I$. The paper uses this to move a four-strand braid into $B_5$, where a parity obstruction can be applied.
3. **Long's criterion** ([Long 1986, Theorem 2.2], quoted in Section 1 of the paper). If $N \trianglelefteq B_n$ is nontrivial and not contained in the centre, and $\rho_n$ is injective on $N$, then $\rho_n$ is injective. This is what reduces the Main Theorem to faithfulness on the Brunnian subgroup $\mathrm{Brun}_4$.
## Significance
Faithfulness of $\rho_4$ closes the classification of the faithful Burau representations: $\rho_n$ is faithful exactly for $n \le 4$. It immediately gives faithfulness of the Jones representation of $B_4$ (Corollary 1.1 of the paper), since the Jones representation contains the reduced Burau representation as a summand. Beyond the statement itself, the kernel and the image of $\rho_n$ for $n \ge 5$ remain poorly understood, and the paper's disk-sequence and parity technology is proposed by its authors as a tool for that problem.
For formalization, essentially nothing of this is machine-checked today: Mathlib has neither braid groups nor the Burau representation. This mission puts in place a checked definition of $\rho_n$ over $\mathbb{Z}[t,t^{-1}]$ (including well-definedness and invertibility), and then asks for the mathematics. Even the three-strand case — Magnus–Peluso, known since 1969 — is not formalized anywhere, and it is the natural first target.
## Difficulty
The obvious approach fails in both directions. One cannot simply compute: a braid in the kernel would have to be found or excluded among infinitely many words, and no normal form for $B_4$ turns injectivity of $\rho_4$ into a finite check. Nor can one argue by a free-subgroup / ping-pong pattern, which is how *non*-faithfulness is proved for $n \ge 5$.
The source argument is topological. To a braid $\Phi$ one associates the arc $\beta = (\beta_*^3)\Phi$ and the sequence of punctured disks cut out by its intersections with a fixed arc $\alpha$; the Moody polynomial $M(\alpha,\beta) \in \mathbb{Z}[t,t^{-1}]$ then obstructs membership in the kernel provided no cancellation occurs among its monomials. Three-strand braids always satisfy the relevant parity condition; four-strand braids do not, and the paper repairs this by pushing a point-pushing braid $\Phi \in K_4$ into $B_5$ and applying Moody's theorem there. A complete formalization therefore needs curves on punctured disks, minimal position, and the Birman exact sequence — none of which exist in Mathlib. Contributions that build any of that infrastructure are as welcome as contributions to the statements themselves.
## Formalization scope
Conventions fixed by the Lean development:
1. $B_n$ is the abstract group given by Artin's presentation, with generators indexed by $\mathrm{Fin}(n-1)$ using truncated subtraction; the generator of index $i$ is $\sigma_{i+1}$. This is the already-published definition reused by the mission, so results proved here interoperate with other braid-group missions.
2. The representation is the **unreduced** Burau representation, of size $n \times n$, not the reduced $(n-1)$-dimensional one; the variable is written $t$ and the coefficient ring is $\mathbb{Z}[t,t^{-1}]$.
3. Faithfulness is stated as injectivity of the group homomorphism, not as triviality of the kernel on some subgroup, and it is the genuine homomorphism out of the presented group: the braid relations are verified for the Burau matrices in the definition file, so no statement here is vacuous or conditional on well-definedness.
4. Long's criterion is stated for all $n$; for $n \le 2$ its noncentrality hypothesis cannot be satisfied, so its content is the case $n \ge 3$ that the paper uses.
A complete development will additionally need: point-pushing subgroups and the Brunnian group $\mathrm{Brun}_4$, the Moody polynomial of a pair of arcs, and winding-number sequences. These are not yet formalized and are deliberately not part of the current statements; proposals for faithful formalizations of them are welcome in the mission discussion.
## Selected references
* V. Bharathram, J. S. Birman, T. E. Brendle, *The Burau representation is faithful for n = 4*, 2026, [arXiv:2607.05283](https://arxiv.org/abs/2607.05283).
* W. Magnus, A. Peluso, *On a theorem of V. I. Arnold*, Comm. Pure Appl. Math. 22 (1969), 683–692, [DOI:10.1002/cpa.3160220508](https://doi.org/10.1002/cpa.3160220508).
* D. D. Long, *A note on the normal subgroups of mapping class groups*, Math. Proc. Cambridge Philos. Soc. 99 (1986), 79–87, [DOI:10.1017/S0305004100063969](https://doi.org/10.1017/S0305004100063969).
* J. A. Moody, *The Burau representation of the braid group $B_n$ is unfaithful for large $n$*, Bull. Amer. Math. Soc. 25 (1991), 379–384, [DOI:10.1090/S0273-0979-1991-16080-5](https://doi.org/10.1090/S0273-0979-1991-16080-5).
* D. D. Long, M. Paton, *The Burau representation is not faithful for $n \ge 6$*, Topology 32 (1993), 439–447, [DOI:10.1016/0040-9383(93)90030-Y](https://doi.org/10.1016/0040-9383(93)90030-Y).
* S. Bigelow, *The Burau representation is not faithful for $n = 5$*, Geom. Topol. 3 (1999), 397–404, [DOI:10.2140/gt.1999.3.397](https://doi.org/10.2140/gt.1999.3.397).
Braids, Links and Mapping Class Groups I: Artin's Presentation of the Braid GroupTextbook
## Motivation
The **braid group** is one of the places where group theory, low-dimensional topology and
knot theory meet. Artin introduced it in 1925 (E. Artin, *Theorie der Zöpfe*, Abh. Math. Sem.
Univ. Hamburg 4 (1925), 47–72) and returned to it in 1947; since then it has become standard
equipment in the study of links (closed braids and Markov's theorem), of mapping class groups
of punctured surfaces, and of configuration spaces. Birman's *Braids, Links, and Mapping Class
Groups* (Annals of Mathematics Studies 82, Princeton University Press, 1974) is the classical
reference that develops all three subjects from the braid group outwards, and its Chapter 1
is the foundation on which the rest of the book rests.
The chapter's structure is itself the reason to formalize it first: everything later in the
book — the closed-braid picture of links, Markov's theorem, the Magnus representations, the
mapping class group of the punctured sphere — is phrased in terms of the group
$\pi_1 B_{0,n}E^2$ and of the presentation established here. A mission that fixes faithful Lean
definitions of the configuration spaces and of the abstract braid group therefore fixes the
vocabulary for the whole series.
Timeline of the results collected here: Artin (1925) gave the presentation and the
characterization of braid automorphisms of a free group; Chow (1948) determined the centre;
Fadell–Neuwirth (1962) introduced the configuration-space fibrations, and Fadell–Van Buskirk
(1962) used them to give the proof of the presentation reproduced by Birman.
## Setting
Write $E^2$ for the Euclidean plane, identified throughout with the complex numbers $\mathbb{C}$.
For $n \ge 0$ let
$$F_{0,n}E^2 = \{\,(z_1,\dots,z_n) \in \mathbb{C}^n : z_i \neq z_j \text{ for } i \neq j\,\}$$
be the **ordered configuration space** of $n$ points in the plane, topologized as a subspace of
$\mathbb{C}^n$. The symmetric group $\Sigma_n$ acts on it by permuting coordinates; the quotient
$$B_{0,n}E^2 = F_{0,n}E^2 / \Sigma_n,$$
with the quotient topology, is the **unordered configuration space**. A point of $B_{0,n}E^2$ is
an unordered set of $n$ distinct points of the plane. The base configuration is
$\bar z^{\,0} = (1,2,\dots,n)$, and all fundamental groups below are taken at $\bar z^{\,0}$ or at
its image.
The **braid group of the plane** is $\pi_1 B_{0,n}E^2$: a loop is a motion of $n$ points of the
plane returning to the same set of points, and homotopy classes of such motions compose as
braids. The **pure braid group** is $P_n = \pi_1 F_{0,n}E^2$, the subgroup of motions returning
each point to its own starting position.
Separately, let $B_n$ denote the abstract group given by generators $\sigma_1,\dots,\sigma_{n-1}$
subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad
\sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$
These are equations (1-1) and (1-2) of the book (p. 11). Geometrically $\sigma_i$ interchanges the
$i$-th and $(i+1)$-st points along a semicircle.
## Formalization targets
### Goal — Theorem 1.8 (Artin, 1925; Birman p. 18)
$$B_n \;\cong\; \pi_1 B_{0,n} E^2 .$$
The group of motions of $n$ points of the plane is the group with generators
$\sigma_1,\dots,\sigma_{n-1}$ and the two families of relations above: the relations are not only
valid but *defining*.
### Milestones
The milestone list follows the chapter: the covering-space description of the projection
$F_{0,n}E^2 \to B_{0,n}E^2$ (Proposition 1.1, p. 11), the Fadell–Neuwirth exact sequence
(Theorem 1.4, p. 14), the semidirect-product decomposition of the pure braid group
(Corollary 1.8.1, p. 24), the faithful representation of $B_n$ by automorphisms of a free group
(Corollary 1.8.3, p. 25), the centre of $B_n$ (Corollary 1.8.4, p. 28, due to Chow), and Artin's
algebraic characterization of the braid automorphisms (Theorem 1.9, p. 30).
## Significance
Theorem 1.8 is what makes the braid group *computable*: with defining relations in hand one can
combine braids into the normal form of Corollary 1.8.2 and solve the word problem, represent
braids by automorphisms of a free group, and pass to the link-theoretic material of Chapters 2
and 5 where braid words, not motions, are the objects manipulated. Corollary 1.8.3 turns braids
into concrete data — a braid is determined by what it does to the generators of a free group —
and Theorem 1.9 says exactly which endomorphisms arise this way; both are the algebraic engine
behind the conjugacy-problem and Magnus-representation chapters.
For formalization the state of play is that Mathlib has free groups, presented groups, the
fundamental groupoid and fundamental group, covering maps and fibre bundles, but no braid
groups and no configuration spaces: nothing here can be assembled from existing declarations.
The mission therefore produces reusable infrastructure — configuration spaces of the plane, the
symmetric-group quotient, the Artin presentation, the Artin action on a free group — as well as
machine-checked proofs of results that are classical but, as far as the mission's search of the
library showed, not yet formalized in Mathlib.
## Difficulty
The generators and relations are easy to write down and easy to verify *in* $\pi_1 B_{0,n}E^2$;
what is hard is completeness, i.e. that no further relations are needed. The naive route —
draw the braid, push it into a normal form by hand — is exactly what a formal proof cannot do.
The Fadell–Van Buskirk argument reproduced by Birman instead runs an induction on $n$ driven by
the fibration $F_{0,n}E^2 \to F_{0,n-1}E^2$: its homotopy exact sequence gives a split extension
of $P_{n-1}$ by a free group, presentations are assembled along the extension, and finally the
covering $F_{0,n}E^2 \to B_{0,n}E^2$ with deck group $\Sigma_n$ transfers the answer from the pure
braid group to the full braid group. Each of those steps needs genuine algebraic topology —
local triviality of the projection, exactness of the homotopy sequence, freeness of
$\pi_1$ of a punctured plane — which is where the formalization work actually lies.
## Formalization scope
The plane is $\mathbb{C}$. $F_{0,n}E^2$ is the subtype of injective functions
$\mathrm{Fin}\,n \to \mathbb{C}$; $B_{0,n}E^2$ is its quotient by the equivalence "differ by
precomposition with a permutation", with the quotient topology. Base point: the configuration
$i \mapsto i+1$, i.e. $(1,2,\dots,n)$, and its image. Fundamental groups are Mathlib's
`FundamentalGroup` at those base points. Braid generators are indexed by $\mathrm{Fin}(n-1)$
with $0$-based indices ($i$ stands for $\sigma_{i+1}$), and free-group generators by
$\mathrm{Fin}\,n$; the abstract braid group is a `PresentedGroup` on that index set. Truncated
subtraction makes the generator set empty for $n \le 1$, so $B_0$ and $B_1$ are trivial, as
intended. Two milestones are stated with the shift $n \mapsto n+1$ (i.e. for the projection
$F_{0,n+1}E^2 \to F_{0,n}E^2$) to avoid truncated subtraction in the maps.
Two conventions are worth flagging because they weaken what the Lean text asserts relative to
the prose. First, the goal asserts the existence of *some* isomorphism $B_n \cong \pi_1B_{0,n}E^2$;
it does not pin the isomorphism down on the geometric generators of Figure 2, since those loops
are not part of the formal development. Second, Artin's representation is formalized as the
existence of a homomorphism $\xi$ from $B_n$ to the automorphism group of the free group whose
value on each $\sigma_i$ is the explicit endomorphism of equation (1-14), together with its
injectivity; Theorem 1.9 is then stated for an arbitrary such $\xi$, given as a hypothesis, and
is non-vacuous precisely because Corollary 1.8.3 supplies one.
No trivializing formalization is available: the goal is an isomorphism statement between two
groups that are both defined independently of it, and the degenerate cases $n \le 1$ (both sides
trivial) are genuine special cases of it, not the content.
Infrastructure a complete development needs, all reusable: freeness of $\pi_1$ of a punctured
plane, local triviality of the Fadell–Neuwirth projection, the homotopy exact sequence of a
fibration in the range needed, presentations of split extensions, and the transfer of a
presentation along a regular covering. Contributions of any of these as standalone lemmas are
welcome, as is a formalization of the geometric generators (1-9) that would let the goal be
strengthened to pin the isomorphism on $\sigma_i$.
## Selected references
- E. Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- E. Artin, *Theory of braids*, Annals of Mathematics 48 (1947), 101–126.
https://doi.org/10.2307/1969218
- W.-L. Chow, *On the algebraical braid group*, Annals of Mathematics 49 (1948), 654–658.
https://doi.org/10.2307/1969333
- E. Fadell, L. Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962), 111–118.
https://doi.org/10.7146/math.scand.a-10517
- E. Fadell, J. Van Buskirk, *The braid groups of $E^2$ and $S^2$*, Duke Mathematical Journal 29
(1962), 243–257. https://doi.org/10.1215/S0012-7094-62-02925-3
- J. S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
Kawahira: The Riemann Hypothesis and Holomorphic Index in Complex DynamicsResearch Paper
## Motivation
The **Riemann hypothesis** asserts that every non-trivial zero of the Riemann zeta function $\zeta$ lies on the line $\operatorname{Re} s = 1/2$; the **simplicity hypothesis** asserts in addition that every such zero is a simple zero of $\zeta$. Both are statements about the location and the order of a discrete set of points in the complex plane, and almost every reformulation of them stays inside analytic number theory.
Kawahira (2016) gives a reformulation of a different kind. He attaches to $\zeta$ an explicit meromorphic self-map of the Riemann sphere and shows that the Riemann hypothesis together with the simplicity hypothesis is *equivalent* to a statement about the local dynamics of that map: it has no attracting fixed point. The translation is elementary once the right object is in place — the **holomorphic index** (residue fixed point index) of a fixed point — and it turns a question about zeros into a question about stability. This mission formalizes that translation, together with the supporting propositions on indices and multipliers that make it work.
## Setting
For a non-constant meromorphic $g : \mathbb{C} \to \widehat{\mathbb{C}}$, define the **nu function**
$$\nu_g(z) \;=\; z - \frac{g(z)}{z\,g'(z)}.$$
If $\alpha \neq 0$ is a zero of $g$ of order $m \ge 1$, then $\alpha$ is a fixed point of $\nu_g$ with **multiplier**
$$\lambda \;=\; \nu_g'(\alpha) \;=\; 1 - \frac{1}{m\alpha},$$
and if $\alpha$ is a pole of order $m$ the multiplier is $1 + \frac{1}{m\alpha}$. A fixed point $\alpha$ of a holomorphic map $f$ is **attracting** if $|f'(\alpha)| < 1$, **indifferent** if $|f'(\alpha)| = 1$, and **repelling** if $|f'(\alpha)| > 1$.
The **holomorphic index** of $f$ at a fixed point $\alpha$ is
$$\iota(f,\alpha) \;=\; \frac{1}{2\pi i}\oint_{C} \frac{dz}{z - f(z)},$$
the integral being over a small positively oriented circle around $\alpha$. When the multiplier $\lambda$ is not $1$ one has $\iota = \frac{1}{1-\lambda}$, and the Möbius map $\lambda \mapsto \frac{1}{1-\lambda}$ carries the unit disk onto the half-plane $\operatorname{Re}\iota > 1/2$. So a fixed point is attracting, indifferent or repelling exactly according to whether $\operatorname{Re}\iota$ is $> 1/2$, $= 1/2$ or $< 1/2$: the critical line reappears, in the index plane.
The point of the construction is that $\nu_g$ is engineered so that the index of $\nu_g$ at a simple zero $\alpha$ of $g$ is $\alpha$ itself (and $m\alpha$ at a zero of order $m$). Writing $\nu_\zeta = \nu_g$ for $g = \zeta$: a non-trivial zero $\alpha$ of order $m$ has index $m\alpha$, so $\operatorname{Re}\iota = m\operatorname{Re}\alpha$, and asking that this equal $1/2$ is asking for $m = 1$ and $\operatorname{Re}\alpha = 1/2$.
## Formalization targets
### Goal — Theorem 1 of the paper, conditions (a), (b), (c)
$$\Big(\text{RH} \wedge \text{simplicity}\Big) \iff \Big(\text{every non-trivial zero is an indifferent fixed point of } \nu_\zeta\Big) \iff \Big(\nu_\zeta \text{ has no attracting fixed point}\Big).$$
### Supporting targets
The milestones are the paper's Propositions 3, 4, 5, 7, 8, 9, its Theorem 11 (the variant for the Riemann xi function $\xi$), and Proposition 13 of the appendix (the Newton map $N_g(z) = z - g(z)/g'(z)$, for which every zero of $g$ becomes an *attracting* fixed point — the contrast that explains why $\nu_g$, and not $N_g$, sees the critical line).
## Significance
The equivalence converts the simultaneous truth of the Riemann and simplicity hypotheses into the non-existence of an attracting fixed point of one explicitly given meromorphic function. Nothing in the translation is conjectural: the content is the index computation, the symmetry $\alpha \mapsto 1 - \alpha$ of the non-trivial zeros supplied by the functional equation, and the classification of fixed points by the real part of the index. What a formalization adds is a machine-checked statement of the dictionary, and a reusable Lean development of the holomorphic index, which Mathlib does not currently contain — the index, its relation to the multiplier, and its behaviour at zeros and poles are general facts of one-variable complex dynamics, independent of this application.
Status, precisely: the Riemann hypothesis is open, and this mission does not ask anyone to settle it. Every target here is a theorem with a published proof; the work is to formalize those proofs. The goal theorem is an equivalence between two open statements, so it is provable without deciding either side.
## Difficulty
The obvious route to the goal — compute $\nu_\zeta'$ at a zero, apply the classification, done — fails in one direction. From "no attracting fixed point" one gets $\operatorname{Re}(m\alpha) \le 1/2$ for each non-trivial zero $\alpha$ of order $m$, which alone excludes neither a multiple zero nor a zero to the left of the critical line. The functional equation must be used to pair $\alpha$ with $1-\alpha$, whose index is $m(1-\alpha)$; only the two inequalities together force $m = 1$ and $\operatorname{Re}\alpha = 1/2$. A complete Lean proof therefore needs, besides the local computation: that the non-trivial zeros lie in the open strip $0 < \operatorname{Re} s < 1$, that $\alpha$ and $1-\alpha$ are zeros of the same order, and that the trivial zeros and the pole at $s = 1$ give repelling fixed points.
The index milestone (Proposition 3) is a residue computation on a small circle, and the hypotheses have to be arranged so that $z - f(z)$ has exactly one zero inside; the other genuinely analytic milestone is the order-$m$ computation of $\nu_g'$, where $g'$ vanishes at the fixed point when $m \ge 2$ and the singularity is removable rather than absent.
## Formalization scope
The development is over $\mathbb{C}$ with Mathlib's `riemannZeta`. Conventions the Lean statements commit to:
1. **Non-trivial zero** means: a zero of $\zeta$ that is not one of $-2, -4, -6, \dots$. Nothing about the critical strip is built into the definition; that the non-trivial zeros lie in $0 < \operatorname{Re} s < 1$ is part of the work.
2. **Simplicity** of a zero $\alpha$ is expressed as $\zeta'(\alpha) \neq 0$.
3. $\nu_g$ is a total function $\mathbb{C} \to \mathbb{C}$, using Lean's convention that division by zero returns zero. At a zero of $g$ this total function agrees with the genuine holomorphic extension of $\nu_g$, so multipliers there are the true ones. At a point where $g$ is non-zero and $g'$ vanishes, and at a pole of $g$, the total function takes an artefactual value; the statements about $\nu_\zeta$ therefore carry the explicit guard $\zeta(\alpha) = 0 \vee \zeta'(\alpha) \neq 0$ together with $\alpha \neq 0, 1$. The excluded points are exactly the pole of $\zeta$ (a repelling fixed point, by Proposition 7 of the paper) and the poles of $\nu_\zeta$, so the guarded statements are equivalent to the paper's, but they are guarded, and a reader should check that they consider the guards faithful.
4. The **xi function** is taken in Kawahira's normalization $\xi(z) = \frac{1}{2}z(1-z)\pi^{-z/2}\Gamma(z/2)\zeta(z)$, written in Lean through Mathlib's entire function $\Lambda_0$ so that the Lean $\xi$ is entire and has the correct values at $z = 0, 1$ rather than removable-singularity artefacts; the definition file carries a proved lemma identifying it with $\frac{1}{2}z(1-z)\Lambda(z)$ off $\{0,1\}$.
5. Conditions **(d)** and **(e)** of the paper's Theorems 1 and 10 — the purely topological reformulations in terms of a topological disk $D$ with $\nu_\zeta(D) \subset D$, and their homeomorphic deformations — are **not** part of this mission. They rest on the topological characterization of attracting fixed points (the paper's Proposition 2), whose proof uses the Riemann mapping theorem and the Schwarz–Pick lemma; the Riemann mapping theorem is not available in Mathlib, and the intended strength of the inclusion $\nu_\zeta(D) \subset D$ (compact containment) needs to be fixed before the statement can be formalized faithfully. Theorem 14 of the appendix, which is of the same topological kind, is likewise out of scope. A contribution supplying Proposition 2 in a defensible form would be welcome, as a separate mission.
Nothing here is vacuous: the goal is an equivalence of two statements each of which is satisfiable in form, and the guards exclude only points at which the Lean encoding of $\nu_\zeta$ is known not to model the meromorphic map.
Reusable beyond this mission: the holomorphic index, the multiplier classification, the general nu-function and Newton-map computations at a zero of order $m$ — all stated for an arbitrary function analytic at the point, not for $\zeta$.
## Selected references
- T. Kawahira, *The Riemann Hypothesis and Holomorphic Index in Complex Dynamics*, Experimental Mathematics (2016). https://doi.org/10.1080/10586458.2016.1217443
- J. Milnor, *Dynamics in One Complex Variable*, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006. (Holomorphic index: Lemma 12.2; topological characterization of fixed points: Section 8.)
- E. C. Titchmarsh, *The Theory of the Riemann Zeta Function*, 2nd ed., Oxford University Press, 1986. (Functional equation; trivial zeros; the xi function.)
- D. Schleicher, *Newton's Method as a Dynamical System: Efficient Root Finding of Polynomials and the Riemann $\zeta$ Function*, Fields Inst. Commun. 53 (2008), 213–224.
Herzog-Schönheim for finite pyramidal groupsResearch Paper
## Motivation
A **coset partition** of a group $G$ is a finite family of left cosets $a_1K_1, \dots, a_tK_t$ of
subgroups $K_i \le G$ that are pairwise disjoint and cover $G$. Asking which multisets of indices
$[G:K_i]$ can occur is a question with two independent origins. For $G = \mathbb{Z}$ the cosets are
arithmetic progressions and a coset partition is an **exact covering system** of the integers;
Erdős asked whether the moduli of such a system can be pairwise distinct, and Davenport and Rado,
and independently Mirsky and Newman, showed they cannot — the largest modulus must repeat. For
general groups, [Herzog and Schönheim (1974)](https://doi.org/10.4153/CMB-1974-025-7) asked the
same question: in any coset partition with $t > 1$, must two of the indices coincide? That question
is still open.
Progress has come by restricting the group. Berger, Felzenbaum and Fraenkel proved the conjecture
for finite **nilpotent** groups in [Canad. Math. Bull. 29 (1986)
329–333](https://doi.org/10.4153/CMB-1986-050-0), and the paper formalized here extends it to a
wider class defined by a chain condition. Later work bounds the order instead of the structure:
[Ginosar and Schnabel (2011)](https://www.researchgate.net/publication/265126234) settle every $G$
whose order has at most two prime divisors, and three prime divisors when $6 \nmid |G|$, while
[Margolis and Schnabel (2019)](https://arxiv.org/abs/1803.03569) verify all $|G| < 1440$. The
conjecture remains open even for finite solvable groups.
## Setting
Let $p(m)$ denote the least prime factor of $m$ and $P(m)$ the greatest, and let $\varphi$ be
Euler's totient function.
A finite group $G$ is **pyramidal** if it admits a chain of subgroups
$$ \{1\} = G_n \subseteq G_{n-1} \subseteq \cdots \subseteq G_1 \subseteq G_0 = G $$
in which every step has index equal to the least prime factor of the order of the preceding term:
$$ [G_{k-1} : G_k] = p\!\left(|G_{k-1}|\right), \qquad 1 \le k \le n. $$
A subgroup whose index is the smallest prime dividing the order is automatically normal, so the
chain is a composition series; consequently every pyramidal group is **solvable**, and every
**supersolvable** group is pyramidal. Pyramidality is therefore a chain condition sitting between
supersolvability and solvability.
Given a coset partition $a_1K_1, \dots, a_tK_t$ of $G$, write
$$ l \;=\; \frac{|G|}{\gcd\!\left(|K_1|, \dots, |K_t|\right)} . $$
## Target
The goal theorem is the multiplicity lower bound of Berger–Felzenbaum–Fraenkel. If $G$ is
pyramidal and the cosets $a_iK_i$, $1 \le i \le t$, partition $G$ with $t > 1$, then at least
$$ x \;=\; \left\lfloor \frac{P(l)\,\varphi(l)}{l} \right\rfloor + 1 $$
of the subgroups $K_i$ have the same order.
Two consequences are separate targets. Since $x \ge 2$ whenever $l \ge 2$, the bound yields the
**Herzog–Schönheim conjecture for pyramidal groups**:
$$ \exists\, i \ne j, \qquad [G : K_i] = [G : K_j], $$
and it likewise settles Burshtein's conjecture in this setting, which concerns the case
$\gcd(|K_i|) = 1$ and bounds the primes dividing $|G|$ in terms of the largest multiplicity.
## Significance
The bound is quantitative where the Herzog–Schönheim conjecture is qualitative: it does not merely
assert that a repetition exists but forces a repetition of prescribed multiplicity, growing with
the largest prime factor of $l$. That is what makes it strong enough to also imply Burshtein's
conjecture, which no purely qualitative statement does.
The class it covers is also of independent interest. Nilpotent groups are pyramidal, so the result
subsumes the authors' earlier theorem, and it reaches groups that are solvable but far from
nilpotent. It remains, more than three decades later, among the structural (as opposed to
order-bounded) cases in which the conjecture is known.
No part of this development is currently formalized: Mathlib has the ingredients — Sylow theory,
Hall subgroups of solvable groups, Euler's totient with Gauss's identity $\sum_{d \mid m}\varphi(d)
= m$ — but neither coset partitions as a structure, nor pyramidality, nor any case of
Herzog–Schönheim. The mission produces the first machine-checked proof of a structural case of the
conjecture, together with a reusable formal vocabulary for coset partitions.
## Difficulty
The reciprocal identity $\sum_i [G:K_i]^{-1} = 1$ is immediate and useless on its own: distinct
indices can satisfy it, so no counting argument over the indices alone can succeed.
The natural attack — induct along the chain, quotienting by $G_1$ — fails because a coset partition
does not descend to a quotient. A part $a_iK_i$ need not lie inside a single coset of $G_1$: if
$K_iG_1 = G$ then it meets every coset of $G_1$, and the induced family on $G/G_1$ is a cover with
multiplicity rather than a partition. Controlling that dichotomy is the first obstacle, and it is
precisely where the definition of pyramidality is used, the index $[G:G_1]$ being the *least* prime
factor of $|G|$ rather than an arbitrary one.
The second obstacle is that the conclusion counts subgroups of equal **order**, so the induction
must carry a lower bound on the size of a union of cosets that is sensitive to the orders $|K_i|$
and not merely to their number. The paper's device is a measure $\mu$ on the naturals with
$\mu(\{m\}) = \varphi(m)$, evaluated on the divisor closure of the set of orders; Gauss's identity
makes $\mu$ interact correctly with divisibility, and the required inequality is genuinely a
statement about the group, not about the multiset of orders. The final step splits off the Sylow
$P(|G|)$-subgroup against a Hall complement, which exists only because pyramidal groups are
solvable.
## Formalization scope
The development commits to the following conventions, all fixed in Lean and worth stating because
the prose leaves them implicit.
Coset partitions are indexed families rather than sets of cosets: `IsCosetPartition K a` asserts
that for every $x$ there is a **unique** index $i$ with $(a_i)^{-1}x \in K_i$. Indexing by `Fin t`
keeps multiplicities visible, which matters since the conclusion counts indices, not distinct
subgroups; and uniqueness encodes disjointness and covering simultaneously. Groups are finite via
`[Finite G]`, and orders and indices are `Nat.card` and `Subgroup.index`.
Pyramidality is stated as the existence of a length $n$ and a chain `c : ℕ → Subgroup G` with
`c 0 = ⊤`, `c n = ⊥`, and `Subgroup.relIndex (c (k+1)) (c k) = Nat.minFac (Nat.card (c k))` for
`k < n`. Normality of each step is a consequence, not a hypothesis, and is deliberately not assumed.
The greatest prime factor is `maxPrimeFac m = m.primeFactors.sup id`, which is $0$ for
$m \in \{0,1\}$; the floor in $x$ is natural-number division, so the goal statement is
`(maxPrimeFac l * Nat.totient l) / l + 1 ≤ …`. Note that the bound is vacuous at $l = 1$ — there
$P(1)\varphi(1)/1 = 0$ and $x = 1$ — so $t > 1$ is a necessary hypothesis and is present in every
statement that needs it; a formalization omitting it would be trivially true and is ruled out.
A complete development needs, beyond the goal: the coset intersection lemma; the least-prime-index
dichotomy; uniqueness of the Sylow $P(|G|)$-subgroup of a pyramidal group; the scaling law
$\mu(D(kR)) = k\,\mu(D(R))$ for the divisor-closure measure; the union lower bound; and
solvability of pyramidal groups. The coset-partition vocabulary and the union bound are reusable
for any other case of Herzog–Schönheim, including the still-open solvable case, and contributions
of alternative proofs or sharper variants are welcome.
## Selected references
- M. A. Berger, A. Felzenbaum, A. S. Fraenkel, *Remark on the multiplicity of a partition of a group into cosets*, Fundamenta Mathematicae **128** (1987) 139–144. [DOI](https://doi.org/10.4064/fm-128-3-139-144)
- M. A. Berger, A. Felzenbaum, A. S. Fraenkel, *The Herzog–Schönheim conjecture for finite nilpotent groups*, Canadian Mathematical Bulletin **29** (1986) 329–333. [DOI](https://doi.org/10.4153/CMB-1986-050-0)
- M. Herzog, J. Schönheim, *Research problem No. 9*, Canadian Mathematical Bulletin **17** (1974) 150.
- N. Burshtein, *On natural exactly covering systems of congruences having moduli occurring at most M times*, Discrete Mathematics **14** (1976) 205–214. [DOI](https://doi.org/10.1016/0012-365X(76)90033-0)
- I. Korec, Š. Znám, *On disjoint covering of groups by their cosets*, Mathematica Slovaca **27** (1977) 3–7.
- Z.-W. Sun, *On the Herzog–Schönheim conjecture for uniform covers of groups*, Journal of Algebra **273** (2004) 153–175. [DOI](https://doi.org/10.1016/S0021-8693(03)00526-X)
- L. Margolis, O. Schnabel, *The Herzog–Schönheim conjecture for small groups and harmonic subgroups*, Beiträge zur Algebra und Geometrie **60** (2019) 399–418. [arXiv](https://arxiv.org/abs/1803.03569)
The Gribov Region: Geometry of the Landau-Gauge Faddeev--Popov OperatorResearch Paper
## Motivation
Quantizing a Yang–Mills theory by the Faddeev–Popov procedure requires a **gauge condition** that picks one representative from each gauge orbit. In the **Landau gauge** the condition is $\partial_\mu A_\mu^a = 0$. Gribov showed in 1978 that this condition is not ideal: a gauge orbit can meet the surface $\partial_\mu A_\mu = 0$ more than once, so gauge-equivalent configurations — **Gribov copies** — are still being integrated over (V. N. Gribov, *Quantization of non-Abelian gauge theories*, Nucl. Phys. B139 (1978) 1). Infinitesimally, a copy of a transverse field $A$ corresponds to a zero mode of the **Faddeev–Popov operator** $M^{ab}(A) = -\partial_\mu D_\mu^{ab}(A)$, which is Hermitian on transverse configurations.
Gribov's proposed remedy is to restrict the functional integral to the **Gribov region** $\Omega$, the set of transverse configurations at which $M(A)$ is positive definite. The interest of $\Omega$ is not only that it removes infinitesimal copies: the fact that it is a *bounded* region of field space is the geometric input of Gribov's confinement scenario, because restricting the integration to a bounded region deforms the gluon propagator in the infrared and produces a mass scale. Whether the restriction to $\Omega$ is the physically correct prescription is still debated; the geometric properties of $\Omega$ themselves are not — they are consequences of the algebraic structure of $M(A)$, and they are what this mission formalizes.
Timeline of the properties at issue, as recorded in §2.2.1 (pp. 188–189) of the review by N. Vandersickel and D. Zwanziger, *The Gribov problem and QCD dynamics*, Phys. Rep. 520 (2012) 175–251 ([doi:10.1016/j.physrep.2012.07.003](https://doi.org/10.1016/j.physrep.2012.07.003)):
- 1978, Gribov: existence of copies infinitesimally across the horizon $\partial\Omega$ (Nucl. Phys. B139 (1978) 1).
- 1982, D. Zwanziger: $\Omega$ is convex and bounded in every direction (Nucl. Phys. B209 (1982) 336).
- 1982, M. Semenov-Tyan-Shanskii and V. Franke: the variational characterization of $\Omega$ by relative minima of $\|A^U\|^2$, and the fact that $\Omega$ still contains copies.
- 1989, G. Dell'Antonio and D. Zwanziger: $\Omega$ is contained in an ellipsoid (Nucl. Phys. B326 (1989) 333).
- 1991, G. Dell'Antonio and D. Zwanziger: every gauge orbit passes inside $\Omega$ (Comm. Math. Phys. 138 (1991) 291–299).
## Setting
Fix a real vector space $V$ of gauge-field configurations (in the physical situation, the transverse fields $A_\mu^a$) and a finite index set $\{1,\dots,n\}$ on which the Faddeev–Popov operator acts (colour index times a finite basis of fluctuation modes $\omega$). The formalization works with the algebraic structure that the Faddeev–Popov operator has, and nothing else:
$$ M(A) \;=\; M_0 \;+\; M_2(A), $$
where
- $M_0$ is the field-independent part, $M_0 = -\partial^2$ in the physical setting, taken here to be a fixed **symmetric positive definite** $n \times n$ real matrix;
- $A \mapsto M_2(A)$ is **linear** in $A$, and each $M_2(A)$ is a **symmetric traceless** real $n \times n$ matrix. In the physical setting $M_2(A)^{ab} = \partial_\mu f^{abc} A_\mu^c$, which is traceless already in the colour indices.
The **Gribov region** is
$$ \Omega \;=\; \{\, A \in V \;:\; M(A) \text{ is positive definite} \,\}, \qquad M(A) \text{ positive definite} \iff \forall\, w \neq 0,\ w^{\mathsf T} M(A)\, w > 0 . $$
This is Eq. (2.52) of the review, with positivity as in Eq. (2.54). The boundary $\partial\Omega$ is the **first Gribov horizon**, where the lowest non-trivial eigenvalue of $M(A)$ vanishes.
## Formalization targets
### Goal — $\Omega$ is a bounded convex set containing the origin
$$ 0 \in \Omega, \qquad \Omega \text{ convex}, \qquad \forall A \neq 0\ \exists \lambda_0 > 0\ \forall \lambda \ge \lambda_0:\ \lambda A \notin \Omega, \qquad \Omega \text{ bounded}. $$
The last two clauses are stated under the assumption that $A \mapsto M_2(A)$ is injective, i.e. that distinct configurations give distinct field-dependent parts; without it $\Omega$ contains the whole kernel of $M_2$ as a linear subspace and no boundedness statement can hold.
### Supporting statements
$$ M(\alpha A_1 + \beta A_2) = \alpha M(A_1) + \beta M(A_2) \quad (\alpha + \beta = 1), $$
$$ M \text{ symmetric},\ \operatorname{tr} M = 0,\ M \neq 0 \;\Longrightarrow\; \exists w:\ w^{\mathsf T} M w < 0 . $$
These are Eq. (2.53) and Eq. (2.58) of the review; they are the two ingredients from which convexity and directional boundedness follow.
## Significance
What the result gives: $\Omega$ is the region to which Gribov's improved gauge fixing restricts the functional integral, and every subsequent construction in this line of work — the no-pole condition, the horizon function and the local Gribov–Zwanziger action — presupposes that the restriction is to a bounded convex region containing the perturbative point $A = 0$. Convexity is what makes the horizon condition a single well-posed constraint; boundedness in every direction is the property from which the infrared suppression of the gluon propagator, and hence Gribov's mass scale, is read off. Without boundedness there is no geometric mechanism for a mass gap in this scenario.
Status honesty: these statements are proved mathematics, not open problems; the arguments in §2.2.1 of the review are short. What is missing is a machine-checked account. No formalization of the Gribov region in Lean is known to the drafter of this proposal; the platform's existing Gribov material concerns Singer's topological obstruction to continuous gauge fixing, which is a different theorem about a different object.
## Difficulty
The statements are elementary once the correct hypotheses are isolated, and the mission is calibrated accordingly: it is a faithfulness exercise rather than a depth exercise. The two places where a naive attempt fails are worth naming. First, directional boundedness does not follow from positivity alone: it needs the *tracelessness* of $M_2(A)$, which is what forces a direction $w$ with $w^{\mathsf T} M_2(A) w < 0$; a positive semidefinite perturbation would give a region unbounded along that ray. Second, "bounded in every direction" does not imply "bounded" for a general set, and the implication used here rests on convexity together with injectivity of $M_2$ — the argument goes through a limit of rescaled configurations and a closure of the positivity condition, not through a uniform bound extracted directly from the ray statement.
## Formalization scope
The mission commits to a finite-dimensional linear-algebra model of the Faddeev–Popov operator, packaged as a structure carrying: the matrix $M_0$ together with a proof that it is positive definite; the linear map $A \mapsto M_2(A)$ together with proofs that each $M_2(A)$ is symmetric and traceless. Configurations live in an arbitrary real vector space $V$, which carries a norm and finite-dimensionality only in the two statements where boundedness is asserted. Positive definiteness is Mathlib's notion for real matrices, which includes symmetry; the region is the set of configurations where it holds strictly, so $\Omega$ is the *open* region and the horizon is not part of it.
This is a model, not the field-theoretic object: it replaces the operator $-\partial_\mu D_\mu$ acting on transverse fields by its finite-dimensional algebraic shadow, and the reviewer should audit it as such. The properties targeted here are exactly those whose proofs in §2.2.1 use only linearity in $A$, symmetry, tracelessness, and positivity of $-\partial^2$; results that genuinely need the infinite-dimensional setting — that every gauge orbit passes inside $\Omega$, and that $\Omega$ still contains copies on its boundary — are deliberately out of scope, since they cannot be stated in this model.
The model is not vacuous: an instance exists already for $V = \mathbb{R}$, $n = 2$, $M_0 = I$ and $M_2(t) = t\,\mathrm{diag}(1,-1)$, with $M_2$ injective, so none of the statements is satisfied vacuously. Nor is any target trivially true: $\Omega$ is a proper nonempty subset of $V$ in that instance.
Infrastructure needed: Mathlib's positive-definiteness API for matrices, the spectral theorem for real symmetric matrices (for the traceless lemma), and basic convexity and boundedness in finite-dimensional normed spaces. The traceless lemma — a nonzero symmetric traceless matrix has a direction of negative quadratic form — is reusable well beyond this mission. Contributions extending the model towards the infinite-dimensional setting, or supplying the explicit ellipsoidal bound of Dell'Antonio–Zwanziger in place of plain boundedness, are welcome.
## Selected references
- N. Vandersickel, D. Zwanziger, *The Gribov problem and QCD dynamics*, Physics Reports 520 (2012) 175–251. https://doi.org/10.1016/j.physrep.2012.07.003
- V. N. Gribov, *Quantization of non-Abelian gauge theories*, Nuclear Physics B139 (1978) 1.
- D. Zwanziger, *Nonperturbative modification of the Faddeev–Popov formula and banishment of the naive vacuum*, Nuclear Physics B209 (1982) 336.
- M. Semenov-Tyan-Shanskii, V. Franke, *A variational principle for the Lorentz condition and restriction of the domain of path integration in non-abelian gauge theory*, 1982.
- G. Dell'Antonio, D. Zwanziger, *Ellipsoidal bound on the Gribov horizon contradicts the perturbative renormalization group*, Nuclear Physics B326 (1989) 333.
- G. Dell'Antonio, D. Zwanziger, *Every gauge orbit passes inside the Gribov horizon*, Communications in Mathematical Physics 138 (1991) 291–299.
Gribov Ambiguity: no continuous gauge fixing (Singer 1978)Research Paper
## Motivation
In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a
gauge-invariant weight over the space $\mathfrak{A}$ of vector potentials (connections) of a
principal bundle. The integrand is constant on the orbits of the group $\mathcal{G}$ of gauge
transformations, so the integral over $\mathfrak{A}$ diverges and one is supposed to integrate
instead over the orbit space $\mathfrak{R} = \mathfrak{A}/\mathcal{G}$. The Faddeev–Popov
procedure realizes this by *fixing a gauge*: choosing, continuously in the orbit, exactly one
vector potential on each orbit, and correcting by a Jacobian determinant.
V. N. Gribov (SLAC Translation 176, 1977) observed that for $SU(2)$ potentials on
$\mathbb{R}^3$ (or $\mathbb{R}^4$) with suitable conditions at infinity, the Coulomb gauge
condition does not do this: the Coulomb slice through the zero potential meets the orbit of the
zero potential again, far from the origin. These extra intersections are the **Gribov copies**;
R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.
I. M. Singer, *Some Remarks on the Gribov Ambiguity* (Commun. Math. Phys. **60** (1978) 7–12),
showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity
are those of Gribov — gauge transformations extending to the one-point compactification with
value $I$ at infinity, so that the base manifold is $M = S^3$ or $M = S^4$ — then **no**
continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space
of irreducible connections is weakly contractible, while the gauge group is not, and a
weakly contractible principal bundle admits no global continuous section.
## Setting
Fix $N \ge 2$ and take the structure group $SU(N)$, the group of $N \times N$ complex matrices
$U$ with $U^\ast U = I$ and $\det U = 1$, topologized as a subspace of matrices. Let
$S^r$ denote the unit sphere of $\mathbb{R}^{r+1}$, with base point $m$ the north pole.
For the trivial $SU(N)$-bundle over a space $M$, a gauge transformation is a map
$\varphi : M \to SU(N)$, and the **gauge group** is
$$\mathcal{G}(M,N) \;=\; C\bigl(M, SU(N)\bigr),$$
continuous maps with pointwise multiplication and the compact-open topology. Two subobjects
matter. The **based gauge group** $\mathcal{G}_m = \{\varphi : \varphi(m) = I\}$ is the subgroup
of transformations that are the identity at the base point. The constant transformations with
value in the centre $Z_N = \{e^{2\pi i k/N} I\}$ of $SU(N)$ form a normal subgroup, and the
**reduced gauge group** is the quotient
$$\overline{\mathcal{G}}(M,N) \;=\; \mathcal{G}(M,N)/Z_N$$
with the quotient topology. The centre acts trivially on vector potentials, so
$\overline{\mathcal{G}}$ is the group that acts effectively.
A group $G$ acting continuously on a space $\mathfrak{A}$ has orbit space
$\mathfrak{A}/G$ with the quotient topology, and a **gauge fixing** is a continuous map
$s : \mathfrak{A}/G \to \mathfrak{A}$ with $p \circ s = \mathrm{id}$, where
$p : \mathfrak{A} \to \mathfrak{A}/G$ is the projection: a continuous choice of exactly one point
on each orbit. The action is **principal** when it is free and the division map, which sends a
pair of points on one orbit to a group element carrying the second to the first, can be chosen
continuously; this is the topological content of "$p$ is a principal $G$-bundle". The space
$\mathfrak{A}$ is **weakly contractible** when it is nonempty and all its homotopy groups vanish.
In the paper, $\mathfrak{A}$ is the affine space of connections, $\mathfrak{R}$ its set of
irreducible members, and Theorems 1 and 2 say exactly that $\mathfrak{R}$ is a weakly
contractible principal $\overline{\mathcal{G}}$-space.
## Formalization targets
### Goal — Corollary 4 (no gauge fixing)
For $r \in \{3,4\}$, $N \ge 2$, and every weakly contractible principal
$\overline{\mathcal{G}}(S^r,N)$-space $A$:
$$\nexists\, s : A/\overline{\mathcal{G}}(S^r,N) \longrightarrow A \quad\text{continuous with}\quad p \circ s = \mathrm{id}.$$
By Theorems 1 and 2 of the paper the space of irreducible connections over $S^3$ or $S^4$ is such
an $A$, so the goal contains Singer's Corollary 4 for that space; it leaves the analytic
construction of the space of connections unfixed, which is what makes it statable today.
### Milestone level — Theorem 3
$$\exists\, j \ge 1: \quad \pi_j\bigl(\overline{\mathcal{G}}(S^r,N)\bigr) \neq 0, \qquad r \in \{3,4\},\ N \ge 2 .$$
### Milestone level — Theorem 5 and its homotopy inputs
$$\pi_j\bigl(\mathcal{G}_m(S^r,N)\bigr) \;\cong\; \pi_{j+r}\bigl(SU(N)\bigr), \qquad
\pi_3(SU(N)) \cong \mathbb{Z}, \qquad \pi_4(SU(N)) = 0 \ (N\ge 3), \qquad \pi_4(SU(2)) \cong \mathbb{Z}/2 .$$
## Significance
The result rules out the existence of a global gauge in the topological sense: every gauge
condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be
read as a local statement, patched with a partition of unity over the orbit space (as the last
section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be
repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction
of the functional integral to a fundamental domain.
Formalizing it adds a machine-checked version of an argument that is quoted far more often than
it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks:
homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for
$0 \to \mathcal{G}_m \to \mathcal{G} \to SU(N) \to 0$, and the classical computations
$\pi_3(SU(N)) \cong \mathbb{Z}$, $\pi_4(SU(N)) = 0$ for $N \ge 3$, $\pi_4(SU(2)) \cong \mathbb{Z}/2$.
Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned
revision contains homotopy groups as a definition together with their group structure, but
essentially no computation of them.
## Difficulty
The naive approach to the goal — build a section by hand, or average over the group — fails
because $\overline{\mathcal{G}}$ is neither compact nor contractible and the obstruction is
global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no
local argument can produce a contradiction. The proof has to convert a section into a
homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the
group as a retract of the total space, so all homotopy groups of the group would vanish; the work
is then to show that some homotopy group of the reduced gauge group does not vanish, which needs
the identification of the based gauge group with a mapping space, the exact sequences relating
$\mathcal{G}_m$, $\mathcal{G}$ and $\overline{\mathcal{G}}$, and non-trivial homotopy groups of
$SU(N)$ — including $\pi_6(S^3) \cong \mathbb{Z}/12$ for the $SU(2)$ case of Theorem 3.
## Formalization scope
The formalization commits to the following conventions, all of them visible in the definitions of
this mission.
- The bundle is the **trivial** $SU(N)$-bundle, so gauge transformations are literally maps
$M \to SU(N)$. This is the case of Gribov's original setting over $S^3$; over $S^4$ the paper
also treats bundles of nonzero Pontrjagin index, which are out of scope here.
- Gauge transformations are **continuous**, not smooth, with the compact-open topology; Singer's
Theorem 5 uses smoothing homotopies to pass between the two, and the homotopy-theoretic content
is the same.
- $SU(N)$ is the special unitary group of complex $N \times N$ matrices, with its subspace
topology; $S^r$ is the unit sphere of $\mathbb{R}^{r+1}$ with its subspace topology.
- Homotopy groups are Mathlib's `HomotopyGroup`, based at the identity element.
- The **space of connections is not constructed**: Mathlib has no space of connections on a
principal bundle, and building one is a mission of its own. The goal therefore quantifies over
an arbitrary topological space carrying a weakly contractible principal action of the reduced
gauge group — exactly the properties Theorems 1 and 2 establish for the irreducible
connections.
- This quantification is not vacuous: such spaces exist (the total space of a universal
$\overline{\mathcal{G}}$-bundle is one), so the goal is a genuine non-existence statement and
not a statement about an empty class. Conversely it is not trivially true: the hypotheses do
not mention any homotopy invariant of the gauge group, and refuting a section requires
Theorem 3.
- The paper's analytic statements — Theorem 1 (openness and density of the irreducible
connections, principal bundle structure), Theorem 2 (weak contractibility), Theorem 6
($\pi_1$ of the irreducible orbit space), Theorem 7 (no flat connection), Theorem 8 (tangency
of orbits to the Coulomb slice) and Theorem 9 (the canonical connection and its curvature) —
are out of scope until a space of connections exists in Lean. Contributions that build one, in
reusable form, are welcome and would let this mission be extended to them.
## Selected references
- V. N. Gribov, *Instability of non-abelian gauge theories and impossibility of choice of Coulomb
gauge*, SLAC Translation 176 (1977); Nucl. Phys. B **139** (1978) 1–19,
[doi:10.1016/0550-3213(78)90175-X](https://doi.org/10.1016/0550-3213(78)90175-X).
- I. M. Singer, *Some Remarks on the Gribov Ambiguity*, Commun. Math. Phys. **60** (1978) 7–12,
[doi:10.1007/BF01609471](https://doi.org/10.1007/BF01609471).
- R. Jackiw, I. Muzinich, C. Rebbi, *Coulomb gauge description of large Yang-Mills fields*,
Phys. Rev. D **17** (1978) 1576, [doi:10.1103/PhysRevD.17.1576](https://doi.org/10.1103/PhysRevD.17.1576).
- H. Toda, *Composition methods in homotopy groups of spheres*, Annals of Mathematics Studies 49,
Princeton University Press (1962).
The de Bruijn–Newman Constant is Non-negativeResearch Paper
## Motivation
The **Riemann hypothesis** asserts that all nontrivial zeros of the Riemann zeta function lie on the critical line. A classical way to measure how far the hypothesis is from failing runs through a one-parameter deformation of the Riemann $\xi$ function by the **backward heat flow**. De Bruijn (1950) introduced a family of entire functions $H_t$, $t \in \mathbb{R}$, with $H_0$ essentially the $\xi$ function, and showed that $H_t$ has only real zeros for $t \ge 1/2$. Newman (1976) proved that there is a finite constant $\Lambda$, now called the **de Bruijn–Newman constant**, such that $H_t$ has only real zeros precisely when $t \ge \Lambda$. The Riemann hypothesis is exactly the statement $\Lambda \le 0$, and Newman conjectured the complementary bound $\Lambda \ge 0$ — in his phrase, that if the Riemann hypothesis is true, then it is only barely so.
Timeline of lower bounds on $\Lambda$, all obtained before 2018 by exhibiting **Lehmer pairs**, that is, pairs of adjacent zeros of $\zeta$ that are unusually close together: $\Lambda > -\infty$ (Newman 1976), $\Lambda \ge -50$ (Csordas–Norfolk–Varga 1988), $\Lambda \ge -5$ (te Riele 1991), $\Lambda \ge -0.385$ (Norfolk–Ruttan–Varga 1992), $\Lambda \ge -0.0991$ (Csordas–Ruttan–Varga 1991), $\Lambda \ge -4.379 \times 10^{-6}$ (Csordas–Smith–Varga 1994), $\Lambda \ge -5.895 \times 10^{-9}$ (Csordas–Odlyzko–Smith–Varga 1993), $\Lambda \ge -2.63 \times 10^{-9}$ (Odlyzko 2000), $\Lambda \ge -1.15 \times 10^{-11}$ (Saouter–Gourdon–Demichel 2011). Rodgers and Tao closed the gap in 2020 by proving $\Lambda \ge 0$. In the other direction, de Bruijn's bound $\Lambda \le 1/2$ was sharpened to $\Lambda < 1/2$ by Ki–Kim–Lee (2009) and to $\Lambda \le 0.22$ by the Polymath 15 project (2019).
## Setting
For a real number $u$ put
$$\Phi(u) := \sum_{n=1}^{\infty}\bigl(2\pi^2 n^4 e^{9u} - 3\pi n^2 e^{5u}\bigr)\exp\bigl(-\pi n^2 e^{4u}\bigr),$$
a function that decays super-exponentially as $|u| \to \infty$ and satisfies $\Phi(u) = \Phi(-u)$. For each $t \in \mathbb{R}$ define the entire function
$$H_t(z) := \int_0^{\infty} e^{t u^2}\,\Phi(u)\,\cos(z u)\,du .$$
Each $H_t$ is even and satisfies $H_t(\bar z) = \overline{H_t(z)}$; the function $H_0$ is $\tfrac18 \xi\bigl(\tfrac12 + \tfrac{iz}{2}\bigr)$, so the Riemann hypothesis says exactly that every zero of $H_0$ is real. Write
$$S := \{\, t \in \mathbb{R} : \text{every zero of } H_t \text{ is real} \,\},\qquad \Lambda := \inf S .$$
By Pólya and Newman, $S$ is the ray $[\Lambda, \infty)$ with $-\infty < \Lambda \le 1/2$.
When $\Lambda < t \le 0$ the zeros of $H_t$ are real, simple, symmetric about the origin and avoid the origin, so they can be listed as $(x_j(t))_{j \in \mathbb{Z}^*}$, indexed by the nonzero integers, with $0 < x_1(t) < x_2(t) < \cdots$ and $x_{-j}(t) = -x_j(t)$. The **classical locations** $\xi_j$ are defined for $j \ge 1$ by $\Psi(\xi_j) = j$ with
$$\Psi(T) := \frac{T}{4\pi}\log\frac{T}{4\pi} - \frac{T}{4\pi},$$
extended by $\xi_{-j} = -\xi_j$; they are the positions the zeros would occupy if the Riemann–von Mangoldt counting formula were exact. Throughout, $\log_+ x := \log(2 + |x|)$.
## Formalization targets
### Goal — Newman's conjecture
$$\Lambda \ge 0, \qquad\text{equivalently}\qquad \text{every } t \text{ with } H_t \text{ having only real zeros satisfies } t \ge 0 .$$
The goal is stated in both forms simultaneously, so that it does not depend on any convention for the infimum of a set that might be empty or unbounded below.
### Milestones
The milestone list follows the architecture of Rodgers–Tao, which is a proof by contradiction: every milestone is stated under the standing hypothesis $\Lambda < 0$ of that paper, in the time ranges the paper uses ($\Lambda < t \le 0$, then $\Lambda/2 \le t \le 0$, then $\Lambda/4 \le t \le 0$). In order: an upper bound for $H_t$ near the real axis (Lemma 4); Riemann–von Mangoldt type counting formulae for the zeros of $H_t$ (Theorem 9); the resulting macroscopic description of the zeros (Corollary 10); the equations of motion $\partial_t x_k = 2\sum_{j \ne k} (x_k - x_j)^{-1}$ (Theorem 11); a quantitative lower bound on gaps between zeros (Proposition 13); a bound on the time-integrated renormalized energy (Theorem 17); and a bound on that energy at time $t = 0$ (Proposition 26). The last of these says that at time zero the zeros are, on average, locally in the equilibrium configuration of an arithmetic progression, which contradicts known results on the local distribution of zeros of $\zeta$.
## Significance
$\Lambda \ge 0$ settles Newman's conjecture, and together with the Riemann hypothesis it would force $\Lambda = 0$. Unconditionally, it says that the zeros of $\xi$ are not in local equilibrium: infinitely often, gaps between consecutive zeros deviate from the mean spacing, which is what makes the pair correlation phenomenology of Montgomery and of Conrey–Ghosh–Goldston–Gonek–Heath-Brown incompatible with $\Lambda < 0$. Any proof of the Riemann hypothesis must therefore be compatible with the hypothesis being tight in this sense.
The theorem has a complete published proof (Rodgers–Tao, *Forum of Mathematics, Pi*, 2020); it is not an open problem. What is missing is a machine-checked proof. To the extent the material has been formalized at all, the underlying objects — the $\xi$ function, the heat flow $H_t$, the counting function for zeros, the zero dynamics, the renormalized energies — are not available in Mathlib, so the mission produces reusable analytic infrastructure: bounds for a Fourier–Laplace type integral by the saddle point method, a Riemann–von Mangoldt counting argument via the argument principle, and a gradient-flow monotonicity framework for an infinite particle system with logarithmic interaction.
## Difficulty
The obvious route to $\Lambda \ge 0$ is the one used for every previous lower bound: exhibit Lehmer pairs of ever higher quality, since if $\Lambda$ were very negative the zeros of $H_0$ would repel each other and unusually close pairs of zeta zeros could not exist. Producing an infinite sequence of Lehmer pairs of arbitrarily high quality is possible under the GUE hypothesis, but the known unconditional upper bounds for small gaps between zeta zeros are too weak, even assuming the Riemann hypothesis. The proof instead upgrades repulsion to relaxation to local equilibrium: it must control the zeros of $H_t$ uniformly for $\Lambda < t \le 0$ at length scales as fine as $\log T$, with only the weaker counting formulae available for negative $t$ (an error term $O(\log_+^2 T)$ rather than $O(\log_+ T)$), and must make sense of a Hamiltonian and an energy that are given by divergent series, which requires truncation, renormalization, and careful control of all the resulting boundary terms.
## Formalization scope
The Lean development commits to the following conventions. $\Phi$ is a `tsum` over the positive integers and $H_t(z)$ is the Bochner integral over $(0, \infty)$ of $e^{tu^2}\Phi(u)\cos(zu)$; no convergence or entireness statement is built into the definition. $\Lambda$ is `sInf` of the set of admissible times, and the goal theorem also states the quantifier form "every admissible $t$ is nonnegative", so it cannot be satisfied by a junk value of the infimum. The zero families $(x_j(t))$ and the classical locations $(\xi_j)$ are not defined by choice functions: they enter the milestones as universally quantified functions $\mathbb{Z} \to \mathbb{R}$ subject to explicit predicates saying exactly which sequences they are, so a milestone asserts something about every valid enumeration. Asymptotic notation is unfolded: $O(\cdot)$ becomes an explicit existential constant, $o_{T \to \infty}(\cdot)$ an explicit $\varepsilon$–$T_0$ statement, and a principal value sum a limit of symmetric partial sums. Where a statement asserts the value of a time integral, absolute integrability is part of the conclusion, so the statement cannot be satisfied by the convention that a non-integrable function has integral zero.
One degeneracy is inherent to the source and is stated here explicitly: since the paper argues by contradiction, each milestone carries the hypothesis $\Lambda < 0$ (directly, or through a time range such as $\Lambda < t \le 0$). Once the goal theorem is proved, those hypotheses are unsatisfiable and the milestones become vacuously true. They are the intended attack path on the goal, not independent targets, and a solver who derives one of them from the goal theorem contributes nothing.
Contributions welcome: the analytic estimates for $H_t$ (Lemma 4) and the counting formulae (Theorem 9) are independent of the dynamical part and are the natural entry points; Mathlib-level infrastructure on the argument principle, the saddle point method, and Stirling asymptotics for $\Gamma$ in vertical strips is reusable well beyond this mission.
## Selected references
- B. Rodgers and T. Tao, *The de Bruijn–Newman constant is non-negative*, Forum of Mathematics, Pi 8 (2020), e6. https://doi.org/10.1017/fmp.2020.6
- N. G. de Bruijn, *The roots of trigonometric integrals*, Duke Math. J. 17 (1950), 197–226. https://doi.org/10.1215/S0012-7094-50-01720-0
- C. M. Newman, *Fourier transforms with only real zeros*, Proc. Amer. Math. Soc. 61 (1976), 246–251. https://doi.org/10.1090/S0002-9939-1976-0434982-5
- G. Csordas, W. Smith and R. S. Varga, *Lehmer pairs of zeros, the de Bruijn–Newman constant $\Lambda$, and the Riemann hypothesis*, Constr. Approx. 10 (1994), 107–129. https://doi.org/10.1007/BF01205170
- H. L. Montgomery, *The pair correlation of zeros of the zeta function*, Proc. Sympos. Pure Math. XXIV (1973), 181–193. https://doi.org/10.1090/pspum/024
- J. B. Conrey, A. Ghosh, D. Goldston, S. M. Gonek and D. R. Heath-Brown, *On the distribution of gaps between zeros of the zeta-function*, Q. J. Math. 36 (1985), 43–51. https://doi.org/10.1093/qmath/36.1.43
- D. H. J. Polymath, *Effective approximation of heat flow evolution of the Riemann $\xi$ function, and a new upper bound for the de Bruijn–Newman constant*, Res. Math. Sci. 6 (2019), 31. https://doi.org/10.1007/s40687-019-0193-1
Algebraicity of Weil classes on abelian sixfolds of discriminant -1Research Paper
## Motivation
The Hodge conjecture predicts that on a non-singular complex projective variety $X$ every rational cohomology class of type $(p,p)$ is a rational linear combination of the classes of algebraic subvarieties of $X$. Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A $2n$-dimensional complex abelian variety $A$ is **of Weil type** for an imaginary quadratic field $K=\mathbb{Q}(\sqrt{-d})$ if $K$ embeds into $\mathrm{End}_{\mathbb{Q}}(A)$ in such a way that both eigenspaces of $\eta(\sqrt{-d})$ meet $H^{1,0}(A)$ in an $n$-dimensional subspace. Such an $A$ carries a distinguished two-dimensional space of rational $(n,n)$-classes, the **Weil classes**, which for a generic $A$ of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.
Timeline of the unconditional results on algebraicity of Weil classes:
- A. Weil (1977) constructed the classes and showed that the generic abelian variety of Weil type has a three-dimensional space of rational $(n,n)$-classes, spanned by $h^n$ and the two-dimensional Weil plane.
- C. Schoen (Compositio Math. 65 (1988) and its 1998 Addendum, Compositio Math. 114) proved algebraicity for fourfolds of Weil type with $K=\mathbb{Q}(\sqrt{-3})$ and arbitrary discriminant, for sixfolds with $K=\mathbb{Q}(\sqrt{-3})$ and trivial discriminant, and for fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; a second proof of the last case is in B. van Geemen's survey (1994).
- K. Koike (Canad. Math. Bull. 47 (2004)) proved algebraicity for sixfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$, which yields fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and arbitrary discriminant.
- E. Markman (JEMS 25 (2023)) proved algebraicity for fourfolds, arbitrary $K$, and discriminant $1$.
- E. Markman, [arXiv:2502.03415](https://arxiv.org/abs/2502.03415), proves algebraicity for **sixfolds of discriminant $-1$ and every imaginary quadratic $K$**, and deduces the Hodge conjecture for all abelian fourfolds.
## Setting
Fix $g$ and present a $g$-dimensional complex torus by its first homology: a complex structure $J$ on $H_1(A,\mathbb{R})=\mathbb{R}^{2g}$ with $J^2=-1$, the lattice being $\mathbb{Z}^{2g}\subset\mathbb{R}^{2g}$. A **polarization** is a rational alternating form $E$ on $H_1(A,\mathbb{Q})=\mathbb{Q}^{2g}$ satisfying the Riemann relations $E(Jx,Jy)=E(x,y)$ and $E(x,Jx)>0$ for $x\neq 0$. Cohomology is $H^k(A,\mathbb{C})=\wedge^k H^1(A,\mathbb{C})$, realized as the alternating $\mathbb{C}$-multilinear forms on $H_1(A,\mathbb{C})=\mathbb{C}^{2g}$; a class is **rational** if its values on rational vectors are rational, and it has **type** $(p,q)$ if it is multiplied by $z^p\bar z^{q}$ under the scaling action $v\mapsto (\mathrm{Re}\,z)v+(\mathrm{Im}\,z)Jv$ of $z\in\mathbb{C}$. A **Hodge class** of degree $2p$ is a rational class of type $(p,p)$.
Let $g=2n$ and $K=\mathbb{Q}(\sqrt{-d})$ with $d>0$. A **polarized abelian $2n$-fold of Weil type** is such an $(A,E)$ together with a rational endomorphism $M=\eta(\sqrt{-d})$ of $H_1(A,\mathbb{Q})$ with
$$M^2=-d,\qquad MJ=JM,\qquad E(Mx,My)=d\,E(x,y),$$
the last condition saying that $\eta(k)$ multiplies the polarization class by the norm $\mathrm{Nm}(k)$, and such that each of the two eigenspaces $W,\overline{W}\subset H_1(A,\mathbb{C})$ of $M$ meets the $i$-eigenspace of $J$ in an $n$-dimensional subspace. The **Hodge–Weil classes** are the rational classes in
$$\widehat{HW}\;=\;\big(\wedge^{2n}W\;\oplus\;\wedge^{2n}\overline{W}\big)\cap H^{2n}(A,\mathbb{Q}),$$
equivalently the rational degree-$2n$ classes that vanish on every tuple of vectors containing both a vector of $W$ and a vector of $\overline{W}$.
The form $H(x,y)=E(Mx,y)+\sqrt{-d}\,E(x,y)$ is $K$-valued and hermitian on $H_1(A,\mathbb{Q})$, viewed as a $K$-vector space through $\eta$. The determinant of its Gram matrix in a $K$-basis lies in $\mathbb{Q}^{\times}$, and its class in $\mathbb{Q}^{\times}/\mathrm{Nm}(K^{\times})$ is the **discriminant** $\det H$ of $(A,\eta,h)$. Discriminant $-1$ means that this determinant equals $-(a^2+dc^2)$ for some rationals $a,c$ not both zero.
**Algebraicity** is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety $X\subseteq\mathbb{P}^N$ by a *projective realization*: a smooth, $\mathbb{Z}^{2g}$-periodic immersion $u:\mathbb{R}^{2g}\to X$, surjective onto $X$ and injective modulo the lattice, whose differential intertwines $J$ with the complex structure of $\mathbb{P}^N$. A class $w\in H^{2p}(A,\mathbb{C})$ is algebraic when some de Rham class of $X$ whose periods over the $2p$-cycles swept out by rational vectors $\lambda_1,\dots,\lambda_{2p}$ equal $w(\lambda_1,\dots,\lambda_{2p})$ is a rational combination of cycle classes $\mathrm{cl}(Z)$ of irreducible subvarieties $Z\subseteq X$ of dimension $g-p$. Cycle classes, de Rham cohomology of a projective variety, $(p,q)$-types and Hodge classes are taken from the platform's `HodgeConjecture` bundle, which formalizes §1 of Deligne's Clay problem description.
## Formalization targets
### Goal — Theorem 1.5.1 of arXiv:2502.03415
$$\text{For every } d>0:\ \text{the Hodge–Weil classes of a polarized abelian sixfold of Weil type with CM by }\mathbb{Q}(\sqrt{-d})\text{ and discriminant }-1\text{ are algebraic.}$$
The statement fixes neither the field $K$ nor the sixfold: it quantifies over every $d>0$, every polarized abelian sixfold of Weil type of discriminant $-1$, and every projective realization of it.
### Milestone — Weil's plane of Hodge–Weil classes (§1.1)
$$\widehat{HW}\ \text{is a two-dimensional }\mathbb{Q}\text{-space, and each of its elements has type }(n,n).$$
### Milestone — Schoen's degeneration step (§1.6)
$$\text{Goal for all sixfolds of discriminant }-1\ \Longrightarrow\ \text{Hodge–Weil classes of every abelian fourfold of Weil type are algebraic,}$$
for every imaginary quadratic $K$ and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.
### Milestone — Corollary 1.6.1
$$\text{The Hodge conjecture holds for abelian fourfolds.}$$
### Milestone — Lefschetz $(1,1)$
Divisor classes: every Hodge class in $H^2$ of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.
## Significance
Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold $H^{2,2}(A,\mathbb{Q})$ is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.
Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.
## Difficulty
The naive attack — write down subvarieties whose classes span $\widehat{HW}$ — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while $H^{n,n}(A,\mathbb{Q})$ is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf $\mathcal{E}$ on $X\times\hat X$, for $X$ the Jacobian of a genus-$3$ curve, whose characteristic class $\kappa(\mathcal{E})$ remains of Hodge type along all deformations of $(X\times\hat X,\eta,h)$ as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.
## Formalization scope
Conventions the Lean development commits to:
1. Complex tori are presented by $(J,E)$ on $\mathbb{R}^{2g}$ with the lattice $\mathbb{Z}^{2g}$; the polarization form is rational rather than integral, which is the isogeny-invariant form of the Riemann relations.
2. Cohomology is the space of alternating multilinear forms on $H_1(A,\mathbb{C})$, i.e. invariant forms on the torus; a period over a lattice cube is used to compare it with the de Rham cohomology of a projective realization.
3. The Weil condition is imposed symmetrically on both eigenspaces of $\eta(\sqrt{-d})$, so it does not depend on the choice of convention for $H^{1,0}$ versus $H^{0,1}$.
4. Discriminant $-1$ is stated as the existence of a $K$-basis in which the Gram determinant of $H$ is $-\mathrm{Nm}(k)$; changing the basis multiplies the determinant by a norm, so the condition is basis-independent.
5. Algebraicity always refers to cycle classes of subvarieties of an actual projective variety, in the sense of Deligne's formulation, never to an abstract subspace of "algebraic" classes; in particular the goal cannot be satisfied by exhibiting a formal object, and the hypotheses are satisfiable — abelian varieties of Weil type of discriminant $-1$ exist for every $K$, and abelian varieties admit projective realizations.
A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian $n$-fold, pure spinors and $K$-secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.
## Selected references
- E. Markman, *Cycles on abelian $2n$-folds of Weil type from secant sheaves on abelian $n$-folds*, arXiv:2502.03415. https://arxiv.org/abs/2502.03415
- A. Weil, *Abelian varieties and the Hodge ring*, Collected Papers III, Springer 1980, 421–429.
- C. Schoen, *Hodge classes on self-products of a variety with an automorphism*, Compositio Math. 65 (1988), 3–32; *Addendum*, Compositio Math. 114 (1998), 329–336. https://eudml.org/doc/89880
- B. van Geemen, *An introduction to the Hodge conjecture for abelian varieties*, Lecture Notes in Math. 1594, Springer 1994, 233–252. https://doi.org/10.1007/BFb0094425
- K. Koike, *Algebraicity of some Weil Hodge classes*, Canad. Math. Bull. 47 (2004), 566–572. https://doi.org/10.4153/CMB-2004-055-3
- B. Moonen, Y. Zarhin, *Hodge classes and Tate classes on simple abelian fourfolds*, Duke Math. J. 77 (1995), 553–581. https://doi.org/10.1215/S0012-7094-95-07717-5
- B. Moonen, Y. Zarhin, *Hodge classes on abelian varieties of low dimension*, Math. Ann. 315 (1999), 711–733. https://doi.org/10.1007/s002080050333
- J. Ramón Marí, *On the Hodge conjecture for products of certain surfaces*, Collect. Math. 59 (2008), 1–26. https://doi.org/10.1007/BF03191179
- E. Markman, *The monodromy of generalized Kummer varieties and algebraic cycles on their intermediate Jacobians*, J. Eur. Math. Soc. 25 (2023), 231–321. https://doi.org/10.4171/JEMS/1199
- P. Deligne, *The Hodge conjecture*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/hodge.pdf
## Motivation
Almost every classical question about prime values of polynomials is a special case of one
statement. Are there infinitely many twin primes? Infinitely many primes of the form $n^2+1$?
Infinitely many Sophie Germain primes $p$ with $2p+1$ prime? Each asks whether a fixed finite
list of integer polynomials takes prime values simultaneously infinitely often.
**Schinzel's Hypothesis H** (A. Schinzel and W. Sierpiński, 1958) is the single conjecture that
predicts "yes" in all these cases, subject to the two obvious obstructions: a polynomial that
factors cannot be prime infinitely often, and neither can a family whose product is always
divisible by some fixed prime.
**Timeline.**
- **1837** — Dirichlet proves the degree-one, single-polynomial case: if $\gcd(a,b)=1$ and
$a>0$, then $an+b$ is prime for infinitely many $n$.
- **1857** — Bunyakovsky states the single-polynomial case for arbitrary degree. It is open for
every fixed polynomial of degree $\ge 2$; not one instance, not even $n^2+1$, is known.
- **1904** — Dickson states the case of arbitrarily many linear polynomials.
- **1958** — Schinzel and Sierpiński state Hypothesis H in the generality used here
([Acta Arith. 4 (1958), 185–208](https://doi.org/10.4064/aa-4-3-185-208)).
- **1962** — Bateman and Horn give the conjectural asymptotic count of such $n \le N$, refining
Hypothesis H to a quantitative form
([Math. Comp. 16 (1962), 363–367](https://doi.org/10.1090/S0025-5718-1962-0148632-7)).
- **1978** — Iwaniec proves that $n^2+1$ has at most two prime factors infinitely often; the
sieve barrier that blocks "exactly one" has not been broken.
- **2004** — Green and Tao prove the analogous simultaneous-prime statement for systems of linear
forms of finite complexity, which yields arbitrarily long arithmetic progressions of primes but
does **not** cover Dickson's conjecture in full (the pair $n$, $n+2$ has infinite complexity).
- **2013** — Zhang, and then Maynard and Tao, establish bounded gaps between primes, i.e. that
*some* admissible pair $\{n+h_1, n+h_2\}$ is simultaneously prime infinitely often — but the
method does not identify which pair.
Hypothesis H itself remains open in every case that is not covered by Dirichlet's theorem.
## Setting
Work in the ring $\mathbb{Z}[X]$ of polynomials with integer coefficients. Fix a finite set
$\mathcal{F} \subseteq \mathbb{Z}[X]$ of polynomials $f$, each subject to the **Bunyakovsky
condition**:
- $\deg f \ge 1$;
- the leading coefficient of $f$ is positive;
- $f$ is irreducible in $\mathbb{Z}[X]$.
Irreducibility in $\mathbb{Z}[X]$ is strictly stronger than irreducibility in $\mathbb{Q}[X]$: it
also forces the content of $f$ to be $1$, ruling out $2X^2+2$.
Even an irreducible family can be blocked by congruences. The polynomial $X^2+X+2$ is
irreducible with positive leading coefficient, yet $n^2+n+2$ is even for every integer $n$, so it
is prime only when it equals $2$. The family $\mathcal{F}$ therefore also has to satisfy the
**Schinzel condition**: for every prime $p$ there exists an integer $n$ with
$$p \nmid \prod_{f \in \mathcal{F}} f(n).$$
Equivalently, no prime is a *fixed divisor* of the product $\prod_{f\in\mathcal{F}} f$. A family
satisfying both conditions is called **admissible**.
## Target
For an admissible family $\mathcal{F}$, write
$$S(\mathcal{F}) \;=\; \{\, n \in \mathbb{N} \;:\; |f(n)| \text{ is prime for every } f \in \mathcal{F} \,\}.$$
The goal of the mission is Hypothesis H:
$$\mathcal{F} \text{ admissible} \;\Longrightarrow\; S(\mathcal{F}) \text{ is infinite.}$$
The milestones are, in order: the linear one-polynomial case (Dirichlet); the reduction of the
Schinzel condition to the finitely many primes $p \le \sum_{f\in\mathcal F}\deg f$; the necessity
of the Schinzel condition; and three specializations of the goal — Bunyakovsky's conjecture, the
twin prime conjecture, and Landau's problem on $n^2+1$ — each stated as an implication from the
goal statement, so that they can be proved before the goal itself is.
## Significance
*The result itself.* Hypothesis H implies the twin prime conjecture, the Sophie Germain prime
conjecture, Landau's conjecture that $n^2+1$ is prime infinitely often, the infinitude of primes
in every admissible constellation, and Dickson's conjecture; with Bateman–Horn it also predicts
the density of such $n$. Nothing beyond the degree-one case is known, and the conjecture is the
standard yardstick against which sieve-theoretic progress on prime values of polynomials is
measured.
*Formalizing it.* The goal is open, so the mission's deliverable is not a proof of it but a
formal, audited statement of it together with a supporting environment: the admissibility
predicates, the classical reductions, and machine-checked derivations of the famous corollaries
from the goal. Dirichlet's theorem on primes in arithmetic progressions is already formalized in
Mathlib, so the linear milestone is a matter of connecting that result to this mission's
formulation rather than of new mathematics. The three "H implies …" milestones are provable now,
unconditionally, because they are implications; they are also the sharpest available check that
the goal statement has been formalized faithfully, since a mis-stated goal will usually fail to
yield twin primes.
## Difficulty
The obvious first idea — sieve the values $\prod_{f} f(n)$ for $n \le N$ and count survivors — is
exactly the idea that fails. Sieve methods lose a constant factor (the parity problem): they can
show that $\prod_f f(n)$ has few prime factors infinitely often, but they cannot distinguish
"one prime factor" from "two", which is why Iwaniec's $n^2+1$ result stops at $P_2$. The
analytic input that works for degree one — the nonvanishing of Dirichlet $L$-functions on
$\Re s = 1$ — has no known analogue for a polynomial of degree $\ge 2$, because the relevant
counting problem is not governed by characters of a finite abelian group. Milestones 1–3 are
elementary or already available in Mathlib; the goal itself is not expected to be resolved here.
## Formalization scope
Conventions fixed by the Lean development, and deliberately so:
- The family is a finite *set* of polynomials, so repeated polynomials collapse, and it is
allowed to be empty (the goal is then a statement about all of $\mathbb{N}$, and true).
- Primality is asserted of the absolute value $|f(n)|$ as a natural number. Since the leading
coefficient is positive and $\deg f \ge 1$, the values are eventually positive, so this is
equivalent to asking for a positive prime value at all large $n$.
- The variable $n$ ranges over $\mathbb{N}$, not $\mathbb{Z}$, and "infinitely often" means that
the set of such $n$ is infinite.
- Irreducibility is irreducibility in $\mathbb{Z}[X]$ (so primitivity is included), and the
degree hypothesis is $\deg f \ge 1$ in the sense of the natural-number degree.
- The Schinzel condition is stated as a condition on the product over the family, quantified over
all primes $p$ — not over $p$ up to a bound; milestone 2 is what reduces it to a finite check.
The statement admits no trivializing reading: the hypotheses are satisfiable (for example
$\{X, X+2\}$ and $\{X^2+1\}$ are admissible, as milestones 5 and 6 require one to verify), so the
goal is not vacuous, and the conclusion asserts infinitude rather than the existence of a single
$n$.
A complete development needs the admissibility predicates (supplied as the mission's definition
bundle), Mathlib's polynomial and modular-arithmetic APIs for the fixed-divisor arguments, and
Mathlib's Dirichlet theorem for milestone 1. The definition bundle and milestones 2–3 are
reusable for any future mission on Bateman–Horn, Dickson's conjecture, or prime constellations.
Contributions of further conditional consequences of the goal (Sophie Germain primes, prime
$k$-tuples, cousin primes) are welcome as additions to the tree.
## Selected references
- A. Schinzel and W. Sierpiński, *Sur certaines hypothèses concernant les nombres premiers*,
Acta Arithmetica 4 (1958), 185–208. [DOI](https://doi.org/10.4064/aa-4-3-185-208)
- P. T. Bateman and R. A. Horn, *A heuristic asymptotic formula concerning the distribution of
prime numbers*, Mathematics of Computation 16 (1962), 363–367.
[DOI](https://doi.org/10.1090/S0025-5718-1962-0148632-7)
- H. Iwaniec, *Almost-primes represented by quadratic polynomials*, Inventiones Mathematicae 47
(1978), 171–188. [DOI](https://doi.org/10.1007/BF01578070)
- B. Green and T. Tao, *The primes contain arbitrarily long arithmetic progressions*, Annals of
Mathematics 167 (2008), 481–547. [arXiv:math/0404188](https://arxiv.org/abs/math/0404188)
- J. Maynard, *Small gaps between primes*, Annals of Mathematics 181 (2015), 383–413.
[arXiv:1311.4600](https://arxiv.org/abs/1311.4600)
Algorithmic Game Theory V: Stable Matching and Trading without MoneyTextbook
# Algorithmic Game Theory V: Stable Matching and Trading without Money
## Motivation
When money is off the table and the Gibbard–Satterthwaite theorem (Mission III of this series) blocks general strategyproof choice, restricted preference domains reopen the door. The two great examples both come from allocation: Shapley–Scarf's housing market (1974), where Gale's Top Trading Cycle algorithm finds the unique core allocation and Roth (1982) showed the mechanism is strategy-proof; and the Gale–Shapley marriage market (1962), where deferred acceptance produces a stable matching, the men-optimal one, which Dubins–Freedman (1981) and Roth (1982) showed cannot be manipulated by any man. This machinery runs the US medical residency match and school choice systems worldwide, and the 2012 Nobel memorial prize to Roth and Shapley cites exactly the results of this mission. Chapter 10 (Schummer–Vohra, "Mechanism Design without Money") of Nisan–Roughgarden–Tardos–Vazirani (eds.), *Algorithmic Game Theory* (Cambridge, 2007) is the source text; its single-peaked §10.2 is left to a possible later mission, since it needs its own preference-domain machinery.
## Setting
**Marriage market** (§10.4): finite sets $M$ of men and $W$ of women, each agent holding a strict preference ordering over the opposite side (the preference-profile vocabulary of Mission III; $P\,i\,a\,b$ reads "$i$ strictly prefers $a$ to $b$"). Following the book's dummy-partner convention, $|M| = |W|$ and a **matching** is a bijection $\mu : M \simeq W$. A pair $(m, w)$ **blocks** $\mu$ if each prefers the other to their assigned partner; $\mu$ is **stable** if no pair blocks it. A stable $\mu$ is **male-optimal** if every man weakly prefers it to every stable alternative. A coalition **dominates** $\mu$ if it can rematch within itself with every member strictly better off; the **core** is the set of undominated matchings.
**Housing market** (§10.3): a finite set $N$ of agents, agent $i$ owning house $i$, each with a strict preference over all houses; an **allocation** is a permutation of $N$. A coalition **blocks** an allocation if it can redistribute the houses its members own so that all are weakly and someone strictly better off.
## Formalization targets
### Goal (capstone) — Theorem 10.13
Any mechanism selecting the male-optimal stable matching is strategy-proof for the men: no man can misreport his ordering and obtain a wife he truly prefers.
### Theorem 10.10 — existence
Every marriage market has a stable matching.
### Theorem 10.11 / Gale–Shapley 1962 — male-optimality
Some stable matching is weakly best for every man simultaneously. This man-by-man form is Gale–Shapley's optimal assignment (1962, Theorem 2); the book's Theorem 10.11 phrases male-optimality as the absence of a stable alternative making every man weakly and some man strictly better off, which is equivalent for finite strict markets — the equivalence being a (short) theorem, the attribution follows Gale–Shapley.
### Theorem 10.12 — the core
A matching is stable iff it is in the core of the matching game.
### Theorems 10.6 and 10.7 — housing
The core of the housing market is a single allocation, and the mechanism selecting it is strategy-proof.
## Significance
These are the foundational theorems of market design — the branch of mechanism design with the strongest record of deployed systems — and none of them exists in Lean. The mission also settles a methodological point for the series: algorithm-defined objects (deferred acceptance, top trading cycles) enter through the properties that characterize their outputs — male-optimality, core membership — so the theorems are statements about all mechanisms with the given property, and any construction of the algorithm proves the existence milestones. The matching vocabulary (bijections as matchings, blocking, stability, domination) is reusable for the college-admissions and roommates variants beyond this mission.
## Difficulty
Existence (10.10) is the real formalization work: whether by formalizing deferred acceptance and its termination or by another route (e.g. Adachi's fixed-point formulation, which the book sketches as Theorem 10.14 via Tarski), the solver must build the proposal machinery. Male-optimality (10.11) rides on the same construction with the "no man is ever rejected by an achievable wife" invariant. The core equivalence (10.12) is deliberately light — a transposition embeds a blocking pair as a two-agent coalition. Housing uniqueness (10.6) needs the cycle-peeling induction of TTC. The two strategyproofness results are the subtle ones: both known proof routes (Dubins–Freedman's combinatorial argument, or Roth's via the blocking lemma) require careful bookkeeping of which coalitions can improve under a misreport, and the mechanism is pinned only by its defining property, so proofs must use optimality/core facts rather than algorithm internals.
## Formalization scope
Preferences are strict total orders as in Mission III (`IsPrefProfile`), oriented "first argument preferred". Matchings are `Equiv`s; the book's $|M| = |W|$ convention enters the existence statements as the hypothesis `Nonempty (M ≃ W)` and nothing else about cardinalities is assumed. Domination and house-blocking quantify a rematching `Equiv` together with the improving coalition, coalitions being sets closed under the rematching — single-agent and pair coalitions are special cases, so no separate pair-blocking clause is needed in the core theorems. Mechanisms in the strategyproofness results are arbitrary functions constrained only by their defining property (male-optimal selection; core selection), quantified before the misreport — nothing may be chosen with hindsight. Both sides keep finiteness only where used: the core equivalence (10.12) holds for arbitrary types and carries no `Fintype`.
## Selected references
- D. Gale, L. S. Shapley, *College admissions and the stability of marriage*, Amer. Math. Monthly 69 (1962), 9–15. [DOI](https://doi.org/10.2307/2312726)
- L. Shapley, H. Scarf, *On cores and indivisibility*, J. Math. Econ. 1 (1974), 23–37. [DOI](https://doi.org/10.1016/0304-4068(74)90033-0)
- L. E. Dubins, D. A. Freedman, *Machiavelli and the Gale–Shapley algorithm*, Amer. Math. Monthly 88 (1981), 485–494. [DOI](https://doi.org/10.2307/2321753)
- A. E. Roth, *The economics of matching: stability and incentives*, Math. Oper. Res. 7 (1982), 617–628. [DOI](https://doi.org/10.1287/moor.7.4.617)
- A. E. Roth, *Incentive compatibility in a market with indivisible goods*, Econ. Letters 9 (1982), 127–132. [DOI](https://doi.org/10.1016/0165-1765(82)90003-9)
- N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), *Algorithmic Game Theory*, Cambridge University Press, 2007, Chapter 10. [DOI](https://doi.org/10.1017/CBO9780511800481)
Algorithmic Game Theory IV: VCG and the Limits of TruthfulnessTextbook
## Motivation
Mission III of this series ends at an impossibility: without money, incentive compatibility over three or more alternatives means dictatorship. This mission formalizes the classical escape route — **quasilinear utilities and payments** — and the exact price of it. Vickrey (1961) discovered that a second-price auction makes truth-telling dominant; Clarke (1971) and Groves (1973) generalized the idea to arbitrary social choice: welfare-maximizing rules can always be made truthful by the right payments. The converse program — which choice rules are implementable at all — runs through Rochet (1987) and Myerson (1981) to Saks–Yu (2005): weak monotonicity characterizes implementability on convex domains, and on single-parameter domains the characterization is complete and elementary — monotone rules with critical-value payments. Chapter 9, §§9.3 and 9.5 of Nisan–Roughgarden–Tardos–Vazirani (eds.), *Algorithmic Game Theory* (Cambridge, 2007), written by Nisan, is the source text.
## Setting
A set $A$ of **alternatives** and a finite set $\iota$ of **players**. Player $i$ holds a private **valuation** $v_i : A \to \mathbb{R}$ from a publicly known domain $V_i \subseteq \mathbb{R}^A$; utilities are quasilinear: choosing $a$ and charging $p_i$ gives $i$ utility $v_i(a) - p_i$. A **(direct revelation) mechanism** is a social choice function $f$ from valuation profiles to $A$ together with payment functions $p_i$ (Definition 9.14). The mechanism is **incentive compatible** if no unilateral misreport from the domain ever beats the truth (Definition 9.15).
A **VCG mechanism** (Definition 9.16) has $f$ maximizing social welfare $\sum_i v_i(a)$ and payments of the Groves form $p_i = h_i(v_{-i}) - \sum_{j\ne i} v_j(f(v))$; the **Clarke pivot rule** takes $h_i(v_{-i}) = \max_b \sum_{j \ne i} v_j(b)$. A rule is **weakly monotone** (Definition 9.28) if a unilateral change of valuation that moves the outcome from $a$ to $b$ satisfies $v_i'(b) - v_i'(a) \ge v_i(b) - v_i(a)$. A **single-parameter domain** (Definition 9.33) is given by a win set $W_i \subseteq A$ per player and bids $t \in [t_0, t_1]$: the valuation is $t$ on $W_i$ and $0$ elsewhere.
## Formalization targets
### Goal (capstone) — Theorem 9.36
A normalized mechanism (losers pay 0) on a single-parameter domain is incentive compatible **iff** the rule is monotone and every winning bid pays the critical value — the threshold below which the bid loses.
### Theorem 9.17 — VCG is truthful
Every VCG mechanism is incentive compatible.
### Lemma 9.20 — Clarke pivot
With Clarke pivot payments, a welfare-maximizing rule makes no positive transfers, and is individually rational when valuations are nonnegative.
### Theorem 9.29 — weak monotonicity
Necessity: incentive compatibility forces WMON, on any domain. Sufficiency: on convex domains, WMON rules admit implementing payments (Saks–Yu).
## Significance
These are the working theorems of every later mechanism-design mission: the approximation mechanisms of Chapter 12, the profit-maximization results of Chapter 13, and the sponsored-search analysis of Chapter 28 all argue through Theorem 9.36's monotonicity-plus-critical-value normal form, and VCG is the benchmark they approximate. Formalizing the cluster produces the platform's quasilinear-mechanism vocabulary — domains, truthfulness, Groves payments, weak monotonicity, single-parameter settings — on top of the social-choice layer of Mission III.
The capstone and Theorem 9.17 are textbook results with complete proofs in the source; the Saks–Yu half of Theorem 9.29 is stated but not proved in the book ("quite involved"), so that milestone carries a genuinely hard formalization with a published paper proof. None have prior Lean formalizations.
## Difficulty
Theorem 9.17 is a three-line inequality chase once the Groves form is unfolded — a deliberate warm-up. Lemma 9.20 adds the attained maximum over a finite alternative set. The necessity half of 9.29 is a two-application argument; the sufficiency half is the hard point of the mission: the known proofs walk two-cycle inequalities into a path-integral construction of payments on a convex domain, and nothing of the kind exists in Mathlib. For the capstone, the delicate part is the critical value: the book defines it as a supremum that "is undefined" when the player always wins, and the honest formal rendering — a constant payment `c` that is a least upper bound of the losing bids *whenever losing bids exist* — makes the case split explicit; the equivalence proof must thread monotonicity, the threshold structure of the winning set, and normalization through both directions.
## Formalization scope
Valuations are functions `A → ℝ`; domains are sets `V i : Set (A → ℝ)`; mechanisms are total functions with every property quantified only over profiles from the domain, so behavior on invalid inputs carries no content. The Groves term `hᵢ` is a function of the full profile constrained to be invariant under changes of coordinate `i` — the standard rendering of "depends only on $v_{-i}$". The Clarke payment uses a `Finset.sup'` over a finite nonempty `A`, so no junk supremum arises. In the single-parameter setting the valuation induced by a bid is `Set.indicator`, bids live in `Set.Icc t0 t1` with `t0 ≤ t1`, and the critical value is characterized by `IsLUB` guarded by nonemptiness of the losing set — the book's "undefined" caveat made precise without a junk `sSup`. Weak monotonicity's sufficiency half carries `Convex ℝ (V i)` and finite `A` (the Saks–Yu setting); the necessity half deliberately carries no hypotheses beyond incentive compatibility itself.
## Selected references
- W. Vickrey, *Counterspeculation, auctions, and competitive sealed tenders*, J. Finance 16 (1961), 8–37. [DOI](https://doi.org/10.1111/j.1540-6261.1961.tb02789.x)
- E. H. Clarke, *Multipart pricing of public goods*, Public Choice 11 (1971), 17–33. [DOI](https://doi.org/10.1007/BF01726210)
- T. Groves, *Incentives in teams*, Econometrica 41 (1973), 617–631. [DOI](https://doi.org/10.2307/1914085)
- M. Saks, L. Yu, *Weak monotonicity suffices for truthfulness on convex domains*, Proc. 6th ACM EC (2005), 286–293. [DOI](https://doi.org/10.1145/1064009.1064040)
- N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), *Algorithmic Game Theory*, Cambridge University Press, 2007, Chapter 9, §§9.3, 9.5. [DOI](https://doi.org/10.1017/CBO9780511800481)
An Introduction to Stochastic PDEs I: The Cameron–Martin TheoremTextbook
## Motivation
A stochastic partial differential equation is driven by noise that lives on an infinite-dimensional function space, and the first object one has to control is the law of that noise: a **Gaussian measure** on a separable Banach space. Martin Hairer's lecture notes *An Introduction to Stochastic PDEs* ([arXiv:0907.4178](https://arxiv.org/abs/0907.4178)) devote their first technical chapter (Section 4) to exactly this, because every later construction — stochastic convolutions, invariant measures for semilinear equations, the ergodic theory of the stochastic Navier–Stokes equations — is phrased against it.
The single structural fact that chapter produces is the **Cameron–Martin theorem** (Theorem 4.44, p. 31). It answers the question: in which directions may one translate an infinite-dimensional Gaussian measure without destroying its null sets? In finite dimensions the answer is "all of them", because Lebesgue measure is translation invariant. In infinite dimensions the admissible directions form a proper, and typically much smaller, Hilbert subspace $H_\mu \subset B$ — the Cameron–Martin space — and the translated measure is either equivalent to $\mu$ or mutually singular with it, with nothing in between. This dichotomy is the reason Girsanov-type changes of measure, Schilder-type large deviation rate functions, support theorems and Malliavin calculus all take the form they do.
## Setting
Throughout, $B$ is a separable Banach space, $B^{*}$ its topological dual, and $\mu$ a Borel probability measure on $B$.
$\mu$ is **Gaussian** (Definition 4.4, p. 19) if for every continuous linear functional $\ell \in B^{*}$ the push-forward $\ell_{*}\mu$ is a Gaussian measure on $\mathbb R$ in the sense of Definition 4.1, i.e. has characteristic function $\exp(-\tfrac{\sigma}{2}\ell^{2} + i\ell m)$; the degenerate case $\sigma = 0$, a Dirac mass, is included. It is **centred** if all these one-dimensional laws have mean zero, which is expressed here as $\int_B x \, \mu(dx) = 0$.
For a centred Gaussian $\mu$ the **covariance form** (4.2, p. 20) is
$$ C_\mu(\ell, \ell') \;=\; \int_B \ell(x)\,\ell'(x)\, \mu(dx), \qquad \ell, \ell' \in B^{*} . $$
It is well defined because $\|x\|^{2}$ is $\mu$-integrable, and it is a bounded bilinear form (Corollary 4.14, p. 22).
The **Cameron–Martin space** (Definition 4.26, p. 27) is classically built as the completion of
$$ \mathring H_\mu \;=\; \{\, h \in B : \exists\, h^{*} \in B^{*} \text{ with } C_\mu(h^{*}, \ell) = \ell(h) \ \ \forall \ell \in B^{*} \,\} $$
under $\|h\|_\mu^{2} = C_\mu(h^{*}, h^{*})$. This mission uses the equivalent intrinsic description of Exercise 4.38 (p. 29), which avoids the completion:
$$ \|h\|_\mu \;=\; \sup\{\, \ell(h) \;:\; \ell \in B^{*},\ C_\mu(\ell, \ell) \le 1 \,\}, \qquad H_\mu = \{\, h \in B : \|h\|_\mu < \infty \,\} . $$
The supremum is taken in $[0, \infty]$; since $-\ell$ is admissible whenever $\ell$ is, it equals $\sup |\ell(h)|$ over the same set. For $h \in B$ write $T_h : B \to B$, $T_h(x) = x + h$.
## Formalization targets
### Goal — Theorem 4.44 (Cameron–Martin)
For a centred Gaussian measure $\mu$ on a separable Banach space $B$ and $h \in B$,
$$ (T_h)_{*}\mu \ \ll \ \mu \qquad \Longleftrightarrow \qquad h \in H_\mu . $$
Both implications are asserted: translation along a Cameron–Martin direction produces an absolutely continuous measure, and translation along any other direction does not (in fact it produces a mutually singular measure).
### Milestones
The milestone list follows the route of Section 4.2:
1. Exercise 4.38 — the supremum description agrees with Definition 4.26 on $\mathring H_\mu$.
2. Proposition 4.32 — $H_\mu \subset B$ with $\|h\|^{2} \le \|C_\mu\| \, \|h\|_\mu^{2}$.
3. Proposition 4.40 — every $L^{2}(\mu)$-limit of elements of $B^{*}$ has a centred Gaussian law whose variance is its own $L^2$ norm squared.
4. Equation (4.14) — the explicit density $D_h(x) = \exp(h^{*}(x) - \tfrac12\|h\|_\mu^{2})$ of the shifted measure, for $h \in \mathring H_\mu$.
5. The total-variation separation bound $\|\mathcal N(0,1) - \mathcal N(m,1)\|_{\mathrm{TV}} \ge 2 - 2e^{-m^{2}/8}$ used in the converse half of Theorem 4.44.
6. Proposition 4.45 — $H_\mu$ is exactly the intersection of all measurable linear subspaces of full measure.
## Significance
The Cameron–Martin theorem is what makes the Cameron–Martin space a canonical object rather than a formal construction: $H_\mu$ is simultaneously the set of admissible shifts, the intersection of all full-measure linear subspaces (Proposition 4.45), and the space whose unit ball governs Gaussian isoperimetry (Theorem 4.53, Borell–Sudakov–Cirel'son). Downstream in the notes it is used to identify invariant measures of linear SPDEs and to compare them; outside the notes it is the starting point of Malliavin calculus and of large deviation theory for Gaussian measures.
Status, precisely. The Mathlib library pinned by this mission already contains a substantial part of Section 4: the predicate `IsGaussian` (Definition 4.4), uniqueness of measures with equal characteristic functionals on a separable Banach space (Propositions 4.8 and 4.11), invariance of $\mu \otimes \mu$ under rotations (Proposition 4.12), Fernique's theorem (Theorem 4.13), and the covariance form of (4.2) together with its boundedness (Corollary 4.14) as a continuous bilinear form on the dual. Those results are therefore not milestones here; they are the assumed foundation. What is absent, and what this mission asks for, is everything from the Cameron–Martin space onwards: its definition, its elementary properties, and Theorem 4.44 itself. No machine-checked proof of the infinite-dimensional Cameron–Martin theorem is known to the captain in any Lean library.
## Difficulty
The naive route — write down the two densities and take their ratio — is unavailable: there is no translation-invariant reference measure on an infinite-dimensional Banach space, so "the density of $\mu$" does not exist and the Radon–Nikodym derivative of $(T_h)_{*}\mu$ with respect to $\mu$ must be produced directly, as the exponential of a random variable.
That random variable is the obstruction. For $h \in \mathring H_\mu$ the functional $h^{*}$ is continuous and the computation is a characteristic-function identity. But $\mathring H_\mu$ is in general strictly smaller than $H_\mu$: a general $h \in H_\mu$ has an associated $h^{*}$ that exists only as an $L^{2}(\mu)$-limit of continuous functionals, defined $\mu$-almost everywhere and linear only on a measurable subspace of full measure (Propositions 4.34 and 4.39). Establishing that these limits are Gaussian with the expected variance (Proposition 4.40) is the technical bridge, and it is why milestone 3 is stated as a statement about $L^{2}$-limits rather than about elements of $B^{*}$.
The converse half has a different shape. One must produce, for $h \notin H_\mu$, a single one-dimensional projection that separates $\mu$ from $(T_h)_{*}\mu$ arbitrarily well; unboundedness of $\ell(h)$ over the covariance unit ball supplies $\ell$ with $C_\mu(\ell,\ell) = 1$ and $\ell(h)$ as large as desired, and the quantitative Gaussian total-variation bound of milestone 5 converts this into total variation distance $2$, i.e. mutual singularity.
## Formalization scope
The development is in Lean 4 with Mathlib, in the namespace `HairerSPDE`, shared by the whole series drawn from these notes. The conventions it commits to:
1. $B$ carries `NormedAddCommGroup`, `NormedSpace ℝ`, its Borel σ-algebra, `CompleteSpace` and `SecondCountableTopology` — the last two encode "separable Banach space".
2. Gaussianity is Mathlib's `IsGaussian`, which is Definition 4.4 verbatim; centredness is the extra hypothesis $\int x \, d\mu = 0$, needed because `IsGaussian` permits a non-zero mean.
3. The covariance form is Mathlib's `covarianceBilinDual`, which equals (4.2) for centred measures with finite second moment and is set to zero otherwise; Fernique's theorem rules the degenerate branch out for Gaussian measures.
4. The Cameron–Martin norm is the $[0,\infty]$-valued supremum above, so membership in $H_\mu$ is finiteness of that supremum; this is the only new definition the mission publishes.
5. Translation is `fun x ↦ x + h`, absolute continuity is Mathlib's `≪`, and "measurable linear subspace" is a `Submodule ℝ B` whose carrier is a measurable set.
The goal is an equivalence, so neither half can be discharged vacuously: the direction $h \in H_\mu \Rightarrow (T_h)_*\mu \ll \mu$ is non-trivial already for $h \ne 0$ in finite dimensions, and the converse has content precisely when $H_\mu \ne B$. Note that $\|0\|_\mu = 0$ always, and that for $\mu$ a Dirac mass the covariance form vanishes and $H_\mu = \{0\}$; both degenerate cases are inside the statement rather than excluded by hypothesis.
Contributions welcome beyond the milestones: the reproducing kernel space $R_\mu$ and the isomorphism of Proposition 4.34, measurable linear extensions (Proposition 4.39), the dilation singularity of Proposition 4.43, and $\mu(H_\mu) = 0$ in the infinite-dimensional case (second half of Proposition 4.45). All of these are reusable outside this mission.
## Selected references
- M. Hairer, *An Introduction to Stochastic PDEs*, lecture notes, 2009/2023. [arXiv:0907.4178](https://arxiv.org/abs/0907.4178)
- V. I. Bogachev, *Gaussian Measures*, Mathematical Surveys and Monographs 62, American Mathematical Society, 1998. [DOI:10.1090/surv/062](https://doi.org/10.1090/surv/062)
- X. Fernique, *Intégrabilité des vecteurs gaussiens*, C. R. Acad. Sci. Paris Sér. A-B 270 (1970), A1698–A1699.
- G. Da Prato, J. Zabczyk, *Stochastic Equations in Infinite Dimensions*, Cambridge University Press, 1992. [DOI:10.1017/CBO9780511666223](https://doi.org/10.1017/CBO9780511666223)
## Motivation
Galois theory attaches to every finite Galois extension $L/K$ a finite group $\mathrm{Gal}(L/K)$, the group of field automorphisms of $L$ fixing $K$ pointwise, and the fundamental theorem of Galois theory turns the subfield structure of $L/K$ into the subgroup structure of that group. The **inverse Galois problem** asks whether this correspondence is surjective over the rationals: given an arbitrary finite group $G$, is there a Galois extension $L/\mathbb{Q}$ with $\mathrm{Gal}(L/\mathbb{Q}) \cong G$? The question was posed in the early nineteenth century and is [unsolved](https://en.wikipedia.org/wiki/Inverse_Galois_problem).
What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.
- Cyclic and, more generally, finite **abelian** groups are realizable over $\mathbb{Q}$ by an explicit cyclotomic construction resting on Dirichlet's theorem on primes in arithmetic progressions.
- **Symmetric** and **alternating** groups are realizable over $\mathbb{Q}$; this is due to Hilbert, who realized them first over the rational function field $\mathbb{Q}(t)$ and then specialized $t$ using his irreducibility theorem.
- Every finite **solvable** group is realizable over $\mathbb{Q}$; this is Shafarevich's theorem (I. R. Shafarevich, *The imbedding problem for splitting extensions*, Dokl. Akad. Nauk SSSR **120** (1958), 1217–1219), obtained by solving embedding problems.
- Over $\mathbb{C}(t)$ — and over $K(t)$ for any algebraically closed $K$ of characteristic zero — *every* finite group is realizable, by the Riemann existence theorem. The obstruction to the goal is not the group theory; it is descending the field of constants to $\mathbb{Q}$.
- Case-by-case work covers large finite lists: all transitive permutation groups of degree at most $23$, and every sporadic simple group, are known to be realizable over $\mathbb{Q}$.
## Setting
Fix a field $K$ and a group $G$. A **Galois realization** of $G$ over $K$ is a field $L$ equipped with a $K$-algebra structure such that the extension $L/K$ is Galois — normal and separable — together with a group isomorphism
$$ G \;\cong\; \mathrm{Gal}(L/K), $$
where $\mathrm{Gal}(L/K)$ denotes the group of $K$-algebra automorphisms of $L$ under composition. The group $G$ is **realizable over $K$**, written `IsRealizable K G`, when at least one Galois realization of $G$ over $K$ exists. No finiteness of $L/K$ is imposed in the definition; it is automatic once $G$ is finite, because an infinite Galois extension has infinite automorphism group.
Two base fields beyond $\mathbb{Q}$ appear throughout. $K(t)$ denotes the field of rational functions in one variable over $K$, written `RatFunc K`; and for the statement that a group is realizable over *some* number field, the base field ranges over the intermediate fields of $\mathbb{C}/\mathbb{Q}$.
## Formalization targets
### Goal — the inverse Galois problem
$$ \text{for every finite group } G, \qquad \exists\, L/\mathbb{Q} \text{ Galois with } \mathrm{Gal}(L/\mathbb{Q}) \cong G. $$
The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.
### Milestones — the known partial results
$$ G \text{ cyclic} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, \qquad G \text{ abelian} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, $$
$$ \mathrm{Sym}(S),\; A_n \text{ realizable over } \mathbb{Q}, \qquad G \text{ solvable} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, $$
$$ \exists\, K,\ \mathbb{Q} \subseteq K \subseteq \mathbb{C},\ G \text{ realizable over } K, $$
$$ G \text{ realizable over } \mathbb{C}(t), \qquad G \text{ realizable over } K(t) \ (K \text{ algebraically closed, char } 0), $$
$$ G \text{ realizable over } \mathbb{Q}(t) \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}. $$
The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.
## Significance
The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over $\mathbb{Q}$: every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over $\mathbb{Q}$ is publishable work, as the recent additions of the degree-$17$ group $17T7$ ([van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024](https://arxiv.org/abs/2411.07857)) and of the Mathieu group $M_{23}$ show.
Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for "$G$ is a Galois group over $K$", nor any of the milestones above. Every milestone here is a *proved* theorem of classical number theory and an *unformalized* one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.
## Difficulty
The obvious strategy fails at a well-understood point. Over $\mathbb{C}(t)$ the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from $\mathbb{Q}(t)$ to $\mathbb{Q}$. What is missing is the step in between: producing the cover *over $\mathbb{Q}$* rather than over $\mathbb{C}$, i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.
A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.
## Formalization scope
The mission fixes one definition file, published first, carrying the structure `GaloisRealization` and the one-field class `IsRealizable`. Conventions it commits to:
- `IsGalois K L` is Mathlib's Galois condition (normal and separable); finiteness of the extension is *not* assumed.
- The isomorphism is with the full automorphism group $L \simeq_{\mathrm{alg}[K]} L$, not with a quotient or a subgroup of it.
- The carrier $L$ of a realization is required to live in the same universe as $K$. This costs no generality for the statements of the mission — for finite $G$ a realization is a finite extension of $K$ — and keeps every statement universe-monomorphic.
- $\mathrm{Sym}(S)$ is `Equiv.Perm S` for a finite type $S$, and $A_n$ is `alternatingGroup (Fin n)`; degenerate small cases are included rather than excluded.
- Solvability is `Group.IsSolvable`.
The statements cannot be satisfied vacuously: `IsRealizable K G` asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over $\mathbb{Q}(t)$ as an explicit hypothesis.
Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form "$\mathrm{Gal}(L/L^H) \cong H$"; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.
## Selected references
- Inverse Galois problem, *Wikipedia*. https://en.wikipedia.org/wiki/Inverse_Galois_problem
- I. R. Shafarevich, *The imbedding problem for splitting extensions*, Dokl. Akad. Nauk SSSR **120** (1958), 1217–1219.
- C. U. Jensen, A. Ledet, N. Yui, *Generic Polynomials: Constructive Aspects of the Inverse Galois Problem*, MSRI Publications 45, Cambridge University Press, 2002. http://library.msri.org/books/Book45/files/book45.pdf
- G. Malle, B. H. Matzat, *Inverse Galois Theory*, Springer Monographs in Mathematics, 1999.
- R. van Bommel, E. Costa, N. D. Elkies, T. Keller, S. Schiavone, J. Voight, *17T7 is a Galois group over the rationals*, arXiv:2411.07857, 2024. https://arxiv.org/abs/2411.07857
Local Connectivity of the Mandelbrot Set (MLC)Open Problem
## The set
For a complex parameter $c$, iterate the quadratic map
$$f_c(z) = z^2 + c$$
starting at the critical point $z = 0$. The **Mandelbrot set** is the set of parameters for which this orbit stays bounded:
$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$
Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.
$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism
$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$
between the complement of $M$ and the exterior of the closed unit disk.
## The question
**MLC conjecture.** *$M$ is locally connected*: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.
By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the *pinched disk* model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the **density of hyperbolicity** in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and **zero area for $\partial M$**.
MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.
## Timeline
- **1982** -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
- **1984/85** -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
- **1990** -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
- **1997** -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
- **1997** -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the *real* quadratic family.
- **1998** -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive *area* remains open.
- **2005** -- Buff and Cheritat construct quadratic *Julia* sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
- **Today** -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.
## What this mission asks for
The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".
The milestones are of three kinds, and are ordered accordingly:
1. **Foundations provable today** -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. **Known theorems from the literature** -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. **The open companions** -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.
All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.
## Motivation
Chapter 11 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) replaces the Riemann integral of Chapter 6 with the **Lebesgue integral**, and the reward
is a theory of integration whose limit theorems have no superfluous hypotheses and whose space
of square-integrable functions is complete. The chapter runs from set functions and outer
measures, through the Carathéodory construction of Lebesgue measure, measurable functions and
the integral, to the convergence theorems (monotone convergence, Fatou, dominated convergence)
and finally to the space $\mathscr{L}^2(\mu)$ and the **Riesz–Fischer theorem** (Theorem 11.42):
$$\text{every Cauchy sequence in } \mathscr{L}^2(\mu) \text{ converges in the mean to an element of } \mathscr{L}^2(\mu).$$
That completeness is what makes $\mathscr{L}^2$ a Hilbert space, and it is the reason the
Fourier series of Chapter 8 converge in the mean to the functions they represent.
This mission is the eleventh and last in a series formalizing Rudin Chapters 1–11. It uses the
Riemann–Stieltjes integral of Mission VI (for Theorem 11.33, comparing the two integrals) and
the trigonometric Fourier series of Mission VIII (for the $\mathscr{L}^2$ reading of Parseval's
theorem).
## Setting
A **set function** on a ring $\mathscr{R}$ of sets is *countably additive* if it takes the value
$\sum \phi(A_n)$ on a countable disjoint union. Rudin constructs an **outer measure** $\mu^*$
from such a $\phi$ by covering with elementary sets and taking an infimum, calls a set
**measurable** when it is approximable by elementary sets in the metric $d(A, B) = \mu^*(A
\triangle B)$, and proves that the measurable sets form a $\sigma$-algebra on which $\mu^*$ is
countably additive (Theorem 11.10). A real function $f$ is **measurable** when $\{x : f(x) > a\}$
is measurable for every $a$, and the integral $\int_E f\,d\mu$ is defined first for simple
functions, then for nonnegative measurable functions as a supremum, and then for general $f$ by
$f = f^+ - f^-$.
The space $\mathscr{L}^2(\mu)$ consists of the measurable $f$ with $\int |f|^2 d\mu < \infty$,
normed by $\|f\|_2 = (\int |f|^2 d\mu)^{1/2}$; a sequence $\{f_n\}$ **converges in the mean** to
$f$ if $\|f_n - f\|_2 \to 0$.
Mathlib's measure theory is used wherever it is mathematically the same object:
`MeasureTheory.OuterMeasure` and its Carathéodory $\sigma$-algebra, `MeasurableSet`,
`Measurable`, the lower Lebesgue integral `∫⁻` for nonnegative extended-real functions, the
Bochner integral `∫` and `Integrable` for the general case. What is set up freshly is Rudin's
$\mathscr{L}^2$ **of functions** — `Rudin.MemL2`, `Rudin.L2Norm`, `Rudin.CauchyL2`,
`Rudin.TendstoL2` — rather than Mathlib's quotient space `Lp`, because the Riesz–Fischer theorem
as Rudin states it produces an honest limit *function*, and the ε-N phrasing of Cauchyness and
of mean convergence is part of the statement.
## Formalization targets
### Goal — the Riesz–Fischer theorem (Theorem 11.42)
If $\{f_n\}$ is a Cauchy sequence in $\mathscr{L}^2(\mu)$, then there exists $f \in
\mathscr{L}^2(\mu)$ with $\|f_n - f\|_2 \to 0$: the space $\mathscr{L}^2(\mu)$ is complete.
Rudin's proof extracts a subsequence with $\|f_{n_{k+1}} - f_{n_k}\|_2 < 2^{-k}$, sums the
telescoping series, uses the monotone convergence theorem and the Schwarz inequality to show
that the sum converges almost everywhere, and identifies the pointwise limit as the mean limit
of the whole sequence. Every ingredient is a milestone of this mission.
### Milestones
$$\text{the measurable sets of an outer measure form a } \sigma\text{-algebra on which it is countably additive} \qquad (11.10)$$
$$\sup_n f_n \text{ and } \limsup_n f_n \text{ are measurable} \qquad (11.17)$$
$$|f|,\ f+g,\ fg \text{ are measurable} \qquad (11.16,\ 11.18)$$
$$E \mapsto \int_E f\,d\mu \text{ is countably additive} \qquad (11.24)$$
$$\left|\int f\,d\mu\right| \le \int |f|\,d\mu \qquad (11.26,\ 11.27)$$
$$\int \lim_n f_n \,d\mu = \lim_n \int f_n\,d\mu \ \text{ for } 0 \le f_1 \le f_2 \le \cdots \qquad (11.28)$$
$$\int \sum_n f_n \,d\mu = \sum_n \int f_n\,d\mu \ \text{ for } f_n \ge 0 \qquad (11.30)$$
$$\int \liminf_n f_n\,d\mu \le \liminf_n \int f_n\,d\mu \qquad (11.31)$$
$$\text{dominated convergence} \qquad (11.32)$$
$$\text{Riemann-integrable} \Rightarrow \text{Lebesgue-integrable, with the same integral} \qquad (11.33)$$
$$\left|\int fg\,d\mu\right| \le \|f\|_2\,\|g\|_2 \qquad (11.35)$$
$$\text{continuous functions are dense in } \mathscr{L}^2[a,b] \qquad (11.38)$$
$$\sum_n c_n^2 = \int f^2 d\mu \text{ for a complete orthonormal system} \qquad (11.45)$$
## Significance
The Lebesgue theory is the point at which analysis acquires limit theorems that do not require
uniform convergence. Monotone convergence, Fatou's lemma and dominated convergence are the three
statements that make the integral usable in probability, in Fourier analysis and in the theory
of partial differential equations, and the Riesz–Fischer theorem is what makes $\mathscr{L}^2$ a
Hilbert space and therefore the natural home of Fourier expansions: Parseval's identity
(11.45) is the assertion that the Fourier coefficient map is an isometry onto $\ell^2$.
Theorem 11.33 is the bridge back to the earlier chapters — every Riemann-integrable function is
Lebesgue-integrable with the same integral, and a bounded function on $[a, b]$ is
Riemann-integrable exactly when it is continuous almost everywhere — so the two halves of the
book agree wherever both apply.
Mathlib has an extensive measure theory and proves many of these results in considerable
generality. This mission's contribution is to state them in Rudin's formulation, for Rudin's
$\mathscr{L}^2$ of functions and with his explicit ε-N definitions, so that the chapter is
available as a coherent, self-contained unit that matches the textbook line by line and links
back to the Riemann–Stieltjes integral of Mission VI.
## Difficulty
Individually, most milestones will reduce to Mathlib results after the correct dictionary is in
place, and the interesting work is exactly in that translation: Rudin's measurability
(`{x : f(x) > a}` measurable) versus Mathlib's `Measurable`, Rudin's integral of a nonnegative
function versus `∫⁻` with values in `ℝ≥0∞`, Rudin's $\mathscr{L}^2$ of genuine functions versus
`Lp` as a quotient by almost-everywhere equality. The last of these is what makes the goal
theorem nontrivial to derive: Mathlib's completeness of `Lp` gives a limit *class*, and one must
choose a measurable representative and verify Rudin's mean convergence with the concrete norm
`Rudin.L2Norm`, which is `Real.sqrt (∫ f²)` and not an `ENNReal` quantity.
Theorem 11.33 (Riemann implies Lebesgue) and Theorem 11.38 (density of continuous functions)
are the two other places where real work is required: the first has to connect the Chapter 6
definition of the Riemann integral with `intervalIntegral`, and the second is an approximation
argument.
## Formalization scope
Conventions fixed by this mission:
* Measure-theoretic vocabulary is Mathlib's: `MeasureTheory.Measure`, `MeasurableSet`,
`Measurable`, `Integrable`, `∫⁻ x, f x ∂μ` for nonnegative `ℝ≥0∞`-valued integrands and
`∫ x, f x ∂μ` for the general real case. Rudin's Carathéodory construction is
`MeasureTheory.OuterMeasure.caratheodory`.
* Statements about suprema and upper limits of sequences of functions (11.17), and about
term-by-term integration of series (11.30) and Fatou's theorem (11.31), use `ℝ≥0∞`-valued
functions, matching Rudin's use of extended real values there.
* `Rudin.MemL2 μ f` is "`f` is measurable and `f²` is integrable"; `Rudin.L2Norm μ f` is
`Real.sqrt (∫ x, (f x)^2 ∂μ)`; `Rudin.CauchyL2` and `Rudin.TendstoL2` are Rudin's ε-N Cauchy
condition and mean convergence. No quotient is taken, so the goal theorem produces a function.
* Theorem 11.33 is stated with `Rudin.RiemannIntegrable` and `Rudin.RiemannIntegral` from
Mission VI, so the two integrals are literally compared.
* Parseval (11.45) is stated for an arbitrary complete orthonormal system in $\mathscr{L}^2(\mu)$,
completeness being phrased as "a function orthogonal to every $\varphi_n$ has norm zero";
the trigonometric case is Theorem 8.16 of Mission VIII.
Contributions of the convergence theorems (11.28, 11.31, 11.32) and of the Schwarz inequality
(11.35) are especially useful, since the goal theorem consumes them directly.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 11 (pp. 300–332).
- Walter Rudin, *Real and Complex Analysis*, 3rd edition, McGraw-Hill, 1987, Chapters 1–3.
## Motivation
Chapter 8 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) puts the general theory of the preceding chapters to work on concrete functions. Power
series are differentiated term by term; the exponential function is *defined* by its series and
the trigonometric functions and the number $\pi$ are extracted from it; the fundamental theorem
of algebra is proved; Fourier series are introduced through general orthonormal systems; and the
Gamma function is characterized by log-convexity.
The chapter's capstone is **Parseval's theorem** (Theorem 8.16): for Riemann-integrable
$2\pi$-periodic functions, the Fourier series converges in the mean square sense and the
$L^2$ inner product is computed by the (absolutely convergent) sum of products of Fourier
coefficients. It is the statement that the trigonometric system is not merely orthonormal but
*complete*, and it is the finite-dimensional Pythagorean theorem carried to infinite dimensions.
This mission is the eighth in a series formalizing Rudin Chapters 1–11; it uses the convergence
tests of Mission III and the uniform-convergence and approximation theorems of Mission VII, and
it is the analytic counterpart of the abstract $L^2$ theory of Mission XI.
## Setting
A **power series** is $\sum c_n x^n$; by Chapter 3 it converges on an interval $(-R,R)$. A
sequence $\{\varphi_n\}$ of complex functions on $[a,b]$ is an **orthonormal system** if
$\int_a^b \varphi_n \overline{\varphi_m} = 0$ for $n \ne m$ and $\int_a^b |\varphi_n|^2 = 1$; the
**Fourier coefficients** of $f$ relative to it are $c_n = \int_a^b f \overline{\varphi_n}$, and
the **Fourier series** is $\sum c_n \varphi_n$. For the trigonometric system on $[-\pi,\pi]$ one
writes
$$c_n = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(x)e^{-inx}\,dx, \qquad
s_N(f;x) = \sum_{n=-N}^{N} c_n e^{inx}, \qquad
\|h\|_2 = \Big(\frac{1}{2\pi}\int_{-\pi}^{\pi}|h|^2\Big)^{1/2}.$$
A **trigonometric polynomial** is a finite sum $\sum_{n=-N}^{N} c_n e^{inx}$. The **Gamma
function** is $\Gamma(x) = \int_0^\infty t^{x-1}e^{-t}\,dt$ for $x > 0$.
## Formalization targets
### Goal — Parseval's theorem (Theorem 8.16)
For Riemann-integrable $2\pi$-periodic $f$ and $g$ with Fourier coefficients $c_n$ and
$\gamma_n$:
$$\lim_{N\to\infty}\|f - s_N(f)\|_2 = 0, \qquad
\frac{1}{2\pi}\int_{-\pi}^{\pi} f\bar g = \sum_{n=-\infty}^{\infty} c_n \overline{\gamma_n},
\qquad
\frac{1}{2\pi}\int_{-\pi}^{\pi} |f|^2 = \sum_{n=-\infty}^{\infty} |c_n|^2 .$$
### Milestones
$$\text{term-by-term differentiation of a power series} \qquad (8.1)$$
$$\textstyle\sum c_n = C \Rightarrow \sum c_n x^n \to C \text{ as } x \to 1^- \qquad (8.2)$$
$$\text{interchange of the order of summation in a double series} \qquad (8.3)$$
$$\text{two power series agreeing on a set with a limit point have equal coefficients} \qquad (8.5)$$
$$E(z+w) = E(z)E(w),\ E' = E,\ \text{growth of } E \qquad (8.6)$$
$$\cos(\pi/2) = 0,\ \cos > 0 \text{ on } [0,\pi/2),\ e^{z+2\pi i} = e^z,\ |z| = 1 \Rightarrow z = e^{it} \qquad (8.7)$$
$$\text{every nonconstant complex polynomial has a root} \qquad (8.8)$$
$$\text{Fourier partial sums minimize the mean square error; Bessel's inequality} \qquad (8.11,\ 8.12)$$
$$\text{a local Lipschitz condition at } x \text{ forces } s_N(f;x) \to f(x) \qquad (8.14)$$
$$\text{trigonometric polynomials approximate continuous periodic functions uniformly} \qquad (8.15)$$
$$\Gamma(x+1) = x\Gamma(x),\ \Gamma(n+1) = n!,\ \log\Gamma \text{ convex} \qquad (8.18)$$
$$\text{Bohr–Mollerup: these three properties characterize } \Gamma \qquad (8.19)$$
## Significance
Parseval's theorem is the completeness statement for the trigonometric system: Bessel's
inequality (8.12) holds for every orthonormal system, and equality for all $f$ is exactly what
distinguishes a complete system. The proof shows how the pieces of the book fit together: it
uses the approximation theorem 8.15 (itself a corollary of Stone–Weierstrass from Chapter 7),
the minimizing property 8.11, and the Schwarz inequality of Chapter 1. Chapter 11 generalizes
the conclusion to arbitrary complete orthonormal systems in $L^2$, where the Riemann-integrable
hypothesis can be dropped.
The other milestones are where the elementary functions acquire their properties: the
$2\pi$-periodicity of the complex exponential, the definition of $\pi$ as twice the first
positive zero of the cosine, and the log-convexity characterization of the Gamma function are
all established here rather than assumed.
Mathlib has the exponential and trigonometric functions, $\pi$, the fundamental theorem of
algebra, the Gamma function with the Bohr–Mollerup theorem, and a Fourier theory on the additive
circle. The work in this mission is to state Rudin's versions — $2\pi$-periodic functions on
$\mathbb{R}$, generic orthonormal systems on an interval, Riemann-integrable rather than
square-integrable hypotheses — and connect them to that library.
## Difficulty
Parseval's theorem is where an approximation argument in the uniform norm has to be converted
into one in the mean square norm. The chain is: approximate $f$ in $\|\cdot\|_2$ by a continuous
periodic $h$ (a nontrivial step for a merely Riemann-integrable $f$, and the place where the
hypothesis is really used), approximate $h$ uniformly by a trigonometric polynomial $P$, and
then use the minimizing property of the partial sums to conclude $\|f - s_N(f)\|_2$ is small.
The first step has no analogue in the uniform theory and is the main obstacle; the third depends
on $s_N$ being an orthogonal projection, which is Theorem 8.11.
## Formalization scope
Conventions fixed by this mission:
* Integrals of complex-valued functions use Mathlib's interval integral
`∫ x in a..b, f x`, not the real-valued Riemann–Stieltjes integral built in Mission VI; for
the Riemann-integrable integrands of this chapter the two agree. Integrability hypotheses are
stated as `IntervalIntegrable`.
* Fourier notions are `Rudin.fourierCoeff`, `Rudin.fourierPartialSum`, `Rudin.L2Norm`,
`Rudin.IsTrigPolynomial`, `Rudin.HasPeriodTwoPi`, and, for general systems,
`Rudin.IsOrthonormalSystem` and `Rudin.genFourierCoeff`, all following Rudin's normalizations
(in particular the $1/2\pi$ in $c_n$ and in $\|\cdot\|_2$).
* Series of real numbers use `Rudin.SeriesConvergesTo` from Mission III, so that conditional
convergence is expressible; the two-sided sums $\sum_{n=-\infty}^{\infty}$ of Parseval are
stated as limits of the symmetric partial sums $\sum_{|n| \le N}$, as in Rudin.
* $\exp$, $\cos$, $\pi$ and $\Gamma$ are Mathlib's; Theorem 8.7 is therefore stated as the list
of properties Rudin derives, not as a redefinition of $\pi$.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 8 (pp. 172–201).
- P. J. Davis, *Leonhard Euler's integral: A historical profile of the Gamma function*,
American Mathematical Monthly 66 (1959), 849–869. https://doi.org/10.2307/2309786
Rudin PMA X: Integration of Differential FormsTextbook
## Motivation
Chapter 10 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) builds the calculus of **differential forms** in $\mathbb{R}^n$ and proves the theorem
that unifies the integral theorems of vector analysis. The fundamental theorem of calculus, the
Green, divergence and classical Stokes theorems all say the same thing — that integrating a
derivative over a region is the same as integrating the original object over the boundary of
that region — and **Stokes' theorem** (Theorem 10.33),
$$\int_\Psi d\omega = \int_{\partial \Psi} \omega ,$$
is that statement, once "region" is made precise as a *chain* of parametrized surfaces and
"derivative" as the exterior derivative.
This mission is the tenth in a series formalizing Rudin Chapters 1–11; it uses the inverse
function theorem and the several-variable calculus of Mission IX.
## Setting
For an open $E \subseteq \mathbb{R}^n$, a **$k$-surface** in $E$ is a $C'$-mapping $\Phi$ from a
parameter domain $D \subseteq \mathbb{R}^k$ — a $k$-cell or the standard simplex
$Q^k = \{u : u_i \ge 0, \sum u_i \le 1\}$ — into $E$; surfaces are maps, not point sets. A
**$k$-form** in $E$ is a formal sum
$$\omega = \sum a_{i_1\cdots i_k}(\mathbf{x})\,dx_{i_1}\wedge\cdots\wedge dx_{i_k}$$
with continuous coefficients, whose meaning is the rule assigning to each $k$-surface $\Phi$ the
number
$$\int_\Phi \omega = \int_D \sum a_{i_1\cdots i_k}(\Phi(\mathbf{u}))\,
\frac{\partial(\varphi_{i_1},\dots,\varphi_{i_k})}{\partial(u_1,\dots,u_k)}\,d\mathbf{u}.$$
The **exterior derivative** of $\omega$ is the $(k+1)$-form with coefficients $D_j a_I$; the
**pullback** $\omega_T$ along a differentiable $T$ substitutes $T$ into the coefficients and the
differentials. A **$k$-chain** is a formal integer combination of $k$-surfaces with parameter
domain $Q^k$, its integral is the corresponding combination of integrals, and its **boundary**
$\partial\Psi$ is obtained from the alternating sum $\sum_j (-1)^j$ of the faces of $Q^k$.
## Formalization targets
### Goal — Stokes' theorem (Theorem 10.33)
If $\Psi$ is a $k$-chain of class $C''$ in an open $V \subseteq \mathbb{R}^n$ and $\omega$ is a
$(k-1)$-form of class $C'$ in $V$, then
$$\int_\Psi d\omega = \int_{\partial\Psi} \omega .$$
For $k = n = 1$ this is the fundamental theorem of calculus, for $k = n = 2$ Green's theorem,
for $k = n = 3$ the divergence theorem, and for $k = 2$, $n = 3$ the theorem of Stokes.
### Milestones
$$\text{the iterated integrals of a continuous function on a cell agree} \qquad (10.2)$$
$$\text{partitions of unity subordinate to an open cover of a compact set} \qquad (10.8)$$
$$\int f(\mathbf{y})\,d\mathbf{y} = \int f(T(\mathbf{x}))\,|J_T(\mathbf{x})|\,d\mathbf{x} \qquad (10.9)$$
$$d(d\omega) = 0 \qquad (10.20)$$
$$(d\omega)_T = d(\omega_T) \qquad (10.22\mathrm{c})$$
$$\int_{T\circ\Phi}\omega = \int_\Phi \omega_T \qquad (10.25)$$
$$\text{reordering the vertices of a simplex multiplies the integral by the sign} \qquad (10.27)$$
$$\text{Poincaré's lemma: on a convex open set, closed forms are exact} \qquad (10.39)$$
## Significance
Stokes' theorem is the organizing theorem of multivariable analysis; its formal content is that
$d$ and $\partial$ are adjoint, which is also the starting point of de Rham cohomology.
Poincaré's lemma is its local converse: on a convex set the only obstruction to a closed form
being exact disappears, so the failure of exactness measures the shape of the domain. The change
of variables theorem (10.9) is what makes integrals independent of the parametrization and is
used in the proof of Stokes itself, and partitions of unity (10.8) are the standard device for
passing from local to global statements.
Mathlib has a general change-of-variables theorem for the Lebesgue integral, smooth partitions
of unity, and the theory of alternating forms and de Rham differentials on manifolds; it does
not have Rudin's concrete apparatus of parametrized surfaces, affine chains, and their
boundaries, nor a version of Stokes' theorem for such chains. This mission builds that
apparatus and states the chapter's theorems for it; the definitions are reusable for any
development that wants a hands-on, coordinate-based treatment of forms.
## Difficulty
This is the most demanding mission of the series, for two reasons. First, the objects have to be
set up before anything can be said: forms as coefficient families, their integrals as Jacobian
integrals, chains, and the boundary operator with its signs. Second, Stokes' theorem is proved
by reducing to a single oriented simplex, transporting along the parametrization by Theorem
10.25, and then computing the integral over $Q^k$ by an iterated integral in which all but two
terms of the boundary cancel; the cancellation is entirely a matter of getting the signs of the
face maps right, and it is where a formalization will spend its time.
A further subtlety: with forms presented by coefficients indexed by *all* index tuples, the
identity $d(d\omega) = 0$ is false coefficient-wise and true as an identity of forms. Since
Rudin defines a form to *be* its integration functional, statements of the shape "this form
vanishes" are formalized as "its integral over every surface vanishes", and that is how 10.20,
10.22(c) and 10.39 are stated here.
## Formalization scope
Conventions fixed by this mission:
* Points of $\mathbb{R}^n$ are `Fin n → ℝ`. A $k$-form is `Rudin.KForm k n`, a coefficient
function indexed by all tuples `Fin k → Fin n`, following Rudin's equation (34).
* `Rudin.integralOverCell` and `Rudin.integralOverSimplex` are Rudin's equation (35) for the two
admissible parameter domains, with `Rudin.jacobian` the determinant of the matrix of partial
derivatives. The integral over the parameter domain is the Lebesgue integral for the volume
measure, which agrees with Rudin's Riemann integral for continuous integrands.
* `Rudin.extDeriv` and `Rudin.pullback` are the exterior derivative and the pullback;
`Rudin.Chain`, `Rudin.Chain.integral` and `Rudin.Chain.boundary` are chains with integer
multiplicities, their integrals, and the boundary built from the faces of the standard simplex
with Rudin's signs $(-1)^j$.
* Regularity is `ContDiff ℝ 1` and `ContDiff ℝ 2` for Rudin's $C'$ and $C''$.
* Equalities between forms are stated as equalities of their integrals over surfaces, as
explained above; the goal theorem is an equality of two real numbers, so it is not vacuous.
Contributions of the supporting differential-form identities (10.20, 10.22, 10.25) are
especially welcome, since they are exactly the lemmas the goal theorem consumes.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 10 (pp. 245–299).
- Michael Spivak, *Calculus on Manifolds*, W. A. Benjamin, 1965.
Rudin PMA IX: Functions of Several VariablesTextbook
## Motivation
Chapter 9 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) develops the differential calculus of mappings $\mathbf{f} : \mathbb{R}^n \to
\mathbb{R}^m$. The definition of the derivative changes character: it is no longer a number but
a **linear transformation** $\mathbf{f}'(\mathbf{x})$, the one that approximates the increment
of $\mathbf{f}$ to first order. Once that is in place, the chapter proves the two theorems that
make nonlinear analysis possible: the **inverse function theorem** (Theorem 9.24), which says
that a continuously differentiable map with invertible derivative at a point is locally
invertible with a continuously differentiable inverse, and the **implicit function theorem**
(9.28), which solves $\mathbf{f}(\mathbf{x},\mathbf{y}) = 0$ locally for $\mathbf{x}$ in terms
of $\mathbf{y}$.
The message of both is that a nonlinear map behaves locally like its linearization, provided
that linearization is invertible and varies continuously.
This mission is the ninth in a series formalizing Rudin Chapters 1–11; it uses the
completeness and compactness results of Missions II and IV and the mean value estimates of
Mission V, and it prepares the change-of-variables machinery used in Mission X.
## Setting
$L(\mathbb{R}^n, \mathbb{R}^m)$ is the space of linear maps with the operator norm
$\|A\| = \sup_{|x| \le 1} |Ax|$. A map $\mathbf{f}$ defined on an open $E \subseteq \mathbb{R}^n$
is **differentiable at** $\mathbf{x}$ with derivative $A \in L(\mathbb{R}^n,\mathbb{R}^m)$ if
$$\lim_{\mathbf{h} \to 0} \frac{|\mathbf{f}(\mathbf{x}+\mathbf{h}) - \mathbf{f}(\mathbf{x}) - A\mathbf{h}|}{|\mathbf{h}|} = 0 ,$$
and $\mathbf{f} \in \mathcal{C}'(E)$ — a **$C'$-mapping** — if it is differentiable on $E$ and
$\mathbf{x} \mapsto \mathbf{f}'(\mathbf{x})$ is continuous. The **partial derivative**
$D_j f_i$ is the derivative of $t \mapsto f_i(\mathbf{x} + t\mathbf{e}_j)$ at $t = 0$. A map
$\varphi$ of a metric space into itself is a **contraction** if
$d(\varphi(x),\varphi(y)) \le c\,d(x,y)$ for some $c < 1$.
## Formalization targets
### Goal — inverse function theorem (Theorem 9.24)
Let $\mathbf{f}$ be a $C'$-mapping of an open $E \subseteq \mathbb{R}^n$ into $\mathbb{R}^n$ and
suppose $\mathbf{f}'(\mathbf{a})$ is invertible at some $\mathbf{a} \in E$. Then there are open
sets $U \ni \mathbf{a}$ and $V \ni \mathbf{f}(\mathbf{a})$ such that
$$\mathbf{f}|_U \text{ is injective}, \qquad \mathbf{f}(U) = V, \qquad
\mathbf{g} = (\mathbf{f}|_U)^{-1} \in \mathcal{C}'(V).$$
### Milestones
$$\text{invertible operators form an open set; inversion is continuous} \qquad (9.8)$$
$$(\mathbf{g}\circ\mathbf{f})'(\mathbf{x}) = \mathbf{g}'(\mathbf{f}(\mathbf{x}))\,\mathbf{f}'(\mathbf{x}) \qquad (9.15)$$
$$\text{differentiability gives all partial derivatives} \qquad (9.17)$$
$$\|\mathbf{f}'\| \le M \text{ on a convex } E \Rightarrow |\mathbf{f}(b)-\mathbf{f}(a)| \le M|b-a| \qquad (9.19)$$
$$\mathbf{f} \in \mathcal{C}'(E) \iff \text{the } D_j f_i \text{ exist and are continuous} \qquad (9.21)$$
$$\text{a contraction of a complete metric space has a unique fixed point} \qquad (9.23)$$
$$\text{implicit function theorem} \qquad (9.28)$$
$$D_{21}f \text{ continuous at } (a,b) \Rightarrow D_{12}f(a,b) = D_{21}f(a,b) \qquad (9.41)$$
$$\text{differentiation under the integral sign} \qquad (9.42)$$
## Significance
The inverse function theorem is the local classification statement of differential calculus: it
says that the only local obstruction to invertibility is degeneracy of the derivative, and it is
the mechanism behind coordinate changes, the rank theorem (9.32), and the change-of-variables
formula for integrals in Chapter 10. The implicit function theorem is its standard reformulation
and is what makes level sets of smooth maps into manifolds. Theorem 9.21 is the practical
criterion for the $C'$ hypothesis, since it reduces it to continuity of finitely many partial
derivatives; Theorem 9.41 shows that the symmetry of second derivatives, though intuitive,
requires a hypothesis; Theorem 9.19 is the several-variable substitute for the mean value
theorem, whose equality form already failed in Chapter 5.
Mathlib has the Fréchet derivative, the inverse and implicit function theorems for Banach
spaces, the Banach fixed-point theorem, and symmetry of second derivatives. This mission states
the Rudin versions concretely in $\mathbb{R}^n$ — with the explicit open sets $U$ and $V$ and
the inverse mapping produced as data, rather than through a bundled local homeomorphism — and
so provides a bridge between the book's formulations and the library's.
## Difficulty
The inverse function theorem is the first theorem in the book whose proof combines several
chapters at once: the contraction principle (9.23) gives local surjectivity by solving
$\mathbf{f}(\mathbf{x}) = \mathbf{y}$ as a fixed point of
$\mathbf{x} \mapsto \mathbf{x} + A^{-1}(\mathbf{y} - \mathbf{f}(\mathbf{x}))$; openness of the
set of invertible operators (9.8) keeps the derivative invertible near $\mathbf{a}$; the mean
value inequality (9.19) controls the error; and the continuity of inversion gives the $C'$
regularity of $\mathbf{g}$. The delicate point is that all estimates must hold *uniformly* on a
neighbourhood chosen in advance, so the order in which the neighbourhoods are shrunk matters.
For Theorem 9.41 the trap is the hypothesis: continuity of $D_{21}f$ at the single point
$(a,b)$ is assumed, not continuity of both mixed partials on a neighbourhood; the conclusion is
existence of $D_{12}f$ at that point, and it genuinely fails without some such hypothesis.
## Formalization scope
Conventions fixed by this mission:
* Euclidean spaces are `EuclideanSpace ℝ (Fin n)`; linear maps are `→L[ℝ]` (continuous linear
maps), which in finite dimension is the same as Rudin's $L(\mathbb{R}^n,\mathbb{R}^m)$, with
the operator norm.
* Derivatives are `HasFDerivAt`, and the $C'$ condition is `ContDiffOn ℝ 1`.
* Partial derivatives are stated as `HasDerivAt` of the line restriction
`t ↦ f (x + t • eⱼ)` at `t = 0`, avoiding any coordinate-projection bookkeeping;
`eⱼ = EuclideanSpace.single j 1`.
* Invertibility of a derivative is `Function.Bijective`, which for a continuous linear map
between finite-dimensional spaces is equivalent to the existence of a continuous linear
inverse.
* In 9.8 the inverse operator is supplied as a function `inv` constrained on the invertible
operators, so that continuity of inversion can be stated without bundling.
* Theorem 9.41 uses explicitly supplied partial derivative functions `D1f`, `D2f`, `D21f`, which
is how Rudin states the hypotheses, and the conclusion asserts existence of `D₁₂f` at the
point as a `HasDerivAt` statement.
* Theorem 9.42 is stated for the Riemann–Stieltjes integral of Mission VI, matching Rudin's
hypotheses `α` increasing and `φ(·,t) ∈ ℛ(α)`.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 9 (pp. 204–243).
Rudin PMA VII: Sequences and Series of FunctionsTextbook
## Motivation
Chapter 7 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) asks when a limit of functions inherits the properties of its members. Pointwise
convergence preserves almost nothing: Rudin's opening examples give continuous $f_n$ with
discontinuous limit, and sequences where $\lim_n \int f_n \ne \int \lim_n f_n$. **Uniform
convergence** is the hypothesis that repairs this, and the chapter's second half asks the
converse question — which functions arise as uniform limits from a given family — answered by
the **Stone–Weierstrass theorem** (Theorem 7.32): an algebra of continuous real functions on a
compact set that separates points and vanishes nowhere is uniformly dense in all continuous
functions there.
The classical Weierstrass approximation theorem (7.26) — polynomials are dense in $C[a,b]$ — is
the special case that made the general theorem worth proving, and is used in Chapter 8 for
Fourier series and in Chapter 11 for the density of continuous functions in $L^2$.
This mission is the seventh in a series formalizing Rudin Chapters 1–11; it uses the compactness
results of Mission II, the continuity results of Mission IV and the Riemann–Stieltjes integral
of Mission VI.
## Setting
A sequence $f_n$ **converges uniformly** to $f$ on $E$ if for every $\varepsilon > 0$ there is
$N$ with $|f_n(x) - f(x)| \le \varepsilon$ for all $n \ge N$ and all $x \in E$ — the same $N$ for
every point. A family $\mathcal{F}$ is **equicontinuous** on $E$ if a single $\delta$ serves all
its members in the definition of uniform continuity; it is **pointwise bounded** if each orbit
$\{f(x) : f \in \mathcal{F}\}$ is bounded, and **uniformly bounded** if one bound works for all
$f$ and all $x$.
A set $\mathcal{A}$ of real functions is an **algebra** if it is closed under addition,
multiplication and multiplication by real scalars; it **separates points** on $K$ if for
$x \ne y$ in $K$ some $f \in \mathcal{A}$ has $f(x) \ne f(y)$; it **vanishes at no point** of $K$
if for each $x \in K$ some $f \in \mathcal{A}$ has $f(x) \ne 0$. The **uniform closure** of
$\mathcal{A}$ on $K$ is the set of uniform limits on $K$ of sequences from $\mathcal{A}$.
## Formalization targets
### Goal — Stone–Weierstrass (Theorem 7.32)
Let $K$ be compact and let $\mathcal{A}$ be an algebra of real continuous functions on $K$ which
separates points on $K$ and vanishes at no point of $K$. Then
$$\overline{\mathcal{A}}^{\,\text{unif}} \supseteq C(K,\mathbb{R}) :$$
every continuous real function on $K$ is a uniform limit on $K$ of members of $\mathcal{A}$.
### Milestones
$$\text{uniform convergence} \iff \text{uniform Cauchy criterion} \qquad (7.8)$$
$$|f_n| \le M_n \text{ on } E,\ \textstyle\sum M_n < \infty \Rightarrow \sum f_n \text{ converges uniformly} \qquad (7.10)$$
$$\lim_{t\to x}\lim_n f_n(t) = \lim_n \lim_{t \to x} f_n(t) \text{ under uniform convergence} \qquad (7.11)$$
$$\text{a uniform limit of continuous functions is continuous} \qquad (7.12)$$
$$f_n \in \mathcal{R}(\alpha),\ f_n \to f \text{ uniformly} \Rightarrow f \in \mathcal{R}(\alpha),\ \int f_n \, d\alpha \to \int f \, d\alpha \qquad (7.16)$$
$$f_n' \to h \text{ uniformly},\ f_n(x_0) \text{ convergent} \Rightarrow f_n \to g \text{ uniformly},\ g' = h \qquad (7.17)$$
$$\text{there is a continuous nowhere differentiable } f : \mathbb{R} \to \mathbb{R} \qquad (7.18)$$
$$\text{pointwise bounded} + \text{equicontinuous on compact} \Rightarrow \text{uniformly bounded, convergent subsequence} \qquad (7.24,\ 7.25)$$
$$\text{polynomials are uniformly dense in } C[a,b] \qquad (7.26)$$
## Significance
Uniform convergence is the standard hypothesis under which limits commute with continuity,
integration and (with an extra condition) differentiation, and Theorems 7.11, 7.12, 7.16 and
7.17 are used throughout the rest of the book; Chapter 8 in particular builds the exponential,
trigonometric and Gamma functions as uniform limits and differentiates them term by term on the
strength of 7.17. Theorem 7.18 shows how weak pointwise differentiability is as a consequence of
continuity: a uniform limit of piecewise-linear functions can fail to be differentiable
anywhere. Arzelà–Ascoli is the compactness criterion for families of functions, and it is the
standard route to existence theorems for differential and integral equations.
Stone–Weierstrass is the structural theorem of the chapter: it replaces the combinatorial
Bernstein-polynomial proof of Weierstrass's theorem with a statement about algebras of
functions, applicable to trigonometric polynomials, polynomials in several variables, and
Lipschitz algebras alike.
Mathlib contains a Stone–Weierstrass theorem for subalgebras of `C(X, ℝ)` on compact Hausdorff
spaces, and a version of Arzelà–Ascoli. This mission states the results in Rudin's terms — plain
sets of functions on a compact subset $K$ of a metric space, uniform closure defined by
sequences — so that they can be used together with the Riemann–Stieltjes integral built in
Mission VI, which is not part of the library.
## Difficulty
Stone–Weierstrass is the one theorem in this mission whose proof is genuinely structural: from
the algebra one first produces $|f|$ as a uniform limit of polynomials in $f$ (which needs the
polynomial approximation of $\sqrt{t}$ on $[0,1]$ and so cannot be circular with Theorem 7.26),
then maxima and minima of pairs, then functions matching prescribed values at two points, and
only then the local-to-global patching over a finite subcover. Each step is short; keeping the
uniform closure a lattice and an algebra simultaneously is the bookkeeping burden.
Two hypotheses are easy to lose and both are necessary: an algebra that vanishes at a point
cannot approximate functions that do not, and one that fails to separate two points cannot
approximate functions that distinguish them.
## Formalization scope
Conventions fixed by this mission:
* Uniform convergence is Mathlib's `TendstoUniformlyOn … atTop`; complex-valued sequences are
used where Rudin allows complex values.
* Algebras, separation, non-vanishing and uniform closure are the predicates
`Rudin.IsFunctionAlgebra`, `Rudin.SeparatesPointsOn`, `Rudin.VanishesAtNoPointOn`,
`Rudin.UniformClosureOn`, defined for sets of functions `X → ℝ` and a compact subset `K`.
The goal's conclusion is membership in the uniform closure, i.e. the existence of an
approximating sequence from the algebra.
* Equicontinuity and the two boundedness notions are `Rudin.EquicontinuousOn`,
`Rudin.PointwiseBoundedOn`, `Rudin.UniformlyBoundedOn`, stated with explicit $\varepsilon$ and
$\delta$ as in Definitions 7.19 and 7.22.
* Theorem 7.16 is stated for the Riemann–Stieltjes integral of Mission VI, not for a Mathlib
integral, so the two missions compose.
* Theorem 7.26 is stated for complex-valued $f$ and polynomials with complex coefficients
evaluated at real points, as in Rudin.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 7 (pp. 143–171).
- M. H. Stone, *The generalized Weierstrass approximation theorem*, Mathematics Magazine 21
(1948), 167–184 and 237–254. https://doi.org/10.2307/3029750
Rudin PMA VI: The Riemann-Stieltjes IntegralTextbook
## Motivation
Chapter 6 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) constructs the **Riemann–Stieltjes integral** $\int_a^b f\,d\alpha$: the Riemann integral
with the increments $\Delta x_i$ of the variable replaced by the increments
$\Delta \alpha_i = \alpha(x_i) - \alpha(x_{i-1})$ of a monotonically increasing *integrator*
$\alpha$. Taking $\alpha(x) = x$ recovers the ordinary Riemann integral; taking $\alpha$ a step
function turns integrals into sums, so series and integrals become special cases of one
construction. This is the reason Rudin develops the theory in this generality: it unifies
Chapter 3's series with the integral, and it is the natural setting for the Fourier coefficients
of Chapter 8.
The chapter's capstone is the **fundamental theorem of calculus** (Theorem 6.21): an
integrable function which is the derivative of some $F$ integrates to $F(b) - F(a)$.
This mission is the sixth in a series formalizing Rudin Chapters 1–11; it uses the uniform
continuity of Mission IV and the mean value theorem of Mission V.
## Setting
A **partition** $P$ of $[a,b]$ is a finite set of points $a = x_0 \le x_1 \le \dots \le x_n = b$,
with increments $\Delta \alpha_i = \alpha(x_i) - \alpha(x_{i-1})$ for a monotonically increasing
$\alpha$. For a bounded real $f$ put
$M_i = \sup_{[x_{i-1},x_i]} f$, $m_i = \inf_{[x_{i-1},x_i]} f$, and
$$U(P,f,\alpha) = \sum_{i=1}^n M_i\,\Delta\alpha_i, \qquad
L(P,f,\alpha) = \sum_{i=1}^n m_i\,\Delta\alpha_i .$$
The **upper** and **lower integrals** are $\inf_P U(P,f,\alpha)$ and $\sup_P L(P,f,\alpha)$;
$f$ is **integrable with respect to $\alpha$**, written $f \in \mathcal{R}(\alpha)$, when they
agree, and the common value is $\int_a^b f\,d\alpha$. $P'$ **refines** $P$ when every division
point of $P$ is one of $P'$. Writing $\mathcal{R}$ for $\mathcal{R}(\alpha)$ with
$\alpha(x) = x$ gives the Riemann integral $\int_a^b f\,dx$.
## Formalization targets
### Goal — the fundamental theorem of calculus (Theorem 6.21)
$$
f \in \mathcal{R} \text{ on } [a,b], \quad F' = f \text{ on } [a,b]
\;\Longrightarrow\;
\int_a^b f(x)\,dx = F(b) - F(a).
$$
### Milestones
$$P' \text{ refines } P \Rightarrow L(P,f,\alpha) \le L(P',f,\alpha),\ U(P',f,\alpha) \le U(P,f,\alpha) \qquad (6.4)$$
$$\underline{\int} f\,d\alpha \le \overline{\int} f\,d\alpha \qquad (6.5)$$
$$f \in \mathcal{R}(\alpha) \iff \forall \varepsilon>0\ \exists P,\ U(P,f,\alpha) - L(P,f,\alpha) < \varepsilon \qquad (6.6)$$
$$f \text{ continuous} \Rightarrow f \in \mathcal{R}(\alpha) \qquad (6.8)$$
$$f \text{ monotone},\ \alpha \text{ continuous} \Rightarrow f \in \mathcal{R}(\alpha) \qquad (6.9)$$
$$\text{linearity of the integral} \qquad (6.12\mathrm{a})$$
$$\text{monotonicity, additivity in the interval, and } \big|\!\int f\,d\alpha\big| \le M(\alpha(b)-\alpha(a)) \qquad (6.12\mathrm{b,c,d})$$
$$\alpha' \in \mathcal{R} \Rightarrow \big(f \in \mathcal{R}(\alpha) \iff f\alpha' \in \mathcal{R}\big),\ \int f\,d\alpha = \int f\alpha'\,dx \qquad (6.17)$$
$$\text{change of variable through a strictly increasing } \varphi \qquad (6.19)$$
$$F(x) = \int_a^x f\,dt \text{ is continuous, and } F'(x_0) = f(x_0) \text{ where } f \text{ is continuous} \qquad (6.20)$$
$$\text{integration by parts} \qquad (6.22)$$
## Significance
The fundamental theorem is what makes the integral computable: it reduces integration to
antidifferentiation and so links Chapters 5 and 6. Theorem 6.20 is its companion — it says the
integral of a continuous function *is* an antiderivative — and together they show the two
operations are mutually inverse to the extent that the hypotheses allow. Theorem 6.17 explains
when a Stieltjes integral collapses to a Riemann integral with the density $\alpha'$, and it is
the computational tool for integrators that are differentiable; the step-function case at the
other extreme (Rudin's 6.15–6.16) is what turns sums into integrals.
Mathlib has no Riemann–Stieltjes integral: it has the Bochner integral, the interval integral,
and a Lebesgue–Stieltjes measure, but the upper-and-lower-sum construction of Chapter 6 is
absent. This mission therefore builds the object from Rudin's definitions and develops its basic
theory; that development is reusable beyond this mission — Chapter 7's interchange theorem
(7.16) and Chapter 8's Fourier coefficients are stated with respect to it.
## Difficulty
Two obstacles are specific to formalizing this chapter. First, the upper and lower integrals are
an infimum and a supremum over the *set of all partitions*, which is not a lattice-friendly
index; every comparison between partitions goes through the common refinement, and Theorem 6.4
is the workhorse that makes such comparisons possible. Second, the fundamental theorem is proved
by choosing a partition on which $U - L < \varepsilon$ and applying the mean value theorem on
each subinterval, so the proof requires selecting an intermediate point per subinterval — a
finite choice that is easy on paper and must be organized explicitly in Lean.
The integrator $\alpha$ is only assumed monotone, so it may be discontinuous, and the theory
must not assume otherwise: Theorem 6.9 needs continuity of $\alpha$ precisely because it is not
available in general.
## Formalization scope
Conventions fixed by this mission:
* A partition of `[a, b]` is `Rudin.Partition a b`: the number `n` of subintervals together with
a monotone placement function `x` with `x 0 = a` and `x n = b`. Rudin allows
$x_{i-1} = x_i$, and so does this structure.
* `Rudin.upperSum`, `Rudin.lowerSum`, `Rudin.upperIntegral`, `Rudin.lowerIntegral`,
`Rudin.RSIntegrable`, `Rudin.RSIntegral` follow Definitions 6.1–6.2 literally, with `sSup` and
`sInf` over the images $f([x_{i-1},x_i])$.
* Since `sSup`/`sInf` on `ℝ` return `0` on unbounded sets, every statement carries Rudin's
boundedness hypothesis for $f$ explicitly; likewise monotonicity of $\alpha$ is assumed as
`MonotoneOn α (Set.Icc a b)` rather than built into a type.
* `Rudin.RiemannIntegrable` and `Rudin.RiemannIntegral` are the case $\alpha = \mathrm{id}$, in
which the goal theorem and Theorems 6.20–6.22 are stated, matching Rudin.
* Derivatives are `HasDerivAt`, so `F' = f` is stated pointwise on `[a, b]` with the value `f x`
supplied, as in Rudin's hypothesis.
The goal is not vacuous, and not a restatement of a library lemma: the integral in it is the one
defined in this mission, so a solution must connect the upper/lower sum construction to
differentiation rather than quoting Mathlib's interval integral.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 6 (pp. 120–142).
## Motivation
Continuity is the hypothesis under which limits may be moved inside a function, and Chapter 4
of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill, 1976) is
about what continuity gives once the domain is compact or connected. Three of its theorems are
used in nearly every later argument of the book: a continuous function on a compact set has
compact image (Theorem 4.14), hence attains its bounds (4.16); a continuous function on a
connected set has connected image (4.22), hence takes intermediate values (4.23); and a
continuous function on a *compact* metric space is **uniformly continuous** (Theorem 4.19) —
the $\delta$ can be chosen independently of the point.
The last of these is the chapter's capstone. Uniform continuity is exactly what is needed to
prove that continuous functions are Riemann-integrable (Chapter 6), and it is the first place
where compactness upgrades a pointwise hypothesis into a global one with a quantitative
conclusion.
This mission is the fourth in a series formalizing Rudin Chapters 1–11; it uses the metric
topology of Mission II and is a prerequisite for Missions V–VII.
## Setting
Let $X, Y$ be metric spaces, $E \subseteq X$, $f : E \to Y$, and let $p$ be a limit point of
$E$. Rudin writes $\lim_{x \to p} f(x) = q$ when for every $\varepsilon > 0$ there is
$\delta > 0$ with $d_Y(f(x), q) < \varepsilon$ for all $x \in E$ satisfying
$0 < d_X(x,p) < \delta$; the exclusion of $x = p$ is deliberate, and it is what makes the
notion agree with continuity only when $f(p) = q$ (Theorem 4.6). $f$ is **continuous at** $p$
if the same holds with the condition $0 < d_X(x,p)$ dropped, and **continuous** if it is
continuous at every point.
$f$ is **uniformly continuous** on $X$ if for every $\varepsilon > 0$ there is a single
$\delta > 0$ such that $d_Y(f(p), f(q)) < \varepsilon$ for *all* $p, q \in X$ with
$d_X(p,q) < \delta$. A real function on $(a,b)$ is **monotonically increasing** if $x < y$
implies $f(x) \le f(y)$; its one-sided limits are written $f(x-)$ and $f(x+)$, and it has a
**discontinuity of the first kind** at $x$ when both exist but do not agree with $f(x)$.
## Formalization targets
### Goal — uniform continuity on compacta (Theorem 4.19)
$$
X \text{ compact metric space},\ f : X \to Y \text{ continuous}
\;\Longrightarrow\;
\forall \varepsilon > 0\ \exists \delta > 0\ \forall p, q \in X,\
d(p,q) < \delta \Rightarrow d(f(p), f(q)) < \varepsilon .
$$
### Milestones
$$f \text{ continuous at } p \iff \lim_{x \to p} f(x) = f(p) \qquad (4.6)$$
$$f \text{ continuous} \iff f^{-1}(V) \text{ open for every open } V \qquad (4.8)$$
$$K \text{ compact} \Rightarrow f(K) \text{ compact} \qquad (4.14)$$
$$\text{a continuous real } f \text{ on a compact } X \text{ attains } \sup f \text{ and } \inf f \qquad (4.16)$$
$$f : X \to Y \text{ continuous bijection, } X \text{ compact} \Rightarrow f^{-1} \text{ continuous} \qquad (4.17)$$
$$E \text{ connected} \Rightarrow f(E) \text{ connected} \qquad (4.22)$$
$$f(a) < c < f(b) \Rightarrow f(x) = c \text{ for some } x \in (a,b) \qquad (4.23)$$
$$f \text{ monotone} \Rightarrow f(x-),\, f(x+) \text{ exist and } f(x-) \le f(x) \le f(x+) \qquad (4.29)$$
$$\text{the discontinuity set of a monotone function is at most countable} \qquad (4.30)$$
## Significance
Uniform continuity is the hypothesis that converts local approximation into global
approximation with a uniform error bound. In Chapter 6 it is what makes the upper and lower
Riemann–Stieltjes sums of a continuous function come together; in Chapter 7 it underlies the
equicontinuity of Arzelà–Ascoli; in Chapter 9 it appears again in the estimate of a $C'$
mapping on a compact ball. The extreme value theorem and the intermediate value theorem are the
two existence theorems of elementary analysis, and both come from this chapter by combining
Chapter 2's compactness and connectedness with continuity.
Theorem 4.30 — a monotone function has at most countably many discontinuities — is the result
that makes monotone integrators well behaved in Chapter 6, and it is the first place in the book
where a countability argument (Chapter 2) pays off analytically.
Mathlib has continuity, compactness and connectedness in general topological spaces, and most
of the milestones can be matched to library results after the statements are put in Rudin's
metric form. The formalization value is again in the dictionary: Rudin's punctured-limit
definition versus `ContinuousWithinAt`, and his $\varepsilon$–$\delta$ uniform continuity versus
the library's uniformity-filter definition.
## Difficulty
There is no single hard step; the difficulty is in the hypotheses being weaker than they look.
In Theorem 4.6 the limit is taken through $E \setminus \{p\}$, so the equivalence with
continuity genuinely needs $p \in E$ *and* $p$ a limit point; dropping the second hypothesis
makes the statement false at isolated points. In Theorem 4.19 the naive proof — pick $\delta_p$
at each point by continuity and take the infimum — fails because the infimum over infinitely
many points can be $0$; compactness is used to reduce to finitely many, and the factor of two
in the radii of the covering balls is essential. Theorem 4.30 requires an injection from the
discontinuity set into $\mathbb{Q}$, built from the gap between $f(x-)$ and $f(x+)$.
## Formalization scope
Conventions fixed by this mission:
* Continuity is Mathlib's `Continuous`, `ContinuousOn`, `ContinuousWithinAt`; Rudin's
$\lim_{x\to p} f(x) = q$ along $E$ is `Filter.Tendsto f (𝓝[E \ {p}] p) (𝓝 q)`.
* Uniform continuity is `Rudin.UniformlyContinuous`, stated with explicit $\varepsilon$ and
$\delta$ as in Definition 4.18, rather than through the uniformity filter.
* Limit points are `Rudin.IsLimitPoint` from the Chapter 2 mission, so the two missions share
one notion.
* Compactness of the domain in 4.16, 4.17 and 4.19 is the typeclass `[CompactSpace X]`, matching
Rudin's phrase "compact metric space"; 4.14 is stated for a compact subset instead, which is
the form later missions use.
* Monotone functions are `MonotoneOn f (Set.Ioo a b)`; one-sided limits are `𝓝[<] x` and
`𝓝[>] x` filters, and 4.29 also identifies them with the supremum and infimum of the
corresponding one-sided images, as Rudin does.
The goal is not vacuous and does not follow by unfolding: uniform continuity fails for
continuous functions on non-compact domains (e.g. $x \mapsto x^2$ on $\mathbb{R}$, or
$x \mapsto 1/x$ on $(0,1)$), so compactness is doing the work.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 4 (pp. 83–101).
Brin–Squier: the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints has no free subgroup of rank greater than oneResearch Paper
## Motivation
[Von Neumann introduced amenability in 1929](http://eudml.org/doc/211921) in response to the
Banach–Tarski paradox: a group is **amenable** when it carries a finitely additive,
translation-invariant probability measure on its subsets, and no amenable group contains a free
subgroup of rank $2$ — which is exactly what the paradox needs. The converse is the **von
Neumann conjecture**, and it is false: [Ol'shanskii](https://doi.org/10.1070/rm1980v035n04abeh001876) in 1980 and
[Adyan](https://doi.org/10.1070/im1983v021n03abeh001799) in 1982 produced finitely generated
counterexamples. A *finitely
presented* counterexample was harder, and one candidate stood out — **Richard Thompson's group
$F$**, finitely presented, with nobody able to decide whether it was amenable.
Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that
$F$, and more generally the group $\mathrm{PLF}(\mathbb{R})$ of piecewise-linear homeomorphisms
of the line with finitely many breakpoints, contains no free subgroup of rank greater than $1$.
Whether $F$ is amenable they could not determine, and it is still open today; claimed proofs
have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes
([Ol'shanskii–Sapir 2002](https://doi.org/10.1007/s10240-002-0006-7);
[Lodha–Moore 2016](https://doi.org/10.4171/ggd/347)), so $F$
is no longer needed as a candidate. This mission formalizes the half that *was* settled.
## Setting
Let $\mathrm{Homeo}_+(\mathbb{R})$ be the **group of orientation-preserving homeomorphisms** of
the line: the strictly increasing bijections $\mathbb{R}\to\mathbb{R}$ under composition. The
**support** of $f$ is the set of points it moves, $\operatorname{supp} f = \{\,t : f(t)\neq t\,\}$, an open subset of $\mathbb{R}$.
A continuous $f$ is **piecewise linear** when there is a *discrete* set $B$ of **breakpoints**
with $f$ differentiable off $B$ and $f'$ constant on each component of $\mathbb{R}\setminus B$;
for finite $B$ this is the same as $f$ being affine on a neighbourhood of every point outside
$B$. Nothing is required at the points of $B$, so the two affine pieces meeting at a breakpoint
may disagree — that is what makes such an $f$ more than an affine map. Write
$\mathrm{PL}(\mathbb{R})$ for the piecewise-linear elements of $\mathrm{Homeo}_+(\mathbb{R})$
and
$$\mathrm{PLF}(\mathbb{R}) = \{\, f \in \mathrm{PL}(\mathbb{R}) : f \text{ has a finite
breakpoint set} \,\}$$
for the subgroup this mission is about. The distinction matters: the goal below holds in
$\mathrm{PLF}(\mathbb{R})$ and fails in $\mathrm{PL}(\mathbb{R})$, where Brin and Squier build
free subgroups of rank $2$ by lifting them from the circle. Write $\mathrm{PLF}'(\mathbb{R})$ for the commutator subgroup, which Brin and Squier identify
as the elements whose **slope at each end** is $1$ — an element has slope $a$ at an end when it
agrees with a single affine map of slope $a$ on a ray out to that end. **Thompson's group $F$** — the piecewise-linear homeomorphisms of $[0,1]$ with dyadic
breakpoints and power-of-two slopes — is realized inside $\mathrm{PLF}(\mathbb{R})$.
## Formalization targets
### Goal — no two elements generate freely
$$\text{for } f,g \in \mathrm{PLF}(\mathbb{R}), \quad F_2 \to \mathrm{PLF}(\mathbb{R}),\
a \mapsto f,\ b \mapsto g \quad\text{is never injective.}$$
Since a free group of rank greater than $1$ contains one of rank $2$, this is Brin and Squier's
Theorem (3.1).
### The dichotomy it rests on
$$G \le \mathrm{PLF}'(\mathbb{R}) \implies G \text{ abelian, or } G \text{ contains a free
abelian subgroup of rank } 2.$$
Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is
infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the
full-strength (3.2) are milestones of their own here. The goal itself only ever uses the
rank-two form.
### The twenty-four milestones
Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in
its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and
published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2)
both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3),
likewise in both strengths. Five are piecewise-linear infrastructure the source treats as
routine: closure of $\mathrm{PLF}(\mathbb{R})$ under composition and under inverse, the same two
for slope $1$ at each end, and finiteness of the number of components of a support. Five more are
steps the source asserts without proof — that the line carries no non-fixed periodic points, that
a map fixing a set's complement preserves its components, that the iterated images of a
pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays
inside the union of the two supports (p. 495), and that the derived subgroup of a free group of
rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian
subgroup of a free group is cyclic, which is what lets the goal finish through
Nielsen–Schreier.
## Significance
The theorem closes the standard route to proving a group **non**-amenable. To show a group
amenable the classical routes are elementary amenability and subexponential growth, and $F$ is
neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth,
having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route
is to exhibit a free subgroup of rank $2$ — the route this theorem closes. $F$ sits in the gap,
which is why its status has survived sustained attention.
The result reaches past $F$. Monod's groups of piecewise *projective* homeomorphisms are
counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no
non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the
corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof
that paper says it will "largely follow [Brin–Squier, § 3]".
**What formalizing it adds.** Mathlib has no piecewise-linear maps and no [amenability predicate for
groups](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Group/FoelnerFilter.lean). This mission builds the piecewise-linear layer: a workable $\mathrm{PLF}(\mathbb{R})$, its
closure properties, and the structure of supports.
## Difficulty
The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the
breakpoint set is what gives an element slopes at $\pm\infty$ at all, and what makes two elements
affine on each side of a common fixed point. Compactness is the other — throughout, $[f,g] = fgf^{-1}g^{-1}$ — and it splits: that the closure of $\operatorname{supp}[f,g]$ is
compact needs only slope $1$ at each end, with no piecewise linearity at all, which is why
(2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays
inside $\operatorname{supp} f \cup \operatorname{supp} g$ is what reaches back to finiteness. Keeping straight which
fact does which job is most of the work.
The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that
makes them commute: only their intersections with one chosen component are disjoint, and
commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.
## Formalization scope
**What the Lean fixes.** Elements are order isomorphisms of $\mathbb{R}$ — strictly increasing
bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows
Mathlib's convention $(f\cdot g)(x) = f(g(x))$, the opposite of the source's right action, so the
conjugation identity reads $\operatorname{supp}(fgf^{-1}) = f(\operatorname{supp} g)$ here;
getting this backwards states a different theorem that still compiles. A support is the bare
moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with
local affineness off it — the set need not be minimal and may be empty.
A copy of $\mathbb{Z}^2$ is an injectivity statement about $(m,n)\mapsto u^m v^n$, not a subgroup
isomorphism, and the goal is about a single pair $f,g$ rather than a subgroup. The dichotomy
hypothesises slope $1$ at both ends directly, not membership in a derived subgroup — that these
coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and
the identification asserted on p. 493 gives the other.
Beyond a workable $\mathrm{PLF}(\mathbb{R})$, the development needs Nielsen–Schreier, already
in Mathlib as `subgroupIsFreeOfIsFree`: it is what lets an abelian subgroup of a free group be
cyclic, and so lets the goal finish without the source's metabelian ending. That ending is
formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a
free group of rank two is non-abelian; the goal simply does not route through it.
**One trivializing reading is ruled out.** Slope $1$ at both ends is not a compact-support
condition — every translation satisfies it — so (3.2) is not secretly a statement about
compactly supported maps.
**Nothing is built for $F$ specifically**, and amenability is not touched. That is the one piece
deliberately omitted, and contributions are welcome on it: modelling $F$ and embedding it in
$\mathrm{PLF}(\mathbb{R})$. The piecewise-linear layer is reusable beyond this theorem — Thompson's groups $T$ and
$V$, and piecewise-linear topology generally, need exactly it.
## Selected references
- M. G. Brin and C. C. Squier, Groups of piecewise linear homeomorphisms of the real line,
Invent. math. **79** (1985), 485–498, [doi:10.1007/BF01388519](https://doi.org/10.1007/BF01388519). Theorem (3.1) is the goal.
- J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups,
L'Enseignement Mathématique **42** (1996), 215–256. Theorem 4.10 and Corollary 4.7.
- N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA **110**
(2013), 4524–4527, [arXiv:1209.5229](https://arxiv.org/abs/1209.5229).
- A. Yu. Ol'shanskii and M. V. Sapir, Non-amenable finitely presented torsion-by-cyclic groups,
Publ. Math. IHÉS **96** (2002), 43–169, [doi:10.1007/s10240-002-0006-7](https://doi.org/10.1007/s10240-002-0006-7).
- Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective
homeomorphisms, Groups Geom. Dyn. **10** (2016), 177–200, [doi:10.4171/ggd/347](https://doi.org/10.4171/ggd/347).
- V. Guba, Amenability problem for Thompson's group $F$: state of the art, J. Groups Complex.
Cryptol. **15** (2023), [arXiv:2305.07113](https://arxiv.org/abs/2305.07113).
Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper
## Motivation
Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$, and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's *A theory of regularity structures* (Invent. Math. 198 (2014) 269–504, [arXiv:1303.5113](https://arxiv.org/abs/1303.5113)) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.
The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.
## Setting
Fix a dimension $d$ and a **scaling** $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$, and put $\|x\|_s = \max_i |x_i|^{1/s_i}$. For $\delta > 0$, a point $x \in \mathbb{R}^d$ and a test function $\varphi$, the **rescaled test function** is
$$ (S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right). $$
Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$. For $\alpha<0$, a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$, $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$, $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$.
A **regularity structure** $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$, bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$, and $\Gamma\mathbf{1} = \mathbf{1}$. Elements of $T_\alpha$ are "homogeneous of order $\alpha$": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$.
A **model** $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$, subject to $\Gamma_{xx}=\mathrm{id}$, $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$, $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds
$$ |(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell. $$
A **modelled distribution** of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$
$$ |||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty; $$
the space of these is $\mathcal{D}^\gamma$, and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a **sector** $V$, that is, a graded $G$-invariant subspace vanishing in degrees below its regularity.
## Formalization targets
### Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$
With $\alpha = \min A < 0$ and $r$ the order attached to $A$, for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a **unique** distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with
$$ \big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}). $$
The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.
### Milestone level — the calculus around the reconstruction operator
The uniqueness clause of Theorem 3.10 in isolation; the existence of a *linear* reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$.
## Significance
The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions.
Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.
## Difficulty
The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$, and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$: one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone.
## Formalization scope
The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are `Fin d → ℝ`. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$. The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$, which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$, and uniqueness simultaneously.
Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$, the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.
## Selected references
- M. Hairer, *A theory of regularity structures*, Inventiones Mathematicae 198 (2014) 269–504. [arXiv:1303.5113](https://arxiv.org/abs/1303.5113), [DOI:10.1007/s00222-014-0505-4](https://doi.org/10.1007/s00222-014-0505-4)
- T. Lyons, *Differential equations driven by rough signals*, Revista Matemática Iberoamericana 14 (1998) 215–310. [DOI:10.4171/RMI/240](https://doi.org/10.4171/RMI/240)
- M. Gubinelli, *Controlling rough paths*, Journal of Functional Analysis 216 (2004) 86–140. [arXiv:math/0306433](https://arxiv.org/abs/math/0306433)
- M. Gubinelli, P. Imkeller, N. Perkowski, *Paracontrolled distributions and singular PDEs*, Forum of Mathematics Pi 3 (2015) e6. [arXiv:1210.2684](https://arxiv.org/abs/1210.2684)
- Y. Bruned, M. Hairer, L. Zambotti, *Algebraic renormalisation of regularity structures*, Inventiones Mathematicae 215 (2019) 1039–1156. [arXiv:1610.08468](https://arxiv.org/abs/1610.08468)