phi_pow16_eq
plain-language theorem explainer
The algebraic identity φ¹⁶ = 987φ + 610 holds exactly for the golden ratio φ. Researchers deriving interval bounds on high powers of φ in algebraic numerics cite this result to convert exact expressions into numerical inequalities. The proof squares the known eighth-power identity, substitutes the quadratic relation φ² = φ + 1, and normalizes the resulting polynomial.
Claim. $φ^{16} = 987φ + 610$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous algebraic bounds on the golden ratio φ = (1 + √5)/2 by exploiting its minimal polynomial and the Fibonacci recurrence φⁿ = Fₙ φ + F_{n-1}. The supplied upstream result states φ⁸ = 21φ + 13, obtained by the same recurrence from lower powers. This setting uses only ring operations and the base relation φ² = φ + 1; no analysis or limits appear.
proof idea
The tactic proof invokes the eighth-power identity and the quadratic relation, then applies a calc chain: square the eighth-power expression, expand the product, substitute φ² = φ + 1, and collect coefficients with ring normalization.
why it matters
The identity is applied directly by the downstream theorems phi_pow16_gt and phi_pow16_lt to obtain the concrete bounds 2206.9 < φ¹⁶ < 2207.5. It supplies one link in the module's chain of exact power identities that support tighter numerical control of φ for Recognition Science numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.