phi8_fibonacci
plain-language theorem explainer
The golden ratio satisfies φ^8 = 21φ + 13. Researchers deriving number-theoretic bounds in Recognition Science cite this Fibonacci relation to control coherence times and rung gaps. The proof invokes the base quadratic identity φ² = φ + 1, derives the next two powers by linear arithmetic, and closes with nlinarith on the nonnegativity of (φ^4)^2.
Claim. $φ^8 = 21φ + 13$
background
The module assembles five canonical identities from the golden ratio φ satisfying φ² = φ + 1. Upstream results in Constants and PhiLadderLattice establish this quadratic as the defining equation of φ. The present identity belongs to the Fibonacci sequence generated by repeated application of that relation and supports the bound φ^8 > 46 that approximates gap45 + 1, where gap45 = D²(D + 2) at D = 3.
proof idea
The proof first obtains the base identity φ² = φ + 1 from phi_sq_eq. It then derives φ³ = 2φ + 1 and φ⁴ = 3φ + 2 by nlinarith. The final nlinarith step uses the nonnegativity of (φ^4)^2 to reach the target equality.
why it matters
This identity is one of the five canonical RS number-theoretic relations catalogued in the module. It is referenced by numberTheoryCert and supplies the value used in coherenceTimeCert, phi12_gt_300, and phi8_gt_46. The relation connects the phi-ladder to the eight-tick octave and the coherence-time bounds required by the J-cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.