技術要約：非局所ゲームにおける完全なプレイの正確な複雑性

1. 問題設定

本論文は、分離されたプレイヤーが、様々な量子力学的モデルの下で、有限の非局所ゲームに（確率1で）確実に勝利できるか否かを判定する決定問題を取り扱う。ゲームの勝率（winning probability）はしばプローチ（supremum）として研究されることが多いが、本研究では完全なプレイ（perfect play）、すなわち、勝率が正確に1に達する戦略が存在することに焦点を当てる。

中心となる問いは、与えられた有限の有理的ブールゲームに対して、完全な戦略が存在するかどうかを判定するために、算術階層のどのレベルが必要か？ ということである。

著者らは、以下のモデルにおける複雑性を分析している：

• 有限次元 ($PERF_q$): 有限次元ヒルベルト空間上の戦略。
• 空間的 ($PERF_{qs}$): 無限次元テンソル積上のノーマル戦略（空間的モデル）。
• 交換 ($PERF_{co}$): 単一のヒルベルト空間上の交換演算子代数によって定義される戦略。
• フォン・ノイマン型: 特定の型（Type I, II, III）のフォン・ノイマン代数にホストされる戦略。
• リソース制約: 有限のマージナル・エントロピーまたは簡約密度行列の有限の $\alpha$ モーメントを要求する変種。

2. 手法

本論文は、演算子論的な提示を有限の非局所ゲームへと翻訳する、演算子論、計算理論、および新しい「コンパイラ」構成の組み合わせを採用している。

2.1 コンパイラ構成

技術的な核心となる貢献は、演算子論的な提示を有限の非局所ゲームへと変換する有限コンパイラである。

• 入力: 中心化ラベル（ユニタリ、射影、コントラクション）と、$h A_\alpha = \nu A_\alpha h$（ここで $h$ は密度、$\nu$ はスケーリング係数）のようなモジュラー関係を含む有理的 $*$-多項式からなる、許容された提示。
• メカニズム: コンパイラは、密度のスケーリングを強制するためにフラグ付きマジックスクエア（FMS）ブリッジを使用する。$n$ 個のブリッジの連鎖は、ソースとターゲットのコーナー間で密度の比を $2^n$ 強制する。これにより、演算子を輸送しながら密度をスケーリングする「モジュラー等長写像（modular isometries）」を構築することが可能になる。
• 出力: ノーマルな空間的戦略が存在する場合に限り、入力の提示がノーマルな実現を持つような、有限の有理的ブールゲーム。
• 健全性と完全性: コンパイラは、ゲームにおけるあらゆる完全な戦略が有効な演算子実現を抽出し、かつ、あらゆる有効な実現が（多くの場合、有限の補助的な因子を付加することで）完全な戦略へと拡張可能であることを保証する。

2.2 量化子による複雑性分析

著者らは、存在条件の論理構造を分析している：

• $\Pi^0_1$ (共再帰的列挙可能): 有限の時間内に反例が見つけられる条件（例：収束する階層の失敗）。
• $\Sigma^0_2$ (停止問題に関する再帰的列挙可能): $\exists \kappa \forall d \, R(G, \kappa, d)$ の形式の条件。ここで $\kappa$ は存在的な整数証拠であり、$d$ は有限のテストの範囲を動く。

2.3 困難性の還元

$\Sigma^0_2$-完全性を証明するために、著者らは**フォック・クロック（Fock clock）と根付き木（rooted tree）**に基づくゲームを構築している：

• 木: 密度重みが幾何級数的に減少する有限単語の木。
• クロック: ルート空間上で作用するワイル対 $(J_W, K_W)$ と位相演算子 $Z_{clk}$。交換関係は、$Z_{clk}$ の位相が位数 $d_{clk}$ の冪根であることを強制する。
• 還元: ゲームは決定可能な述語 $R_{dec}(e, j, t)$ をエンコードする。完全な戦略は、すべての時刻ステップ $t$ において、計算が停止するか、あるいは述語を満たすような、クロックの位数 $d_{clk}$（存在的な整数証拠 $\kappa$）を「選択」しなければならない。困難性は、すべてのYESインスタンスに対して、計算可能な関数では十分なクロックの位数 $d_{clk}$ を制限できないことに起因する。

3. 主な貢献と結果

3.1 複雑性クラスに関する主要な定理

本論文は、様々なモデルにおける完全なプレイの正確な算術的複雑性を確立している（論文内の表1）：

モデル / 条件	複雑性クラス	主要な知見
有限次元 ($PERF_q$)	$\Sigma^0_1$-完全	停止問題に対するオラクルを用いて決定可能（次元に関する探索）。
交換 ($PERF_{co}$)	$\Pi^0_1$-完全	収束する階層を用いて決定可能。失敗は有限ステップで検出可能。
空間的 ($PERF_{qs}$)	$\Sigma^0_2$-完全	有限次元および交換モデルの両方よりも厳密に困難。存在的な整数証拠（例：最大のシュミット係数の逆数の上界）を必要とする。
半有限ホスト ($PERF_{sf}$)	$\Sigma^0_2$-完全	Type II$_1$, II$_\infty$, および一般的な半有限代を含む。
Type III 因子 ($PERF_{III_\lambda}$)	$\Pi^0_1$-完全	交換モデルの複雑性に崩壊する。
有限エントロピー ($PERF_{finS}$)	$\Sigma^0_2$-完全	有限のマージナル・エントロピーを持つ完全なプレイも $\Sigma^0_2$-完全である。
有限 $\alpha$ モーメント ($P_\alpha$)	$\Sigma^0_2$-完全	計算可能な任意の $0 < \alpha < 1$ に対して、$\text{Tr}(h^\alpha) < \infty$ を伴う完全なプレイは $\Sigma^0_2$-完全である。

