phi_fifth_eq
plain-language theorem explainer
The golden ratio satisfies φ^5 = 5φ + 3. Researchers deriving periods in economic cycles or running couplings in gravity cite this identity. The proof chains substitutions from the fourth-power identity and the square relation using ring tactics.
Claim. $φ^5 = 5φ + 3$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The golden ratio φ is the positive root of x² - x - 1 = 0. Upstream phi_sq_eq states the square identity φ² = φ + 1. The upstream phi_fourth_eq gives the key identity φ⁴ = 3φ + 2 (Fibonacci recurrence).
proof idea
A calc block reduces the left side step by step. It rewrites φ^5 as φ times φ^4, applies the fourth-power identity to reach φ(3φ + 2), simplifies to 3φ² + 2φ, substitutes the square identity, and reduces to 5φ + 3.
why it matters
This lemma supplies the base for phi_fifth_bounds and phi_sixth_eq. It is invoked in businessCyclePeriod_lower to show periods exceed 85 ticks and in beta_running_bounds for gravitational running. It corresponds to the Fibonacci step in the phi-ladder, supporting the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.