🔢 mathematics

Carryless Pairing: Additive Pairing in the Fibonacci Basis

本論文は、2 つの数を区切り文字によって分離された非重複のゼッケンドルフ指数帯に符号化する、 $\mathbb{N}^2$ から $\mathbb{N}$ への乗算なし単射ペアリング写像を導入し、乗算や素因数分解を伴わず加法支援操作による評価と逆算を可能にし、その核心的な正しさを Rocq で検証したものである。

原著者： Milan Rosko

公開日 2026-05-12

📖 1 分で読めます🧠 じっくり読む

CC BY 4.0

原著者： Milan Rosko

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

「フィボナッチ基底におけるキャリーレスなペアリング」に関する論文を、平易な言葉と日常的な比喩を用いて解説します。

大きなアイデア：壊さずに 2 つの箱を詰め込む

箱 Xと箱 Yというラベルの付いた、レゴブロックの箱が 2 つあると想像してください。これらを 1 つの巨大な構造物に接着して、単一の物体として持ち運べるようにしたいのですが、後で接着剤、テープ、特別な道具を使わずに、再び引き離せるようにもしたいとします。

数値を組み合わせるほとんどの方法（標準的な数学やコンピュータのコードなど）は、接着剤を使うようなものです。後でそれらを分離するには、複雑な計算を行ったり、数を因数分解したり、桁上げ（通常の加算で $9 + 1 = 10$ の際、1 が次の桁に「繰り上がる」こと）を行ったりする必要があります。この論文は、接着剤も桁上げもゼロで数値を組み合わせる新しい方法を提案しています。

舞台設定：フィボナッチ「レゴセット」

これがどのように機能するかを理解するには、数値の構築ルールを変更する必要があります。この論文では、標準的な 10 進法（1 の位、10 の位、100 の位など）の代わりに、フィボナッチ数列（$1, 2, 3, 5, 8, 13, 21...$）を使用します。

このシステムでは、すべての数値にゼッケンドルフ表現と呼ばれる特別な「レゴの設計図」が存在します。この設計図の黄金律は、連続するフィボナッチ数を 2 つ以上使ってはならないというものです。

悪い例: $5 + 3$ （5 と 3 は数列の中で隣り合っているため）。
良い例: $5 + 2$ （5 と 2 の間には隙間があるため）。

この「連続禁止」のルールこそが、このトリック全体を可能にする秘密のソースです。

魔法のトリック：「偶数」と「奇数」の地区

著者のミラン・ロスコは、箱 X と箱 Y をフィボナッチ数列の異なる「地区」に配置することで、これらを単一の数値に詰め込む方法を開発しました。

偶数地区（箱 X）:
論文は、数値Xの設計図を取り出し、そのすべてのレゴピースをフィボナッチ数列の偶数番目の位置にシフトさせます。
- 比喩: X を本のセットだと想像してください。これらをすべて図書館の偶数番目の棚に置きます。
区切り（フェンス）:
箱 Y を入れる前に、X がどこまで広がっているかを知る必要があります。論文は、X の大きさに基づいて「フェンス」または区切りを計算します。このフェンスをBと呼びましょう。
- 比喩: X が棚 2 から棚 10 までを占めている場合、フェンスは棚 12 に建設されます。
奇数地区（箱 Y）:
次に、数値Yの設計図を取り出し、そのレゴピースを奇数番目の位置にシフトさせますが、フェンス（B）の後から始まる位置にのみ配置します。
- 比喩: Y 用の本をすべて奇数番目の棚に置きますが、フェンスより後の棚 13、15、17 などにのみ置きます。フェンスより前の奇数番目の棚は空のままにします。

なぜ「キャリーレス」なのか（最も素晴らしい部分）

通常の数学では、2 つの数値を足すと「桁上げ」が発生することがあります（例： $5+5=10$ ）。しかし、このフィボナッチシステムでは、「連続する」場所を共有しない 2 つの数値を足した場合、桁上げは発生しません。

論文では、X を偶数の棚に、Y を（その間に隙間を設けて）奇数の棚に配置するため、2 つのレゴピースのセットは決して接触しません。

X は偶数の場所にあります。
Y は（遠く離れた）奇数の場所にあります。
最終的な組み合わせの中に、連続する 2 つの数値は存在しません。

結果: 組み合わされた数値は、すでに完璧な「通常」の形式になっています。修正のための掃除や計算は不要です。2 つの接触しないパズルピースを組み合わせるようなもので、それらは完璧にフィットします。

詰め込みを解く方法（デコーディング）

