eta_eq_one
plain-language theorem explainer
The slow-roll parameter η for the J-cost inflaton potential equals one for every real value of the logarithmic time coordinate. Inflation modelers using Recognition Science would cite this when linking the composition law to α-attractor predictions. The proof is a direct algebraic simplification from the definition of η as the ratio of coshines.
Claim. For the potential $G(t) = cosh(t) - 1$, the second slow-roll parameter defined by $η(t) := G''(t) / (G(t) + 1)$ satisfies $η(t) = 1$ for all real $t$.
background
The module shows that the Recognition Composition Law forces the inflaton potential to take the form J(x) = ½(x + x⁻¹) − 1. In logarithmic coordinates t = ln(x) this becomes G(t) = cosh(t) − 1, with minimum G(0) = 0 and curvature G''(0) = 1. The slow-roll parameters are then extracted from the derivatives of G: ε involves (G')² normalized by G(G+1), while η is the ratio of the second derivative to the normalized potential value G+1.
proof idea
The proof unfolds the definition of slow_roll_eta, which is the ratio cosh(t)/cosh(t), then applies div_self to the nonzero denominator supplied by the positivity of cosh.
why it matters
This identity places the J-cost potential exactly at the self-similar fixed point required for slow-roll inflation. It supports the master certificate InflationFromJCostCert and the derivation of the spectral index 1 − 2/N from curvature. In the framework it realizes the J-uniqueness step and the phi fixed point inside the inflationary sector, with the eight-tick octave supplying the discrete calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.