phi5_eq
plain-language theorem explainer
The golden ratio satisfies the Fibonacci identity φ⁵ = 5φ + 3. Cosmologists working on Recognition Science dark energy models cite it to bound the BIT kernel deviation δ ≤ 1/φ⁵. The proof is a short algebraic reduction that invokes the base quadratic relation and applies linear arithmetic to successive powers.
Claim. $φ^5 = 5φ + 3$, where $φ$ is the golden ratio obeying $φ^2 = φ + 1$.
background
In Recognition Science the golden ratio φ is the self-similar fixed point forced by the J-cost function. The present module develops the dark energy equation of state w(z) on the φ-ladder, enumerating five canonical models and imposing a BIT kernel bound δ ≤ 1/φ⁵. Upstream, phi_sq_eq records the defining quadratic identity φ² = φ + 1 obtained from the minimal polynomial x² - x - 1 = 0.
proof idea
The tactic proof first imports phi_sq_eq. It then obtains φ³ = 2φ + 1 and φ⁴ = 3φ + 2 by nlinarith, after which a final nlinarith step closes the target identity.
why it matters
The identity is invoked inside darkEnergyEoSDepthCert to certify the five-model dark energy package and inside deltaBound_small to establish the numerical bound δ < 0.1. It likewise appears in the Hubble tension and inflaton-potential certificates. The result supplies the φ⁵ term required by RS-native constants (ħ = φ^{-5}) and by the eight-tick octave structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.