consecutive_fib_collapse
plain-language theorem explainer
Consecutive Fibonacci numbers satisfy the recurrence F_n + F_{n+1} = F_{n+2} for every natural number n. Researchers formalizing Zeckendorf representations as J-cost stable configurations on the phi-ladder cite this identity to justify the non-consecutive gap condition. The proof is a one-line wrapper that applies the fib_recurrence lemma and then uses omega to commute the sum.
Claim. For every natural number $n$, the $n$-th Fibonacci number plus the $(n+1)$-th equals the $(n+2)$-th: $F_n + F_{n+1} = F_{n+2}$.
background
The module frames Zeckendorf's theorem as the statement that every positive integer admits a unique J-cost-stable representation on the phi-ladder. Fibonacci numbers occupy phi-ladder rungs because $F_n$ approximates $phi^n / sqrt(5)$. The non-consecutive (gap at least 2) requirement follows because adjacent rungs are unstable: they collapse under the golden recurrence. The local setting therefore treats the classical Fibonacci recurrence as the algebraic signature of J-cost absorption on the ladder.
proof idea
The proof is a one-line wrapper. It invokes the fib_recurrence lemma at n to obtain the defining relation, then applies omega to reorder the addition into the target form.
why it matters
This identity supplies the collapse step used by gap1_absorptive_not_stable to distinguish absorptive gap-1 pairs from merely costly ones. It also appears in zeckendorf_rogers_ramanujan_same_constraint to equate the Zeckendorf gap condition with the Rogers-Ramanujan parts-differ-by-at-least-2 rule via the shared phi-ladder instability. In the Recognition framework it instantiates the adjacent-collapse mechanism that links the J-uniqueness property to the self-similar fixed point on the ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.