Branes with multiplicity are bounded by $\deg\Delta$

Proved

FTheoryK3.sum_rootMultiplicity_discriminant_le

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

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Let $k$ be a field and $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 left-hand side counts, with multiplicity, the degenerate fibres (7-branes) at the points of $S$ ; the inequality says the total brane charge over any finite collection of points is bounded by the degree of the discriminant. Points of $S$ that are not roots of $\Delta$ contribute $0$ .

Formalization Note. The hypothesis $\Delta \ne 0$ is needed for $\deg\Delta$ (natDegree) to be a meaningful bound; the sum ranges over a Finset, whose elements are distinct.

Preamble

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

Formal statement

namespace FTheoryK3
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 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]$ , assuming $4f^3+27g^2 \ne 0$ , and for every finite set $S \subseteq k$ (a Finset), $\sum_{t_0 \in S} \operatorname{ord}_{t_0}(4f^3+27g^2) \le \deg(4f^3+27g^2)$ . Terms where $t_0$ is not a root contribute $0$ . The nonvanishing hypothesis is what makes $\deg(4f^3+27g^2)$ meaningful as a bound. No characteristic assumption is imposed.

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

Branes with multiplicity are bounded by deg⁡Δ\deg\DeltadegΔ

Branes with multiplicity are bounded by $\deg\Delta$