phi_fifth
plain-language theorem explainer
The golden ratio satisfies φ^5 = 5φ + 3. Cross-domain certificates in Recognition Science invoke this to simplify power reductions when establishing bounds for physical quantities. The proof is a direct reference to the algebraic identity already established in the Constants module.
Claim. $φ^5 = 5φ + 3$
background
The module collects Fibonacci-phi identities that reduce any power φ^n to the linear form F(n)φ + F(n-1), where F denotes the Fibonacci sequence with F(0)=0 and F(1)=1. This reduction turns domain-specific bounds into arithmetic facts about Fibonacci numbers plus the numerical interval on φ itself. The golden ratio φ satisfies the quadratic equation x^2 - x - 1 = 0 and therefore the recurrence φ^k = φ^{k-1} + φ^{k-2} for k ≥ 2.
proof idea
One-line wrapper that applies the algebraic identity lemma from Constants, which expands via ring and successive substitution from the fourth-power and square identities.
why it matters
This identity populates the FibonacciPhiCert structure that aggregates the power reductions for cross-domain use. It supplies the concrete case needed to certify bounds such as those appearing in telomere and baryon-asymmetry arguments. The result rests on the self-similar fixed-point property of φ already established upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.