residual_budget

Proved

FTheoryK3Tate.residual_budget

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

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Residual budget. For a characteristic-zero K3-degree model, a finite set $E$ of $E_8$ (type $\mathrm{II}^*$ ) points, and a finite set $S$ disjoint from $E$ , $10|E| + \sum_{t \in S}\operatorname{ord}_t\Delta \le 24$ . In particular two $E_8$ points leave at most $4$ for the remaining fibres. Stated additively to avoid truncated subtraction.

Preamble

import Definitions.Def_FTheoryK3TateCore
open Polynomial

Formal statement

namespace FTheoryK3Tate
variable {k : Type*} [Field k] [CharZero k]
/-- Corollary (residual budget). Fix a finite set `E` of `E₈` (type II*) points and a finite set
    `S` of further base points disjoint from `E`. Each `E₈` point uses `10` of the discriminant
    budget, so
    `10 * |E| + ∑_{t ∈ S} ord_t Δ ≤ 24`.
    In particular, two `E₈` points leave at most `4` for the remaining fibres. Stated additively
    to avoid truncated natural-number subtraction. -/
theorem residual_budget (f g : k[X]) (h : IsK3Data f g)
    (E S : Finset k) (hE : ∀ t ∈ E, IsE8Point f g t) (hd : Disjoint E S) :
    10 * E.card + ∑ t ∈ S, (Δ f g).rootMultiplicity t ≤ 24 := by
  sorry
end FTheoryK3Tate

Source

Kodaira/Tate classification of singular fibres: J. Tate (LNM 476, 1975); M. Schuett, T. Shioda, Elliptic Surfaces, arXiv:0907.0298; F-theory dictionary: T. Weigand, TASI Lectures on F-theory, arXiv:1806.01854.

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