phi5_eq
plain-language theorem explainer
The golden ratio satisfies the Fibonacci identity φ^5 = 5φ + 3. Cosmologists deriving slow-roll parameters or dark-energy equation-of-state bounds in RS models cite this relation when closing numerical estimates on ε, η, or delta. The proof invokes the base quadratic relation, obtains the cubic and quartic cases by linear arithmetic, and closes the target with nlinarith.
Claim. $φ^5 = 5φ + 3$, where $φ = (1 + √5)/2$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module InflatonPotentialStructural treats the RS inflaton potential V(χ) as having five canonical regimes (configDim D = 5): slow-roll plateau, slope, hilltop, reheating, and post-reheating radiation. Slow-roll parameters are written ε = 1/(2φ^5), η = 1/φ^5, with N_e-fold count fixed at 44. The identity supplies the fifth Fibonacci power needed to evaluate these expressions numerically. Upstream, phi_sq_eq states the defining relation φ² = φ + 1 from the quadratic x² - x - 1 = 0; multiple sibling modules (DarkEnergyEquationOfStateDepth, HubbleTensionPipelineFromZAging, OmegaLambdaBITKernelBand, CosmologicalConstantFromRS) carry identical copies of the same quintic identity.
proof idea
The tactic proof first obtains phi_sq_eq as h2. It then derives φ^3 = 2φ + 1 and φ^4 = 3φ + 2 by nlinarith, after which a final nlinarith closes the target equality.
why it matters
darkEnergyEoSDepthCert and hubbleTensionCert both import the identity to certify delta bounds and Hubble-tension channels; inflatonCert likewise depends on it. The relation completes the phi-ladder step required for the five-regime inflaton structure and for the slow-roll expressions ε = 1/(2φ^5), η = 1/φ^5. It is the direct Fibonacci consequence of the self-similar fixed point phi forced at T6 of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.