spectral_index
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the slow-roll approximation from the J-cost functional.
- Does not fix or derive the value of N.
- Does not incorporate log-periodic modulations or Ω₀.
Lean usage
theorem n_s_at_55 : 0.96 < spectral_index 55 ∧ spectral_index 55 < 0.97 := by unfold spectral_index; constructor <;> norm_numformal statement (Lean)
47noncomputable def spectral_index (N : ℝ) : ℝ := 1 - 2 / N
proof body
Definition body.
48
49/-- Tensor-to-scalar ratio: r ≈ 12α/N² = 12φ²/N².
50 This is the RS-SPECIFIC prediction: the standard α-attractor formula
51 with α = φ² (not a free parameter). -/