Carryless Pairing: Additive Pairing in the Fibonacci Basis

Abstract

We define a pairing map $\ddot{I}{€}_{\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.

Theoretical paper in mathematical logic and bounded arithmetic, 11 pages, 4 figures. Establishes an additive arithmetic pairing function. The core claims are mechanized in Rocq