spectral_index_bounds
The spectral index n_s of the primordial power spectrum satisfies the strict inequality 0.5 < n_s < 1 when n_s is given by 1 - 2/phi^3 with phi the golden ratio. Cosmologists working on inflationary models inside Recognition Science would cite this bound when matching the phi-ladder to CMB observables. The proof is a one-line term wrapper that splits the conjunction and invokes the two already-proved component inequalities.
claimLet phi denote the golden ratio. Then 0.5 < 1 - 2/phi^3 < 1.
background
This theorem sits in the Cosmological Predictions — Calculated Proofs module, which supplies explicit bounds for registry items including EU-003 (primordial power spectrum n_s). The quantity n_s is defined via the formula 1 - 2/phi^3, where phi is the self-similar fixed point forced by the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Upstream lemmas establish the separate lower bound (phi^3 > 4) and upper bound (2/phi^3 > 0) using the algebraic relation phi^3 = 2 phi + 1 together with positivity of phi.
proof idea
The proof is a term-mode proof that begins with the constructor tactic to split the conjunction into two subgoals. It then applies the exact tactic to the sibling theorems spectral_index_gt_half and spectral_index_lt_one. Those lemmas in turn rest on phi_sq_eq, pow_pos, and linarith for the positivity and algebraic steps.
why it matters in Recognition Science
The declaration discharges the EU-003 registry item by proving the predicted bounds on the primordial spectral index directly from the phi-ladder. It supports the unification program that derives cosmological parameters from T5 J-uniqueness and T6 phi fixed point, feeding into later claims about the eight-tick octave and D = 3. No scaffolding remains; the bound is fully closed.
scope and limits
- Does not derive the n_s formula itself from the Recognition Composition Law.
- Does not incorporate loop corrections or running of the spectral index.
- Does not compare the bound against Planck or other observational data.
- Does not address the Hubble tension or dark-energy density in the same statement.
formal statement (Lean)
69theorem spectral_index_bounds : (0.5 : ℝ) < 1 - 2 / (phi ^ 3) ∧ 1 - 2 / (phi ^ 3) < 1 := by
proof body
Term-mode proof.
70 constructor
71 · exact spectral_index_gt_half
72 · exact spectral_index_lt_one
73
74/-! ## Section T-001: Hubble Constant -/
75
76/-- **CALCULATED**: Hubble constant H₀ > 0 from ln(φ) > 0. -/