InflatonRegime
The inductive definition enumerates the five structural regimes of the RS inflaton potential V(χ). Cosmologists working with the phi-ladder potential cite it when decomposing the potential into configDim D=5 components. The definition is a direct inductive enumeration that immediately yields Fintype, DecidableEq, and Repr instances.
claimThe inductive type enumerating the five regimes of the inflaton potential is defined by the constructors slow-roll plateau, slow-roll slope, hilltop decline, reheating, and radiation era.
background
In the Recognition Science cosmology module the inflaton potential V(χ) is decomposed into five canonical structural regimes corresponding to configDim D=5. The regimes are slow-roll plateau, slow-roll slope, hilltop decline, reheating, and post-reheating radiation era. The module states the slow-roll parameters ε = 1/(2φ⁵), η = 1/φ⁵ together with n_s − 1 = −2/45 and r = 2/(45 φ²), and fixes the e-fold count at N_e = 44 (gap-45 ladder minus one reheating tick).
proof idea
The declaration is an inductive definition that lists the five regimes explicitly. No lemmas or tactics are invoked; the finite enumeration directly supplies the Fintype instance used downstream.
why it matters in Recognition Science
This definition supplies the five_regimes field of the InflatonCert structure, which also records efolds = 44 and the positivity of the slow-roll parameters. It fills the configDim D=5 slot in the Recognition Science inflaton decomposition, supporting the spectral index band and tensor-to-scalar ratio derivations that sit inside the alpha band. No open scaffolding remains in the module.
scope and limits
- Does not supply the explicit functional form of V(χ).
- Does not derive the slow-roll parameters ε and η.
- Does not compute the e-fold count or spectral observables.
- Does not link to the spatial dimension D=3 from the forcing chain.
formal statement (Lean)
23inductive InflatonRegime where
24 | slowRollPlateau
25 | slowRollSlope
26 | hilltopDecline
27 | reheating
28 | radiationEra
29 deriving DecidableEq, Repr, BEq, Fintype
30