phi_pow8_eq
plain-language theorem explainer
The equality states that the eighth power of the golden ratio satisfies φ⁸ = 21φ + 13. Researchers deriving exact power identities for interval bounds on φ would cite this result. The proof reduces the eighth power to the square of the fourth power, substitutes the known fourth-power identity, expands via ring, substitutes the square relation, and simplifies coefficients.
Claim. Let φ denote the golden ratio. Then φ⁸ = 21φ + 13.
background
The module supplies rigorous algebraic bounds on the golden ratio φ = (1 + √5)/2. It starts from the defining relation φ² = φ + 1 and builds exact linear expressions for higher powers whose coefficients are Fibonacci numbers. The immediate predecessor states φ⁴ = 3φ + 2, obtained by the same pattern from the cubic case.
proof idea
The tactic proof opens a calc block that rewrites φ⁸ as φ⁴ ⋅ φ⁴. It substitutes the fourth-power identity, expands the product with ring, substitutes the square identity into the resulting terms, and reduces the coefficients with ring to reach 21φ + 13.
why it matters
This identity is invoked directly by the sixteenth-power theorem to obtain φ¹⁶ = 987φ + 610 and by the two bounding theorems that place 46.97 < φ⁸ < 46.99. The chain of exact power identities supports interval arithmetic for φ inside the Recognition Science numerics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.