nsRS_band
plain-language theorem explainer
The theorem pins the Recognition Science spectral index strictly inside (0.955, 0.957). Cosmologists comparing RS inflation to Planck 2018 CMB data would cite this interval when checking consistency with the observed n_s ≈ 0.965. The proof is a one-line wrapper that unfolds the closed-form value of nsRS and applies numerical normalization.
Claim. $0.955 < n_s^{RS} < 0.957$ where $n_s^{RS} := 1 - 2/45$.
background
In the Inflation Spectral Index from J-Cost module the RS spectral index is introduced as the noncomputable definition nsRS := 1 - 2/gap45. The upstream theorem nsRS_val proves the concrete equality nsRS = 1 - 2/45, which follows from the gap-45 slow-roll parameter in the RS-Starobinsky picture. The module setting derives this from the phi-ladder gap structure, yielding a prediction 1 - 2/45 ≈ 0.956 that sits inside the Planck band 0.965 ± 0.004.
proof idea
The proof is a one-line wrapper: it rewrites by the equality nsRS_val and then invokes norm_num to discharge the two strict inequalities on the resulting rational.
why it matters
The bound is consumed directly by the SpectralIndexCert structure (and its constructor spectralIndexCert), which packages both the band and the near-Planck distance |nsRS - nsPlanck| < 0.015. It supplies the concrete numerical anchor for the RS inflation claim inside the A2 cosmology depth, linking the gap-45 rung to the observed spectral tilt without invoking extra slow-roll parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.