phi_pow6_eq
plain-language theorem explainer
Algebraic reduction yields φ^6 = 8φ + 5 for the golden ratio φ. Numerics teams in Recognition Science invoke this to anchor interval arithmetic on higher powers. The tactic proof chains the fourth-power identity through multiplication and ring simplification.
Claim. $φ^6 = 8φ + 5$, where $φ = (1 + √5)/2$ satisfies $φ^2 = φ + 1$.
background
The module supplies rigorous bounds on the golden ratio φ = (1 + √5)/2 by leveraging its algebraic properties and the defining equation φ² = φ + 1. It builds exact linear expressions for successive integer powers before numerical comparison. The immediate predecessor states that φ⁴ = 3φ + 2, obtained from φ³ = 2φ + 1 multiplied by φ.
proof idea
The proof applies phi_pow4_eq to obtain φ⁴ = 3φ + 2 together with the standard relation φ² = φ + 1. A calc block expands φ^6 = φ⁴ · φ², substitutes the two expressions, and reduces via ring and rewrite steps to collect coefficients into 8φ + 5.
why it matters
The identity feeds directly into phi_pow6_gt and phi_pow6_lt, which establish the numerical interval 17.944 < φ^6 < 17.948. In the Recognition Science framework it advances the phi-ladder used for mass formulas and the T6 self-similar fixed point. It supplies the exact recurrence step required before the eight-tick octave and D = 3 constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.