Technical Summary: The Exact Complexity of Perfect Play in Nonlocal Games

1. Problem Statement

The paper addresses the decision problem of determining whether two separated players can win a finite nonlocal game with certainty (probability 1) under various quantum mechanical models. While the winning probability of a game is often studied as a supremum, this work focuses on perfect play: the existence of a strategy that attains a winning probability of exactly one.

The central question is: What is the exact level of the arithmetical hierarchy required to decide the existence of a perfect strategy for a given finite rational Boolean game?

The authors analyze this across several models:

• Finite-dimensional ($PERF_q$): Strategies on finite-dimensional Hilbert spaces.
• Spatial ($PERF_{qs}$): Normal strategies on infinite-dimensional tensor products (spatial model).
• Commuting ($PERF_{co}$): Strategies defined by commuting operator algebras on a single Hilbert space.
• Von Neumann Type: Strategies hosted by specific types of von Neumann algebras (Type I, II, III).
• Resource Constraints: Variants requiring finite marginal entropy or finite $\alpha$-moments of the reduced density matrix.

2. Methodology

The paper employs a combination of operator algebra, computability theory, and a novel "compiler" construction to establish complexity bounds.

2.1 The Compiler Construction

A core technical contribution is a finite compiler that translates operator-theoretic presentations into finite nonlocal games.

• Input: An admissible presentation consisting of centralizer labels (unitaries, projections, contractions) and rational $*$-polynomial equations, including modular relations of the form $h A_\alpha = \nu A_\alpha h$ (where $h$ is a density and $\nu$ is a scaling factor).
• Mechanism: The compiler uses flagged magic-square (FMS) bridges to enforce density scaling. A chain of $n$ bridges forces a density ratio of $2^n$ between source and target corners. This allows the construction of "modular isometries" that transport operators while scaling the density.
• Output: A finite rational Boolean game where a perfect normal spatial strategy exists if and only if the input presentation has a normal realization.
• Soundness and Completeness: The compiler ensures that any perfect strategy in the game extracts a valid operator realization, and any valid realization can be extended to a perfect strategy (often by adjoining finite ancillary factors).

2.2 Complexity Analysis via Quantifiers

The authors analyze the logical structure of the existence conditions:

• $\Pi^0_1$ (Co-recursively enumerable): Conditions where a counter-example can be found in finite time (e.g., failure of a convergent hierarchy).
• $\Sigma^0_2$ (Recursively enumerable in the halting problem): Conditions of the form $\exists \kappa \forall d \, R(G, \kappa, d)$, where $\kappa$ is an existential integer witness and $d$ ranges over finite tests.

2.3 Hardness Reductions

To prove $\Sigma^0_2$-completeness, the authors construct games based on the Fock clock and a rooted tree:

• The Tree: A tree of finite words where density weights decay geometrically.
• The Clock: A Weyl pair $(J_W, K_W)$ and a phase operator $Z_{clk}$ acting on the root space. The commutation relations force the phase of $Z_{clk}$ to be a root of unity of order $d_{clk}$.
• The Reduction: The game encodes a decidable predicate $R_{dec}(e, j, t)$. A perfect strategy must "choose" a clock order $d_{clk}$ (the existential witness $\kappa$) such that for all time steps $t$, the computation halts or satisfies the predicate. The hardness arises because no computable function can bound the sufficient clock order $d_{clk}$ for all YES instances.

3. Key Contributions and Results

3.1 Main Theorems on Complexity Classes

The paper establishes the exact arithmetical complexity for perfect play in various models (Table 1 in the paper):

Model / Condition	Complexity Class	Key Finding
Finite-Dimensional ($PERF_q$)	$\Sigma^0_1$-complete	Decidable with an oracle for the halting problem (search over dimension).
Commuting ($PERF_{co}$)	$\Pi^0_1$-complete	Decidable with a convergent hierarchy; failure is detectable in finite steps.
Spatial ($PERF_{qs}$)	$\Sigma^0_2$-complete	Strictly harder than both finite-dimensional and commuting models. Requires an existential integer witness (e.g., a bound on the inverse of the largest Schmidt coefficient).
Semifinite Hosts ($PERF_{sf}$)	$\Sigma^0_2$-complete	Includes Type II$_1$, II$_\infty$, and general semifinite algebras.
Type III Factors ($PERF_{III_\lambda}$)	$\Pi^0_1$-complete	Collapses to the commuting model complexity.
Finite Entropy ($PERF_{finS}$)	$\Sigma^0_2$-complete	Perfect play with finite marginal entropy is also $\Sigma^0_2$-complete.
Finite $\alpha$-Moments ($P_\alpha$)	$\Sigma^0_2$-complete	For any fixed computable $0 < \alpha < 1$, perfect play with $\text{Tr}(h^\alpha) < \infty$ is $\Sigma^0_2$-complete.

