efoldCount
plain-language theorem explainer
The declaration fixes the e-fold count N_e at 44 on the gap-45 ladder for the Recognition Science inflaton model. Cosmologists working inside the RS framework cite this constant when verifying slow-roll observables or building the InflatonCert structure. It is supplied as a bare definition with no lemmas or computational steps.
Claim. The e-fold count is defined by $N_e := 44$.
background
The Inflaton Potential Structural module organizes the RS inflaton potential V(χ) into five canonical regimes (configDim D = 5): slow-roll plateau, slow-roll slope, hilltop decline, reheating, and post-reheating radiation. Slow-roll parameters are stated as ε = 1/(2φ⁵), η = 1/φ⁵, with n_s - 1 = -2/45 and r = 2/(45 φ²). The module documentation fixes the e-fold count at 44, obtained as gap-45 minus one tick for reheating transit.
proof idea
This is a direct definition that assigns the natural number 44 with no lemmas or tactics.
why it matters
The definition supplies the efolds field required by the InflatonCert structure, which certifies the five-regime potential together with the slow-roll parameters. It implements the N_e = 44 slot stated in the module documentation for the gap-45 ladder, supporting downstream calculations of spectral index and tensor ratio inside the Recognition Science cosmology setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.