n_s_55_in_planck_band
plain-language theorem explainer
The spectral index at 55 e-folds satisfies 0.96 < n_s < 0.97, placing the J-cost inflaton inside the Planck 2018 window. Cosmologists matching alpha-attractor models to CMB data would cite this bound when testing Recognition Science against observations. The proof is a one-line wrapper that invokes the upstream n_s_at_55 theorem.
Claim. $0.96 < n_s(55) < 0.97$, where $n_s(N) := 1 - 2/N$ is the slow-roll spectral index obtained from the curvature of the J-cost potential $G(t) = J(e^t) = cosh(t) - 1$.
background
The JCostInflaton module shows that the Recognition Composition Law forces the inflaton potential to be the J-cost function. In logarithmic coordinates t = ln(x) the potential becomes G(t) = cosh(t) - 1, a Starobinsky-style plateau with G(0) = 0, G'(0) = 0 and G''(0) = 1. The spectral index is defined by the upstream result spectral_index N := 1 - 2/N, the standard slow-roll formula for this potential shape.
proof idea
The proof is the term n_s_at_55, a one-line wrapper that applies the theorem n_s_at_55 from the Inflation module. That upstream theorem unfolds the spectral_index definition and discharges the numerical bounds by norm_num.
why it matters
This result confirms that the J-cost-derived spectral index at N = 55 lies inside the Planck 2018 band, supporting the module's main claims such as n_s_from_jcost and InflationFromJCostCert. It closes the loop from T5 J-uniqueness through the phi fixed point to the observed CMB tilt, with the eight-tick octave structure implicit in the slow-roll parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.