Milestone 2 — local orders bounded by $\deg\Delta$

Proved

FTheoryK3Tate.sum_rootMultiplicity_discriminant_le

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

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Let $k$ be a field, $f, g \in k[X]$ with $\Delta = 4f^3 + 27g^2 \ne 0$ . For every finite set $S \subseteq k$ of base points, $\sum_{t_0 \in S} \operatorname{ord}_{t_0}(\Delta) \le \deg \Delta$ : the degenerate fibres over $S$ , counted with multiplicity, are bounded by the degree of the discriminant. Points of $S$ that are not roots contribute $0$ ; the elements of the Finset $S$ are distinct.

Preamble

import Definitions.Def_FTheoryK3TateCore
open Polynomial

Formal statement

namespace FTheoryK3Tate
variable {k : Type*} [Field k]
/-- Milestone (local orders bounded by the discriminant degree). For `Δ ≠ 0` and any finite
    set `S` of base points, the discriminant orders at the points of `S`, summed with
    multiplicity, are bounded by `deg Δ`. -/
theorem sum_rootMultiplicity_discriminant_le (f g : k[X]) (h : Δ f g ≠ 0) (S : Finset k) :
    (∑ t₀ ∈ S, (Δ f g).rootMultiplicity t₀) ≤ (Δ f g).natDegree := 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$ , all $f, g \in k[X]$ , assuming $4f^3+27g^2 \ne 0$ , and for every finite set $S \subseteq k$ of distinct elements: $\sum_{t_0 \in S} \operatorname{rootMultiplicity}_{t_0}(4f^3+27g^2) \le \operatorname{natDegree}(4f^3+27g^2)$ . Both sides are natural numbers; the inequality is non-strict. Elements of $S$ that are not roots contribute $0$ ; the empty set gives $0 \le \deg\Delta$ . The hypothesis $\Delta \ne 0$ is what makes the degree a meaningful bound. No characteristic assumption.

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 2 — local orders bounded by deg⁡Δ\deg\DeltadegΔ

Milestone 2 — local orders bounded by $\deg\Delta$