3.2 「トレースのコスト」

本論文は、トレースは正確に一つの存在量化子をコストとして支払うと論じている。

• 空間的モデルでは、完全な戦略の存在は、最大のシュミット係数（または、半有限代における有限のコーナーとのオーバーラップ）を制限することを要求する。この制限が、存在的な証拠 $\kappa$ として機能する。
• Type III 代数には、有限のコーナー（トレース）が存在しないため、言語は $\Pi^0_1$（交換的な完全性）へと崩壊する。
• 著者らは、「厳格な梯子（strict ladder）」となるリソース条件を構築している：$P_0 \subsetneq P_\alpha \subsetneq P_1 \subsetneq P_{normal}$。ここで、$P_0$ は有限ランク、$P_\alpha$ は有限 $\alpha$ モーメント、$P_1$ は有限エントロピーである。これらの中間ステップはすべて $\Sigma^0_2$-完全である。

3.3 ゼロエラー通信

これらの結果は、ワンショットのゼロエラー通信にも拡張される：

• ノーマルなもつれ（entanglement）を持つゼロエラー符号の存在を判定することは $\Sigma^0_2$-完全である。
• 著者らは、ノーマルなもつれを持つゼロエラー符号が存在するが、あらゆるそのような符号が無限のマージナル・エントロピーを必要とする有限の古典チャネルを構築している。これは、コードの存在と、それが消費するもつれリソースの有限性の間の分離を示している。

3.4 形式検証

著者らは、Theorem A（空間的完全性）のLean 4による形式検証を提供している。この証明は、Leanの標準的な3つの公理（propext, Classical.choice, Quot.sound）以外の公理を使用していない。検証は、コンパイラの契約、上界（コンパクト性の議論）、および困難性の還元をカバーしている。

4. 意義と主張

本論文は、非局所ゲームにおける完全なプレイの正確な計算複雑性を解決したと主張しており、非単調な難易度の階層を明らかにしている：

1. 非単調性: 相関集合の観点からは有限次元モデルと交換モデルの中間に位置する空間的モデルは、完全なプレイを決定するという点において、そのどちらよりも厳密に困難である。
   • 有限次元: $\Sigma^0_1$
   • 交換: $\Pi^0_1$
   • 空間的: $\Sigma^0_2$
2. 量化子の必要性: 困難性の証明は、存在量化子が証明技法の副産物ではなく、不可欠なものであることを示している。すべてのYESインスタンスに対して、完全な戦略に必要な「クロック周期」や「シュミット層（Schmidt stratum）」を制限できる計算可能な関数は存在しない。
3. リソースの分離: 本研究は、完全な戦略の存在と、それが消費するリソースを区別している。空間的プレイは、有限次元戦略が失敗する場合や、有限エントロピー戦略が存在しない場合でも存在し得ることを示している。
4. 運用的分割: 論文は、半有限代（トレースが存在し、複雑性が $\Sigma^0_2$）とType III 因子（トレースが存在せず、複雑性が $\Pi^0_1$ に低下する）の間の明確な運用的分割を特定している。

著者らは、これらの結果が単なる勝率の最高値（supremum）ではなく、到達（attainment）（確率1での勝利）に関するものであることを強調している。彼らは、最高値が1であっても、特定のモデルではそれを達成する戦略が存在しない可能性があること、そして空間的モデルにおいてその存在を決定することは、停止問題に対するオラクルを用いても決定不能であることを明確にしている。

5. 限界と未解決問題

本論文はいくつかの未解決の問いを認めている：

• 漸近容量: 結果はワンショットのゼロエラー通信に適用される。もつれを補助とする漸近的なゼロエラー容量の計算可能性は未解決のままである。
• 規定されたテーブル: （単にある完全な戦略の存在ではなく）特定の規定された相関テーブルに対するメンバーシップ判定の複雑性は、シナリオに関する一様性の観点から、すべてのケースにおいて完全には解決されていない。
• 最適境界: 論文は、還元ゲームのサイズや、必要とされるシュミット層の有効な境界を提示しておらず、それらの存在のみを示している。

要約すると、本論文は完全な量子戦略を巡る決定問題の厳密な分類を提供し、トレースの存在（または最大のシュミット係数を制限できる能力）が、複雑性を $\Pi^0_1$ または $\Sigma^0_1$ から $\Sigma^0_2$ へと押し上げ、完全な空間的プレイを停止問題のオラクルを持ついかなるアルゴリズムによっても根本的に決定不能にすることを確立している。