InflationModel
plain-language theorem explainer
InflationModel enumerates the five canonical inflation scenarios in the Recognition Science cosmology setting. Cosmologists working with J-cost dynamics for the inflaton would cite it to fix the model count at configDim = 5. The declaration is introduced directly as an inductive type carrying five named constructors together with derived instances for decidable equality and finite cardinality.
Claim. The set of canonical inflation models is the five-element collection consisting of chaotic inflation, natural inflation, Starobinsky inflation, Higgs inflation, and axion monodromy inflation.
background
In the Cosmic Inflation from J-Cost module the inflaton field follows the same J-cost dynamics as any recognition ratio. When the field value greatly exceeds one the associated J-cost is large and drives slow-roll inflation; as the field approaches one the J-cost vanishes and inflation ends. The module equates the five canonical models with configuration dimension D = 5 and states that reheating occurs at the canonical J-threshold of zero.
proof idea
The declaration is a direct inductive definition that introduces five constructors for the listed models and derives the instances DecidableEq, Repr, BEq and Fintype automatically.
why it matters
The type supplies the model enumeration required by CosmicInflationCert, whose fields include the cardinality statement Fintype.card InflationModel = 5 together with the reheating condition J(1) = 0. It thereby anchors the Recognition Science claim that the number of viable inflation models equals the configuration dimension five, consistent with the J-cost forcing chain and the phi-ladder structure. The same enumeration is referenced by the downstream InflationaryCosm structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.