Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound

技術要約：最小Kochen–Specker境界の幾何学的半分に対する機械検証済み証明書

問題表明

最小Kochen–Specker (KS) 問題は、$\mathbb{R}^3$ における非ゼロベクトル $n$ 個の最小数を求めるものである。ここで、各ベクトルは半直線として互いに異なり、その直交グラフは、すべての直交ペアが最大で1つの $1$を含み、すべての直交トライアドが正確に1つの$1$を含むような${0, 1}$-彩色を持たない。既知の最良の下界は$n \ge 24$ であり、これは Li らおよび Kirchweger らによって計算機的に確立されている。

この証明は2つの部分から構成される：

1. 組合せ論的部分： 次数23までの候補グラフに対する、同型自由なSAT列挙。充足不能の結果には、独立して検証可能なDRAT証明が伴う。
2. 幾何学的部分： 列挙されたすべての候補グラフが $\mathbb{R}^3$ に埋め込み不可能であることを示す。この部分は、非ゼロかつ半直線として異なるベクトルの割り当てにおいて、直交制約を満たすものが存在しないことを決定するために、Z3の非線形実算術 (NRA) ソルバーに依存している。

本研究で特定された決定的なギャップは、幾何学的部分が検証可能な証明オブジェクトを生成しないことである。信頼の連鎖は $\exists\mathbb{R}$-hardな理論に対するZ3の決定手続きで終了しており、コミュニティは非埋め込みの判定を信頼に基づいて受け入れざるを得ない。さらに、公開されているパイプラインは、最小の非埋め込み部分グラフの「ブロッキング・データベース」に依存しているが、これもZ3由来であり、検証されていない。

手法

著者らは、実数の非埋め込み性に対する厳密な有理数ケースツリー証明書を生成および検証するためのフレームワークを導入する。この手法は、不透明なZ3の決定手続きを、透明な代数的検証プロセスに置き換えるものである。

1. 証明書の構造
証明書は、以下の要素からなる自己完結型のオブジェクトである：

• アンカーと伝播： 正規化ステップ（直交トライアドまたはエッジの固定）に続き、外積と平面のパラメータ化を用いて、少数のパラメータによってすべての頂点ベクトルを表現する伝播スケジュール。
• ケースツリー： 内部ノードが以下の条件に基づく分岐を表すツリー構造：
  • 因数分解： $p = \prod f_k$。展開によって検証される。
  • 平方和 (SOS)： $p = \sum c_k m_k^2$（ただし $c_k \in \mathbb{Q}_{>0}$）。展開によって検証される。
• リーフ（葉）： 枝は以下の4つのメカニズムのいずれかによって閉じられる：
  • 単射衝突 (Injectivity Collision)： 2つの異なる頂点が平行な半直線へと写ることを証明する。
    数式が恒等的にゼロであることを示す。
  • イデアル所属 (Ideal Membership)： 多項式が制約によって生成されるイデアルに含まれることを示す明示的な余因子。
  • Positivstellensatz型の正値性： 正の項の和（単射多項式）が平方和の和に等しいことを示し、実数点において矛盾を導く一般化された議論。

2. 検証アーキテクチャ
システムは、証明書生成器とコードを共有しない2つの独立したチェッカーを採用している：

• Pure-Python 再演： 厳密な有理数演算を用いて証明書のロジックを実行する。
• Lean 4 完全チェッカー： Lean 4 証明助手で実装されたリフレクティブ関数 Cert.check。
  • カーネル還元可能性： 判定が閉じたカーネル定理であることを保証するため、著者らは gcd-free な有理数演算レイヤー (KRat) と燃料構造再帰 (fuel-structural recursion) を実装した。これにより、ネイティブな簡約やカスタム公理を用いることなく、計算全体をLeanカーネルによって還元できる。
  • 公理の閉包： 正当性定理は {propext, Classical.choice, Quot.sound} のみに依存し、検証されていないネイティブな簡約を回避している。

