phi_eighth
plain-language theorem explainer
The declaration establishes the algebraic identity φ⁸ = 21φ + 13 for the golden ratio φ. Cross-domain researchers reducing high powers via the Fibonacci recurrence would cite it when assembling certificates that convert per-domain bounds into arithmetic facts about Fibonacci numbers. The proof is a one-line term wrapper that directly invokes the corresponding lemma from the Constants module.
Claim. $φ^8 = 21φ + 13$
background
The Fibonacci-Phi Identity Universality module collects already-proved power reductions φ^n = F(n)·φ + F(n-1), where F denotes the Fibonacci sequence with F(0)=0, F(1)=1. These identities allow any bound expressed as a power of φ to collapse to a numerical check on the Fibonacci coefficients plus the known bracket on φ itself. The upstream lemma phi_eighth_eq supplies the explicit case for n=8 via a calc chain that repeatedly applies the base recurrence φ² = φ + 1 together with ring simplification.
proof idea
The proof is a direct term-mode reference to the lemma phi_eighth_eq. That lemma proceeds by a calc block: φ^8 expands as φ·φ^7, substitutes the seventh-power identity, distributes, replaces φ² with φ+1, and simplifies by ring to the target linear form.
why it matters
This identity populates the FibonacciPhiCert structure that aggregates the core power reductions for cross-domain reuse. It implements the C20 wave of the Recognition framework, where the self-similar fixed-point property of φ (T6) generates the Fibonacci recurrence that underpins bounds such as telomere halving and baryon asymmetry. The certificate is consumed by the downstream definition fibonacciPhiCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.