The Four-Qubit Hyperbolic Quadric Has Contextuality Degree 315

技術要約：4量子ビット双曲型二次曲面のコンテクチュアリティ次数は315である

問題設定
本論文は、4量子ビット双曲型二次曲面 $Q^+(7, 2)$ の**コンテクチュアリティ次数（contextuality degree）**の計算に取り組んでいる。コッヘン・スペッカー（Kochen–Specker）定理の文脈において、パウリ・コンテクストの集合に対するコンテクチュアリティ次数は、非コンテクシュアルな $\pm 1$ の割り当てが最小でいくつのコンテクストを違反するかとして定義される。4量子ビット系において、観測量はシンプレクティック極空間 $W(7, 2)$ の点に対応し、双曲型二次曲面 $Q^+(7, 2)$ は135個の点（実パウリ観測量）と1575個の直線（コンテクスト）から構成される。

本研究以前、この構成の正確な次数は未知であった。Mullerら [44] によるヒューリスティック探索は、315という上界を示唆し、最適な割り当てにおける違反コンテクストの集合が双対極空間 $DW(5, 2)$ を形成するという予想を立てていた。しかし、この問題はSATソルバーや疎な線形代数による直接的な計算では解決できず、これまでの試みでは500の上界を示すにとどまっていた。

手法
著者らは、有限幾何学、組合せ論的平均化、およびコンピュータ支援による検証を組み合わせたハイブリッド・アプローチを採用している。

1. 幾何学的平均化（下界）:
   下界の証明の核となるのは、二次曲面内に埋め込まれたドイリー（doilies）（一般化四角形 $GQ(2, 2)$）の構造である。

   • 著者らは、すべてのドイリーが10個のペレス・メーレン・グリッド（Peres–Mermin grids）（$GQ(2, 1)$）を含むという事実を利用している。
   • パリティ引数（補題5）とこれらのグリッドの性質（補題6）を用いることで、単一のドイリー内において、いかなる割り当ても少なくとも3本の直線を違反することを証明している。
   • 決定的なことに、補題8は、二次曲面のすべての直線が特定のドイリー内のちょうど4つのグリッドによってカバーされていること、およびドイリーが15本の直線を含むことを示している。
   • 40,320個のドイリー全体で違反数を平均化し、ウィットの定理を用いて直交群が直線に対して推移的に作用することを活用することで、以下のタイトな下界を導出している：
     $$\text{deg} \ge \frac{3 \times (\text{ドイリーの数})}{\text{ドイリーあたりの直線数}} \times \frac{\text{ドイリーあたりの直線数}}{\text{全直線数}} = \frac{3}{15} \times 1575 = 315.$$
   • この議論は、グローバルな最適化問題をドイリーによるローカルな制約へと還元することで、網羅的な探索を回避している。

2. SATエンコーディングと列挙（上界および分類）:
   著者らは、幾何学的知見をSATエンコーディングへと翻訳している：

   • 直接的なMaxSAT定式化（30分以内の解決に失敗したもの）の代わりに、局所的な基数制約を課すために命題14を用いている。これは「すべてのドイリーは、ちょうど3本の違反直線を含む」というものである。
   • さらに、命題10から導かれる冗長な**ペア節（pair clauses）**を追加し、ドイリー内の3本の直線が互いに素である（ルーリングを形成する）ことを強制している。
   • このエンコーディングと、解を列挙するためのブロッキング節を組み合わせることで、SATソルバー（CaDiCaL）は、停止に失敗することなく、数秒ですべての最適解を見つけることができる。
   • 列挙の完全性（他の解が存在しないことの証明）は、drat-trim によって検証された DRAT証明 によって保証されている。

3. 形式検証:
   下界の証明および次数の定義は、Mathlibライブラリを用いた Lean 4 において形式化されている。Leanカーネルは、グリッド構造やパリティ引数を含むすべての有限な事実を独立して検証しており、この証明が未検証の計算ステップを含まず、標準的な公理のみに基づいていることを保証している。

主要な結果

• 定理11: 4量子ビット双行型二次曲面 $Q^+(7, 2)$ のコンテクチュアリティ次数は、正確に 315 である。
• 定理15: 最小値を達成する違反直線の集合は、正確に 240 通り存在する。これらの集合は、直交群 $O^+(8, 2)$ の下で単一の軌道を形成する。各集合は、双対極空間 $DW(5, 2)$ と同型である。
• 命題14: 割り当てが最適であるための必要十分条件は、二次曲面のすべてのドイリーにおいて、ちょうど3本の直線が違反しており、それらがドイリーのいずれかのグリッドのルーリングを形成していることである。
• 定理17: 著者らは下界を $N \ge 3$ 量子ビットのすべての二次曲面に一般化し、次数は少なくとも $\lceil L/5 \rceil$ （ここで $L$ は直線の数）であることを証明した。この境界は、$N=3$ および4量子ビット双曲型二次曲面においてタイトである。
• 系18: この構成は、古典的境界が945、量子値が1575である状態独立非コンテクシュアル不等式をもたらす。いかなる非コンテクシュアルな割り当ても、コンテクストの最大 $4/5$ しか満たさない。

意義および主張
本論文は、4量子ビット双曲型二次曲面のコンテクチュアリティ次数に関する長年の予想を解決したと主張している。その主な貢献は以下の通りである：

1. 計算上の障壁の解消: 直接的なソルバーによる攻撃に抵抗した問題を、まず数学的な下界を導出し、その下界を用いてSATエンコーディングを構造化することによって解決できることを示した。「数学が最適化問題を完全に決定し」、ソルバーには最適解の分類のみを残す。これにより、制約を与えた後にのみ実行可能となる。
2. 平均化原理のタイト性: ドイリーによる平均化原理が、4量子ビット双曲型二次曲面においてタイトであることを示し、より高次元の二次曲面に対する最初の正確な下界を提供した。
3. 形式的厳密性: 著者らは、Lean 4 を用いた機械検証可能な証明と、最適集合の列挙のための認定されたDRAT証明を提供しており、組合せ論的証明と形式検証の組み合わせの標準を確立している。
4. 幾何学的特性: 最適なモデルにおける「満たされない」構成はランダムではなく、硬直した幾何学的構造（$DW(5, 2)$）を形成していることを確認した。これは、満たされない直線がスプリット・ケイリー・ヘキサゴンを形成するという3量子ビットの図式を拡張するものである。

著者らは将来的な影響については控えめな姿勢を保っており、この境界は双曲型二次曲面についてはタイトであるが、楕円型二次曲面や $N \ge 5$ 量子ビットにおいてタイトであるかどうかは未解決の問題であると述べている。彼らは新しい実験セットアップを提案しているのではなく、この規模の構成において古典的境界が945であることは正確であり、理論的ベンチマークとして重要であることを強調している。