nS_RS
plain-language theorem explainer
The declaration defines the RS spectral index as one minus two divided by the e-fold count. Cosmologists testing Recognition Science inflation predictions against Planck data would cite this expression for n_s. It is introduced by direct substitution of the constant N_e = 44.
Claim. $n_s = 1 - 2/N_e$ with $N_e = 44$.
background
In the module on inflation e-folds from gap-45 the RS framework sets the e-fold count during inflation to gap(3) - 1 = 44. Nefolds is the sibling definition that fixes this count as the natural number 44. The upstream result in InflationaryCosmologyFromRS likewise declares Nefolds as the e-fold count tied to the baryon rung.
proof idea
Direct definition that casts Nefolds to real numbers and performs the arithmetic 1 - 2 divided by that value.
why it matters
Supplies the concrete n_s value required by InflationEfoldCert to certify the interval (0.95, 0.96) and by nS_RS_val to prove equality with 1 - 2/44. This anchors the RS inflation prediction inside the T7 eight-tick octave and the phi-ladder mass formula, placing n_s near 0.9545 against the observed Planck band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.