ZeckendorfRepr
plain-language theorem explainer
ZeckendorfRepr encodes a positive integer as a sum of non-consecutive Fibonacci numbers through a list of indices. Number theorists and Recognition Science researchers cite it when mapping classical decompositions onto J-cost stable configurations on the phi-ladder. The definition supplies four predicates on the index list together with a direct summation for the represented value.
Claim. A Zeckendorf representation consists of a strictly increasing list of integers $i_1 < i_2 < … < i_m$ with each $i_k ≥ 2$ and $i_{k+1} ≥ i_k + 2$, whose value equals $∑_k F_{i_k}$ where $F_n$ is the $n$th Fibonacci number.
background
The module treats Zeckendorf representations as the combinatorial objects that realize J-cost stability on the phi-ladder. Fibonacci numbers occupy rungs scaled by powers of phi; the gap condition of at least 2 prevents adjacent occupation, which would collapse under the identity phi^n + phi^{n+1} = phi^{n+2}. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost function whose non-negativity and convexity underwrite the stability interpretation.
proof idea
The structure is introduced by four fields that directly encode the classical Zeckendorf constraints: indices ≥ 2, strict increase, and pairwise gaps ≥ 2. The value field is a one-line fold that sums fib i over the index list.
why it matters
The structure supplies the data type required by the downstream theorem zeckendorf_is_Jcost_stable, which asserts that every such list satisfies the JCostStable predicate. It thereby embeds Zeckendorf’s 1939 theorem inside the Recognition Science forcing chain at the J-uniqueness step (T5) and the phi-ladder stability analysis. The module doc-comment notes that the same gap condition also aligns with the greedy descent interpretation of the Rogers-Ramanujan constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.