efoldCount_eq
plain-language theorem explainer
The equality fixes the e-fold count at 44 in the Recognition Science inflaton model. Cosmologists using the RS framework cite it to confirm the duration of the slow-roll phase before reheating. The proof is a direct reflexivity reduction to the upstream definition of the e-fold count.
Claim. The e-fold count satisfies $N_e = 44$, where $N_e$ is the number of e-folds on the gap-45 ladder minus one tick for reheating transit.
background
The module treats the RS inflaton potential with five structural regimes (configDim D=5): slow-roll plateau, slope, hilltop decline, reheating, and post-reheating radiation. Slow-roll parameters are stated as ε = 1/(2φ⁵) and η = 1/φ⁵, with the e-fold count fixed at 44. The upstream definition states: e-fold count N_e = 44 (gap-45 ladder).
proof idea
The proof is a one-line term that applies reflexivity to the definition of efoldCount.
why it matters
This supplies the efolds field to the InflatonCert structure, which also records the five regimes, phi5 relation, and positivity of the slow-roll parameters. It completes the structural count required by the inflaton potential analysis. The value 44 aligns with the gap-45 step on the phi-ladder adjusted for reheating transit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.