spectral_index_60efolds
plain-language theorem explainer
The result fixes the RS spectral index at exactly 1 minus 1/30 when the number of e-foldings is set to 60, yielding the approximate value 0.967 used for the primordial tilt. Cosmologists matching inflationary spectra to BAO data or CMB constraints would cite this numerical instance. The proof is a direct substitution into the defining formula followed by arithmetic normalization.
Claim. In the Recognition Science framework the spectral index for sixty e-foldings satisfies $n_s = 1 - 1/30$.
background
The BAO module derives the sound horizon and related observables from an RS-predicted primordial spectrum. The spectral index is introduced via the upstream definition rs_spectral_index(N_e) := 1 - 2/N_e, which encodes the slow-roll tilt for N_e e-foldings. The module doc states that this supplies n_s ≈ 0.967 for use in baryon loading and sound-speed integrals.
proof idea
The term proof unfolds the definition of rs_spectral_index and applies norm_num to reduce the arithmetic expression 1 - 2/60 to the fraction 1 - 1/30.
why it matters
This supplies the concrete numerical value of the spectral index required by the BAO sound-horizon and baryon-loading calculations in the same module. It instantiates the general RS inflation formula at the conventional N_e = 60 point, closing the link between the primordial spectrum and observable BAO parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.