spectral_index_gt_half
plain-language theorem explainer
The theorem establishes that the spectral index n_s defined by 1 minus 2 over phi cubed exceeds 0.5. Cosmologists deriving primordial power spectrum bounds from Recognition Science would cite this result to anchor the lower edge of the interval 0.5 less than n_s less than 1. The proof proceeds by algebraic expansion of phi cubed using the identity phi squared equals phi plus one, combined with the lower bound phi greater than 1.5 to reach phi cubed greater than 4, followed by a direct comparison on the reciprocal term.
Claim. $1 - 2/φ³ > 0.5$ where $φ = (1 + √5)/2$ denotes the golden ratio satisfying $φ² = φ + 1$.
background
This declaration sits inside the module Cosmological Predictions — Calculated Proofs, which supplies rigorous bounds for registry items including EU-003 on the primordial power spectrum n_s. The golden ratio φ enters via the phi-ladder lattice and the forcing chain, where φ is the unique positive fixed point of the self-similar map. Upstream results supply the defining identity φ² = φ + 1 (from both Constants and PhiLadderLattice) and the sharpened lower bound φ > 1.5 obtained by comparing √5 > 2.
proof idea
The tactic proof first applies phi_sq_eq to obtain the cubic identity φ³ = 2φ + 1. It then invokes phi_gt_onePointFive to replace φ by a number larger than 1.5, yielding φ³ > 4 by nlinarith. The reciprocal comparison 2/φ³ < 0.5 follows from the positivity of φ³ and a direct application of div_lt_iff₀. The final step closes the target inequality by linarith.
why it matters
The result supplies the lower bound half of spectral_index_bounds and is invoked inside cosmological_predictions_cert_exists to witness the existence of the CosmologicalPredictionsCert. It discharges the calculated status for EU-003 in the module registry, linking the phi-forcing chain (T5 J-uniqueness through T6 phi fixed point) to observable cosmology. No open scaffolding remains for this specific inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.