Carryless Pairing: Additive Pairing in the Fibonacci Basis
For researchers in combinatorial number theory and formal verification, this provides a novel, carryless pairing method with mechanized correctness, though it is incremental.
The paper introduces a pairing function that encodes two natural numbers into a single Zeckendorf representation without carries, enabling efficient encoding and decoding using only additive operations. The construction is mechanized in Rocq, and image membership is decidable.
We define a pairing map $π_{\mathsf{CL}} : \mathbb{N}^2\to\mathbb{N}$ that encodes $x$ and $y$ into two disjoint bands of Zeckendorf indices separated by a delimiter computed from $x$. The construction is "carryless" by design: the combined support has no consecutive indices, so each produced code is already in Zeckendorf-normal form, and both evaluation and inversion proceed by additive support operations alone, without multiplication, factorization, or positional digit interleaving. The map is injective not surjective, image membership is decidable by the same support machinery used for decoding. The core correctness theorems are mechanized in Rocq.