spectralIndex_band
Recognition Science derives the spectral index relation n_s - 1 = -2/45 from the slow-roll parameters ε = 1/(2φ^5) and η = 1/φ^5. The theorem confirms that this yields n_s strictly between 0.955 and 0.957. Cosmologists modeling the inflaton potential would cite the interval to align with CMB observations near 0.96. The proof is a one-line wrapper that refines the conjunction and applies norm_num to discharge both inequalities by direct arithmetic.
claim$0.955 < 1 - 2/45 < 0.957$, which places the spectral index $n_s$ in the open interval $(0.955, 0.957)$ when $n_s - 1 = -2/45$.
background
The Inflaton Potential Structural module treats the RS inflaton potential V(χ) as having five canonical regimes fixed by configDim D = 5. Slow-roll parameters are given explicitly as ε = 1/(2φ^5), η = 1/φ^5, with the derived relations n_s - 1 = -2/45 and r = 2/(45 φ²). The e-fold count is set to 44 after subtracting one tick for reheating transit. The module states that Lean status is zero sorry and zero axiom.
proof idea
The proof is a one-line wrapper. It refines the goal into the two conjuncts of the inequality and applies norm_num to both, which reduces the claim to verified rational arithmetic.
why it matters in Recognition Science
The result supplies the spectral index band required by the downstream inflatonCert definition that assembles the five-regime certification. It instantiates the slow-roll approximation inside the T5-T8 forcing chain, where J-uniqueness and the phi-ladder fix the potential shape and the numerical value -2/45. The bound closes a concrete numerical check that aligns the Recognition Science cosmology module with the observed alpha band and phi^5 scaling.
scope and limits
- Does not derive n_s from the Recognition Composition Law.
- Does not address quantum corrections to the classical slow-roll regime.
- Does not compute the tensor-to-scalar ratio r.
- Does not link the interval to specific CMB data releases.
formal statement (Lean)
60theorem spectralIndex_band :
61 ((0.955 : ℝ) < 1 - 2/45) ∧ (1 - 2/45 < (0.957 : ℝ)) := by
proof body
One-line wrapper that applies refine.
62 refine ⟨?_, ?_⟩ <;> norm_num
63