InflationaryCosm
InflationaryCosm packages the claim that exactly five inflation models exist in the RS framework together with the fixed e-fold count of 44. Cosmologists tracing predictions from the J-cost function to observable cosmology would cite this record when confirming the model enumeration matches configDim D=5. The structure is realized directly by the Fintype cardinality of the local inductive type and the constant definition of Nefolds.
claimThe structure InflationaryCosm asserts that the set of inflation models has cardinality five and that the e-fold number satisfies $N_e=44$.
background
The module defines InflationModel as an inductive type with five constructors (starobinsky, natural, higgs, chaotic, axionMonodromy) that carries a Fintype instance. Nefolds is the constant natural number 44, identified with the baryon-rung e-fold count. The module documentation states that these five models correspond to configuration dimension D=5 and that the Lean development contains zero sorries. Upstream results supply analogous inductive enumerations in CosmicInflationFromJCost and InflationModelsFromConfigDim, both of which also fix five models.
proof idea
The declaration is a bare structure definition whose fields are filled by the Fintype.card of the sibling inductive type InflationModel and by the direct constant definition of Nefolds. No tactics or lemmas are applied; the record simply records the two equalities.
why it matters in Recognition Science
The structure supplies the data consumed by the downstream certificate inflationaryCosmCert, which builds an instance via inflationModelCount and reflexivity. It records the concrete link between the five-model enumeration (tied to D=5) and the e-fold value 44 that appears in the RS forcing chain and phi-ladder constructions. The module documentation explicitly connects the model count to the five canonical potentials derived from the Recognition Composition Law.
scope and limits
- Does not derive the numerical value 44 from the J-cost equation.
- Does not establish slow-roll parameters or spectral indices for any model.
- Does not prove dynamical stability or attractor behavior.
- Does not address the relation to the fine-structure constant band.
Lean usage
def cert : InflationaryCosm := inflationaryCosmCertformal statement (Lean)
33structure InflationaryCosm where
34 five_models : Fintype.card InflationModel = 5
35 Nefolds_eq : Nefolds = 44
36