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: 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: mysticflounder
Near enemies: spherical sets project to minimal-energy images in general positionResearch Paper
## Motivation
How few distinct distances can a planar point set determine? The near enemies
of this mission are the closest competitors to the extremal configuration:
points in **no-three-collinear position** (no line through three of them) and
points lying on a common **sphere** — the lattice-sphere slice of
Erdős–Füredi–Pach–Ruzsa is the motivating example. The **bisector energy** of a
set counts ordered quadruples $(a,b,c,d)$ of points for which the pair $a,b$ and
the pair $c,d$ have the same perpendicular bisector; it measures how far the set
is from generic. Lund–Sheffer–de Zeeuw fixed the floor of this statistic:
$2n(n-1)$ is a universal lower bound, and bisector injectivity is sufficient
for equality. The Near Enemy theorem is the projection statement on top of it —
every admissible set admits one generic projection whose image attains that
floor, sits in general position, has zero rotation energy, and carries the
whole distance-transport package.
## Setting
Work with finite sets $P$ of points in the Euclidean plane
(`EuclideanSpace ℝ (Fin 2)`), and in the transport direction with points in
`EuclideanSpace ℝ ι` for a general finite index type. Following
Lund–Sheffer–de Zeeuw, the **bisector energy** is
$$\mathcal{E}(P) = \bigl|\{(a,b,c,d) \in P^4 \;:\; a \neq b,\; c \neq d,\; \mathrm{perpBisector}(a,b) = \mathrm{perpBisector}(c,d)\}\bigr|.$$
The **rotation energy** counts the ordered congruent quadruples whose difference
vectors are neither equal nor opposite, so it discards the translation and
half-turn channels and isolates the proper-rotation one. A linear map $T$ is
**projection-generic** for a set $G$ when exactly two conditions hold: $T$ sends
the difference of any two distinct points of $G$ to a nonzero vector, and for
two distinct unordered pairs of $G$ the images never combine a parallel pair of
differences with an orthogonal midpoint difference. Perpendicular bisectors,
difference classes and distance images are all `Finset` operations.
## Target
The mission goal is the spherical complete profile: for every finite set $G$
lying on a common sphere, in any dimension, there is a linear map $T$ to the
plane whose image satisfies six conclusions at once —
$$\exists\,T:\quad \mathcal{E}(T(G)) = 2|G|(|G|-1) \;\wedge\; \mathcal{E}(T(G)) \le \mathcal{E}(P') \text{ for every } |P'| = |G| \;\wedge\; \mathrm{rotationEnergy}(T(G)) = 0$$
together with injectivity of $T$ on $G$, general position of the image (no three
collinear, no four cospherical), and exact distance transport. The projection is
chosen per set — its very type depends on the ambient dimension — but a single
projection delivers all six conclusions together, and that bundled form is what
downstream incidence arguments consume.
Milestones ascend in five steps: the universal energy floor, the
bisector-injectivity equality case, the attainment of the floor by
projection-generic maps, the existence of such a map for every
no-three-collinear set, and the no-three-collinear transport bundle that the
goal then specialises to the spherical case.
## Significance
The extremal picture for bisector energy at the level of the exact constant was introduced in Lund–Sheffer–de Zeeuw, and, in footnote 1 on p. 538 of the SoCG 2015 version
(LIPIcs vol. 34, 537–552), state that $\mathcal{E}(P) = 2n(n-1)$ when every
distinct pair determines a distinct bisector, with the enumeration of the
trivial quadruples that proves the floor. The universal asymptotic form
$\mathcal{E}(P) = \Omega(n^2)$ is a remark in their §3.4.
This mission builds a complete machine-checked development of the
floor, its attainment and the sufficiency direction, from first principles in
Lean 4 over mathlib; the `rotationEnergy` statistic together with the
`rotationEnergy = 0` certificate for the projected image, where
`rotationEnergy(P) = 0` follows from the published "distance Sidon set"
property; and a **single** generic projection of a given set that carries the
bisector floor at the same time as the Erdős–Füredi–Pach–Ruzsa general-position
package. Four of that bundle's six conjuncts are already in
Erdős–Füredi–Pach–Ruzsa 1993, whose Theorem 3.1 supplies them.
Formalizing it matters because the argument composes analysis (generic
projections obtained from nonvanishing of circle determinants), algebra
(inner-product and determinant polynomial witnesses carrying
`linear_combination` certificates) and counting (fiberwise difference-class
tallies) — and the interfaces between the three must agree exactly. The
projection-genericity and polynomial-witness lemmas are reusable for any
Euclidean extremal formalization.
## Difficulty
The hard step is keeping the projection generic through every predicate at once:
a projection that preserves no-three-collinearity can still kill a circle
determinant, or create a coincidence that the counting needs to keep distinct.
The naive first idea — project along a random direction and hope — fails because
each predicate forbids a different algebraic hypersurface of directions; the fix
is a single simultaneous-avoidance argument over the union, with each forbidden
set shown proper by an explicit polynomial witness. That step is the largest
proof in the mission and carries its own milestone.
## Formalization scope
Points are `EuclideanSpace`; finite sets are `Finset`; energies are `ℕ`-valued
statistics. Generic projections are linear maps carrying the explicit
two-clause `ProjectionGeneric` predicate, so there is no hidden regularity
assumption. Dimension is a general `ι` with `[Fintype ι]` wherever the transport
needs it. The goal's only hypothesis is membership of a common sphere;
no-three-collinearity is derived from it rather than assumed, because a line
meets a sphere at most twice. No statement is vacuous: explicit witnesses were
checked in the kernel for the goal and for every milestone.
Welcome contributions: the converse of the equality case — bisector injectivity
is proved here to be sufficient for the floor, and necessity is open in this
development; sharpness examples beyond the Erdős–Füredi–Pach–Ruzsa
configuration; and the incidence assembly that consumes this mission's output.
## Selected references
- B. Lund, A. Sheffer and F. de Zeeuw, Bisector energy and few distinct
distances, Proc. 31st SoCG 2015, LIPIcs vol. 34, 537–552, DOI
[10.4230/LIPIcs.SOCG.2015.537](https://doi.org/10.4230/LIPIcs.SOCG.2015.537);
journal version *Discrete Comput. Geom.* **56** (2016), no. 2, 337–356,
DOI 10.1007/s00454-016-9783-5,
[arXiv:1411.6868](https://arxiv.org/abs/1411.6868). Source of the
bisector-energy statistic and its upper bounds. Footnote 1 on p. 538 of the
SoCG version gives $\mathcal{E}(P) = 2n(n-1)$ for every set whose pairs have
distinct bisectors, with the count of trivial quadruples that proves the
floor; §3.4 (p. 545) gives $\mathcal{E}(P) = \Omega(n^2)$ for every set. The
footnote is not in arXiv:1411.6868v1.
- P. Erdős, Z. Füredi, J. Pach and I. Z. Ruzsa, The grid revisited,
*Discrete Math.* **111** (1993), 189–196,
DOI 10.1016/0012-365X(93)90155-M — the lattice-sphere-slice configuration
that gives this mission its name, and (proof of Theorem 3.1, p. 193) the
generic planar projection that is injective, keeps general position and
transports distances.
- J. Solymosi and T. Tao, An incidence theorem in higher dimensions,
*Discrete Comput. Geom.* **48** (2012), no. 2, 255–280,
DOI 10.1007/s00454-012-9420-x,
[arXiv:1103.2926](https://arxiv.org/abs/1103.2926), §5.1 — the canonical
statement of the generic-projection trick this construction borrows. The same
trick is used in J. Pach and F. de Zeeuw, Distinct distances on algebraic
curves in the plane, *Combin. Probab. Comput.* **26** (2017), no. 1, 99–117,
[arXiv:1308.0177](https://arxiv.org/abs/1308.0177).
- McKenna, Lean formalization (mathlib-only, axiom-clean),
[lean-formalizations](https://github.com/mysticflounder/lean-formalizations),
module `Geometry.Euclidean.NearEnemyTheorem`.
20 thms1 active userReviewed
🏆Completed
Captain: mysticflounder
Pach-de Zeeuw: finite Bezout bound for real plane curvesResearch Paper
## Motivation
The **distinct-distances problem** asks how few distinct distances a finite planar
point set can determine. Guth and Katz proved the near-optimal bound
$\Omega(n / \log n)$ in 2015. Their argument passes through incidence geometry:
distances become incidences between points and curves, and the Elekes–Sharir
framework converts the problem into an incidence bound for lines in
three-space. Pach and de Zeeuw showed the same pipeline works for points on a
fixed algebraic curve, replacing line incidences with curve incidences. The
algebraic prerequisite for that replacement — that two bounded-degree real
plane curves with no shared component meet in finitely many points, with an
explicit degree-dependent bound — is what this mission formalizes.
## Setting
A **real plane curve** here is the real zero set of a nonzero bivariate polynomial
$p \in \mathbb{R}[x, y]$, written $V(p) = \{(x,y) : p(x,y) = 0\}$. Its
**total degree** is the maximum $i+j$ over monomials $x^i y^j$ with nonzero
coefficient. A curve is **irreducible** when its polynomial is irreducible.
The paper says two curves have a **common component** when their polynomials
share a nonconstant factor. The Lean development uses a different, weaker
hypothesis, `NoCommonCurveComponent`: no *infinite* irreducible real curve lies
inside both sets. A shared factor whose real zero set is finite (for example
$x^2 + y^2$) violates the paper's hypothesis but satisfies the Lean one, so the
Lean theorem covers strictly more pairs of curves than the paper's statement.
**Currying** views $p$ as a univariate polynomial in one coordinate whose
coefficients are polynomials in the other. In the Lean code the polynomial
variable is coordinate $0$ and the coefficient (base) variable is coordinate $1$;
this description writes the base coordinate as $x$ and the fiber coordinate as
$y$, so a line $\{x = c\}$ is called **vertical**. The **resultant** of two
curried polynomials is a polynomial in $x$ alone. The development uses one
direction of its defining property: if the two specializations at $x$ share a
real root, the resultant vanishes at $x$. All Lean statements use
`MvPolynomial (Fin 2) ℝ` for plane polynomials and `EuclideanSpace ℝ (Fin 2)`
for points.
## Target
The mission's goal is a finite-intersection bound in the spirit of Theorem 2.1
of Pach–de Zeeuw (Bézout's inequality), but it is not that theorem. It differs
in both directions:
$$ \forall d_1, d_2,\ \exists C > 0,\ \forall C_1, C_2 \text{ of total degree} \le d_1, d_2 \text{ with no common infinite irreducible component}:\quad C_1 \cap C_2 \text{ is finite and } |C_1 \cap C_2| \le C. $$
- The conclusion is an existential degree-dependent constant. The proof's
witness is $C = (d_1+d_2+1)^8 + 1$. The paper's sharp bound $d_1 \cdot d_2$ is
not proved here.
- The hypothesis is the weaker "no common infinite irreducible component"
described above, so the statement is not a formal consequence of the paper's
Theorem 2.1; the shared-finite-factor case is handled separately in the proof
by a singular-point count.
The six milestones are the algebraic inputs: coefficient-root counting, the two
resultant-nonvanishing criteria, the fiber bound, and the two mixed
vertical/nonvertical pair bounds that carry the constant $d_1 \cdot d_2$. The
nonvertical–nonvertical pair bound (`primitive_nonvertical_pair_intersection_bound`)
carries the cruder constant $((d_1+d_2)^2+1)\cdot\max(d_1,d_2)$. Above the
milestones sit the irreducible-pair assembly with constant $(d_1+d_2+1)^4$ and
the factorized assembly with constant $(d_1+d_2+1)^8$, from which the goal
follows.
## Significance
The result is the algebraic input to the Pach–de Zeeuw distinct-distances
theorem for points on curves: without a uniform finite-intersection bound, the
incidence count that drives the distance bound cannot even be stated. The
formalization pins down every constant and every non-degeneracy hypothesis
(non-verticality, no shared infinite component, coprimality) that the argument
consumes.
The proof composes four toolkits — univariate root counting, Sylvester-matrix
resultant degree bounds, normalized-factor decompositions, and a smooth
implicit-function nonsingularity argument — whose interfaces must agree
exactly. The resulting lemmas (resultant criteria, fiber bounds,
partial-derivative degree bounds) are reusable for other real-algebraic
incidence formalizations over `MvPolynomial`.
## Difficulty
The central difficulty is elimination with explicit constants: the resultant
converts a two-variable intersection problem into a one-variable root count,
but every step (currying, specialization, factor-pair summation) must preserve
a usable degree bound, and the degenerate configurations (vertical fibers,
shared factors with finite real zero set, singular points) each need a separate
finite bound.
The textbook route — Bézout's inequality over $\mathbb{C}$, then observing
that real intersection points are complex ones — is not taken, for two
reasons. Mathlib has no plane-curve Bézout theorem to invoke. And under the
weaker Lean hypothesis the two polynomials may share an irreducible factor with
finite real zero set, in which case the complex intersection is infinite and no
complex count applies; that branch is closed by bounding the singular points of
the shared factor instead.
## Formalization scope
Points are `EuclideanSpace ℝ (Fin 2)`; curves are `MvPolynomial (Fin 2) ℝ`
zero sets; finiteness is `Set.Finite` with `Set.ncard` bounds. The development
commits to total degree (not weighted degrees) and to the currying order that
eliminates Lean coordinate $0$; `variable`-style implicit degree bounds
$d_1, d_2$ are explicit `{d₁ d₂ : ℕ}` binders on the platform. No statement is
vacuous: every intersection bound carries the non-degeneracy hypothesis
(non-associated irreducibles, non-divisibility, nonzero partials) that excludes
the infinite-intersection cases. Contributions welcome: the sharp $d_1 d_2$
general bound (currently an existential constant), the paper's hypothesis form
(no common factor at all), and the incidence assembly that consumes this
mission's output.
## Selected references
- János Pach and Frank de Zeeuw, Distinct distances on algebraic curves in the
plane, Combin. Probab. Comput. 26 (2017), no. 1, 99–117,
[arXiv:1308.0177](https://arxiv.org/abs/1308.0177), DOI
10.1017/S0963548316000225. Theorem 2.1 there cites C. G. Gibson, Elementary
Geometry of Algebraic Curves, Lemma 14.4, for Bézout's inequality.
- McKenna, Lean formalization of the algebraic preliminaries and Bézout bound,
[lean-formalizations](https://github.com/mysticflounder/lean-formalizations),
modules `PachDeZeeuw.AlgebraicPrelim` and `PachDeZeeuw.Bezout` (mathlib-only,
axiom-clean).
39 thms1 active userReviewed
🏆Completed
Captain: Lucas
Esquisse d'un Programme I: Dessins d'Enfants and the Faithfulness of the Galois ActionResearch Paper
## Motivation
In *Esquisse d'un Programme* (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a **dessin d'enfant**, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above $0$, $1$ and $\infty$, and that curve and map are defined over the field $\overline{\mathbb{Q}}$ of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group $\Gamma = \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function $f(z) = P(z)/Q(z)$, the action of $\gamma \in \Gamma$ is obtained simply by applying $\gamma$ to the coefficients of $P$ and $Q$. Grothendieck states in §2 (p. 9) that the resulting outer action of $\Gamma$ on the profinite fundamental group $\hat{\pi}_{0,3}$ of $\mathbb{P}^1 \smallsetminus \{0,1,\infty\}$ is **faithful**, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.
Timeline of the results this mission formalizes. Belyi (1979, *On Galois extensions of a maximal cyclotomic field*, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over $\mathbb{C}$ is defined over a number field if and only if it admits a map to $\mathbb{P}^1$ unramified outside $\{0,1,\infty\}$; the "only if" half is an explicit construction with polynomials over $\mathbb{Q}$. Grothendieck (1984) drew the consequence that $\Gamma$ acts on dessins and asserted faithfulness of the action on $\hat{\pi}_{0,3}$. Lenstra, in an appendix to L. Schneps (ed.), *The Grothendieck Theory of Dessins d'Enfants* (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of **plane trees**, equivalently on **Shabat polynomials**. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.
## Setting
Work over $\overline{\mathbb{Q}}$, realized as the algebraic closure of $\mathbb{Q}$, and write $\Gamma$ for its group of field automorphisms fixing $\mathbb{Q}$ pointwise.
A nonconstant polynomial $P$ over a field $K$ is a **Belyi polynomial** (classically a *Shabat polynomial*) when every critical value of $P$ lies in $\{0,1\}$: for every $z \in K$ with $P'(z) = 0$ one has $P(z) = 0$ or $P(z) = 1$. Over an algebraically closed field of characteristic zero this says exactly that $P$, viewed as a degree-$n$ map $\mathbb{P}^1 \to \mathbb{P}^1$, is unramified outside the fibres over $0$, $1$ and $\infty$. The associated dessin is the preimage $P^{-1}([0,1])$, a plane tree with $n$ edges whose vertices are the points above $0$ and $1$, with vertex orders equal to the multiplicities of the corresponding roots of $P$ and of $P - 1$.
Two Belyi polynomials define the same dessin exactly when they are **affinely equivalent**: $Q = P(aX + b)$ for some $a \neq 0$ and some $b$. The target coordinate is already rigidified by the normalisation of the critical values to $\{0,1\}$; only the source coordinate remains free.
The group $\Gamma$ acts coefficientwise: $P^{\gamma}$ is the polynomial obtained from $P$ by applying $\gamma$ to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.
## Formalization targets
### Goal — faithfulness of the Galois action on plane trees
$$\forall\, \gamma \in \Gamma,\quad \gamma \neq 1 \ \Longrightarrow\ \exists\, P \in \overline{\mathbb{Q}}[X] \text{ a Belyi polynomial with } P \not\sim_{\mathrm{aff}} P^{\gamma}.$$
Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.
### Supporting targets
- **Belyi's theorem, polynomial form.** For every finite set $S \subseteq \overline{\mathbb{Q}}$ there is a Belyi polynomial $f \in \mathbb{Q}[X]$ with $f(S) \subseteq \{0,1\}$.
- **Descent to $\overline{\mathbb{Q}}$.** Every Belyi polynomial over $\mathbb{C}$ is affinely equivalent to one whose coefficients are algebraic over $\mathbb{Q}$.
- **Galois equivariance and invariants.** $P^{\gamma}$ is again a Belyi polynomial of the same degree, and the multiplicity of $z$ as a root of $P - c$ equals the multiplicity of $\gamma(z)$ as a root of $P^{\gamma} - \gamma(c)$: the dessin's vertex and face orders are Galois invariants.
- **Finiteness of the orbit.** The set of Galois conjugates of a fixed polynomial over $\overline{\mathbb{Q}}$ is finite — the "visibly finite number of conjugates" of §3.
- **Finiteness in a fixed degree.** For each $n$ there are only finitely many monic Belyi polynomials of degree $n$ over $\overline{\mathbb{Q}}$ with vanishing subleading coefficient.
- **Separation.** For every $\alpha \in \overline{\mathbb{Q}}$ there is a Belyi polynomial $P$ such that every $\gamma$ fixing the class of $P$ fixes $\alpha$. The goal follows from this by taking $\alpha$ with $\gamma(\alpha) \neq \alpha$.
## Significance
The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of $\Gamma$: every nontrivial automorphism of $\overline{\mathbb{Q}}$ is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that $\Gamma$ embeds into the outer automorphism group of $\hat{\pi}_{0,3}$.
Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over $\overline{\mathbb{Q}}$ and $\mathbb{C}$, so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.
## Difficulty
The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all $\gamma \neq 1$, and $\Gamma$ has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number $\alpha$, a tree whose isomorphism class remembers $\alpha$; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over $\mathbb{C}$ is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.
## Formalization scope
Conventions fixed in the Lean development, and not to be re-litigated by solvers:
- $\overline{\mathbb{Q}}$ is `AlgebraicClosure ℚ`, and $\Gamma$ is its group of $\mathbb{Q}$-algebra automorphisms.
- "Belyi polynomial" means: positive degree, and every root of the formal derivative is sent to $0$ or $1$. Critical values are required to lie *in* $\{0,1\}$, not to be exactly $\{0,1\}$; degenerate cases such as $X^n$ (one finite critical value) are therefore included.
- Being a Belyi polynomial is stated over an arbitrary field but is only intended over algebraically closed fields ($\overline{\mathbb{Q}}$, $\mathbb{C}$), where quantifying over the field's own elements captures all critical points.
- Dessin isomorphism is modelled as affine equivalence of the source variable only; conjugating by an affine map of the target is excluded, since the target is rigidified by $\{0,1\}$.
- The Galois action is coefficientwise application of $\gamma$.
Trivialization is ruled out as follows: the goal asserts the *existence* of a moved Belyi polynomial for each nontrivial $\gamma$, with the nondegeneracy `0 < deg P` built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ($\gamma \neq 1$ is satisfiable).
A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over $\mathbb{C}$ as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.
## Selected references
- A. Grothendieck, *Esquisse d'un Programme* (1984), published in L. Schneps and P. Lochak (eds.), *Geometric Galois Actions 1*, LMS Lecture Note Series 242, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511758874
- G. V. Belyi, *On Galois extensions of a maximal cyclotomic field*, Izv. Akad. Nauk SSSR Ser. Mat. 43 (1979), 267–276. English translation: Math. USSR-Izv. 14 (1980), 247–256. https://doi.org/10.1070/IM1980v014n02ABEH001096
- L. Schneps (ed.), *The Grothendieck Theory of Dessins d'Enfants*, LMS Lecture Note Series 200, Cambridge University Press, 1994. https://doi.org/10.1017/CBO9780511569302
- S. K. Lando and A. K. Zvonkin, *Graphs on Surfaces and Their Applications*, Encyclopaedia of Mathematical Sciences 141, Springer, 2004. https://doi.org/10.1007/978-3-540-38361-1