InflatonCert
plain-language theorem explainer
InflatonCert packages the structural properties of the RS inflaton potential: five regimes from the configDim D=5 space, exactly 44 e-folds, the Fibonacci identity phi^5 = 5 phi + 3, positivity of the slow-roll parameters epsilon and eta, and the spectral index 1-2/45 inside the observed interval (0.955, 0.957). Cosmologists in the Recognition Science track cite it to certify consistency between the phi-ladder potential and CMB data. The declaration is realized as a plain structure definition whose fields record module constants and positivity.
Claim. The structure asserts that the inflaton potential admits five regimes, the e-fold count equals 44, $phi^5 = 5 phi + 3$, the first slow-roll parameter $epsilon > 0$, the second $eta > 0$, and $0.955 < 1 - 2/45 < 0.957$.
background
The module states that the RS inflaton potential V(chi) has five canonical structural regimes (= configDim D=5): slow-roll plateau, slow-roll slope, hilltop decline, reheating, and post-reheating radiation era. Slow-roll parameters are given by epsilon = 1/(2 phi^5) and eta = 1/phi^5, with n_s - 1 = -2/45 and N_e-fold count = 44 (gap-45 ladder minus one tick). The inductive type InflatonRegime enumerates exactly these five cases and derives Fintype. Upstream, slowRollEpsilon and slowRollEta in the Inflation module define the general expressions (V'/V)^2/2 and V''/V from the potential V = (phi + 1/phi)/2 - 1; the local versions specialize them to the phi^5 form.
proof idea
The declaration is a structure definition. Its fields directly invoke the Fintype.card instance on InflatonRegime, the constant efoldCount, the phi5_fibonacci lemma from NumberTheoryFromRS, and the positivity statements slowRollEpsilon_pos and slowRollEta_pos already proved in the same module.
why it matters
InflatonCert supplies the certificate consumed by the downstream inflatonCert definition. It encodes the A2-depth claims of five regimes matching configDim D=5, 44 e-folds, and the spectral index inside the observed band, while the phi^5 = 5 phi + 3 identity closes the Fibonacci relation required by the phi-ladder. The construction sits between the slow-roll parameter definitions and the final inflatonCert object; it touches the T5 J-uniqueness and T6 phi fixed-point steps via the Fibonacci identity but does not itself derive the potential from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.