phi_eighth
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 in Recognition Science
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.
scope and limits
- Does not prove the general recurrence φ^n = F(n)φ + F(n-1) for arbitrary n.
- Does not supply numerical bounds or approximations for φ.
- Does not derive physical constants such as α or G from this identity.
- Does not address convergence properties of the Fibonacci sequence.
Lean usage
noncomputable def myCert : FibonacciPhiCert where phi_eighth := phi_eighthformal statement (Lean)
41theorem phi_eighth : phi ^ 8 = 21 * phi + 13 := phi_eighth_eq
proof body
Term-mode proof.
42
43/-- Fibonacci coefficients F(1), F(2), ..., F(11) match the coefficients above. -/