spectral_index_bounds
plain-language theorem explainer
The theorem establishes that the spectral index n_s = 1 - 2/φ³ satisfies the strict bounds 0.5 < n_s < 1. Cosmologists working on primordial power spectrum predictions within Recognition Science would cite this result to constrain early-universe fluctuations. The proof is a direct conjunction of the two component inequalities already shown in sibling lemmas.
Claim. The spectral index of the primordial power spectrum satisfies $0.5 < n_s < 1$ where $n_s = 1 - 2 / ϕ^3$ and ϕ obeys ϕ² = ϕ + 1.
background
This module supplies calculated proofs for the cosmological predictions listed in the COMPLETE_PROBLEM_REGISTRY, using explicit bounds derived from φ. The entry EU-003 concerns the primordial power spectrum n_s, obtained here as 1 - 2/φ³ from the self-similar scaling fixed by the forcing chain. The constant φ is the positive root of x² - x - 1 = 0, appearing throughout the phi-ladder and the eight-tick octave construction.
proof idea
A one-line wrapper that applies constructor to combine the already-proved theorems spectral_index_gt_half and spectral_index_lt_one.
why it matters
This theorem completes the bound required for the primordial power spectrum prediction (EU-003) and supports the certification object cosmological_predictions_cert_exists. It instantiates the phi-based formulas from the Recognition framework, relying on the self-similar fixed point property of φ (T6) to fix the interval without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.