Termination of Zeckendorf Successor Carries
Abstract
Zeckendorf successor carry chains terminate within the highest occupied index.
Definition 1.1 (CarrySteps records the exact number of local rewrites).
Lean statement: D5/S1/Digit/Carry/Successor.CarrySteps
Formalization. D5/S1/Digit/Carry/Successor.CarrySteps (✓ std3).
Source. Repository-derived.
Commentary.
CarrySteps k before after is generated by a zero-step identity and a constructor that appends one existing CarryStep. The natural parameter therefore measures the chain length rather than merely asserting reflexive-transitive reachability.
Theorem 1.2 (Successor carries terminate before passing the highest index).
Proof. Machine-checked in Lean as D5/S1/Digit/Carry/Successor.zeckendorf_successor_carry_terminates (✓ std3). ∎
Source. Repository-derived.
Commentary.
Adding the least Fibonacci digit has two possible cascades. If the least digit is occupied, the first rewrite is the special double-zero carry and subsequent carries consume occupied even indices. Otherwise, adjacent carries consume occupied odd indices. In either case the first missing digit of that parity gives the exact number of rewrites.
Finite support places that first missing digit no later than one plus the largest occupied raw index. The endpoint is canonical, every local rewrite preserves raw value, and Zeckendorf uniqueness identifies the endpoint with the representation of n+1.
Pinned Mathlib and the repository were searched before proving. Mathlib provides Zeckendorf existence and uniqueness, while the repository already provides the four local carry rules and a general well-founded normalizer. No existing theorem exposed the exact successor carry chain together with this highest-index bound, so the result is derived here from those checked parts.
References
- Truth anchor:
D5/S1/Digit/Carry/Successor.CarrySteps - Truth anchor:
D5/S1/Digit/Carry/Successor.zeckendorf_successor_carry_terminates - Dependency: D5/S1/Digit/Carry