phi_pow_fibonacci_sum_le
plain-language theorem explainer
The theorem states that powers of the golden ratio satisfy the Fibonacci recurrence for every natural number n. Workers on the fermion mass spectrum in Recognition Science cite it to establish that masses on the phi-ladder obey m_{r+2} = m_{r+1} + m_r. The proof is a one-line wrapper applying the base recursion lemma through linear arithmetic.
Claim. For every natural number $n$, $phi^n + phi^{n+1} = phi^{n+2}$.
background
The Quantum-Gravity Octave Duality module derives all results from the J-cost functional, defined as the AM-GM gap J(x) = (x-1)^2/(2x) for x>0. It proves the central relation kappa * hbar = 8 with kappa = 8 phi^5 and hbar = phi^{-5}, together with G * hbar = 1/pi. The local setting is the eight-tick octave cycle that forces D=3 and the phi-ladder mass formula. Upstream, phi_fibonacci_recursion encodes the characteristic equation phi^2 = phi + 1 that propagates to all higher powers.
proof idea
One-line wrapper that applies the lemma phi_fibonacci_recursion n inside linarith.
why it matters
This supplies the explicit recurrence needed for QG-004 (mass ladder is Fibonacci) inside the module's complete QG Octave Duality Certificate. It directly supports the claim that the fermion mass spectrum m_r = y * phi^r forms a Fibonacci sequence of energies. The result sits between the J-cost uniqueness (T5) and the eight-tick octave (T7) in the forcing chain, closing the link from recognition cost to the discrete mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.