spectral_index
plain-language theorem explainer
The spectral index n_s is defined as 1 - 2/N for N e-foldings in slow-roll inflation. Cosmologists matching RS-derived primordial spectra to CMB data would cite this when evaluating tilt at N around 55. The declaration is a direct algebraic assignment reproducing the standard slow-roll formula without additional lemmas.
Claim. The spectral index as a function of the number of e-foldings is given by $n_s(N) = 1 - 2/N$.
background
The Inflation from phi module formalizes RS inflationary predictions in which the α-attractor parameter equals φ² from cost-functional self-similarity. The spectral index follows the standard slow-roll result n_s ≈ 1 - 2/N. Upstream structures supply tensor definitions in 4D spacetime and empirical program classes, but the present definition stands independently as the tilt expression.
proof idea
This is a direct definition that assigns the expression 1 - 2/N verbatim. No lemmas or tactics are invoked beyond the assignment itself.
why it matters
The definition supplies the spectral index required by the InflationCert structure and the n_s_at_55 theorem, which confirms the value at N = 55 lies in (0.96, 0.97). It feeds the PowerSpectrum and observedSpectrum constructions in the cosmology module. Within the framework it realizes the parameter-free slow-roll tilt consistent with the eight-tick octave and φ-ladder predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.