phi_squared_bounds
plain-language theorem explainer
The theorem establishes that the square of the golden ratio satisfies 2.59 < φ² < 2.62. Researchers deriving scaling relations for orbital gaps, Damköhler numbers, and spin-glass ratios cite the result to anchor numerical bands. The proof substitutes the algebraic identity φ² = φ + 1, imports the tightened interval 1.61 < φ < 1.62, and discharges both conjuncts by nonlinear arithmetic.
Claim. $2.59 < φ^2 ∧ φ^2 < 2.62$
background
Recognition Science obtains φ as the unique positive fixed point of the self-similar map J(x) = (x + x^{-1})/2 - 1. The identity φ² = φ + 1 follows at once from the quadratic x² - x - 1 = 0. The module assembles calculated proofs for cosmological registry items (primordial spectrum, dark-energy density, Hubble parameter) that all rest on explicit numerical intervals for powers of φ.
proof idea
The argument invokes the identity lemma phi_sq_eq to replace φ² by φ + 1. It then obtains the bounding lemmas 1.61 < φ < 1.62 and splits the target conjunction. Each conjunct is settled by a single nlinarith tactic.
why it matters
Fifteen downstream declarations invoke the bound, including the gap-skip ratio in planetary formation and the critical Damköhler interval in combustion stabilization. The result supplies the concrete window required to place scaling factors inside the empirical bands demanded by the Recognition Composition Law and the eight-tick octave. It thereby completes one of the calculated items listed for the cosmological predictions registry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.