inflatonCert
plain-language theorem explainer
inflatonCert assembles a concrete certificate that the RS inflaton potential exhibits exactly five regimes, 44 e-folds, the phi^5 = 5 phi + 3 identity, positive slow-roll parameters, and spectral index inside the 0.955-0.957 window. Cosmologists using Recognition Science would cite it to confirm structural consistency of the inflaton model with the phi-ladder before computing observables. The definition is a direct bundling of six pre-established component theorems from the same module.
Claim. Let phi denote the golden ratio. The certificate inflatonCert satisfies: the inflaton potential has five regimes, the e-fold count equals 44, phi^5 = 5 phi + 3, the slow-roll parameter epsilon is positive, eta is positive, and 0.955 < 1 - 2/45 < 0.957.
background
The module treats the RS inflaton potential V(chi) as having five structural regimes (slow-roll plateau, slope, hilltop decline, reheating, post-reheating radiation) fixed by configDim D = 5. Slow-roll parameters are given by epsilon = 1/(2 phi^5) and eta = 1/phi^5, with N_e = 44 and n_s - 1 = -2/45. Upstream theorem phi5_eq proves phi^5 = 5 phi + 3 by nlinarith from the quadratic relation phi^2 = phi + 1; inflatonRegime_count proves the regime count equals 5 by decide; efoldCount_eq fixes the e-fold count at 44.
proof idea
The definition is a direct record that populates each field of the InflatonCert structure by referencing the corresponding theorem: inflatonRegime_count supplies the regime cardinality, efoldCount_eq supplies the e-fold number, phi5_eq supplies the Fibonacci identity, slowRollEpsilon_pos and slowRollEta_pos supply positivity, and spectralIndex_band supplies the index interval.
why it matters
This certificate consolidates the structural properties of the inflaton potential required by the Recognition Science forcing chain, in particular the phi-ladder relations and slow-roll conditions that follow from T5 J-uniqueness and T6 phi fixed point. It provides a verified bundle that downstream cosmological calculations can reference without re-deriving the component equalities. No immediate parent theorem appears in the used-by list, leaving open the question of its integration into a full Hubble-tension pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.