Tate table: type II\* ( $E_8$ ) has $\operatorname{ord}\Delta = 10$

Proved

FTheoryK3Tate.discOrder_IIstar

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 \in k[X]$ . If the fibre at $t_0 \in k$ has Kodaira/Tate type $\mathrm{II^*}$ — i.e. $\operatorname{ord} f \ge 4$ and $\operatorname{ord} g = 5$ — then the discriminant $\Delta = 4f^3 + 27g^2$ vanishes at $t_0$ to order exactly $10$ : $\operatorname{ord}_{t_0}(\Delta) = 10$ . This is the corresponding entry of the Tate table; in characteristic zero the constants $4, 27$ are units, so $\operatorname{ord}(4f^3) = 3\operatorname{ord} f$ and $\operatorname{ord}(27g^2) = 2\operatorname{ord} g$ , and $\Delta$ inherits the smaller of the two orders when they differ. This is the $E_8$ entry.

Preamble

import Definitions.Def_FTheoryK3TateCore
open Polynomial

Formal statement

namespace FTheoryK3Tate
variable {k : Type*} [Field k] [CharZero k]
/-- Tate table, type **II\*** (gauge algebra `E₈`): `ord f ≥ 4`, `ord g = 5` force `ord Δ = 10`.
    (Here `ord(27g²) = 10 < 12 ≤ ord(4f³)`.) This is the `E₈` entry of the table. -/
theorem discOrder_IIstar (f g : k[X]) (t₀ : k) (h : HasKodaira f g t₀ Kodaira.IIstar) :
    (Δ f g).rootMultiplicity t₀ = 10 := 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, all $f, g \in k[X]$ and $t_0 \in k$ : if $(X - C\,t_0)^4 \mid f$ (order of $f$ at $t_0$ at least $4$ , satisfied also by $f = 0$ ) and $g.\text{rootMultiplicity}\,t_0 = 5$ (exact — forces $g \ne 0$ , order precisely $5$ ), then $\operatorname{rootMultiplicity}_{t_0}(4f^3 + 27g^2) = 10$ (exact; in particular $\ne 0$ ). Asymmetric: divisibility on $f$ (allows $f = 0$ ), exact multiplicity on $g$ (excludes $g = 0$ ).

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

Tate table: type II\* (E8E_8E8​) has ord⁡Δ=10\operatorname{ord}\Delta = 10ordΔ=10

Tate table: type II\* ( $E_8$ ) has $\operatorname{ord}\Delta = 10$