phi5_eq
plain-language theorem explainer
The theorem establishes the algebraic identity φ⁵ = 5φ + 3 for the golden ratio φ. Cosmologists working within the Recognition Science framework cite this identity when deriving bounds on the cosmological constant Λ_RS or Hubble tension parameters. The proof proceeds by invoking the base relation φ² = φ + 1 and then applying linear arithmetic to obtain the higher powers.
Claim. $φ^5 = 5φ + 3$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
In the Recognition Science framework the golden ratio φ is defined by the quadratic equation whose positive root satisfies φ² = φ + 1. The present module derives the cosmological-constant band Λ_RS = 8φ⁵/45 ∈ (1.88, 2.03) from the BIT kernel; the key algebraic step is the Fibonacci identity φ⁵ = 5φ + 3. Upstream, phi_sq_eq supplies the base relation φ² = φ + 1 (from the defining equation x² - x - 1 = 0).
proof idea
The proof invokes phi_sq_eq to obtain φ² = φ + 1. It then derives φ³ = 2φ + 1 and φ⁴ = 3φ + 2 by nlinarith, and finally applies nlinarith to reach φ⁵ = 5φ + 3.
why it matters
This identity is used directly by darkEnergyEoSDepthCert, hubbleTensionCert, inflatonCert and the associated band-certification theorems. It supplies the Fibonacci step required by the Omega Lambda BIT Kernel Band module to obtain the RS prediction Λ_RS ∈ (1.88, 2.03). In the larger framework it connects to the phi-ladder lattice and the self-similar fixed-point property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.