元の箱を取り戻すには、組み合わされた数値を見て、2 つの簡単な質問に答えるだけです。

偶数の棚にいるのは誰か？（それが X です）。
フェンスの後の奇数の棚にいるのは誰か？（それが Y です）。

ルールが非常に厳格であるため（接触禁止、特定の隙間）、混乱は発生しません。どのピースが X に属し、どのピースが Y に属するかを常に正確に特定できます。

重要な制限（「全射ではない」部分）

この論文は、この方法があらゆる可能な数値のコードを作成するわけではないことを認めています。

比喩: 車（数値）が特定の場所だけに駐車できる駐車場を想像してください。「接触禁止」ルールや「フェンス」ルールに違反する場所に車を駐車しようとすると、その場所は空のままになります。
論文はこれを単射的だが全射的ではないと呼んでいます。
- 単射的: 任意の (X, Y) のペアには、一意のコードが割り当てられます。異なる 2 つのペアが同じ数値を作ることはありません。
- 全射的ではない: 世の中にあるすべての数値が、この方法で形成されるわけではありません。ランダムな数値を選んだ場合、それが有効な「詰め込まれた」ペアであるとは限りません。

ただし、論文は簡単なテストを提供しています。数値を解凍して、再び詰め込み直したときに、元の数値と完全に一致すれば、それは有効なペアでした。もし数値が変化すれば、最初から有効なペアではなかったということです。

なぜこれが重要なのか（「なぜ」）

著者は、あなたの携帯電話用のより高速な計算機を作ろうとしているわけではありません。動機は、論理と数学の基礎に深く根ざしています。

純粋な加算: 数値を組み合わせるほとんどの方法は、乗算や複雑な除算（素因数分解など）に依存しています。この方法は、加算のみと位置の確認に依存しています。
弱い数学システム: 乗算を使用することが許されない非常に基本的な論理システムでは、2 つの数値を結合して再び取り出すことができることを証明できません。この論文は、単純な加算のみを使用してそれを行う方法を示しており、論理が機能するために必要な絶対的な最小要件を理解する上で、数学者の助けとなります。
証明の検証: プロセスが非常に単純であるため（位置を見て加算するだけ）、コンピュータが混乱することなく、数学が正しいことを検証することが非常に容易です。

1 文で要約

この論文は、フィボナッチ数列を用いて 2 つの数値を 1 つに組み合わせる巧妙な方法を紹介しており、その 2 つの数値は互いに接触しない分離された「領域」に住むため、ごちゃごちゃした数学なしで加算でき、単にどこに座っているかを見るだけで引き離すことができます。

技術的概要：フィボナッチ基底におけるキャリーレスペアリング

問題定義
本論文は、ゼッケンドルフ（フィボナッチ）基底の加法的制約のみに厳密に従って動作するペアリング関数 $\pi: \mathbb{N}^2 \to \mathbb{N}$ の構成を取り扱います。従来のペアリング方式は、多くの場合、位置記数法における桁の交互配置（例：Z オーダー/モーコード）や、乗算および素因数分解を伴う算術演算（例：ゲーデル番号付け、カントールのペアリング）に依存しています。著者は、ペア $(x, y)$ の符号化と復号が、乗算、指数演算、およびデータ結合中の「キャリー」伝搬や正規化ステップを必要とせず、支持集合の抽出と加法的演算のみに依存するメカニズムを求めます。これは、乗算が仮定されていない、あるいは高コストである弱い算術基盤（ $I\Delta_0$ など）における不完全性論証や証明論的調査を支援したいという動機に基づいています。

手法
提案される解決策は「キャリーレスペアリング（ $\pi_{CL}$ ）」と称され、ゼッケンドルフ支持に基づき、2 つの自然数をフィボナッチ指数の互いに重ならない「バンド」に符号化します。

