card_IVstar_le_three
ProvedFTheoryK3Tate.card_IVstar_le_threealgebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics
On a characteristic-zero K3-degree model, the set of type () points is finite and has at most three elements: each contributes to the discriminant budget and .
Preamble
import Definitions.Def_FTheoryK3TateCore open Polynomial
Formal statement
namespace FTheoryK3Tate
variable {k : Type*} [Field k] [CharZero k]
/-- Corollary (`E6` cap). On a Calabi–Yau/K3 model the set of type IV\* (`E6`) points is finite
and has at most three elements — each contributes `8` to the discriminant budget and
`4 × 8 = 32 > 24`. -/
theorem card_IVstar_le_three (f g : k[X]) (h : IsK3Data f g) :
{t₀ : k | HasKodaira f g t₀ Kodaira.IVstar}.Finite ∧
Nat.card {t₀ : k | HasKodaira f g t₀ Kodaira.IVstar} ≤ 3 := 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
Confirmed by the mission captain (proposal self-audit).