inflatonRegime_count
plain-language theorem explainer
The theorem establishes that the inductive type enumerating the structural regimes of the RS inflaton potential contains exactly five elements. Cosmologists assembling the inflatonCert object in the Recognition Science framework would cite this cardinality when confirming the completeness of the potential's phase structure. The proof is a one-line decision procedure that evaluates the Fintype instance derived from the five-constructor inductive definition.
Claim. The set of canonical structural regimes for the RS inflaton potential has cardinality five, consisting of the slow-roll plateau, the slow-roll slope, the hilltop decline, reheating, and the radiation era.
background
The Inflaton Potential Structural module partitions the RS inflaton potential V(χ) into five regimes that realize configDim D = 5. These regimes are the constructors of the inductive type with cases slow-roll plateau, slow-roll slope, hilltop decline, reheating, and radiation era; the module also records the slow-roll parameters ε = 1/(2φ⁵), η = 1/φ⁵ and the e-fold count N_e = 44 drawn from the gap-45 ladder. Upstream results supply the gap function as the logarithmic residue F(Z) = ln(1 + Z/φ) / ln(φ) at the anchor scale, which fixes the gap-45 derivation used for the e-fold count.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card expression. The tactic succeeds because the inductive type derives a Fintype instance directly from its five constructors, allowing the decision procedure to compute the cardinality as 5 without further lemmas.
why it matters
This result supplies the five_regimes field of the inflatonCert definition, which collects the complete certification of the inflaton potential including e-folds, phi5 equality, and positivity of the slow-roll parameters. It realizes the structural claim in the module documentation that the potential has five regimes tied to the gap-45 ladder. Within the Recognition Science framework it extends the forcing chain to cosmological scales while preserving the phi-ladder mass formula and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.