phi_pow5_eq
plain-language theorem explainer
The theorem establishes the exact algebraic identity φ^5 = 5φ + 3 for the golden ratio φ. Numerics and constants researchers building phi-ladder expressions would cite it to obtain closed forms for higher powers. The proof is a short algebraic reduction that multiplies the known quartic identity by φ and simplifies using the quadratic relation φ² = φ + 1.
Claim. $φ^5 = 5φ + 3$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous algebraic bounds on φ using its minimal polynomial and the Fibonacci recurrence for its powers. Upstream results include phi_cubed_eq, which states 'Key identity: φ³ = 2φ + 1 (Fibonacci recurrence)' and is proved by expanding φ³ = φ · φ² with φ² = φ + 1, and phi_pow4_eq, which states φ⁴ = 3φ + 2 by the same recurrence pattern. These identities are reused across astrophysics, climate, and constants modules to maintain exact phi-ladder relations.
proof idea
The proof invokes phi_cubed_eq and phi_pow4_eq, then applies the ring tactic to compute φ^5 = φ^4 · φ, substitutes the quartic expression, expands the product, replaces φ² by φ + 1 via goldenRatio_sq, and collects coefficients to reach 5φ + 3.
why it matters
This identity is invoked by the bounding theorems phi_pow5_gt and phi_pow5_lt to derive numerical inequalities, and by phi_pow7_eq to continue the ladder to φ^7 = 13φ + 8. It supports the Recognition Science phi-ladder used for native-unit constants such as ħ = φ^{-5} and G = φ^5 / π, and for the mass formula on the phi-ladder. The result closes an exact algebraic step required for the self-similar fixed point and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.