inflationModelCount
plain-language theorem explainer
The declaration proves that the inductive type InflationModel has cardinality exactly five. Cosmologists working in the Recognition Science framework cite it to confirm that the count of canonical models matches the configuration dimension. The proof is a one-line decision procedure that exhausts the finite enumeration of the five constructors.
Claim. The cardinality of the set of canonical inflation models is five: $|$ {chaotic, natural, Starobinsky, Higgs inflation, axion monodromy} $| = 5$.
background
The Cosmic Inflation from J-Cost module treats the inflaton field as obeying the same J-cost dynamics as any recognition ratio. The inductive type InflationModel lists five constructors: chaotic, natural, starobinsky, higgsInflation, axionMonodromy. The module states that phi_inf >> 1 produces large J-cost during slow roll while phi_inf approaching 1 drives J-cost to zero at reheating, with the model count asserted equal to configDim D = 5.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the inductive definition derives Fintype and the five constructors are explicitly enumerated.
why it matters
This supplies the five_models component to cosmicInflationCert and inflationaryCosmCert. It realizes the RS prediction that the number of canonical inflation models equals configDim D = 5, consistent with the forcing chain landmarks including the eight-tick octave. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.