rs_spectral_index
plain-language theorem explainer
The RS spectral index is defined as n_s = 1 - 2/N_e for N_e e-foldings in slow-roll inflation. Cosmologists deriving BAO sound horizons and CMB power spectra from Recognition Science parameters cite this when fixing the red tilt at N_e ≈ 60. The declaration is a direct algebraic definition with no lemmas or tactics required.
Claim. The spectral index is defined by the formula $n_s(N_e) = 1 - 2/N_e$, where $N_e$ is the number of e-foldings during inflation.
background
The BAO module computes the sound horizon r_s ≈ 147 Mpc from RS cosmological parameters, including baryon density, matter density, and the primordial spectral index. It lists the sound speed formula c_s = c/√(3(1+R)) and the integral r_s = ∫ c_s dz/H(z) as core results, with the spectral index supplied as n_s ≈ 0.967 from RS inflation. The module imports JcostCore but this definition stands independently as the slow-roll approximation.
proof idea
The declaration is a one-line definition that directly encodes the expression 1 - 2/N_e. Downstream theorems apply it by unfolding the definition and invoking norm_num for the numerical case or linarith for the inequality.
why it matters
This definition supplies the spectral index used in spectral_index_60efolds to obtain n_s = 1 - 1/30 for 60 e-foldings and in spectral_index_red_tilt to prove n_s < 1. It fills the spectral_index entry among the module's key results and supports the BAO sound horizon derivation in RS_Baryon_Acoustic_Oscillations.tex. In the framework it aligns with the T7 eight-tick octave by providing the tilt consistent with the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.