card_IIIstar_le_two
ProvedFTheoryK3Tate.card_IIIstar_le_twoalgebraic-geometryelliptic-curveselliptic-surfacesf-theorymathematical-physics
On a characteristic-zero K3-degree model, the set of type () points is finite and has at most two elements: each contributes and .
Preamble
import Definitions.Def_FTheoryK3TateCore open Polynomial
Formal statement
namespace FTheoryK3Tate
variable {k : Type*} [Field k] [CharZero k]
/-- Corollary (`E7` cap). On a Calabi–Yau/K3 model the set of type III\* (`E7`) points is finite
and has at most two elements — each contributes `9` to the discriminant budget and
`3 × 9 = 27 > 24`. -/
theorem card_IIIstar_le_two (f g : k[X]) (h : IsK3Data f g) :
{t₀ : k | HasKodaira f g t₀ Kodaira.IIIstar}.Finite ∧
Nat.card {t₀ : k | HasKodaira f g t₀ Kodaira.IIIstar} ≤ 2 := 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).