A type II\* ( $E_8$ ) fibre has $\operatorname{ord}_{t_0}\Delta = 10$

Proved

FTheoryK3.rootMultiplicity_discriminant_of_isE8Point

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

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Let $k$ be a field of characteristic zero and let $f, g \in k[X]$ . Suppose $t_0 \in k$ is an $E_8$ (Kodaira type II*) point, i.e.

\operatorname{ord}_{t_0}(f) \ge 4 \qquad\text{and}\qquad \operatorname{ord}_{t_0}(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 local fingerprint of a type II* fibre: $\operatorname{ord}_{t_0}(4f^3) = 3\,\operatorname{ord}_{t_0}(f) \ge 12$ exceeds $\operatorname{ord}_{t_0}(27g^2) = 10$ , so the discriminant inherits the smaller order. It is the per-brane multiplicity summed against the global bound.

Formalization Note. Characteristic zero guarantees $4$ and $27$ are nonzero in $k$ . An order of exactly $10$ implies in particular that $\Delta \ne 0$ .

Preamble

import Definitions.Def_FTheoryK3Core
open Polynomial
variable {k : Type*} [Field k] [CharZero k]

Formal statement

namespace FTheoryK3
theorem rootMultiplicity_discriminant_of_isE8Point
    (f g : k[X]) (t₀ : k) (h : IsE8Point f g t₀) :
    (Δ f g).rootMultiplicity t₀ = 10 := 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 $k$ be a field of characteristic zero. For all $f, g \in k[X]$ and every $t_0 \in k$ , if $\operatorname{ord}_{t_0}(f) \ge 4$ (forcing $f\ne 0$ and $t_0$ an actual root of $f$ ) and $\operatorname{ord}_{t_0}(g) = 5$ (forcing $g\ne 0$ and $t_0$ an actual root of $g$ ), then $\operatorname{ord}_{t_0}(4f^3+27g^2) = 10$ . A multiplicity of exactly $10$ in particular asserts $t_0$ is a genuine root of $4f^3+27g^2$ and that this polynomial is nonzero.

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

A type II\* (E8E_8E8​) fibre has ord⁡t0Δ=10\operatorname{ord}_{t_0}\Delta = 10ordt0​​Δ=10

A type II\* ( $E_8$ ) fibre has $\operatorname{ord}_{t_0}\Delta = 10$