gap1_absorptive_not_stable
plain-language theorem explainer
The declaration proves that consecutive Fibonacci numbers satisfy the absorption identity F_n + F_{n+1} = F_{n+2} for every natural number n. Analysts of J-cost stability on the phi-ladder cite this to justify exclusion of adjacent rungs from normal-form representations. The proof is a direct one-line application of the consecutive Fibonacci collapse lemma.
Claim. For every natural number $n$, if $F_n$ denotes the $n$th Fibonacci number then $F_n + F_{n+1} = F_{n+2}$.
background
The ZeckendorfJCost module identifies Fibonacci numbers with positions on the phi-ladder via $F_n ≈ phi^n / sqrt(5)$. J-cost is the cost function induced by a multiplicative recognizer on positive ratios, and a representation is J-cost stable precisely when no two occupied rungs are adjacent. The module documentation states that adjacent occupation is J-unstable because phi^n + phi^{n+1} = phi^{n+2} (collapses), so the non-consecutive condition of Zeckendorf's theorem is exactly the J-cost admissibility constraint.
proof idea
The proof is a one-line wrapper that applies the consecutive_fib_collapse lemma.
why it matters
This supplies the arithmetic fact required to treat gap-1 pairs as absorptive rather than merely costly, thereby grounding the claim that Zeckendorf representations are the J-cost-stable configurations on the phi-ladder. It connects directly to the Recognition Composition Law and the forcing-chain steps T5 (J-uniqueness) and T6 (phi fixed point). The result appears in the section introducing the greedy algorithm as J-cost descent and supports later statements on Rogers-Ramanujan constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.