Elliptic K3 (F-theory): the Kodaira/Tate 7-brane budget and E-series boundsResearch Paper
## Motivation
In **F-theory**, the non-abelian gauge algebra of an elliptic fibration is read off from the **Kodaira/Tate type** of the singular fibres over the discriminant locus, via the fibre--gauge-algebra dictionary (T. Weigand, *TASI Lectures on F-theory*, arXiv:1806.01854). For a locally minimal short Weierstrass model $y^2 = x^3 + f x + g$, each potentially good additive Kodaira type has a fixed **discriminant vanishing order** $\operatorname{ord}\Delta$ — the entries of Tate's table — and the exceptional types $\mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$ have Dynkin types $E_6, E_7, E_8$ (the gauge algebra in the split/geometric setting; a nonsplit $\mathrm{IV}^*$ instead gives $F_4$). On an **elliptically fibered K3** the **global** discriminant divisor has degree $24 = e(\mathrm{K3}) = 12\,\chi(\mathcal{O}_{\mathrm{K3}})$ (the topological Euler characteristic; the formalized affine statement is $\deg\Delta \le 24$), so the total discriminant charge of the singular fibres is capped. This mission formalizes the potentially good additive rows of the Tate table and the resulting **7-brane budget**.
## Setting
Fix a field $k$; work with $y^2 = x^3 + f x + g$, $f, g \in k[X]$, discriminant $\Delta = 4f^3 + 27g^2$ (up to the unit $-16$). Write $\operatorname{ord}_{t_0}(p)$ for the multiplicity of $t_0$ as a root of $p$; for the $\mathrm{I}_0^*$ row, whenever $(X - t_0)^2 \mid f$ and $(X - t_0)^3 \mid g$, write $f = (X - t_0)^2 F$ and $g = (X - t_0)^3 G$ and set the **reduced coefficients** $c_2 = F(t_0)$, $d_3 = G(t_0)$ (equivalently the order-$2$ and order-$3$ Taylor coefficients of $f$ and $g$ at $t_0$). The **K3 degree data** is $\deg f \le 8$, $\deg g \le 12$, $\Delta \ne 0$. The seven potentially good additive types ($\mathrm{II}, \mathrm{III}, \mathrm{IV}, \mathrm{I}_0^*, \mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$) are encoded by their $(\operatorname{ord} f, \operatorname{ord} g)$ signatures (`HasKodaira`), with lower bounds written as divisibility $(X - t_0)^n \mid \cdot$ and exact orders as `rootMultiplicity`.
## Formalization targets
### Goal — the 7-brane budget
For $k$ of characteristic zero and $(f,g)$ satisfying the K3 degree data, any finite set $S$ of base points, and any assignment $\tau$ of a Kodaira type each point genuinely carries,
$$\sum_{t \in S} \operatorname{discOrder}(\tau(t)) \le 24.$$
### Milestones — the Tate table (each entry: fibre signature $\Rightarrow$ exact $\operatorname{ord}\Delta$)
1. $\deg\Delta \le 24$ under $\deg f \le 8$, $\deg g \le 12$.
2. Local orders are bounded by the degree: $\sum_{t \in S}\operatorname{ord}_t\Delta \le \deg\Delta$ ($\Delta \ne 0$, $S$ finite).
3. Type $\mathrm{II}$: $(\operatorname{ord} f \ge 1, \operatorname{ord} g = 1) \Rightarrow \operatorname{ord}\Delta = 2$.
4. Type $\mathrm{III}$: $(\operatorname{ord} f = 1, \operatorname{ord} g \ge 2) \Rightarrow \operatorname{ord}\Delta = 3$.
5. Type $\mathrm{IV}$: $(\operatorname{ord} f \ge 2, \operatorname{ord} g = 2) \Rightarrow \operatorname{ord}\Delta = 4$.
6. Type $\mathrm{I}_0^*$ (full row): $(\operatorname{ord} f \ge 2, \operatorname{ord} g \ge 3,\ 4c_2^3+27d_3^2 \ne 0) \Rightarrow \operatorname{ord}\Delta = 6$.
7. Type $\mathrm{IV}^*$ ($E_6$): $(\operatorname{ord} f \ge 3, \operatorname{ord} g = 4) \Rightarrow \operatorname{ord}\Delta = 8$.
8. Type $\mathrm{III}^*$ ($E_7$): $(\operatorname{ord} f = 3, \operatorname{ord} g \ge 5) \Rightarrow \operatorname{ord}\Delta = 9$.
9. Type $\mathrm{II}^*$ ($E_8$): $(\operatorname{ord} f \ge 4, \operatorname{ord} g = 5) \Rightarrow \operatorname{ord}\Delta = 10$.
### Corollaries (also milestones)
10. Exceptional-fibre budget: $8 N_{\mathrm{IV}^*} + 9 N_{\mathrm{III}^*} + 10 N_{\mathrm{II}^*} \le 24$ (pairwise-disjoint IV*/III*/II* loci).
11. At most three type $\mathrm{IV}^*$ ($E_6$) points ($4 \times 8 = 32 > 24$).
12. At most two type $\mathrm{III}^*$ ($E_7$) points ($3 \times 9 = 27 > 24$).
13. At most two type $\mathrm{II}^*$ ($E_8$) points ($3 \times 10 = 30 > 24$).
14. Residual budget: for any finite set $E$ of $\mathrm{II}^*$ ($E_8$) points and any finite $S$ disjoint from $E$, $10\,|E| + \sum_{t \in S}\operatorname{ord}_t\Delta \le 24$ (two $E_8$ points leave at most $4$; note $S$ need not be classified by the seven types).
## Significance
Every entry of the table is load-bearing for the budget: the goal converts each $\operatorname{discOrder}(\tau(t))$ into the true local order $\operatorname{ord}_t\Delta$ (milestones 3--9), then bounds the sum by $\deg\Delta \le 24$ (milestones 1--2). Corollaries recover the physics: at most two $\mathrm{II}^*$, at most two $\mathrm{III}^*$, and at most three $\mathrm{IV}^*$ fibres (the $E_8, E_7, E_6$ loci in the split/geometric setting -- a nonsplit $\mathrm{IV}^*$ gives $F_4$); the exceptional budget $8 N_{\mathrm{IV}^*} + 9 N_{\mathrm{III}^*} + 10 N_{\mathrm{II}^*} \le 24$; and the residual budget $10\,\#E + \sum_{t \in S} \operatorname{ord}_t\Delta \le 24$, so two $\mathrm{II}^*$ points leave at most $4$ for the other fibres. Mathlib has a single-curve `WeierstrassCurve`/`EllipticCurve` library but **no elliptic-fibration theory**: this mission builds a machine-checked slice of the Kodaira/Tate fibre-order table over Mathlib's `Polynomial` API. The results are classical (Kodaira; Tate's algorithm; Schuett--Shioda, arXiv:0907.0298), so the work is the formalization.
## Difficulty
The six "clean" rows ($\mathrm{II}, \mathrm{III}, \mathrm{IV}, \mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$) sit at *unequal* orders $3\operatorname{ord} f \ne 2\operatorname{ord} g$, so the order of the sum is the smaller summand's order — an order-of-a-sum computation, valid in characteristic zero where $4, 27$ are units. The genuinely hard row is $\mathrm{I}_0^*$, which needs finer data than the raw orders. Writing $f = (X - t_0)^2 F$, $g = (X - t_0)^3 G$ with $c_2 = F(t_0)$, $d_3 = G(t_0)$, both terms of $\Delta = 4f^3 + 27g^2$ have order at least $6$, and the coefficient of $(X - t_0)^6$ is $4c_2^3 + 27 d_3^2$; its nonvanishing gives $\operatorname{ord}_{t_0}\Delta = 6$. This covers the three branches $(\operatorname{ord} f, \operatorname{ord} g) = (2,3),\ (2, {\ge} 4),\ ({\ge} 3, 3)$ uniformly — only in the $(2,3)$ branch, where $3\operatorname{ord} f = 2\operatorname{ord} g = 6$, can two nonzero order-$6$ contributions cancel. The nonvanishing is the distinct-roots criterion for the reduced cubic $x^3 + c_2 x + d_3$ and, under $\operatorname{ord} f \ge 2$ and $\operatorname{ord} g \ge 3$, characterizes the $\mathrm{I}_0^*$ row; when it vanishes, further valuation data distinguish the $\mathrm{I}_n^*$ series, the higher potentially good types, and nonminimal cases. The budget itself then needs the local-to-global degree bound (milestones 1--2).
## Formalization scope
Over a characteristic-zero field $k$ (intended $k = \mathbb{C}$), Mathlib-native `Polynomial` API only (`natDegree`, `rootMultiplicity`, `roots`, `taylor`). Lower-bound orders use divisibility $(X - t_0)^n \mid \cdot$, which faithfully includes the $f = 0$ / $g = 0$ ($\operatorname{ord} = +\infty$) corner that a `rootMultiplicity`-only encoding drops; exact orders use `rootMultiplicity`. No global minimality predicate is assumed; at every point classified by `HasKodaira`, the stated signature implies local minimality (one of $\operatorname{ord} f$, $\operatorname{ord} g$ lies below the non-minimal threshold $\operatorname{ord} f \ge 4 \wedge \operatorname{ord} g \ge 6$). The potentially multiplicative $\mathrm{I}_n$ and $\mathrm{I}_n^*$ series are **excluded** by design (their discriminant orders form unbounded families, not fixed by $(\operatorname{ord} f, \operatorname{ord} g)$). The budget goal is an **upper bound over the fibres one classifies** — it assumes a valid type assignment on $S$ but neither constructs it nor proves the existence and uniqueness of the complete Kodaira classification, and $S$ need not exhaust the singular locus. A full exhaustive classification, the $\mathrm{I}_n^*$ series, and the literal $\mathbb{P}^1$ statement (fibre at infinity via homogeneous forms) are natural future extensions. Characteristic zero is assumed for uniformity, not necessity: the degree bound is characteristic-free and the local order lemmas only need $4, 27 \ne 0$ (characteristic $\ne 2, 3$). Over a non-closed field the classification counts $k$-rational affine points; base-change to $\bar{k}$ recovers the geometric statement. Counts are over the affine chart $\mathbb{A}^1 \subset \mathbb{P}^1$.
## Selected references
- J. Tate, *Algorithm for determining the type of a singular fiber in an elliptic pencil*, in Modular Functions of One Variable IV, LNM 476 (1975), 33--52.
- M. Schuett, T. Shioda, *Elliptic Surfaces*, Adv. Stud. Pure Math. 60 (2010), 51--160. https://arxiv.org/abs/0907.0298
- T. Weigand, *TASI Lectures on F-theory*, arXiv:1806.01854 (2018). https://arxiv.org/abs/1806.01854
16 thms0 active usersReviewed
🏆Completed
Captain: lisamegawatts
Winding Arithmetic II: Conserved Phase BasesResearch Paper
## Motivation
Winding number is a topological integer: continuous deformation preserves it, while crossing a branch cut or registering a reset can change it by an integer amount. Transcendence theory gives a different kind of rigidity. For a nonzero algebraic coupling $\alpha$, the phases $e^{i\alpha n}$ attached to distinct integers $n$ are linearly independent over the field $\overline{\mathbb Q}$ of algebraic complex numbers. This mission joins those statements at their exact formal interfaces.
The result is useful wherever a model first produces an integer winding label and then represents that label by a complex phase. Topology supplies the discrete coordinate, dynamics determines when it is conserved or reset, and Lindemann–Weierstrass supplies arithmetic distinguishability. None of those layers is asked to manufacture the others.
The foundation comes from three completed private missions: *Winding Dynamics I: Homotopy Conservation and Reset Balance*, *Integer Winding Transcendence I: Exponential Phase Independence*, and *Lindemann–Weierstrass I: Exponential Independence*. The transcendence proof is an attributed Lean 4.30-compatible port of Yuyang Zhao's [mathlib PR #28013](https://github.com/leanprover-community/mathlib4/pull/28013).
## Setting
Let $S^1$ be the complex unit circle. A **based Circle loop** is a continuous path in $S^1$ that starts and ends at $1$. Its canonical real lift through the exponential covering starts at $0$; the lift endpoint determines an integer $\operatorname{wind}(\gamma)$.
For $\beta\in\mathbb C$ and $n\in\mathbb Z$, define the **integer exponential character**
$$
\chi_\beta(n)=\exp(n\beta).
$$
The arithmetic consumer uses $\beta=i\alpha$, where $\alpha$ is nonzero and algebraic over $\mathbb Q$. Thus a loop $\gamma$ carries the phase $\chi_{i\alpha}(\operatorname{wind}(\gamma))$.
A **closed Circle field** is a jointly continuous map on the time/spatial square $I\times I$ whose two spatial endpoints agree at every time. Each spatial slice is normalized by its moving basepoint, producing a based loop. A **carrier/readout segment** generalizes this: an ambient trajectory remains in a registered carrier subspace and is observed through a continuous map from that carrier to $S^1$.
The discontinuous branch is represented separately by a finite **reset ledger**. It stores successive integer edge-turn cochains. Pairing those cochains with a certified closed edge cycle produces integer winding values and reset periods.
## Formalization targets
### Circle winding separates algebraic phases
For a family of loops $(\gamma_j)_{j\in J}$ with pairwise-distinct windings,
$$
\left(e^{i\alpha\operatorname{wind}(\gamma_j)}\right)_{j\in J}
\text{ is linearly independent over }\overline{\mathbb Q}.
$$
### Continuous evolution preserves the phase basis
If the initial windings of a family of closed Circle fields are distinct, then the initial phase family is linearly independent, every phase is unchanged between endpoint times, and the final phase family remains linearly independent. The same conclusion is exposed through the carrier/readout interface.
### Reset balance becomes phase factorization
If a reset ledger has endpoint winding change $W_{\mathrm f}-W_{\mathrm i}$ and registered reset periods $\Delta W_j$, then
$$
\chi_\beta(W_{\mathrm f}-W_{\mathrm i})
=\prod_j\chi_\beta(\Delta W_j).
$$
This is the multiplicative image of the exact additive ledger balance.
### The phase readout is faithful
For nonzero algebraic $\alpha$, the character $\chi_{i\alpha}$ is injective on
$\mathbb Z$. Consequently, two actual Circle loops have equal algebraic phase
readouts exactly when they have equal canonical winding. On the reset branch,
$$
\prod_j\chi_{i\alpha}(\Delta W_j)=1
\quad\Longleftrightarrow\quad W_{\mathrm f}=W_{\mathrm i}.
$$
Thus the multiplicative reset record detects zero net winding change without
losing integer information.
## Significance
The main theorem upgrades conservation of a single integer to conservation of an arithmetic basis. Distinct homotopy classes do not merely retain distinct integer labels: after the algebraic exponential readout, the corresponding phases admit no nontrivial finite linear relation with algebraic coefficients. This lets downstream consumers treat a family of winding sectors as a linearly independent family over $\overline{\mathbb Q}$.
The reset theorem provides the matching event law. Continuous evolution preserves the basis, whereas a registered reset multiplies phases according to the reset periods. The two branches share one character but retain different hypotheses, so a discontinuous ledger event is not misrepresented as a continuous homotopy.
The algebraic readout is also faithful: despite taking values on the complex
exponential curve, it neither aliases two winding sectors nor hides a nonzero
net reset behind total phase $1$ under the stated algebraic hypothesis.
This does not establish a particle–wave duality or a quantum-mechanical interpretation. It establishes a precise mathematical analogy: an integer topological label has a complex character representation whose distinct values enjoy a strong arithmetic independence theorem under an algebraic nonresonance condition.
## Difficulty
The individual deductions are short only because three difficult interfaces have already been proved. Replacing an arbitrary integer map by actual Circle winding requires using the canonical covering lift rather than postulating labels. Preserving the phase basis requires transporting injectivity and linear independence through a jointly continuous moving-basepoint normalization. The reset branch requires respecting the sign convention and mapping a finite sum to a finite product, including the empty ledger.
Several tempting statements would be false. Duplicate winding labels cannot give a linearly independent family. The exponent $\alpha=0$ collapses every phase to $1$. Continuity of finitely many vertex phases does not by itself define a continuous spatial Circle field, and crossing the principal cut can change a discrete principal-turn winding. A global readout from a simply connected carrier such as all of $SU(2)$ cannot support nonzero loop winding without a separately registered non-simply-connected subcarrier or channel.
For a general complex coupling, exponential resonance can destroy injectivity.
The nonzero algebraic hypothesis excludes that resonance here through the
proved Lindemann--Weierstrass theorem; it is not merely a convenient side
condition.
## Formalization scope
All artifacts use Lean 4.30 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`. The Circle winding is the floor of the canonical zero-based lift endpoint divided by $2\pi$. Closed fields live on $I\times I$ and are normalized at spatial coordinate zero. The coupling $\alpha$ is an arbitrary complex algebraic number, not necessarily real, and must be nonzero.
The main carrier/readout theorem is conditional on an explicit continuous carrier-valued trajectory, closed spatial slices, and continuous Circle readout. It does not prove existence of a Kuramoto, XY, or Lohe solution, nor preservation of a particular carrier by such an ODE. Those are model-specific successors.
The reset factorization consumes the registered coherent ledger and certified closed cycle. It is an exact algebraic event law, not an energy estimate and not a claim that every physical trajectory realizes such a ledger. Its vertex and edge types retain the universe-zero scope of the existing reset interface.
## Selected references
- Yuyang Zhao, *The Lindemann–Weierstrass theorem*, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
- Nathan Jacobson, *Basic Algebra I*, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
- Allen Hatcher, *Algebraic Topology*, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
13 thms0 active usersReviewed
🏆Completed
Captain: andreaskapfer
Elliptic K3 surfaces: discriminant degree 24 and at most two E₈ pointsResearch Paper
## Motivation
**F-theory** geometrizes the strongly coupled regime of type IIB string theory by encoding the varying axio-dilaton as the complex structure of an elliptic curve fibered over a base. Non-abelian gauge symmetry is read off from the **Kodaira/Tate type** of the singular fibres over the discriminant locus, following the fibre--gauge-algebra dictionary of the classification of singular fibres (T. Weigand, *TASI Lectures on F-theory*, arXiv:1806.01854). The simplest compact example is an **elliptically fibered K3 surface**, the arena of 8d F-theory and its duality with the heterotic string on $T^2$; there the **global** discriminant divisor has degree $24$ ("24 seven-branes", equal to the topological Euler characteristic $e(\mathrm{K3}) = 12\,\chi(\mathcal{O}_{\mathrm{K3}})$; the formalized affine statement is $\deg\Delta \le 24$), and an elliptic K3 can contain **at most two** type II\* fibres. A configuration with two such fibres realizes the $E_8 \oplus E_8$ enhancement familiar from eight-dimensional heterotic/F-theory duality.
## Setting
Fix a field $k$ and work with the (short) Weierstrass model $y^2 = x^3 + f\,x + g$ whose coefficients are polynomials $f, g \in k[X]$ on the affine base line. Its **discriminant** is $\Delta = 4f^3 + 27g^2$ (the usual discriminant up to the unit $-16$). For $t_0 \in k$ write $\operatorname{ord}_{t_0}(p)$ for the multiplicity of $t_0$ as a root of $p \in k[X]$, and $\deg p$ for its degree. A base point $t_0$ is an **$E_8$ point** when $\operatorname{ord}_{t_0}(f) \ge 4$ and $\operatorname{ord}_{t_0}(g) = 5$ (the vanishing orders of a Kodaira type **II\***). The **Calabi--Yau/K3 degree data** condition is $\deg f \le 8$, $\deg g \le 12$, and $\Delta \ne 0$.
## Formalization targets
### Goal
$$\#\{\, t_0 \in k : \operatorname{ord}_{t_0}(f) \ge 4 \text{ and } \operatorname{ord}_{t_0}(g) = 5 \,\} \le 2$$
for $k$ of characteristic zero and $(f,g)$ satisfying the K3 degree data, together with finiteness of that set.
### Milestones
1. $\deg\Delta \le 24$ under $\deg f \le 8$, $\deg g \le 12$.
2. $\operatorname{ord}_{t_0}(\Delta) = 10$ at an $E_8$ point (char $0$).
3. $\sum_{t_0 \in S} \operatorname{ord}_{t_0}(\Delta) \le \deg\Delta$ for finite $S$ and $\Delta \ne 0$.
## Significance
The count of $E_8$ points controls the maximal non-abelian enhancement of an elliptic K3: two disjoint type II\* fibres **consume $20$ of the global discriminant budget of $24$** ($2 \times 10 = 20$), leaving **at most $4$** units for the remaining singular fibres, and realize $E_8 \oplus E_8$; a third is obstructed ($3 \times 10 = 30 > 24$). This is the F-theory count underlying the two $E_8$ factors of the 8d heterotic string, and a prerequisite for classifying 8d gauge groups. (It bounds the number of $E_8$ factors; it is not by itself the full rank-$16$ statement, which additionally involves the Shioda--Tate/Neron--Severi lattice.)
On the formalization side, Mathlib has a substantial single-curve `WeierstrassCurve`/`EllipticCurve` library but **no theory of elliptic surfaces or elliptic fibrations**: discriminants as sections over a base, vanishing orders, and fibre counting are absent. This mission builds the first fibration-level results directly on top of Mathlib's `Polynomial` API. The results are established classically (Kodaira; Tate's algorithm; the Euler-number/discriminant-degree identity in M. Schuett and T. Shioda, *Elliptic Surfaces*, arXiv:0907.0298), so the work here is the machine-checked formalization, not new mathematics.
## Difficulty
Two things are worth separating.
**The cardinality bound itself is elementary.** An $E_8$ point forces $\operatorname{ord}_{t_0}(g) = 5$, so distinct $E_8$ points contribute coprime factors $(X - t_0)^5$ of $g$; then $\deg g \le 12$ already caps their number at two ($3 \times 5 = 15 > 12$). This uses neither the discriminant, nor $f$, nor characteristic zero. The goal is stated in the finiteness-*and*-cardinality form precisely so it cannot be satisfied vacuously.
**The fibration-level content is the milestones**, which are the genuine Kodaira/Tate statements and are independently meaningful: that an $E_8$ point contributes *exactly* $10$ to the discriminant order (milestone 2 -- an order-of-a-sum computation valid because $3\operatorname{ord}(f) \ge 12 > 10 = 2\operatorname{ord}(g)$ and $4, 27$ are units in characteristic zero); the global degree bound $\deg\Delta \le 24$ (milestone 1); and the local-to-global inequality $\sum \operatorname{ord}_{t_0}\Delta \le \deg\Delta$ (milestone 3). These are the load-bearing steps for the *stronger* statements about $E_8$ points coexisting with other fibres -- e.g. that fixing two $E_8$ points leaves only degree $4$ of discriminant for all remaining singular fibres ($\sum_{t \in S}\operatorname{ord}_t\Delta \le 4$) -- which is the natural next goal and cannot be shortcut through $g$.
## Formalization scope
Everything is stated over a characteristic-zero field $k$ (the intended model is $k = \mathbb{C}$) using only Mathlib's `Polynomial` API: `natDegree`, `rootMultiplicity`, `roots`. The discriminant is $\Delta = 4f^3+27g^2$ (up to the unit $-16$). An $E_8$ point is `IsE8Point`: $\operatorname{ord}_{t_0}(f) \ge 4$ and $\operatorname{ord}_{t_0}(g) = 5$. The predicate `IsK3Data` fixes $\deg f \le 8$, $\deg g \le 12$, $\Delta \ne 0$ -- the degree bound characterizing the maximal (K3) elliptic surface and below; it is **not** a full surface-theoretic K3 hypothesis. To rule out a trivializing reading: the goal asserts finiteness of the $E_8$-point set *conjoined with* the cardinality bound, so it cannot be satisfied vacuously through the convention that an infinite set has cardinality $0$; and $\Delta \ne 0$ is assumed wherever $\deg\Delta$ is used as a bound.
**Convention note.** Mathlib's `rootMultiplicity` is $0$ at the zero polynomial, so `IsE8Point` implicitly forces $f \ne 0$ and $g \ne 0$; in particular the degenerate $f \equiv 0$ type II\* locus (where $\operatorname{ord} f = +\infty \ge 4$ morally holds) is excluded by this encoding. This only shrinks the $E_8$-point set, so it does not affect the bound; a faithful $f \equiv 0$-inclusive definition is a candidate refinement.
Characteristic zero is assumed for uniformity rather than necessity: the degree bound is characteristic-free, and the local order calculation only needs $4, 27 \ne 0$ (characteristic $\ne 2, 3$). Over a non-closed field the count is of $k$-rational affine points; base-change to $\bar{k}$ recovers the geometric statement. The count is taken over the affine chart $\mathbb{A}^1 \subset \mathbb{P}^1$; the literal $\mathbb{P}^1$ statement (adding the fibre at infinity via homogeneous forms) is a natural extension and a welcome future contribution, as are the remaining Kodaira/Tate fibre-order lemmas.
## Selected references
- M. Schuett, T. Shioda, *Elliptic Surfaces*, Advanced Studies in Pure Mathematics 60 (2010), 51--160. https://arxiv.org/abs/0907.0298
- T. Weigand, *TASI Lectures on F-theory*, arXiv:1806.01854 (2018). https://arxiv.org/abs/1806.01854
5 thms1 active userReviewed
🏆Completed
Captain: lisamegawatts
Winding Dynamics I: Homotopy Conservation and Reset BalanceTextbook
## Motivation
Phase winding is an integer attached to a circle-valued field on a closed spatial cycle. It distinguishes configurations that cannot be continuously deformed into one another while remaining circle-valued and spatially continuous. In oscillator and spin models this integer is often described informally as conserved by smooth evolution, while changes of winding are attributed to phase slips, vortices, singularities, or branch-cut crossings. The purpose of this mission is to turn that informal division into an exact Lean interface.
The continuum and finite-lattice settings must be separated. A jointly continuous field on a spatial circle really does provide a homotopy of circle maps, so its degree is invariant. A finite list of continuously moving vertex phases does not by itself determine a continuous field on the geometric realization of the lattice. Principal shortest-arc interpolation becomes ambiguous at antipodal bonds, and the corresponding discrete winding can jump even though every vertex phase remains continuous. The mission therefore treats winding as a first integral only on the regular sector and records every failure of regularity through an integer reset ledger.
This distinction is relevant to circle-valued reductions of the Kuramoto model, the finite XY model, and Lohe-type dynamics. Kuramoto's original synchronization model concerns coupled phase oscillators, while Lohe's non-Abelian extension replaces phases by group-valued variables. A model-specific conservation theorem is justified only after the dynamics has been connected to an actual circle-valued spatial loop or to the registered finite principal-branch interface.
## Setting
A **circle loop** is a continuous map from a closed parameter interval to $S^1$ whose two endpoints agree. Its **winding number** is the integer obtained from the endpoint of a lift to the universal cover $\mathbb R\to S^1$. When the loop's basepoint moves during a deformation, the loop is normalized by the inverse of its value at the chosen spatial basepoint; this produces a based loop without changing its winding.
A **continuous Circle-field segment** is a jointly continuous map
$$
U:[t_0,t_1]\times S^1\longrightarrow S^1.
$$
Each time slice $U_t$ is a spatial loop. Such a segment has no branch-cut convention: it is intrinsic topological data.
For a finite directed edge system (including a finite periodic lattice), a state assigns a real lift to every vertex. Each oriented edge receives an integer principal turn. A state is **branch regular** when no stored edge is antipodal. A coherent finite reset ledger stores successive principal-turn cochains $T_i$ and defines the reset $k_i=T_{i+1}-T_i$. For a certified closed integer cycle $C$, the pairing $\langle k_i,C\rangle$ is its registered winding jump.
A Kuramoto, XY, or Lohe consumer must supply the missing model-specific data. For a continuum consumer this is a jointly continuous circle-valued field. For a finite consumer it is a continuous vertex trajectory together with branch regularity away from registered events. A Lohe consumer additionally needs a continuous Circle readout or invariant Circle carrier; preservation of a rotor constraint alone does not provide that reduction.
## Formalization targets
### Continuous-field conservation
For every jointly continuous Circle-field segment, the two endpoint loops have equal winding:
$$
\operatorname{wind}(U_{t_1})=\operatorname{wind}(U_{t_0}).
$$
The statement must cover moving loop basepoints through explicit normalization. Winding is defined directly from Mathlib's exponential covering map as the floor of the zero-based lift endpoint divided by $2\pi$.
### Branch-regular finite conservation
For every finite directed principal-phase trajectory on a preconnected time domain that remains branch regular, every registered integer-chain winding is constant:
$$
W_C(t_1)=W_C(t_0).
$$
Continuity of the vertex phases alone is not a sufficient hypothesis and must not appear as a replacement for branch regularity or spatial interpolation.
### Exact reset balance
For a finite coherent ledger with steps $i=0,\ldots,N-1$, endpoint winding change equals the sum of the reset periods:
$$
W_C(T_N)-W_C(T_0)
=\sum_{i=0}^{N-1}\langle k_i,C\rangle.
$$
The conservation theorem is the empty-ledger or zero-period special case. The statement is an exact integer identity and does not assert an energy lower bound, vortex separation, or a thermodynamic-limit result.
### Dynamics adapters
The generic dynamics adapter requires a jointly continuous ambient-state segment, a registered carrier containing it, closed spatial profiles, and a continuous readout from that carrier to the Circle. Kuramoto/XY or Lohe consumers must separately prove those hypotheses for their model. A second fence states that a global continuous readout from a simply connected carrier maps every loop to a nullhomotopic Circle loop; nonzero Lohe winding therefore requires a separately registered non-simply-connected carrier, such as a preserved $U(1)$ orbit, or a different explicit interface.
## Significance
The resulting theorem family makes precise the statement that winding obstructs unwinding. In the intrinsic continuum setting, winding cannot change while the field remains a continuous $S^1$-valued map. In the finite principal-branch setting, winding is piecewise constant and every change has an exact integer certificate. This separates a topological conservation law from the physical or analytic question of how much energy is needed to realize a certificate.
For formalization, the mission supplies a reusable boundary between topology and dynamics. A dynamics development can establish continuity and carrier preservation without reimplementing covering-space winding. A lattice development can consume the same integer through reset cochains without claiming that a vertex-only path is a homotopy of spatial loops. Later energy-barrier, vortex, and transport results can depend on the reset balance rather than on an informal conservation principle.
## Difficulty
The principal difficulty is that several superficially similar notions of continuity have different consequences. Continuity in time of finitely many vertex phases is continuity into the configuration torus $(S^1)^V$, which is connected and does not preserve a principal-edge winding sector. Continuity of a map on time times the geometric spatial cycle is stronger. A formal statement that confuses them would make the desired theorem false.
There are two additional interface risks. First, the canonical Circle lift is based, whereas a physical phase field normally has a moving value at the chosen spatial origin. Second, the current Lohe development establishes algebraic identities and infinitesimal rotor preservation, not a global continuous flow in a selected Circle subgroup. These distinctions remain visible in the theorem hypotheses.
## Formalization scope
The mission targets Lean 4.30 with Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, matching the cited LeanProofs development. It reuses Mathlib's unit interval, continuous maps, path homotopies, Circle covering map, local constancy, and finite sums. The continuum statement concerns spatial $S^1$ only. The finite theorem is graph-generic: it uses finite oriented edges, integer edge cochains, certified closed integer cycles, coherent successive reset states, and branch regularity on a preconnected time domain.
The scope excludes ODE or PDE existence and uniqueness, preservation of a Circle carrier by a particular Lohe vector field, extraction of a coherent reset ledger from a physical event trajectory, arbitrary graph interpolation, accumulating reset times, thermodynamic limits, and energetic barriers. Those may be attached later through explicit interfaces. No theorem claims global winding conservation for an unrestricted finite vertex trajectory, and no theorem identifies group-valued Lohe motion with Circle motion without a declared continuous readout.
## Selected references
- Monumental Systems, *CircleFundamentalGroupWindingV1*, LeanProofs commit `b656238b73d5f0f74515f6574a1dcb4e0216129f`, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleFundamentalGroupWindingV1.lean#L81
- Monumental Systems, *FiniteTorusPrincipalResetEventV1*, LeanProofs commit `b656238b73d5f0f74515f6574a1dcb4e0216129f`, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/StatMech/FiniteTorusPrincipalResetEventV1.lean#L152-L167
- Monumental Systems, *CircleWindingTranslationHolonomyV1*, LeanProofs commit `b656238b73d5f0f74515f6574a1dcb4e0216129f`, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleWindingTranslationHolonomyV1.lean#L107
- Y. Kuramoto, “Self-entrainment of a population of coupled non-linear oscillators,” in *International Symposium on Mathematical Problems in Theoretical Physics*, Lecture Notes in Physics 39, 1975, pp. 420–422. https://doi.org/10.1007/BFb0013365
- M. A. Lohe, “Non-Abelian Kuramoto models and synchronization,” *Journal of Physics A: Mathematical and Theoretical* 42 (2009), 395101. https://doi.org/10.1088/1751-8113/42/39/395101
- A. Hatcher, *Algebraic Topology*, Chapter 1, Cambridge University Press, 2002. https://pi.math.cornell.edu/~hatcher/AT/ATch1.pdf
6 thms0 active usersReviewed
Captain: Lucas
Undecidability of the Spectral GapResearch Paper
## Motivation
The **spectral gap** of a quantum many-body Hamiltonian is the difference between the energy of its ground state and the energy of its first excited state, in the limit of infinitely many particles. Whether a given microscopic interaction produces a gapped or a gapless system decides much of the macroscopic physics: gapped systems have exponentially decaying correlations and well-defined quantum phases, gapless systems sit at critical points and can display algebraically decaying correlations. Several long-standing questions — the **Haldane conjecture** for antiferromagnetic spin chains, the existence of gapped topological spin liquids, and the **Yang–Mills mass gap** — are instances of the question "given the interaction, is the system gapped?".
Cubitt, Pérez-García and Wolf proved that this question, posed for families of two-dimensional translationally invariant nearest-neighbour spin models, admits no algorithmic answer: the **spectral gap problem is undecidable** ([Nature 528, 207–211 (2015)](https://doi.org/10.1038/nature16059); full version: [Forum of Mathematics, Pi 10:e14 (2022)](https://doi.org/10.1017/fmp.2021.15), also [arXiv:1502.04573](https://arxiv.org/abs/1502.04573)).
Timeline of the ingredients the proof rests on: Turing's undecidability of the halting problem (1936); Berger's undecidability of the domino problem (1966) and Robinson's aperiodic tile set ([Inventiones 12, 177–209 (1971)](https://doi.org/10.1007/BF01418780)); Feynman's and Kitaev's circuit-to-Hamiltonian constructions, which turn a computation into a ground state; Gottesman and Irani's translationally invariant one-dimensional Hamiltonians encoding computation ([FOCS 2009](https://arxiv.org/abs/0905.2419)); and Bitansky–Vadhan-style quantum Turing machine engineering from Bernstein and Vazirani ([SIAM J. Comput. 26, 1411–1473 (1997)](https://doi.org/10.1137/S0097539796300921)). The 2015 result was later sharpened to one-dimensional chains by Bausch, Cubitt, Lucia and Pérez-García ([PRX 10, 031038 (2020)](https://doi.org/10.1103/PhysRevX.10.031038)).
## Setting
Fix a local dimension $d$ and, for each side length $L$, the square lattice $\Lambda(L)=\{1,\dots,L\}^2$ with **open boundary conditions**. Each site carries a copy of $\mathbb{C}^d$, so the state space of the lattice has the standard product basis indexed by assignments of a level in $\{1,\dots,d\}$ to each site. A model is specified by three Hermitian matrices: an on-site term $h_1$ of size $d\times d$, and two interactions $h_{\mathrm{row}},h_{\mathrm{col}}$ of size $d^2\times d^2$ acting on horizontally and vertically adjacent pairs. The Hamiltonian of the finite lattice is
$$H^{\Lambda(L)} \;=\; \sum_{\text{horizontal edges}} h_{\mathrm{row}}^{(i,j)} \;+\; \sum_{\text{vertical edges}} h_{\mathrm{col}}^{(i,j)} \;+\; \sum_{k\in\Lambda(L)} h_1^{(k)},$$
the same three matrices being used at every edge and every site, which is what **translational invariance** means here. The quantity $\max\{\|h_1\|,\|h_{\mathrm{row}}\|,\|h_{\mathrm{col}}\|\}$ is the **local interaction strength**.
Write $\lambda_0(H^{\Lambda(L)})\le\lambda_1(H^{\Lambda(L)})\le\cdots$ for the eigenvalues and $\Delta(H^{\Lambda(L)})=\lambda_1-\lambda_0$ for the finite-size gap. The family $\{H^{\Lambda(L)}\}_L$ is
- **gapped** (Definition 1 of the source) if there are $\gamma>0$ and $L_0$ such that for all $L>L_0$ the ground state of $H^{\Lambda(L)}$ is non-degenerate and $\Delta(H^{\Lambda(L)})\ge\gamma$;
- **gapless** (Definition 2 of the source) if there is $c>0$ such that for every $\varepsilon>0$ there is an $L_0$ with: for all $L>L_0$, every point of $[\lambda_0,\lambda_0+c]$ lies within $\varepsilon$ of the spectrum of $H^{\Lambda(L)}$.
These two conditions are not negations of each other; the construction guarantees that every instance falls into one of them. The **ground state energy density** is $E_\rho=\lim_{L\to\infty}\lambda_0(H^{\Lambda(L)})/L^2$.
## Formalization targets
### Goal — Theorem 3 of the source
For a fixed universal machine and every $n$, one explicit family of interactions, built from fixed integer-valued matrices $A,A',B,C,D,D'$, a diagonal projector $\Pi$, a rational $\beta>0$ that may be taken arbitrarily small, and an algebraic $\alpha(n)\le 2\beta$,
$$h_1(n)=\alpha(n)\Pi,\qquad h_{\mathrm{col}}(n)=D+\beta D',$$
$$h_{\mathrm{row}}(n)=A+\beta\Bigl(A'+e^{i\pi\varphi}B+e^{-i\pi\varphi}B^{\dagger}+e^{i\pi 2^{-|\varphi|}}C+e^{-i\pi 2^{-|\varphi|}}C^{\dagger}\Bigr),$$
with $\varphi=\varphi(n)$ the rational whose binary expansion after the point is the binary expansion of $n$ reversed, satisfies: the local interaction strength is at most $1$; if the machine halts on input $n$ the family is gapped with gap at least $1$; and if it does not halt the family is gapless. Since halting is undecidable, no algorithm decides gappedness, even with the promise that exactly one of the two alternatives holds and even at fixed local dimension $d$.
### Milestones
The milestone list follows the numbering of the full version: Lemma 8 and Theorem 9 (reduction of halting to ground state energy and to arbitrary low-energy properties), Corollary 7 (the same undecidability for unconstrained local dimension, with rational interactions), Proposition 53 and Corollary 54 (the diverging ground state energy and its promise version), and Theorem 5 (undecidability of the ground state energy density).
## Significance
The result rules out a general algorithm — and therefore any complete general method — for deciding gappedness from the interaction matrices, however much computing power is available; the property genuinely depends on arbitrarily large system sizes. It also implies, via the standard link between undecidability and independence, that there are concrete finite-dimensional models whose gap is independent of the axioms of any consistent recursively axiomatized formal system (Corollary 4 of the source), and it transfers to other low-energy properties such as the existence of algebraically decaying ground-state correlations.
The theorem is proved; none of it is formalized. This mission produces the machine-checked version. The reusable infrastructure it forces into existence is substantial on its own: a formal model of translationally invariant lattice Hamiltonians and their thermodynamic-limit spectral behaviour, the tiling layer, and computational-history-state Hamiltonians. Each milestone is a self-contained statement that can be attacked without the others.
## Difficulty
The obvious approach — encode a halting computation as an energy penalty — gives the ground state *energy* of a finite lattice, not a property of the limit; this is exactly what Lemma 8 achieves, and it is not enough, because a gap is a statement about the sequence of spectra as $L\to\infty$ and is insensitive to any single lattice size. The construction must make the halting information visible at *all* sufficiently large sizes at once while a fixed finite local dimension carries every instance $n$. That forces three separate difficulties: an aperiodic (Robinson) tiling to create squares of every size $2^n$ inside one translationally invariant model; a quantum phase-estimation Turing machine whose transition amplitudes encode $n$ in a single phase $e^{i\pi\varphi(n)}$, so that the instance index does not inflate the local dimension; and a history-state Hamiltonian whose low-energy spectrum can be controlled well enough that a positive energy density in the halting case turns into a genuine spectral gap, and a vanishing one into a dense spectrum above the ground state.
## Formalization scope
The development commits to the following conventions, all of which are visible in the definition items of this mission.
1. Lattices are finite: sites are pairs of indices in $\{0,\dots,L-1\}$, edges are consecutive pairs within a row or a column (**open boundary conditions**; the periodic case of Section 6.3 of the source is out of scope).
2. Operators are complex matrices indexed by product-basis configurations; the interactions are embedded by acting as the given matrix on the two sites of an edge and as the identity elsewhere.
3. The spectrum is taken as the set of **real** numbers in the matrix spectrum, and $\lambda_0$ is its infimum; every statement carries the Hermiticity hypotheses that make this the usual spectrum. Multiplicities are dimensions of eigenspaces, which is how the "identity of spectra as multisets" of Theorem 9 is expressed.
4. Gapped, gapless and the energy density are properties of the whole family $\{H^{\Lambda(L)}\}_L$ generated by a fixed triple of matrices, exactly as in Definitions 1 and 2.
5. Operator norms are $\ell_2$ operator norms; the local interaction strength is the maximum of the three.
6. Machines are represented by partial recursive codes: "halts on input $n$" is definedness of the evaluation, and "has not halted after $L$ steps" is the step-bounded evaluation returning nothing. The explicit local-dimension bounds of Lemma 8 and Theorem 9, which are stated in the source in terms of the number of internal states and the alphabet size of a Turing machine, are replaced by the existence of a finite local dimension.
Degenerate readings are excluded: a zero local dimension satisfies none of the statements, since a non-degenerate ground state requires a one-dimensional eigenspace and the gapless condition requires a non-empty spectrum; and every existential statement fixes the matrices before quantifying over all instances $n$ and all lattice sizes $L$.
Contributions are welcome at any milestone, and also on the infrastructure the milestones need — Wang tilings and the Robinson tile set, Gottesman–Irani history-state Hamiltonians, and quantum Turing machines in the Bernstein–Vazirani sense — which are needed for Theorem 6 and Lemma 47 of the source and are not yet part of this mission's item list.
## Selected references
- T. S. Cubitt, D. Pérez-García, M. M. Wolf, *Undecidability of the Spectral Gap* (full version), Forum of Mathematics, Pi 10:e14, 1–102 (2022). https://doi.org/10.1017/fmp.2021.15 — the version all statements of this mission are formalized against; preprint: https://arxiv.org/abs/1502.04573
- T. S. Cubitt, D. Pérez-García, M. M. Wolf, *Undecidability of the spectral gap*, Nature 528, 207–211 (2015). https://doi.org/10.1038/nature16059
- R. M. Robinson, *Undecidability and nonperiodicity for tilings of the plane*, Inventiones Mathematicae 12, 177–209 (1971). https://doi.org/10.1007/BF01418780
- D. Gottesman, S. Irani, *The quantum and classical complexity of translationally invariant tiling and Hamiltonian problems*, FOCS 2009. https://arxiv.org/abs/0905.2419
- E. Bernstein, U. Vazirani, *Quantum complexity theory*, SIAM J. Comput. 26, 1411–1473 (1997). https://doi.org/10.1137/S0097539796300921
- J. Bausch, T. S. Cubitt, A. Lucia, D. Pérez-García, *Undecidability of the spectral gap in one dimension*, Phys. Rev. X 10, 031038 (2020). https://doi.org/10.1103/PhysRevX.10.031038
15 thms2 active usersReviewed
🏆Completed
Captain: Lucas
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.
8 thms3 active usersReviewed
Captain: Lucas
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).
8 thms1 active userReviewed
Captain: Yivy Yu
Birkhoff's Retrograde Global-Section Conjecture in the Planar Circular Restricted Three-Body ProblemOpen Problem
## Motivation and historical timeline
In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit ([Birkhoff 1915](https://doi.org/10.1007/BF03015982); [Liu--Salomão, Section 1.4](https://arxiv.org/abs/2506.17867v2)). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics ([Joung--van Koert, Introduction](https://arxiv.org/abs/2407.19159v3)).
In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 ([Joung--van Koert, Theorem 1.3](https://arxiv.org/abs/2407.19159v3); [Hryniewicz](https://arxiv.org/abs/0812.4076v8)). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for \(0\leq\mu\leq 1/2\) and \(2.1\leq c\leq 2.1+10^{-6}\) ([Theorems 1.2 and 1.5](https://arxiv.org/abs/2407.19159v3)). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to \(1/2\), in fact obtaining rational open books bound by every retrograde orbit in that regime ([Theorem 1.16](https://arxiv.org/abs/2506.17867v2)). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem ([Liu--Salomão 2026](https://arxiv.org/abs/2606.12912)). These results leave the universal finite-mass, all-subcritical statement below as the open target.
## Setting
Two primaries of masses \(1-\mu\) and \(\mu\), with \(0<\mu<1\), are fixed in rotating coordinates at \((-\mu,0)\) and \((1-\mu,0)\). For a massless particle with phase coordinates \((q_1,q_2,p_1,p_2)\), the Hamiltonian is
$$
H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1
-\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}}
-\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.
$$
This is equation (1.1) of [Joung--van Koert](https://arxiv.org/abs/2407.19159v3). Let \(h_1(\mu)=H_\mu(L_1)\) be the smallest collision-free critical value, where \(L_1\) lies between the primaries. The subcritical range is \(H_\mu=-c<h_1(\mu)\); there are then two bounded physical components, one around each primary ([Liu--Salomão, Section 4](https://arxiv.org/abs/2506.17867v2)).
The mission labels the primary at \((-\mu,0)\). With complex Levi-Civita variables \(z=z_1+iz_2\) and \(w=w_1+iw_2\), the inverse position map is \(q+\mu=2z^2\), and the regularized Hamiltonian is
$$
\begin{aligned}
K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2}
+2|z|^2(z_1w_2-z_2w_1)\\
&-\mu(z_1w_2+z_2w_1)
-\frac{\mu|z|^2}{|2z^2-1|}.
\end{aligned}
$$
On the collision-free domain, \(K_{\mu,c}=|z|^2(H_\mu+c)\), and its zero level regularizes collision with the labeled primary ([Joung--van Koert, equation (2.2)](https://arxiv.org/abs/2407.19159v3)). The selected component \(\Sigma_{\mu,c}\) is anchored at \((z,w)=(0,\sqrt{1-\mu})\). Below \(h_1\), it is a star-shaped three-sphere, invariant under the free antipodal deck map \((z,w)\mapsto(-z,-w)\), and it double-covers the corresponding Moser-regularized \(\mathbb{R}P^3\) component ([Joung--van Koert, Proposition 2.4](https://arxiv.org/abs/2407.19159v3)).
## Target
For every \(0<\mu<1\), every \(-c<h_1(\mu)\), and every complete flow \(\varphi\) on \(\Sigma_{\mu,c}\) generated by \(X_{K_{\mu,c}}\) and commuting with the antipodal map, prove
$$
\exists\,\delta\quad
\operatorname{GeometricRetrograde}(\delta)\ \land\
\operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).
$$
Here \(\delta\) consists of \(x\in\Sigma_{\mu,c}\) and a quotient period \(P>0\) with \(\varphi_P(x)=-x\), with no earlier positive time reaching either \(x\) or \(-x\). Its physical projection is required to be a \(q_2\)-symmetric, simple, collision-free loop of winding \(+1\) around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in [Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3](https://arxiv.org/abs/2407.19159v3).
The rational page is encoded by a smooth immersive disk lift \(\widetilde f:D^2\to\Sigma_{\mu,c}\). Its lift is embedded, its interior is transverse to \(X_{K_{\mu,c}}\), and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section ([Hryniewicz, Definition 1.1](https://arxiv.org/abs/0812.4076v8)).
## Significance
A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences ([Birkhoff 1915](https://doi.org/10.1007/BF03015982); [Joung--van Koert, Introduction](https://arxiv.org/abs/2407.19159v3)). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.
## Difficulty
Existence of a \(q_2\)-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every \(0<\mu<1\) and every energy below \(L_1(\mu)\) ([Liu--Salomão, Theorem 5.1](https://arxiv.org/abs/2506.17867v2)). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges ([Joung--van Koert, Theorem 1.5](https://arxiv.org/abs/2407.19159v3); [Liu--Salomão, Theorem 1.16](https://arxiv.org/abs/2506.17867v2)).
## Formalization scope
The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual `Flow` together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.
The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.
All theorem rows are Lean declarations ending in `by sorry`. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.
## Selected references
- G. D. Birkhoff, *The restricted problem of three bodies*, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. [DOI](https://doi.org/10.1007/BF03015982).
- U. Hryniewicz, *Fast finite-energy planes in symplectizations and applications*, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. [arXiv:0812.4076v8](https://arxiv.org/abs/0812.4076v8).
- C. Joung and O. van Koert, *Computational symplectic topology and symmetric orbits in the restricted three-body problem*, Nonlinearity 38 (2025), 025015. [arXiv:2407.19159v3](https://arxiv.org/abs/2407.19159v3).
- L. Liu and P. A. S. Salomão, *Finite energy foliations and global dynamics in the restricted three-body problem*, arXiv:2506.17867v2 (25 May 2026). [Preprint](https://arxiv.org/abs/2506.17867v2).
- L. Liu and P. A. S. Salomão, *Birkhoff conjecture and finite energy foliations in Hill's lunar problem*, arXiv:2606.12912 (2026). [Preprint](https://arxiv.org/abs/2606.12912).
20 thms4 active usersReviewed
🏆Completed
Captain: He Wang
Kerr Vacuum Solution Verification in Boyer–Lindquist CoordinatesResearch Paper
## Why a coordinate verification of Kerr
The Kerr metric (Kerr, 1963) is the exact solution of the vacuum Einstein equations that describes the exterior gravitational field of a rotating mass. It is the working model for astrophysical black holes: gravitational-wave templates, black-hole imaging and the classification results of the uniqueness theorems all take it as their starting point. Its form in the coordinates of Boyer and Lindquist (1967) is the one found in every textbook, and the statement that this line element has vanishing Ricci tensor is the single most-cited computation of the subject. That computation is long, it is almost never printed, and in practice it is trusted because computer-algebra systems agree on it. The parent project of this mission builds a certified-discovery pipeline for exact solutions of Einstein's equations in which a symbolic verifier is the oracle; this mission asks for the Kerr instance of that oracle's verdict to be re-established inside a proof assistant, so that the pipeline's benchmark result rests on a kernel-checked proof rather than on a simplification routine.
Timeline: Kerr (1963) found the metric in Kerr-Schild and in his original coordinates; Boyer and Lindquist (1967) introduced the coordinates $(t,r,\theta,\varphi)$ in which the metric below is written and described its maximal analytic extension; Carter (1968) established the separability structure that underlies the closed-form inverse. None of these results has, to the authors' knowledge, a machine-checked proof.
## Setting
Fix real parameters $M$ and $a$. A point of $\mathbb R^4$ is written $x=(x_0,x_1,x_2,x_3)=(t,r,\theta,\varphi)$; in Lean it is a function `Pt := Fin 4 → ℝ`. Write $s=\sin\theta$, $c=\cos\theta$ and
$$\Sigma := r^2+a^2\cos^2\theta,\qquad \Delta := r^2-2Mr+a^2 .$$
The **Boyer-Lindquist Kerr metric** is the symmetric $4\times4$ matrix of functions
$$g_{tt}=-\Big(1-\frac{2Mr}{\Sigma}\Big),\quad g_{rr}=\frac{\Sigma}{\Delta},\quad g_{\theta\theta}=\Sigma,\quad g_{\varphi\varphi}=\Big(r^2+a^2+\frac{2Mra^2\sin^2\theta}{\Sigma}\Big)\sin^2\theta,\quad g_{t\varphi}=-\frac{2Mar\sin^2\theta}{\Sigma},$$
with all other entries zero (signature $(-,+,+,+)$, $G=c=1$). Its **closed-form inverse** $\hat g$ has $\hat g^{rr}=\Delta/\Sigma$, $\hat g^{\theta\theta}=1/\Sigma$ and a $(t,\varphi)$ block with denominator $\Sigma\Delta\sin^2\theta$. The **regular coordinate domain** is
$$\mathrm{Reg}_{M,a}(x)\ :\Longleftrightarrow\ \Sigma\neq0\ \wedge\ \Delta\neq0\ \wedge\ \sin\theta\neq0 .$$
For any matrix of functions $g$ with candidate inverse $\hat g$, the **coordinate partial derivative** $\partial_i f(x)$ is the one-variable derivative at $u=x_i$ of the slice $u\mapsto f(x[i\mapsto u])$, and the **coordinate Christoffel symbols** and **coordinate Ricci tensor** are
$$\Gamma^a_{bc}=\tfrac12\sum_k\hat g^{ak}\big(\partial_c g_{kb}+\partial_b g_{kc}-\partial_k g_{bc}\big),\qquad R_{bd}=\sum_i\Big(\partial_i\Gamma^i_{bd}-\partial_d\Gamma^i_{bi}+\sum_j\big(\Gamma^i_{ij}\Gamma^j_{bd}-\Gamma^i_{dj}\Gamma^j_{bi}\big)\Big).$$
These four definitions (`pd`, `christoffel`, `ricci`, `ricciOf`) form the definition bundle `KerrBL_CoordGeometry`; the metric, its inverse and the regular domain form `KerrBL_Kerr_Metric`.
## Formalization targets
### Goal: Kerr vacuum theorem in Boyer-Lindquist coordinates (`KerrBL.vacuum_Kerr`)
For all real $M,a$ and every $x$ with $\mathrm{Reg}_{M,a}(x)$:
$$\sum_k\hat g^{ik}(x)g_{kj}(x)=\delta_{ij},\qquad u\mapsto g_{ij}(x[l\mapsto u])\ \text{and}\ u\mapsto\Gamma^i_{jk}(x[l\mapsto u])\ \text{are differentiable at } x_l,\qquad R_{bd}(x)=0\ \ \forall\,b,d .$$
The goal deliberately bundles the inverse identity and the two differentiability clauses with Ricci-flatness. Without the first, `ricciOf g ĝ` with a wrong $\hat g$ could vanish trivially; without the other two, the derivative in the definition of $R_{bd}$ could be Mathlib's default value $0$ at a non-differentiable slice. With them, the last clause is a statement about the genuine coordinate Ricci tensor.
### Supporting targets
The milestones follow the three layers of the proof: (I) the inverse identity; (II) the bridge from the generic definitions to explicit closed forms, through derivative certification of the metric, the Christoffel bridge, derivative certification of the generic Christoffel symbols, and the Ricci bridge $R_{bd}(x)=\mathrm{RicciKerr}_{bd}(x)$; (III) the vanishing of the explicit expression for each of the eight components that are not structurally zero, as rational identities in the seven variables $(M,a,r,s,c,S,D)$ under $s^2+c^2=1$, $S=\Sigma$, $D=\Delta$, and finally the vanishing of all sixteen generic components.
## Significance
The result itself is classical: the Boyer-Lindquist Kerr family is a vacuum solution wherever the coordinates are regular. What the mission adds is a proof in which the trusted base is explicit and small: a 45-line generic layer defining $\partial_i$, $\Gamma$ and $R$, and the transcription of five metric components from a hash-locked source file, with source-lock lemmas proving that the compact definitions equal the transcriptions. Everything else, including roughly 120 kB of generated closed forms, is bridged by proof; a wrong closed form can make a bridge theorem unprovable but never a false theorem provable. The generic layer and the bridge pattern are reusable for any coordinate metric in four dimensions, and the pattern of certifying a computer-algebra derivation through polynomial witnesses checked by `linear_combination` is reusable for any rational-function identity.
Status: the theorem is proved in the classical sense since 1963 and verified by every computer-algebra system; the machine-checked coordinate proof is what this mission records. At launch every node of the mission carries an accepted proof.
## Difficulty
The obvious argument is to compute. The difficulty is size and control, not ideas. The Ricci components of Kerr are rational functions whose numerators have up to a few hundred monomials in seven variables; a normalisation tactic applied to the raw expression does not terminate in practice, and a naive $\mathrm{simp}$-based unfolding of the double sums over $\mathrm{Fin}\,4$ produces terms whose elaboration alone exceeds the server budget. The proof therefore has to be organised: opaque atoms for $\Sigma$ and $\Delta$ so that denominators are monomials, per-term clearing lemmas over a common denominator, and a single polynomial identity per component certified by explicit quotient witnesses of the relations $s^2+c^2=1$, $S=\Sigma$, $D=\Delta$. Mathlib's derivative also needs care: `deriv` returns $0$ where a function is not differentiable, so every derivative used in the Ricci formula must be accompanied by a `HasDerivAt` witness, and the differentiability of the generic Christoffel symbols has to be transferred from their closed forms by a locality argument on the open regular domain.
## Formalization scope
The Lean representation commits to the following. Points are `Fin 4 → ℝ` with $0=t$, $1=r$, $2=\theta$, $3=\varphi$; there is no manifold, no chart, no periodicity of $\varphi$ and no range restriction on $r$. Derivatives are Mathlib's `deriv` of coordinate slices. The candidate inverse is data; its correctness is a theorem. The parameters $M,a$ are arbitrary reals: the mission proves Ricci-flatness of the Boyer-Lindquist Kerr family on the regular coordinate domain used by the formalization, not a global Lorentzian-manifold theorem and not a statement restricted to the black-hole regime $M>0$, $|a|\le M$. The axis $\sin\theta=0$ is excluded (the inverse carries $1/\sin^2\theta$) although the metric is smooth there; the loci $\Sigma=0$ and $\Delta=0$ are excluded. Nothing is asserted about signature, uniqueness, symmetry of $R_{bd}$ (all sixteen components are proved separately) or any coordinate-independent curvature quantity. A trivialising formalization is ruled out by the goal's first clause: the Ricci tensor of the specification layer takes the inverse as an argument, and the goal certifies that argument.
Independent blind read-back of the definitions and main statements, performed by a separate agent that saw only the Lean text, returned the following honest statement, recorded here verbatim: "For every pair of real numbers $M$, $a$ and every point $(t,r,\theta,\varphi)\in\mathbb R^4$ at which $r^2+a^2\cos^2\theta\neq0$, $r^2-2Mr+a^2\neq0$ and $\sin\theta\neq0$, all sixteen numbers $R_{bd}$ obtained by evaluating the explicit coordinate formula [...] vanish, where $g$ is the explicitly transcribed Boyer-Lindquist Kerr component matrix, $\hat g$ is an explicitly transcribed matrix that (by `ginv_mul_g_Kerr`, under the same hypothesis) satisfies $\hat g g=I$ at that point, and $\partial_i$ is Mathlib's one-variable `deriv` of the coordinate slice." The two should-fix findings of that read-back (inverse coupling; junk derivative values) are addressed by the first three clauses of the goal.
Infrastructure: three definition bundles (`KerrBL_CoordGeometry`, hand-written; `KerrBL_Kerr_Metric`, generated from the source file and human-auditable; `KerrBL_Kerr_ClosedForms`, generated and untrusted). Reusable beyond the mission: the generic layer, the locality lemma, and the bridge pattern. Natural extensions welcome after release: the two-sided inverse, the $a=0$ reduction to Schwarzschild, and curvature invariants such as the Kretschmann scalar.
## Selected references
- R. P. Kerr, *Gravitational field of a spinning mass as an example of algebraically special metrics*, Phys. Rev. Lett. 11 (1963) 237-238. https://doi.org/10.1103/PhysRevLett.11.237
- R. H. Boyer and R. W. Lindquist, *Maximal analytic extension of the Kerr metric*, J. Math. Phys. 8 (1967) 265-281. https://doi.org/10.1063/1.1705193
- B. Carter, *Global structure of the Kerr family of gravitational fields*, Phys. Rev. 174 (1968) 1559-1571. https://doi.org/10.1103/PhysRev.174.1559
- S. Chandrasekhar, *The Mathematical Theory of Black Holes*, Oxford University Press, 1983, Chapter 6.
- S. M. Carroll, *Spacetime and Geometry*, Cambridge University Press, 2019, Section 6.6.
24 thms1 active userReviewed
🏆Completed
Captain: lisamegawatts
Finite Reflection Positivity Methods I: Split Weights and Infrared ModesTextbook
### Motivation
Reflection positivity and infrared bounds form a standard finite-volume route
from the geometry of a lattice reflection to quantitative control of long
wavelength fluctuations. In the classical argument, reflection positivity
supplies a Cauchy--Schwarz inequality for reflected observables, while Fourier
diagonalization of the lattice Laplacian identifies the free covariance used
in the infrared comparison. These ingredients underlie rigorous results on
continuous-symmetry lattice systems in Fröhlich, Simon, and Spencer's
development of infrared bounds and spontaneous symmetry breaking
([1976](https://doi.org/10.1007/bf01608557)), and the general theory of
reflection positivity developed by Fröhlich, Israel, Lieb, and Simon
([1978](https://doi.org/10.1007/bf01940327)). Related technology appears in
Fröhlich and Spencer's treatment of the two-dimensional Abelian spin systems
and Coulomb gas ([1981](https://doi.org/10.1007/bf01208273)).
The analytic and model-specific theorems are substantial, but their finite
algebraic interface is sharply separable. This mission isolates that interface
so later clock, XY, and Gaussian-domination developments can share one checked
notion of reflection, one spectral covariance convention, and one treatment of
the constant mode.
### Setting
Let $X$ be a finite set of configurations on one side of a reflection plane.
A full split configuration is a pair $(x,y)\in X\times X$, and reflection
exchanges its two entries. A plus-half observable is a function $F:X\to
\mathbb R$ lifted to $X\times X$ through the first coordinate. Its reflected
copy therefore depends on the second coordinate.
A split weight is specified by a finite feature index $A$, real coefficients
$c_a$, and features $\phi_a:X\to\mathbb R$:
$$
W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y).
$$
For a finite family of plus-half observables $F_i$, the reflected kernel is
$$
K_{ij}=\sum_{(x,y)\in X\times X}
W(x,y)F_i(x)F_j(y).
$$
A real matrix is positive semidefinite here when it is symmetric and its
quadratic form is nonnegative on every real coordinate vector.
The spectral side uses a finite mode set $I$ with a distinguished zero mode
$0$. An infrared spectrum consists of a function $\lambda:I\to\mathbb R$
that is nonnegative and vanishes exactly at $0$. For $\beta>0$, the free
mode covariance is diagonal, equals zero at the constant mode, and has entry
$$
G_{kk}=\frac{1}{\beta\lambda_k}
$$
away from zero. Covariance domination is tested only on source vectors whose
zero-mode coordinate vanishes. The concrete spectral fixture is the
$4\times4$ periodic square lattice, with tensor-product discrete Fourier modes
and the nearest-neighbor graph Laplacian.
### Formalization targets
#### Finite reflection positivity
The first target identifies the split reflection pairing with the explicit
double sum over the two halves. Under $c_a\ge0$, the resulting reflected
kernel must be positive semidefinite:
$$
\sum_{i,j}u_iK_{ij}u_j\ge0.
$$
Every such kernel must satisfy the two-observable chessboard inequality
$$
K_{ij}^{2}\le K_{ii}K_{jj}.
$$
#### Typed finite spectrum
For every Torus-4 frequency $k$ and site $x$, the registered Fourier mode
$\psi_k$ must satisfy the pointwise eigenvalue equation
$$
(\Delta_{\mathrm{T4}}\psi_k)(x)=\lambda_k\psi_k(x).
$$
The eigenvalues must be nonnegative and vanish exactly at the constant mode,
and these laws must be packaged as the same spectrum type consumed by the
infrared definitions.
#### Zero-mode-restricted infrared bound
The diagonal free covariance must be positive semidefinite for $\beta>0$.
If an interacting covariance $C$ is quadratically dominated by $G$ on sources
with $u_0=0$, then every nonzero Fourier mode must satisfy
$$
C_{kk}\le\frac{1}{\beta\lambda_k}\qquad(k\ne0).
$$
Two finite counterfixtures are part of the target. They assert that an
arbitrary full-vertex reflected two-point matrix need not be positive
semidefinite, and that domination restricted away from the zero mode need not
extend to full-matrix domination.
### Significance
The resulting interface prevents three substitutions that otherwise look
notational but change the theorem. Reflection positivity is tested on
observables supported on one half rather than on an arbitrary matrix indexed
by all vertices. The infrared comparison excludes the constant mode rather
than forcing a fluctuating zero mode below a covariance with zero diagonal.
The graph-Laplacian eigenvalue is connected to the Fourier mode by an explicit
pointwise theorem rather than by assigning a function the name
`laplacianEigenvalue`.
Several ingredients already have machine-checked Lean proofs in the
LeanProofs repository: the finite matrix Cauchy--Schwarz theorem, the Torus-4
DFT diagonalization and zero-mode theorem, and the diagonal free-covariance
calculation. This mission reorganizes those results around a corrected
consumer boundary and adds the split-half and off-zero adapters. It does not
present the finite statements as new mathematics.
### Difficulty
The main difficulty is maintaining the correct domain at each interface. A
reflection of lattice sites does not by itself imply positive semidefiniteness
of a correlation matrix indexed by every site; the tested observables and
their support are part of the assertion. Likewise, a free covariance whose
constant-mode entry is defined to be zero cannot dominate an arbitrary
covariance on all source vectors. Finally, a Fourier multiplier used for a
pseudospectral derivative is not automatically the eigenvalue of the
nearest-neighbor graph Laplacian. The formal statements must keep these three
objects distinct.
### Formalization scope
All configuration, feature, observable, and mode types are finite. Kernels,
weights, coefficients, source vectors, and quadratic forms are real. Complex
numbers occur only in the explicit discrete Fourier modes. Reflected pairings
are unnormalized finite sums; no partition function or probability measure is
introduced. The inverse temperature satisfies $\beta>0$. The distinguished
zero mode is part of the spectrum interface, and infrared domination is
restricted to source vectors that vanish at that coordinate.
The mission does not assert reflection positivity of a clock or XY Gibbs
measure, nonnegative Fourier coefficients of a physical cross-bond weight,
Gaussian domination, a thermodynamic limit, a Kosterlitz--Thouless transition,
or a universal jump. It also does not identify the Torus-4 graph spectrum with
the Grid3 pseudospectral multiplier from the Fourier--Hodge packet. Those are
separate future missions requiring additional model and analytic input.
The reusable outputs are the split-weight RP interface, the finite
positive-semidefinite kernel API, the typed spectrum object, and the
zero-mode-restricted domination predicate. Contributions should preserve the
explicit half support and zero-mode restrictions; a proof obtained by adding
the desired conclusion as a hypothesis is outside scope.
### Selected references
- J. Fröhlich, B. Simon, and T. Spencer, *Infrared bounds, phase transitions
and continuous symmetry breaking*, Communications in Mathematical Physics
50 (1976), 79--95. https://doi.org/10.1007/bf01608557
- J. Fröhlich, R. Israel, E. H. Lieb, and B. Simon, *Phase transitions and
reflection positivity. I. General theory and long range lattice models*,
Communications in Mathematical Physics 62 (1978), 1--34.
https://doi.org/10.1007/bf01940327
- J. Fröhlich and T. Spencer, *The Kosterlitz--Thouless transition in
two-dimensional Abelian spin systems and the Coulomb gas*, Communications in
Mathematical Physics 81 (1981), 527--602.
https://doi.org/10.1007/bf01208273
- LeanProofs, `ReflectionPositivityInfraredBound.lean`, exact repository
snapshot `dbf503b2909cc17787d40a21eb75a0c9354cc6ef`.
https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean
11 thms1 active userReviewed
🏆Completed
Captain: lisamegawatts
Finite Lattice Vortex Methods I: Green Variational EnergyTextbook
## Motivation
Two-dimensional lattice models admit topological defects whose energetic cost competes with their configurational multiplicity. The later stages of a finite vortex argument therefore need a trustworthy bridge from a prescribed vorticity to the least quadratic energy of a compatible field. This mission isolates that bridge. It does not attempt a phase-transition theorem; it establishes only the finite-dimensional variational identity on which a later, model-specific energy estimate can rest.
The algebra belongs to finite discrete Hodge theory. A finite cochain complex supplies a differential from degree one to degree two and an adjoint codifferential in the reverse direction. A normalized Green operator inverts the degree-two Laplacian on realizable vorticities and annihilates the harmonic obstruction. Such finite-complex harmonic methods go back at least to Beno Eckmann's 1944 treatment of harmonic functions and boundary-value problems on complexes. The vortex motivation comes from the energy--entropy mechanism discussed by Kosterlitz and Thouless for two-dimensional systems, but no claim from their thermodynamic analysis is included here.
## Setting
Let $C^0,C^1,C^2$ be finite-dimensional real inner-product spaces. A **finite Hodge complex** consists of linear maps
$$
d_0:C^0\to C^1,\qquad d_1:C^1\to C^2,
$$
together with specified adjoints $\delta_1$ and $\delta_2$, and the cochain relation $d_1d_0=0$. The degree-two Laplacian is
$$
L_2=d_1\delta_2.
$$
The **vorticity space** is $\operatorname{range}(d_1)$. A normalized **degree-two Green owner** supplies a unique self-adjoint linear map $G:C^2\to C^2$ satisfying both inverse identities with the orthogonal projector onto that range, taking values in the range, and vanishing on $\ker(\delta_2)$.
For a realizable source $\omega\in\operatorname{range}(d_1)$, define the canonical one-cochain
$$
a_\omega=\delta_2G\omega.
$$
The physical vortex normalization scales the prescribed vorticity by $2\pi$, so the canonical physical field is $2\pi a_\omega$. For a coupling $J\in\mathbb R$, the quadratic energy of $a\in C^1$ is
$$
E_J(a)=\frac J2\lVert a\rVert^2.
$$
## Formalization targets
### Exact Green variational decomposition
For every realizable $\omega$ and every field $a$ satisfying $d_1a=2\pi\omega$, establish
$$
E_J(a)=2\pi^2J\langle\omega,G\omega\rangle
+E_J\bigl(a-2\pi\delta_2G\omega\bigr).
$$
The equality is required for every real $J$. Its unscaled components assert the exact Poisson equation, closedness and orthogonality of the residual, the Pythagorean norm decomposition, and the identity
$$
\lVert\delta_2G\omega\rVert^2=\langle\omega,G\omega\rangle.
$$
### One-sided minimum-energy bound
For $J\ge0$, conclude
$$
2\pi^2J\langle\omega,G\omega\rangle\le E_J(a).
$$
Two controls are part of the target boundary: zero coupling must not identify a unique minimizer, and zero vorticity must not imply that the underlying field or its positive-coupling energy vanishes.
## Significance
The result separates universal finite linear algebra from geometry that depends on a particular lattice. Once a periodic square torus is registered as a finite Hodge complex, a later theorem may specialize the Green quadratic form to dipole charges and investigate its dependence on separation. Entropy can then be compared with a genuine energy inequality without redefining energy through the desired conclusion.
Formalizing this layer provides reusable interfaces for Poisson solvability, orthogonal residuals, exact quadratic energy splitting, and the nonnegative-coupling lower bound. It also makes normalization errors visible: the factor $2\pi$ in the source and the factor $J/2$ in the energy force the coefficient $2\pi^2J$. The underlying Green-owner infrastructure already has a machine-checked implementation in LeanProofs; the propositions in this mission are new proof obligations derived from that interface.
## Difficulty
The central issue is not an asymptotic estimate. It is maintaining the exact relationship among the Laplacian sign, the orthogonal projector, the Green normalization, adjointness, and the physical $2\pi$ scaling. A proof that silently projects a non-realizable source changes the problem. A proof that divides by $J$ loses the $J=0$ case. A proof that treats zero vorticity as a zero-field assertion discards closed and harmonic residuals. Each of these shortcuts is ruled out by the formal target or its controls.
## Formalization scope
The Lean development uses arbitrary finite-dimensional real inner-product spaces rather than a concrete torus. All maps are continuous only through finite-dimensional linear structure; there is no measure theory, probability, or limiting process. A source is explicitly required to lie in $\operatorname{range}(d_1)$. The exact decomposition permits every real $J$, while the inequality requires $0\le J$. Existence of a Green owner is supplied as data; this mission neither constructs a second inverse nor changes the existing normalization.
The mission does not define integer charge, torus distance, plaquette winding, or a concrete lattice Laplacian. It proves no logarithmic Green estimate, cosine-energy comparison, entropy bound, Gibbs statement, vortex proliferation result, thermodynamic limit, BKT transition, or universal jump. In particular, the target cannot be satisfied by choosing a convenient torus size or hard-coding a Green kernel: it is group-generic finite-dimensional algebra conditional on the stated Hodge and Green structures.
Contributions are welcome on the independent Poisson, orthogonality, norm, scaling, and control nodes. A later mission can add the square-torus realization and the separate analytic capacity estimate needed for a sharp logarithmic lower bound.
## Selected references
- Beno Eckmann, *Harmonische Funktionen und Randwertaufgaben in einem Komplex*, Commentarii Mathematici Helvetici 17 (1944/45), 240--255. https://doi.org/10.1007/BF02566245
- J. M. Kosterlitz and D. J. Thouless, *Ordering, metastability and phase transitions in two-dimensional systems*, Journal of Physics C 6 (1973), 1181--1203. https://doi.org/10.1088/0022-3719/6/7/010
- LeanProofs, finite Hodge Green-owner foundation at commit `dbf503b2909cc17787d40a21eb75a0c9354cc6ef`. https://github.com/MonumentalSystems/LeanProofs/commit/dbf503b2909cc17787d40a21eb75a0c9354cc6ef