spectral_index_lt_one
plain-language theorem explainer
The theorem establishes that the spectral index n_s of the primordial power spectrum satisfies n_s < 1 when expressed as 1 minus 2 over phi cubed. Cosmologists working from Recognition Science predictions would cite it to close the upper bound on EU-003. The proof is a short term-mode argument that invokes positivity of phi cubed, positivity of the subtracted term, and linarith.
Claim. Let $phi > 1$ be the self-similar fixed point of the Recognition Composition Law. Then $1 - 2 / phi^3 < 1$.
background
This theorem sits inside the module that supplies calculated proofs for cosmological predictions drawn from the COMPLETE_PROBLEM_REGISTRY. It targets the primordial power spectrum entry EU-003 and supplies one side of the bound on n_s expressed through powers of phi. The module states that all such proofs rely on norm_num, nlinarith and positivity with explicit bounds from the phi ladder.
proof idea
The proof is a short term-mode argument. It applies pow_pos to Constants.phi_pos to obtain phi cubed positive, then div_pos with a norm_num witness to obtain that 2 over phi cubed is positive, and finally closes with linarith.
why it matters
The result supplies the upper half of spectral_index_bounds, which is then used inside cosmological_predictions_cert_exists to witness the full certificate for the registry items. It completes the calculated proof for EU-003 listed in the module doc-comment. Within the framework it rests on the phi fixed point obtained at T6 of the forcing chain and on the positivity properties bundled in the upstream Constants structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.