fibonacci_lattice_is_unique
plain-language theorem explainer
Zeckendorf representations of positive integers as sums of non-consecutive Fibonacci numbers are unique. Number theorists and Recognition Science researchers working on phi-ladder J-cost stability would cite this result. The proof recovers each input list from its Fibonacci sum via the standard zeckendorf recovery property and equates them after the given sum equality.
Claim. If $l_1$ and $l_2$ are lists of natural numbers satisfying the Zeckendorf non-consecutive condition and the sum of Fibonacci numbers indexed by $l_1$ equals the sum indexed by $l_2$, then $l_1 = l_2$.
background
The module frames Zeckendorf representations as the J-cost-stable points on the phi-ladder: non-consecutive Fibonacci indices prevent adjacent-rung collapse under the J functional, since consecutive terms satisfy the Fibonacci recurrence and reduce total J-cost. The fib abbreviation is the standard Fibonacci sequence (1,1,2,3,5,...), imported from Nat.fib and aligned with the Gap45 and ContinuedFractionPhi definitions. The map operation from RSNative.Core preserves measurement structure while applying the index-to-Fibonacci conversion.
proof idea
The tactic proof introduces the two lists and their IsZeckendorfRep hypotheses. It applies Nat.zeckendorf_sum_fib to obtain that each list equals the zeckendorf decomposition of its Fibonacci sum. The given sum equality is rewritten into the first recovery equation, after which symmetry and transitivity yield list equality.
why it matters
The result supplies the uniqueness half of the classical Zeckendorf theorem inside the RS-native J-cost setting, confirming that every positive integer possesses a unique stable representation on the phi-ladder. It directly supports the module's claim that the greedy algorithm realizes J-cost descent and connects to T5 J-uniqueness and the self-similar fixed point phi. No downstream uses appear yet, but the theorem closes the uniqueness step required for later stability and Rogers-Ramanujan comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.