InflatonRegime
plain-language theorem explainer
InflatonRegime enumerates the five structural phases of the RS inflaton potential: slow-roll plateau, slow-roll slope, hilltop decline, reheating, and radiation era. Cosmologists working within Recognition Science cite it to certify that the potential's configuration dimension equals five. The declaration is an inductive definition deriving Fintype, which immediately enables the cardinality result used in the certification structure.
Claim. The inflaton potential $V(χ)$ admits five structural regimes: slow-roll plateau, slow-roll slope, hilltop decline, reheating, and radiation-dominated era.
background
The module states that the RS inflaton potential has five canonical regimes (= configDim D = 5). Slow-roll parameters are ε = 1/(2φ⁵), η = 1/φ⁵, with spectral index n_s - 1 = -2/45 and tensor-to-scalar ratio r = 2/(45 φ²). The e-fold count is fixed at N = 44 (gap-45 ladder minus one reheating transit tick).
proof idea
Inductive definition introducing five constructors and deriving DecidableEq, Repr, BEq, Fintype. No tactics or lemmas are applied; the Fintype instance directly supports the downstream cardinality theorem.
why it matters
This supplies the enumeration required by the InflatonCert structure, whose five_regimes field asserts Fintype.card InflatonRegime = 5 together with efolds = 44 and positivity of the slow-roll parameters. It realizes the configDim D = 5 step inside the cosmology module and connects to the phi-ladder and eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.