fibonacci_recurrence
plain-language theorem explainer
The golden ratio satisfies the recurrence φ^{n+2} = φ^{n+1} + φ^n for every natural number n. Researchers deriving thermal eigenvalues or self-similar hierarchies on the recognition lattice cite this identity when fixing the leading correlation-length exponent. The proof is a three-step algebraic reduction that factors the left side, substitutes the defining square identity, and redistributes.
Claim. For every natural number $n$, $φ^{n+2} = φ^{n+1} + φ^n$.
background
In the thermal fixed-point operator the φ-ladder is the unique geometric scaling sequence forced by self-similarity. The Fibonacci recurrence on this ladder is the statement that consecutive rungs obey K(ℓ+2) = K(ℓ+1) + Kℓ, the capacity relation that arises from J-cost-optimal partitioning. The upstream identity phi_sq_eq supplies the algebraic engine: φ² = φ + 1, the defining equation of the golden ratio.
proof idea
The proof is a calc block. The first step rewrites the left side as φ^n · φ² by ring. The second step replaces φ² by φ + 1 via rw [phi_sq_eq]. The final step expands the product by ring to obtain the right-hand side.
why it matters
This identity supplies the algebraic step from PhiForcing (T6) to the thermal eigenvalue y_t = φ and therefore ν₀ = 1/φ. It is invoked directly by fibonacci_partition_forces_phi, fibonacci_ratio_forces_golden, no_alternative_ratio and phiHierarchy_fibonacci, which together prove that any self-similar Fibonacci hierarchy must have ratio exactly φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.