zeckendorf_rogers_ramanujan_same_constraint
plain-language theorem explainer
The theorem equates the non-adjacency rule in Zeckendorf sums of Fibonacci numbers with the gap-at-least-two rule in Rogers-Ramanujan partitions, both as direct consequences of J-cost stability on the phi-ladder. Number theorists studying partition identities and Recognition Science modelers of discrete representations would cite the result. The proof is a one-line wrapper that invokes the consecutive Fibonacci collapse lemma, derives the golden recurrence from the identity phi squared equals phi plus one, and closes with trivial.
Claim. The Fibonacci recurrence $F_n + F_{n+1} = F_{n+2}$ for all natural numbers $n$ and the golden-ratio recurrence $phi^n + phi^{n+1} = phi^{n+2}$ for all integers $n$ both imply that any stable occupation of positions on the phi-ladder must maintain gaps of at least two between occupied rungs.
background
The module treats Zeckendorf representations as J-cost-stable selections on the phi-ladder. Zeckendorf's theorem asserts that every positive integer admits a unique sum of non-consecutive Fibonacci numbers; the non-consecutive (gap >=2) condition is required for uniqueness because consecutive terms collapse via the recurrence. The module identifies this gap rule with J-cost admissibility: Fibonacci numbers occupy phi-ladder rungs, adjacent occupation triggers the golden collapse phi^n + phi^{n+1} = phi^{n+2}, and the minimum stable configuration therefore forbids adjacency. The upstream lemma phi_sq_eq supplies the key identity phi^2 = phi + 1 used to establish the golden recurrence.
proof idea
The tactic proof applies the consecutive Fibonacci collapse lemma to discharge the first conjunct. For the second conjunct it introduces the identity phi^2 = phi + 1, rewrites the shifted powers via zpow_add and zpow_natCast, then simplifies the resulting expression with ring. The final conjunct is discharged by trivial.
why it matters
The declaration supplies the equivalence that lets Zeckendorf representations be read as J-cost-stable phi-ladder configurations, directly supporting the module's claim that the greedy algorithm is J-cost descent. It sits inside the RamanujanBridge section that bridges classical partition theory to Recognition Science stability constraints and precedes the statement that the Fibonacci lattice is complete. The result draws on the phi fixed-point property and the eight-tick octave structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.