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.

翻译：我们定义了一个配对映射 $π_{\mathsf{CL}} : \mathbb{N}^2\to\mathbb{N}$，该映射通过从 $x$ 计算得出的分隔符，将 $x$ 与 $y$ 编码到两个不重叠的齐肯多夫指数带中。该构造在本质上实现了“无进位”：组合支撑集不含连续指数，因此每个生成的编码已处于齐肯多夫范式，而求值与逆运算仅需通过加法支撑运算完成，无需乘法、因式分解或位置数字交替操作。该映射为单射而非满射，其像成员判定可通过解码所用的同一支撑机制实现。核心正确性定理已在Rocq中机械化验证。