We define a pairing map $π: \mathbb{N}^2\to\mathbb{N}$ that encodes $x$ and $y$ into disjoint index bands inside the Zeckendorf support of a single integer. Evaluation and inversion use only addition, comparison, and bounded scans of supports; no multiplication, factorization, or digit interleaving is used. The device is carryless by construction: supports remain non-adjacent, so the output is already in Zeckendorf-normal form. The map is injective but not surjective; membership in its image is decidable by the same support machinery used for decoding. The core claims are mechanized in Rocq.

翻译：我们定义了一个配对映射 $π: \mathbb{N}^2\to\mathbb{N}$，它将 $x$ 和 $y$ 编码到单个整数的 Zeckendorf 支撑集内互不相交的索引带中。求值与求逆仅使用加法、比较和有界支撑集扫描；无需乘法、因式分解或数位交错。该机制在构造上是无进位的：支撑集始终保持非相邻性，因此输出已处于 Zeckendorf 正规形式。该映射是单射而非满射；其像集中的成员资格可通过与解码相同的支撑集机制判定。核心断言已在 Rocq 中实现机械化验证。