24 seven-branes: $\deg\Delta \le 24$

Proved

FTheoryK3.discriminant_natDegree_le

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

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Let $k$ be a field and let $f, g \in k[X]$ be the coefficients of the Weierstrass model $y^2 = x^3 + f\,x + g$ . If

\deg f \le 8 \qquad\text{and}\qquad \deg g \le 12,

then the discriminant $\Delta = 4f^3 + 27g^2$ satisfies

\deg \Delta \le 24.

In F-theory language these degree bounds are the Calabi--Yau condition for an elliptic fibration over $\mathbb{P}^1$ , and $\deg\Delta = 24$ counts the 7-branes (equal to $\chi(\mathrm{K3})$ ). The bound $\deg\Delta \le 24$ is the algebraic content of that count; the extremal value is attained in the generic K3 case.

Formalization Note. Degrees use natDegree, so the zero polynomial has degree $0$ and the inequality holds trivially if $\Delta = 0$ .

Preamble

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

Formal statement

namespace FTheoryK3
theorem discriminant_natDegree_le
    (f g : k[X]) (hf : f.natDegree ≤ 8) (hg : g.natDegree ≤ 12) :
    (Δ f g).natDegree ≤ 24 := 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. For 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 if $4f^3+27g^2$ is the zero polynomial its degree is $0$ , trivially satisfying the bound). No characteristic assumption is imposed, so $4, 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

24 seven-branes: deg⁡Δ≤24\deg\Delta \le 24degΔ≤24

24 seven-branes: $\deg\Delta \le 24$