nsPlanck
nsPlanck supplies the central value 0.965 for the scalar spectral index reported by Planck 2018. Cosmologists testing Recognition Science against CMB data cite it to bound the distance between the framework prediction nsRS and observation. The declaration is a direct constant assignment with no computation or lemmas.
claimThe Planck 2018 central value of the scalar spectral index is given by $n_s = 0.965$.
background
The module Inflation Spectral Index from J-Cost derives the RS prediction for the scalar spectral index from the J-cost slow-roll parameters on the phi-ladder. It states that n_s equals 1 minus 2 over gap45, where gap45 is the 45-rung gap that yields n_s approximately 0.956. The module contrasts this interval (0.955, 0.957) with the Planck 2018 observation n_s = 0.965 plus or minus 0.004.
proof idea
Direct constant definition. The body is the literal real number 0.965 with no tactics or upstream lemmas applied.
why it matters in Recognition Science
The definition anchors the comparison theorems nsRS_near_planck and the SpectralIndexCert structure that certify both the RS band and proximity to observation. It supplies the observational anchor for the cosmology section that links the J-cost functional equation to inflation parameters via the gap construction on the phi-ladder.
scope and limits
- Does not derive the numerical value from Recognition Science axioms or the J-cost equation.
- Does not include measurement error bars or uncertainty intervals.
- Does not specify the rung or gap parameter underlying the RS prediction.
- Does not address higher-order slow-roll corrections beyond the leading 1 minus 2 over gap45 term.
Lean usage
theorem nsRS_near_planck : |nsRS - nsPlanck| < 0.015 := by rw [nsRS_val]; unfold nsPlanck; rw [abs_lt]; constructor <;> norm_numformal statement (Lean)
51def nsPlanck : ℝ := 0.965