Milestone 1 — $\deg\Delta \le 24$ (24 seven-branes)

Proved

FTheoryK3Tate.discriminant_natDegree_le

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

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Let $k$ be a field and $f, g \in k[X]$ . If $\deg f \le 8$ and $\deg g \le 12$ , then the discriminant $\Delta = 4f^3 + 27g^2$ satisfies $\deg \Delta \le 24$ . This is the 7-brane count $\deg\Delta = \chi(\mathrm{K3}) = 24$ (with multiplicity). Formalization note. Degrees are natDegree (zero polynomial has degree $0$ ), so the bound holds trivially if $\Delta = 0$ ; no characteristic hypothesis is needed.

Preamble

import Definitions.Def_FTheoryK3TateCore
open Polynomial

Formal statement

namespace FTheoryK3Tate
variable {k : Type*} [Field k]
/-- Milestone (24 seven-branes). Under the Calabi–Yau degree bound `deg f ≤ 8`, `deg g ≤ 12`,
    the discriminant `Δ = 4f³ + 27g²` has degree at most `24`. -/
theorem discriminant_natDegree_le (f g : k[X])
    (hf : f.natDegree ≤ 8) (hg : g.natDegree ≤ 12) :
    (Δ f g).natDegree ≤ 24 := 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$ and all $f, g \in k[X]$ : if $\deg f \le 8$ and $\deg g \le 12$ (zero polynomial counted as degree $0$ ), then $\deg(4f^3+27g^2) \le 24$ (again with the convention that the zero polynomial has degree $0$ , so the bound is trivial if $4f^3+27g^2=0$ ). The hypotheses are $\le$ , not equalities, and the conclusion is an upper bound, not an equality — no claim that the degree equals $24$ or that the leading term is nonzero. No characteristic assumption is imposed, so $4$ or $27$ may vanish in $k$ .

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

Milestone 1 — deg⁡Δ≤24\deg\Delta \le 24degΔ≤24 (24 seven-branes)

Milestone 1 — $\deg\Delta \le 24$ (24 seven-branes)