3.2 The "Trace Cost"

The paper argues that a trace costs exactly one existential quantifier.

• In the spatial model, the existence of a perfect strategy requires bounding the largest Schmidt coefficient (or equivalently, the overlap with a finite corner in semifinite algebras). This bound acts as the existential witness $\kappa$.
• In Type III algebras, there are no finite corners (no trace), and the language collapses to $\Pi^0_1$ (commuting perfection).
• The authors construct a "strict ladder" of resource conditions: $P_0 \subsetneq P_\alpha \subsetneq P_1 \subsetneq P_{normal}$, where $P_0$ is finite rank, $P_\alpha$ is finite $\alpha$-moment, and $P_1$ is finite entropy. All intermediate steps remain $\Sigma^0_2$-complete.

3.3 Zero-Error Communication

The results extend to one-shot zero-error communication:

• Deciding the existence of a zero-error code with normal entanglement is $\Sigma^0_2$-complete.
• The authors construct a finite classical channel where a zero-error code exists with normal entanglement, but every such code requires infinite marginal entropy. This demonstrates a separation between the existence of a code and the finiteness of its entanglement resources.

3.4 Formal Verification

The authors provide formal verification of Theorem A (Spatial Perfection) in Lean 4. The proof uses no axioms beyond Lean's standard three (propext, Classical.choice, Quot.sound). The verification covers the compiler contract, the upper bounds (compactness arguments), and the hardness reduction.

4. Significance and Claims

The paper claims to resolve the exact computational complexity of perfect play in nonlocal games, revealing a non-monotonic hierarchy of difficulty:

1. Non-Monotonicity: The spatial model, which sits between finite-dimensional and commuting models in terms of correlation sets, is strictly harder to decide for perfect play than either.
   • Finite-dimensional: $\Sigma^0_1$
   • Commuting: $\Pi^0_1$
   • Spatial: $\Sigma^0_2$
2. The Necessity of the Quantifier: The hardness proofs demonstrate that the existential quantifier is not an artifact of the proof technique but is necessary. No computable function can bound the "clock period" or "Schmidt stratum" required for a perfect strategy.
3. Resource Separation: The work distinguishes between the existence of a perfect strategy and the resources it consumes. It shows that perfect spatial play can exist even when finite-dimensional strategies fail, and even when finite-entropy strategies do not exist.
4. Operational Split: The paper identifies a sharp operational split between semifinite algebras (where a trace exists and complexity is $\Sigma^0_2$) and Type III factors (where no trace exists and complexity drops to $\Pi^0_1$).

The authors emphasize that these results are about attainment (winning with probability 1), not just the supremum of winning probabilities. They clarify that while the supremum might be 1, the strategy achieving it may not exist in certain models, and the decision of whether it exists in the spatial model is undecidable even with an oracle for the halting problem.

5. Limitations and Open Problems

The paper acknowledges several open questions:

• Asymptotic Capacity: The results apply to one-shot zero-error communication; the computability of the asymptotic entanglement-assisted zero-error capacity remains open.
• Prescribed Tables: The complexity of deciding membership for specific prescribed correlation tables (rather than just existence of some perfect strategy) is not fully resolved for all cases, particularly regarding uniformity over scenarios.
• Optimal Bounds: The paper does not provide optimal effective bounds for the size of the reduction games or the required Schmidt strata, only their existence.

In summary, the paper provides a rigorous classification of the decision problems surrounding perfect quantum strategies, establishing that the presence of a trace (or the ability to bound the largest Schmidt coefficient) elevates the complexity from $\Pi^0_1$ or $\Sigma^0_1$ to $\Sigma^0_2$, making perfect spatial play fundamentally undecidable by any algorithm with a halting problem oracle.