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 thms1 active userReviewed
🏆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 thms1 active userReviewed
🏆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 thms1 active userReviewed
🏆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
🏆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