phi5_eq
plain-language theorem explainer
The golden ratio satisfies the Fibonacci identity φ⁵ = 5φ + 3. Cosmologists working on the Hubble tension pipeline cite it to normalize the amplitude correction 1/φ⁵ in the Z-aging formula for the H0 late/early ratio. The proof reduces higher powers from the base quadratic relation φ² = φ + 1 via successive linear arithmetic steps.
Claim. $φ^5 = 5φ + 3$, the Fibonacci identity for the golden ratio satisfying $φ^2 = φ + 1$.
background
In the Hubble tension pipeline the amplitude normaliser is scaled by 1/φ⁵, with φ the golden ratio. The module states that RS predicts the H0 ratio lies in (1.075, 1.091) once φ⁵ is replaced by its closed form 5φ + 3. The upstream result phi_sq_eq supplies the defining relation φ² = φ + 1 (from x² - x - 1 = 0).
proof idea
The tactic proof first obtains φ² = φ + 1 from phi_sq_eq. It then applies nlinarith to obtain the cubic identity φ³ = 2φ + 1 and the quartic identity φ⁴ = 3φ + 2. A final nlinarith step closes the target equation φ⁵ = 5φ + 3.
why it matters
The identity is invoked inside hubbleTensionCert to certify that the predicted band contains the empirical ratio 1.083, and inside darkEnergyEoSDepthCert to bound the dark-energy depth parameter. It supplies the explicit rung-5 value on the phi-ladder, consistent with the self-similar fixed point and the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.