nsRS_near_planck
plain-language theorem explainer
The theorem establishes that the Recognition Science spectral index differs from the Planck 2018 measurement by less than 0.015. Cosmologists comparing alternative inflation models to CMB data would cite this bound for consistency checks. The proof is a short term-mode reduction that substitutes the explicit RS value, unfolds the Planck constant, splits the absolute-value inequality, and discharges both sides by numerical normalization.
Claim. Let $n_s^{RS} = 1 - 2/45$ be the Recognition Science spectral index and let $n_s^{Planck} = 0.965$ be the Planck observed value. Then $|n_s^{RS} - n_s^{Planck}| < 0.015$.
background
In the Inflation Spectral Index from J-Cost module the Recognition Science framework predicts the CMB spectral index from the gap-45 rung on the phi-ladder: $n_s = 1 - 2/45$. The upstream definition nsRS sets this expression directly, while nsPlanck records the observed central value 0.965. The supporting theorem nsRS_val proves that the RS index equals exactly 1 - 2/45 after casting gap45 to reals. The module context is to formalize that the RS-Starobinsky formula lies inside the Planck 2018 error band (0.965 ± 0.004) and inside the tighter interval (0.955, 0.957).
proof idea
The term proof first rewrites with the valuation theorem nsRS_val to replace nsRS by its explicit form 1 - 2/45. It then unfolds the definition of nsPlanck to the literal constant 0.965. The absolute-value inequality is rewritten via the abs_lt lemma, which produces two one-sided bounds. Both bounds are discharged by the norm_num tactic performing exact rational comparison.
why it matters
The result supplies the proximity field required by the SpectralIndexCert structure, which bundles this bound together with the band membership nsRS_band. It therefore closes the formal link between the gap-45 step in the forcing chain and the observed CMB spectral index. In the Recognition Science framework the theorem supports the claim that the J-cost slow-roll parameter at rung 45 reproduces the Planck central value within the reported uncertainty, consistent with the eight-tick octave and the D = 3 spatial dimensions derived from the same chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.