zeckendorf_is_Jcost_stable
plain-language theorem explainer
Zeckendorf representations consist of non-consecutive Fibonacci indices on the phi-ladder and satisfy the J-cost stability condition that no two indices differ by one. Number theorists and Recognition Science researchers cite this equivalence to connect classical uniqueness theorems to the cost function induced by multiplicative recognizers. The proof performs case analysis on index order and invokes the built-in gap-two property of the ZeckendorfRepr structure to establish the absolute difference bound.
Claim. Let $z$ be a Zeckendorf representation: a strictly increasing list of integers at least 2 whose pairwise gaps are at least 2. Then the index list satisfies J-cost stability: for all distinct indices $i,j$ in the list, $|i-j|geq 2$.
background
ZeckendorfRepr is a structure whose indices field is a list of Fibonacci positions that are non-consecutive, satisfying the gap condition that any two differ by at least 2. JCostStable is the proposition that a list of occupied rungs has no pair with absolute difference exactly 1, which is the stability requirement under the J-cost function derived from the multiplicative recognizer. The module sets Zeckendorf representations as the J-cost stable configurations on the phi-ladder, where adjacent occupations collapse under the relation phi^n + phi^{n+1} = phi^{n+2}. This links the classical theorem that every positive integer has a unique non-consecutive Fibonacci sum to the Recognition Science cost analysis. Upstream results include the cost definition from MultiplicativeRecognizerL4, which supplies the J-cost comparator used to define stability.
proof idea
The tactic proof introduces the indices i and j, then splits into cases i < j and j < i. In each case it applies the gap_two field of the ZeckendorfRepr to obtain a gap of at least 2, converts to integers, and uses absolute value lemmas together with omega to conclude that the absolute difference is at least 2.
why it matters
This theorem establishes that Zeckendorf representations are precisely the J-cost stable partitions on the phi-ladder, filling the link between number-theoretic uniqueness and the Recognition Science forcing chain. It supports downstream definitions such as representationCost and the connection to Rogers-Ramanujan identities noted in the module. The result closes one step in translating classical Fibonacci decompositions into the eight-tick octave and D=3 spatial structure of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.