Prove2Me

At most two E8E_8 points on an elliptic K3

Proved
FTheoryK3.at_most_two_E8

by andreaskapfer · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Let kk be a field of characteristic zero and let f,g∈k[X]f, g \in k[X] satisfy the Calabi--Yau/K3 degree data

deg⁡f≤8,deg⁡g≤12,Δ=4f3+27g2≠0.\deg f \le 8,\qquad \deg g \le 12,\qquad \Delta = 4f^3 + 27g^2 \ne 0.

Call t0∈kt_0 \in k an E8E_8 point if ord⁡t0(f)≥4\operatorname{ord}_{t_0}(f) \ge 4 and ord⁡t0(g)=5\operatorname{ord}_{t_0}(g) = 5. Then the set of E8E_8 points is finite, and

#{ t0∈k:t0 is an E8 point }≤2.\#\{\, t_0 \in k : t_0 \text{ is an } E_8 \text{ point} \,\} \le 2.

Each E8E_8 point forces the discriminant to vanish to order 1010 there, while the total available order is deg⁡Δ≤24\deg\Delta \le 24; hence at most two such points occur. This is the geometric origin of the heterotic E8×E8E_8 \times E_8 gauge symmetry: an elliptic K3 accommodates at most two type II* fibres.

Formalization Note. The statement bundles finiteness of the E8E_8-point set with the cardinality bound, so it does not rely on the convention that the cardinality of an infinite set is 00. The count is over the affine chart; see the mission's formalization-scope note.

Preamble
import Definitions.Def_FTheoryK3Core
open Polynomial
variable {k : Type*} [Field k] [CharZero k]
Formal statement
namespace FTheoryK3
theorem at_most_two_E8
    (f g : k[X]) (h : IsK3Data f g) :
    {t₀ : k | IsE8Point f g t₀}.Finite ∧
    Nat.card {t₀ : k | IsE8Point f g t₀} ≤ 2 := by
  sorry
end FTheoryK3
Source
Kodaira classification of singular fibres and Tate's algorithm: M. Schuett and T. Shioda, "Elliptic Surfaces," Adv. Stud. Pure Math. 60 (2010), arXiv:0907.0298 (Euler number of an elliptic surface = degree of the discriminant divisor = 12*deg L; elliptic K3 => 24 singular fibres). F-theory dictionary between Kodaira/Tate fibre types and gauge algebras up to E8, and 7-branes: T. Weigand, "TASI Lectures on F-theory," arXiv:1806.01854.
Read-back

What the Lean code literally says, in plain math · claude-opus-4-8

Read-back (blind, independent auditor). Let kk be a field of characteristic zero. For all f,g∈k[X]f, g \in k[X], assume deg⁡f≤8\deg f \le 8, deg⁡g≤12\deg g \le 12 (zero-polynomial-degree-00 convention), and 4f3+27g2≠04f^3+27g^2 \ne 0. Then the set T={ t0∈k∣ord⁡t0(f)≥4 and ord⁡t0(g)=5 }T = \{\, t_0 \in k \mid \operatorname{ord}_{t_0}(f) \ge 4 \text{ and } \operatorname{ord}_{t_0}(g) = 5 \,\} is finite, and card⁡T≤2\operatorname{card} T \le 2. Each qualifying t0t_0 is a point where ff vanishes to order ≥4\ge 4 and gg to order exactly 55. Because finiteness is asserted separately, the cardinality bound does not rely on the Nat.card-of-infinite-set=0=0 convention.

Human review

  • Endorsed by Shuze Chen · Sep 22, 2026

  • Endorsed by andreaskapfer · Sep 22, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph