phi8_fibonacci
plain-language theorem explainer
φ^8 equals 21φ + 13 as a Fibonacci identity for the golden ratio. Workers deriving coherence times on the φ-ladder or populating the NumberTheoryCert would cite this result to bound amplitudes at rung 8. The proof reduces powers via the base relation φ² = φ + 1, derives expressions for φ³ and φ⁴, then closes with nlinarith.
Claim. Let φ = (1 + √5)/2 be the golden ratio. Then φ^8 = 21φ + 13.
background
In the Recognition Science module on quantum coherence times, the golden ratio φ is the self-similar fixed point whose powers give ladder rungs for decoherence times τ = τ₀ φ^k. The base identity φ² = φ + 1 (from phi_sq_eq in Constants and PhiLadderLattice) generates all higher Fibonacci relations needed for φ^12 calculations at biological scales. Upstream phi_sq_eq states that φ² = φ + 1 from the quadratic x² - x - 1 = 0.
proof idea
Import phi_sq_eq to obtain φ² = φ + 1. Derive φ³ = 2φ + 1 and φ⁴ = 3φ + 2 by nlinarith. Apply nlinarith to the non-negativity of (φ^4)² to close the target equality for φ^8.
why it matters
This identity populates the NumberTheoryCert (via phi8_fibonacci) and supplies the φ^8 value inside CoherenceTimeCert, which certifies bounds φ^8 > 46 and φ^12 > 300 for coherence amplitudes. It realizes the Fibonacci structure forced by the self-similar fixed point T6 and supports the eight-tick octave scaling in the unified forcing chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.