Corollary — at most two $E_8$ points ( $f=0$ -faithful)

Proved

FTheoryK3Tate.at_most_two_E8

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

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Let $k$ be a field of characteristic zero and $(f,g)$ satisfy the K3 degree data. Then the set of $E_8$ points (type $\mathrm{II}^*$ fibres, IsE8Point) is finite and has at most two elements. The finiteness is asserted jointly with the cardinality bound, so it cannot be met vacuously via the convention that an infinite set has cardinality $0$ . This restates the headline $E_8 \times E_8$ count on the $f = 0$ -faithful IsE8Point (encoding $\operatorname{ord} f \ge 4$ as $(X - t_0)^4 \mid f$ ).

Preamble

import Definitions.Def_FTheoryK3TateCore
open Polynomial

Formal statement

namespace FTheoryK3Tate
variable {k : Type*} [Field k] [CharZero k]
/-- Corollary (`E₈ × E₈` maximal enhancement). On a Calabi–Yau/K3 model there are only finitely
    many `E₈` (type II*) points, and at most two of them — since each contributes `10` to the
    discriminant budget and `3 × 10 = 30 > 24`. This restates the headline count on the
    `f = 0`-faithful `IsE8Point` (via `(X - C t₀)^4 ∣ f`), fixing the earlier
    `rootMultiplicity`-only encoding. -/
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 FTheoryK3Tate

Source

Kodaira classification of singular fibres and Tate's algorithm: J. Tate, "Algorithm for determining the type of a singular fiber in an elliptic pencil" (Modular Functions of One Variable IV, LNM 476, 1975); M. Schuett and T. Shioda, "Elliptic Surfaces," Adv. Stud. Pure Math. 60 (2010), arXiv:0907.0298 (Euler number = degree of the discriminant divisor = 12*deg L; elliptic K3 => 24). 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

Blind read-back (independent auditor). For a field $k$ of characteristic zero and all $f, g \in k[X]$ : assume $\deg f \le 8$ , $\deg g \le 12$ , $4f^3+27g^2 \ne 0$ . Let $T = \{\, t_0 \in k \mid (X - C\,t_0)^4 \mid f \ \wedge\ \operatorname{rootMultiplicity}_{t_0}(g) = 5 \,\}$ (the unfolding of IsE8Point; note $(X-t_0)^4 \mid f$ is a lower bound allowing $f = 0$ , while $\operatorname{rootMultiplicity} = 5$ forces $g \ne 0$ ). The conclusion is the conjunction: $T$ is finite and $\operatorname{Nat.card} T \le 2$ . Because finiteness is asserted separately, the bound does not rely on the Nat.card-of-infinite-set $=0$ convention; the empty case ( $T = \varnothing$ , e.g. $g = 0$ ) satisfies it trivially.

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

Corollary — at most two E8E_8E8​ points (f=0f=0f=0-faithful)

Corollary — at most two $E_8$ points ( $f=0$ -faithful)