ゼッケンドルフ表現: 任意の自然数 $n$ は、連続しないフィボナッチ数 $F_k$ （ただし $k \ge 2$ ）の和として一意に表現されます。指数の集合を $Z(n)$ と表記します。
区切り文字の構築: ペア $(x, y)$ に対して、アルゴリズムはまず $r(x)$ を計算します。ここで $r(x)$ は $F_{r(x)} > x$ となる最小の指数と定義されます。区切り文字 $B(x)$ を $2r(x)$ に設定します。
バンドの分離:
- 偶数バンド（ $x$ 用）: $x$ の支持の指数 $Z(x)$ を、 $e \mapsto 2e$ によって偶数指数に写像します。これらは範囲 $[4, 2r(x))$ に配置されます。
- 奇数バンド（ $y$ 用）: $y$ の支持の指数 $Z(y)$ を、 $j \mapsto B(x) + (2j - 1)$ によって奇数指数に写像します。これらは区切り文字 $B(x)$ より厳密に上位に配置されます。
キャリーレス不変量: $Z(x)$ は連続する整数を含まないため、写像された偶数指数の間隔は少なくとも 4 になります。同様に、写像された奇数指数の間隔も少なくとも 4 になります。重要なのは、区切り文字 $B(x)$ により、 $x$ が使用する最大の偶数指数が、 $y$ が使用する最小の奇数指数より厳密に小さくなることを保証することです。その結果、これら 2 つの指数集合の和集合には連続する整数は含まれません。
符号化: 符号化された値は、これらの指数の和集合に対応するフィボナッチ数の和です。支持に連続する指数が含まれないため、結果は自動的にゼッケンドルフ正規形となり、キャリー伝搬は必要ありません。

主要な貢献

完全な加算デバイス: 本論文は、乗算や因数分解を用いず、加算と有界スキャンのみを使用してゼッケンドルフ支持上で動作するペアリング写像 $\pi_{CL}$ と逆写像 unpair を定義します。
単射性と決定可能性: 写像は単射であることが証明されています。全射ではありませんが、像への所属は「固定点テスト」を通じて決定可能です。すなわち、数 $n$ が像に含まれるのは、 $\pi_{CL}(\text{unpair}(n)) = n$ である場合に限られます。
1 ステップ正規化: 本論文は、正規化関数 $can(n) = \pi_{CL}(\text{unpair}(n))$ を導入します。この関数は、任意の自然数を $\pi_{CL}$ の像における一意の代表元へ 1 ステップで写像します。
安定性補題: 本論文は、2 番目の座標 $y$ を変更すること（支持から指数の追加または削除）が、 $x$ が固定されている限り、符号化された値に対する局所的な変化（特定のフィボナッチ数の加算または減算）をもたらすことを確立しています。
機械化: すべての核心的な正しさの定理（逆写像と単射性）は、Gallina 仕様言語を使用して Rocq（旧 Coq）で機械化されています。形式化には、ゼッケンドルフ支持の存在と一意性の証明が含まれており、ペアリングデバイスが支持インターフェースに関する証明されていない公理に依存しないことを保証しています。

結果

正しさ: 定理 6.0.1 は、unpair $\circ$ $\pi_{CL}$ が $\mathbb{N}^2$ 上の恒等写像であることを証明します。
非全射性: 写像は全射ではありません。多くの自然数（例：6）は、そのゼッケンドルフ支持が特定の偶奇性と区切り文字の制約に整合しないため、この方式における有効なペアに対応しません。
計算量: ペアリングとアンペアリングのコストは、主に支持抽出ステップ（通常、貪欲スキャンの場合 $O(r(n))$ ）によって支配されます。本論文は、これらが証明された計算量定理ではなく、形式的な観察であることを指摘しています。
比較: ゼッケンドルフ番号付け（因数分解が必要）やカントールのペアリング（乗算と平方根が必要）とは異なり、 $\pi_{CL}$ は純粋に加算的に動作します。Z オーダー（固定された 2 進位置を交互に配置する）とは異なり、 $\pi_{CL}$ は 1 番目のオペランドのランクに基づいて 2 番目のオペランドの位置をシフトさせ、動的な区切り文字を生成します。

意義と主張
本論文は、この構成を逆数学および弱い算術基盤の研究のためのツールとして位置づけています。乗算を回避するペアリング関数を提供することで、著者は、乗算が利用できない、または制限されているシステムにおける整合性論証や証明可能性の調査に有用である可能性を指摘しています（Buss, 1997; Friedman, 1976 を参照）。

著者は、より広範な含意については謙虚に述べています。

本論文は、ゼッケンドルフ支持インターフェース自体を加算のみの原理から導出するとは主張していません。そのような導出が存在しない可能性を仮定しています。
$\pi_{CL}$ の像の単純な閉形式による特徴付けを主張するものではありません。決定手続きは、支持に基づく固定点テストです。
主要な貢献は、「キャリーレス」デバイスの明示的な構築と、その性質の検証であり、これにより像とその幾何学的構造が理論的解析のために直接検査可能になります。

この研究は、一般的な計算のための実用的なデータ構造というよりも、論理と証明論における理論的有用性を強調する基礎的な算術デバイスとして提示されています。