n_s_at_55
plain-language theorem explainer
The theorem establishes that the spectral index at 55 e-foldings satisfies 0.96 < n_s < 0.97. Cosmologists comparing Recognition Science inflation to Planck CMB data would cite this bound when checking consistency with observations. The proof is a term-mode wrapper that unfolds the spectral index definition and discharges the numerical inequalities by direct computation.
Claim. For $N=55$, the spectral index satisfies $0.96 < 1 - 2/55 < 0.97$.
background
The Gravity.Inflation module formalizes RS inflationary predictions from the phi-based α-attractor, where α = φ² follows from cost-functional self-similarity. The spectral index is defined directly as spectral_index(N) := 1 - 2/N, the standard slow-roll result. Module documentation states: 'Spectral index: n_s ≈ 1 - 2/N (standard slow-roll result).' and 'Tensor-to-scalar ratio: r ≈ 12φ²/N² (RS-specific).'
proof idea
The proof is a term-mode wrapper. It unfolds the spectral_index definition to expose 1 - 2/55, splits the conjunction via constructor, and applies norm_num to verify both sides of the inequality by arithmetic reduction.
why it matters
This supplies the spectral_ok field in inflation_cert and is reused verbatim in n_s_55_in_planck_band and n_s_at_55_from_jcost to confirm the Planck 2018 band. It also appears in baryogenesis_cert. The result fills the N=55 case in the parameter-free predictions forced by J-cost uniqueness (T5), the phi fixed point (T6), and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.