nsRS
RS spectral index is defined as 1 - 2/gap45 with gap45 the effective e-fold gap parameter. Cosmologists testing Recognition Science inflation against Planck CMB data cite this expression for the predicted n_s near 0.956. The declaration is a direct definition that encodes the gap-45 formula without reduction steps.
claim$n_s = 1 - 2 / g$ where $g$ denotes the Recognition Science gap parameter fixed at 45 e-folds.
background
The module InflationSpectralIndexFromJCost develops the scalar spectral index in Recognition Science cosmology. It begins from Planck 2018 data n_s = 0.965 ± 0.004 and adopts the RS form n_s = 1 - 2/gap45, where gap45 arises as N_e = gap(3) + δ = 45 + corrections. gap45 is the discrete gap on the phi-ladder consistent with the eight-tick octave of the forcing chain.
proof idea
The declaration is a direct definition. It assigns the real value 1 - 2/gap45 to nsRS with no lemmas or tactics applied.
why it matters in Recognition Science
This definition supplies the core RS spectral index expression used by nsRS_val, nsRS_band, nsRS_near_planck and SpectralIndexCert. It realizes the RS-Starobinsky formula n_s = 1 - 2/gap45 ∈ (0.955, 0.957) stated in the module documentation and links to the J-cost and gap structure in the UnifiedForcingChain. It leaves open a derivation of the exact gap45 value strictly from the Recognition Composition Law.
scope and limits
- Does not derive gap45 from the J-cost or Recognition Composition Law.
- Does not compute higher-order slow-roll corrections to the index.
- Does not predict the tensor-to-scalar ratio.
- Does not perform full statistical fit to Planck likelihoods.
Lean usage
theorem example : nsRS < 1 := by unfold nsRS gap45; norm_numformal statement (Lean)
35noncomputable def nsRS : ℝ := 1 - 2 / (gap45 : ℝ)
proof body
Definition body.
36