Carryless Pairing: Additive Pairing in the Fibonacci Basis

We define a pairing map ${\pi }_{\mathsf{C}\mathsf{L}}:{\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.