spectralIndex_band
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.