A trace costs one quantifier: the exact complexity of perfect play in nonlocal games
Seth Douglas, Nidhal Mghirbi
quant-ph
Nov 7, 2026 · v1
math.LO math.OA
TL;DR
Main theorem (Σ⁰₂-completeness of perfect spatial play, with and without finite entropy) is proved in Lean 4 with Mathlib, axiom-free beyond standard axioms, and kernel-checked independently.
Abstract
Given a finite nonlocal game, can the players win with certainty? We prove that the existence of a perfect normal spatial strategy is $Σ^0_2$-complete, even when restricted to games of value one, so it cannot be decided even with an oracle for the halting problem. This is strictly harder than perfect play in the finite-dimensional and commuting-operator models, which are $Σ^0_1$-complete and $Π^0_1$-complete. Within the commuting model, the existence of a perfect normal strategy with a finite or semifinite von Neumann host is $Σ^0_2$-complete, whereas for every fixed type $\mathrm{III}_λ$ subtype it has the same $Π^0_1$-complete language as unrestricted commuting play. A trace thus costs one existential number quantifier: the hardness constructions force every perfect strategy to choose a finite clock period or a finite tree depth. Spatial $Σ^0_2$-completeness also holds when finite entanglement entropy is required, and both forms are formally verified in Lean. For every computable $0<α<1$, perfect spatial play with $\mathrm{Tr}\,h^α<\infty$ for the reduced density $h$ is $Σ^0_2$-complete as well; these conditions form a strict ladder between finite rank and finite entropy. We also prove $Σ^0_2$-completeness for one-shot zero-error communication with normal entanglement, and construct a finite channel with zero-error codes of a given size each of which needs infinite entanglement entropy.
Problem
The question is how hard it is to decide whether a finite nonlocal game admits a perfect quantum strategy, and how the answer depends on the model: finite-dimensional, normal spatial, commuting-operator, or a von Neumann algebra host type.
Approach
Upper bounds come from stratifying strategies by an integer bound on the inverse largest Schmidt probability, or on the inverse tracial-corner overlap; each stratum is compact and Π⁰₁. Hardness comes from a finite game compiler that turns operator presentations into games. The compiled presentations are a rooted four-ary tree ('Fock clock') and a Weyl clock with finite period, which together encode Σ⁰₂ predicates. The main theorem is formalized in Lean 4 (version 4.35.0) with a pinned Mathlib commit, and selected lemmas are also checked.
Results
Perfect normal spatial play is Σ⁰₂-complete, also when finite entanglement entropy is required, and so is finite or semifinite-host play. Fixed type III_λ hosts give Π⁰₁-complete problems. Analogous Σ⁰₂-completeness holds for Bell-functional attainment and zero-error communication. The Lean proof of Theorem A depends only on propext, Classical.choice and Quot.sound, and passes the leanchecker and nanoda kernel checkers.
| Decision problem | Complete class |
|---|
| Perfect finite-dimensional strategy | Σ⁰₁ |
| Perfect commuting strategy | Π⁰₁ |
| Perfect spatial strategy (also finite entropy) | Σ⁰₂ |
| Perfect play in semifinite algebra | Σ⁰₂ |
| Perfect play in type III_λ factor | Π⁰₁ |
Complexity of perfect play by model
