fib_recurrence
plain-language theorem explainer
The Fibonacci recurrence asserts that the (n+2)th term equals the sum of the two preceding terms. Researchers tracing Zeckendorf representations to J-cost stability on the phi-ladder cite this identity to justify the collapse of adjacent rungs. The proof is a one-line wrapper that invokes Nat.fib_add_two after reordering via add_comm.
Claim. For every natural number $n$, the $(n+2)$th Fibonacci number equals the sum of the $(n+1)$th and $n$th: $F_{n+2} = F_{n+1} + F_n$.
background
The module treats Zeckendorf representations as J-cost-stable sums on the phi-ladder, where Fibonacci numbers occupy ladder positions via the approximation $F_n ≈ ϕ^n / √5$. Non-consecutive selection (gap ≥ 2) enforces J-cost admissibility because adjacent occupations satisfy the collapse $ϕ^n + ϕ^{n+1} = ϕ^{n+2}$. The local setting is the RS decipherment of Zeckendorf's 1939 theorem as the unique minimal-J-cost decomposition under the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies the Mathlib lemma Nat.fib_add_two (n := n) and uses simpa with add_comm to match the target ordering of summands.
why it matters
This identity is the direct input to consecutive_fib_collapse, which rewrites the recurrence as absorption of adjacent phi-ladder positions into the next rung, the same mechanism as PhiLadderStability. It anchors the RamanujanBridge claim that Zeckendorf decompositions are exactly the J-cost-stable configurations, linking to the forced phi fixed point (T6) and the eight-tick octave. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.