phi_fourth_bounds
plain-language theorem explainer
The lemma establishes that the fourth power of the golden ratio satisfies 6.5 < φ⁴ < 6.9. Cosmologists using Recognition Science predictions cite this bound when scaling the BAO radius or Hubble parameter from the phi-ladder. The proof reduces the claim via the identity φ⁴ = 3φ + 2 and then applies the interval 1.5 < φ < 1.62 through linear arithmetic.
Claim. $6.5 < φ^4 ∧ φ^4 < 6.9$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The Constants module supplies numerical bounds on integer powers of the golden ratio φ, the self-similar fixed point forced in the Recognition Science chain. The identity φ⁴ = 3φ + 2 follows from the Fibonacci recurrence that holds once φ² = φ + 1. Upstream lemmas give the tighter interval 1.5 < φ < 1.62 by comparing √5 to 2 and 2.24 respectively.
proof idea
The proof rewrites the goal with the identity lemma phi_fourth_eq. It then obtains the bounds on φ from phi_gt_onePointFive and phi_lt_onePointSixTwo. The conjunction is formed and linear arithmetic dispatches both inequalities.
why it matters
This bound is invoked directly by the cosmological predictions certificate and by the φ⁵ bounds lemma in Unification.CosmologicalPredictionsProved. It supplies the concrete numerical step required for the phi-ladder mass formula and the eight-tick octave structure. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.