3. 正当性定理
中核となる定理 check_sound は、check c = true であれば、グラフの実装が存在しないことを述べる。実装とは、非ゼロベクトル、エッジ上の直交性、およびすべての頂点ペアに対する相互の半直線としての相異性（単射性）を満たす $\mathbb{R}^3$ への写像として定義される。

主な貢献

1. 厳密な有理数証明書： 数値近似や不透明なソルバーを、厳密な有理数演算、多項式の因数分解、およびSOS分解に置き換える証明書形式の導入。
2. ブロッキング・データベースの完全な網羅： 公開されているPhysicsCheckのブロッキング・リスト（次数10–13）に含まれる全291行（180の異なるグラフを代表）の証明。すべてのZ3の判定を機械検証済みの定理に置き換えた。
3. 二重の独立した再演： PythonとLeanという2つの異なるチェッカーによる検証。これらは、正当な証明書を受け入れる一方で、115個の敵対的な変異（例：係数の改ざん、枝の削除）を拒絶した。
4. 定式化による発見： 厳密な定式化により、元のパイプラインにおける特定の問題が明らかになった：
   • 単射性の重要性： 元のZ3エンコーディングは、隣接するペアだけでなく、すべてのペアに対して半直線としての相異性を強制していた。データベース内のいくつかのグラフは、この単射性の制約のみによって非埋め込みとなっており、これは標準的な幾何学的ソルバーでは不可視なニュアンスである。
   • 隠れたWLOGケース： 元のパイプラインで使用された直交平面のパラメータ化は、単射性の議論によって明示的に解消されるべき退化ケース（平行なベクトル）を隠蔽していた。
   • 経験的最適化： 元のパイプラインにおける「非彩色性」の最適化は、負荷を担う補題ではなく、経験的なものであることが判明した。
   • 再現可能なカウント： 公開されていた最終的な次数23の候補数（41）は、アーティファクトから再現不可能であった。正しい数は43であり、そのうち42は新しい次数13の証明書によって解消されている。

結果

• 検証範囲： ブロッキング・データベース内の全180の異なるグラフについて、非埋め込み性を証明する閉じたカーネル定理が現在存在する。
• パフォーマンス： 標準的なノートPCにおいて、カーネル評価のコストは次数10/11/12のグラフで約0.5秒、次数13のグラフで1.8秒である。検証スイート全体は数分で完了する。
• 境界への影響： 7つの新しい次数13の証明書は、検証済みの部分グラフ単調性を通じて、次数22/23の列挙における44個の候補のうち42個を解消する。残りの2つの候補は、明示的な機械可読の義務として追跡されている。
• 敵対的堅牢性： 両方のチェッカーは、継続的インテグレーションにおいて115個の変異した証明書をすべて拒絶することに成功し、検証ロジックが単なる生成器の出力の再演ではなく、真に独立したチェックであることを示した。

意義

本論文は、ブロッキング・データベースに関する最小KS境界の幾何学的半分についての信頼のギャップを埋めるものである。検証されていないZ3の判定を閉じたカーネル定理に変換することで、本研究は、決定的な部分グラフの非埋め込み性が、もはやブラックボックス・ソルバーへの信頼の問題ではないことを保証している。

著者らは、定式化のプロセス自体が主要な価値の源泉であり、元のワークフローでは不可視であった隠れた仮定（単射性）、隠れたケースの義務、およびデータの不一致を浮き彫りにしたことを強調している。本論文は（SAT列挙の規模と標準性の証明のため）$n \ge 24$ に対する完全に検証されたエンドツーエンドの定理をまだ構成していないが、検証済みの幾何学的基盤を確立し、スケーラブルな進むべき道を示している。本研究は、量子基礎論における複雑な幾何学的推論が、厳密な算術と最小限の公理を用いて、完全に機械検証可能にできることを示している。