phi_fibonacci_recursion
plain-language theorem explainer
The golden ratio satisfies the recurrence φ^{n+2} = φ^{n+1} + φ^n for every natural number n. Mass spectrum modelers cite it to establish that fermion masses on the phi-ladder form a Fibonacci sequence. The proof is a short algebraic reduction that invokes the identity φ² = φ + 1 twice inside ring rewrites.
Claim. For every natural number $n$, the equality $φ^{n+2} = φ^{n+1} + φ^n$ holds, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The Quantum-Gravity Octave Duality module establishes relations that lock quantum mechanics and gravity through the octave factor 8. This theorem supplies the algebraic step for QG-004, which states that the fermion mass spectrum m_r = y · φ^r obeys the Fibonacci recursion m_{r+2} = m_{r+1} + m_r. It depends on the upstream lemma phi_sq_eq that records the identity φ² = φ + 1 derived from the quadratic equation defining the golden ratio. In the Recognition Science setting, masses are expressed as yardstick times a power of phi on the ladder, consistent with the self-similar fixed point.
proof idea
The tactic proof uses a calc block. It rewrites the left-hand side as φ² · φ^n by ring, substitutes φ² = φ + 1 via the phi_sq_eq lemma, then distributes the product by ring to reach the right-hand side.
why it matters
This result is invoked by the downstream fibonacci_mass_recursion theorem that states the fermion mass ladder and by phi_pow_fibonacci_sum_le. It realizes the QG-004 step in the module documentation and feeds the qg_octave_cert that packages the full duality including κ · ℏ = 8. The identity aligns with the phi fixed point from the forcing chain and supports the mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.