IndisputableMonolith.Cosmology.InflationModelsFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Inflation Models from configDim — A2 Depth
   6
   7Five canonical inflaton-potential families (= configDim D = 5):
   8  chaotic (m²φ²), new inflation (plateau), hybrid, natural (axion-like),
   9  alpha-attractor (conformal).
  10
  11Each has a distinct slow-roll prediction for n_s and r.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Cosmology.InflationModelsFromConfigDim
  17
  18inductive InflationModel where
  19  | chaoticQuadratic
  20  | newInflationPlateau
  21  | hybrid
  22  | naturalAxionLike
  23  | alphaAttractor
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem inflationModel_count : Fintype.card InflationModel = 5 := by decide
  27
  28structure InflationModelsCert where
  29  five_models : Fintype.card InflationModel = 5
  30
  31def inflationModelsCert : InflationModelsCert where
  32  five_models := inflationModel_count
  33
  34end IndisputableMonolith.Cosmology.InflationModelsFromConfigDim
  35