Tate table: type II has $\operatorname{ord}\Delta = 2$

Proved

FTheoryK3Tate.discOrder_II

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 1$ and $\operatorname{ord} g = 1$ — then the discriminant $\Delta = 4f^3 + 27g^2$ vanishes at $t_0$ to order exactly $2$ : $\operatorname{ord}_{t_0}(\Delta) = 2$ . 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.

Preamble

import Definitions.Def_FTheoryK3TateCore
open Polynomial

Formal statement

namespace FTheoryK3Tate
variable {k : Type*} [Field k] [CharZero k]
/-- Tate table, type **II**: `ord f ≥ 1`, `ord g = 1` force `ord Δ = 2`.
    (Here `ord(4f³) ≥ 3 > 2 = ord(27g²)`, so the discriminant inherits the smaller order.) -/
theorem discOrder_II (f g : k[X]) (t₀ : k) (h : HasKodaira f g t₀ Kodaira.II) :
    (Δ f g).rootMultiplicity 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, all $f, g \in k[X]$ and $t_0 \in k$ : if $(X - C\,t_0) \mid f$ (divisibility — order of $f$ at $t_0$ at least $1$ , satisfied also by $f = 0$ ) and $g.\text{rootMultiplicity}\,t_0 = 1$ (exact — forces $g \ne 0$ and $t_0$ a root of $g$ of order precisely $1$ ), then $\operatorname{rootMultiplicity}_{t_0}(4f^3 + 27g^2) = 2$ . The conclusion is an exact equality, so in particular $4f^3+27g^2 \ne 0$ . The two hypotheses are asymmetric (divisibility on $f$ , exact multiplicity on $g$ ).

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 has ord⁡Δ=2\operatorname{ord}\Delta = 2ordΔ=2

Tate table: type II has $\operatorname{ord}\Delta = 2$