nsRS_lt_one
plain-language theorem explainer
The theorem establishes that the Recognition Science spectral index is strictly less than one. Cosmologists comparing the phi-ladder model to CMB observations would cite this bound to confirm the predicted red tilt. The proof is a one-line wrapper that unfolds the spectral index definition together with the gap parameter and resolves the resulting numerical inequality by normalization.
Claim. Let $n_s = 1 - 2 / g_{45}$ where $g_{45}$ is the Recognition Science gap parameter fixed at 45. Then $n_s < 1$.
background
The module develops the spectral index within the Recognition Science cosmology framework, where the index is obtained from the gap parameter on the phi-ladder. The upstream definition states that the spectral index equals one minus twice the reciprocal of gap45, which encodes the slow-roll relation $n_s = 1 - 2/g_{45}$ and produces the numerical value approximately 0.956. The module documentation places this construction in the A2 Cosmology Depth, linking the J-cost derived gaps to inflationary observables and noting proximity to the Planck 2018 measurement of 0.965.
proof idea
The proof is a one-line wrapper. It unfolds the spectral index definition and the gap parameter, reducing the claim to a concrete numerical inequality that norm_num discharges directly.
why it matters
This bound confirms that the Recognition Science prediction lies below unity, consistent with the observed red tilt in the CMB spectrum. It supports the gap-45 formula $n_s = 1 - 2/g_{45} ∈ (0.955, 0.957)$ given in the module documentation. Within the framework it contributes to the chain from J-uniqueness through the phi-ladder to cosmological predictions, although no downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.