phi_pow7_eq
plain-language theorem explainer
The declaration proves that the seventh power of the golden ratio equals thirteen times the golden ratio plus eight. Numerics researchers extending the phi-ladder relations in Recognition Science cite it when building exact algebraic identities for higher powers. The proof reduces the exponent by factoring into the known square and fifth-power identities, then applies ring expansion and substitution to collect coefficients.
Claim. $φ^7 = 13φ + 8$, where $φ = (1 + √5)/2$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module Numerics.Interval.PhiBounds supplies rigorous algebraic bounds and identities for the golden ratio φ using its minimal polynomial. It begins from the defining relation φ² = φ + 1 and derives higher powers as integer linear combinations of φ and 1, with coefficients following the Fibonacci sequence. The immediate predecessor phi_pow5_eq establishes the identity φ^5 = 5φ + 3, which is invoked directly in the calculation here. The local setting relies on Mathlib's goldenRatio definition together with real exponentiation to preserve exact equalities without approximation.
proof idea
The proof recalls the square identity goldenRatio^2 = goldenRatio + 1 and the fifth-power identity from phi_pow5_eq. It rewrites the seventh power as the product of those two, expands the product via ring, substitutes the square identity again, and finishes with a final ring simplification to reach the target coefficients 13 and 8.
why it matters
This identity continues the sequence of exact power relations that support the phi-ladder appearing in mass formulas and constant derivations. It aligns with the self-similar fixed-point property of φ (T6) and the eight-tick octave structure in the forcing chain. No immediate downstream theorems are recorded, yet the result closes algebraic scaffolding needed for consistent powering up to φ^7 in the numerics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.