phi_pow4_eq
plain-language theorem explainer
The equality φ⁴ = 3φ + 2 holds for the golden ratio φ = (1 + √5)/2. Numerics researchers in Recognition Science cite it when deriving exact expressions for higher powers on the phi-ladder. The proof is a short algebraic reduction that substitutes the cubic identity φ³ = 2φ + 1 together with the quadratic φ² = φ + 1 and simplifies via ring.
Claim. $φ^4 = 3φ + 2$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous algebraic bounds and identities for the golden ratio using its defining quadratic relation φ² = φ + 1. This relation generates the Fibonacci-like recurrence for integer powers. Upstream results include phi_cubed_eq, documented in Constants as the key identity φ³ = 2φ + 1 (Fibonacci recurrence). The local setting uses these exact reductions to support interval bounds such as 1.618 < φ < 1.6185.
proof idea
The proof introduces the cubic identity via phi_cubed_eq and the quadratic via goldenRatio_sq. It then executes a calc chain: rewrite φ⁴ as φ³ · φ, substitute the cubic, expand with ring, rewrite the quadratic, and simplify to 3φ + 2.
why it matters
This identity serves as a building block for the phi-ladder, directly feeding phi_pow5_eq (φ⁵ = 5φ + 3) and the bounding theorems phi_pow4_gt and phi_pow4_lt. It aligns with the self-similar fixed point property of φ (T6 in the forcing chain) and supports mass formulas on the phi-ladder. No open questions are touched; it closes an algebraic step in the numerics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.