budget_exceptional

Proved

FTheoryK3Tate.budget_exceptional

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

algebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics

Exceptional-fibre budget. For a characteristic-zero Weierstrass model with $\deg f \le 8$ , $\deg g \le 12$ , $\Delta \ne 0$ , and pairwise-disjoint finite sets $S_6, S_7, S_8$ of base points carrying Kodaira types $\mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$ respectively, $8|S_6| + 9|S_7| + 10|S_8| \le 24$ . Geometrically these are the $E_6, E_7, E_8$ loci.

Preamble

import Definitions.Def_FTheoryK3TateCore
open Polynomial

Formal statement

namespace FTheoryK3Tate
variable {k : Type*} [Field k] [CharZero k]
/-- Corollary (exceptional-fibre budget). For a Calabi–Yau/K3 model, given pairwise-disjoint
    finite sets `S6, S7, S8` of base points carrying types `IV*`, `III*`, `II*` respectively,
    the weighted count is bounded by the discriminant degree:
    `8·|S6| + 9·|S7| + 10·|S8| ≤ 24`. Geometrically these are the `E6`, `E7`, `E8` loci (in the
    split/geometric setting). -/
theorem budget_exceptional (f g : k[X]) (h : IsK3Data f g)
    (S6 S7 S8 : Finset k)
    (d67 : Disjoint S6 S7) (d68 : Disjoint S6 S8) (d78 : Disjoint S7 S8)
    (h6 : ∀ t ∈ S6, HasKodaira f g t Kodaira.IVstar)
    (h7 : ∀ t ∈ S7, HasKodaira f g t Kodaira.IIIstar)
    (h8 : ∀ t ∈ S8, HasKodaira f g t Kodaira.IIstar) :
    8 * S6.card + 9 * S7.card + 10 * S8.card ≤ 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