A trace costs one quantifier: the exact complexity of perfect play in nonlocal games

Douglas, Seth; Mghirbi, Nidhal

doi:10.5281/zenodo.23962890

Results · The price of perfection · Finite games and operator-algebra type · Quantum channels and memory

A trace costs one quantifier: the exact complexity of perfect play in nonlocal games

Seth Douglas and Nidhal Mghirbi · version 1.0.0 · Zenodo, 4 November 2026 · 117 pages · doi:10.5281/zenodo.23962890 · PDF

In plain wordsNo computer can tell from a finite win-or-lose game’s rules whether two players sharing an entangled state of two possibly infinite quantum systems can win it every time, not even one that could solve the halting problem; the paper finds exactly how hard the question is for each standard model of quantum players, and the same difficulty for sending a fixed number of messages through a channel used once with no chance of error. Whether the algebra of the players’ measurements has a trace changes the answer: in the paper’s words, a trace costs one existential quantifier.

The result

As the paper states it, in briefGiven a finite nonlocal game, can the players win with certainty? We find the exact level of the arithmetical hierarchy at which this is decided, for each standard model of quantum strategy. With normal states on tensor products of Hilbert spaces, perfect play is Σ⁰₂-complete, also when the strategy must have finite entanglement entropy, so it cannot be decided even with an oracle for the halting problem. This completes a table in which finite-dimensional perfection is Σ⁰₁-complete, commuting perfection is Π⁰₁-complete and value one is Π⁰₂-complete. Inside the commuting model the answer depends on the von Neumann type of the players' algebra: perfect play in a type II₁ algebra, or in any semifinite algebra, is Σ⁰₂-complete, while in a type III_λ factor, for each fixed λ ∈ [0,1], it is equivalent to commuting perfection. In this sense a trace costs one existential quantifier. Commuting perfect play without semifinite perfect play is Π⁰₂-complete; the remaining semifinite-without-spatial differences are D₂(Σ⁰₂)-complete. In the hardness proofs the existential witness is a finite object that every perfect strategy must choose: the order of a clock phase in the spatial model, or the depth of a critical binary tree in semifinite algebras. The same level governs communication: deciding whether a finite classical channel can send a given number of messages in one use with zero error, helped by normal entanglement, is Σ⁰₂-complete, and some channel's zero-error codes all need infinite entanglement entropy. Positive computable moment orders below one form a strict Σ⁰₂-complete resource ladder; the infimal critical indices of spatially perfect games (attained by the realizing games) are exactly the right-c.e.-in-0′ reals in [0,1].

For an expert
The four main theorems, as stated in the paper

Theorem A (spatial perfection)

Deciding whether a finite rational $0 / 1$ game has a perfect normal spatial strategy is $Σ_{2}^{0}$ -complete. The same holds when a perfect strategy with finite marginal entropy is required. Hardness holds under the promise $ω_{q} (G) = 1$ , for a family in which no instance has a perfect finite-dimensional strategy.

Theorem B (perfect play by von Neumann type)

Perfect normal play in a finite algebra, a type II₁ algebra, or a semifinite algebra is $Σ_{2}^{0}$ -complete. The same holds for the type II_∞ and type II existence languages. For every fixed $λ \in [0, 1]$ , the type III_λ language equals commuting perfection and is $Π_{1}^{0}$ -complete. Commuting perfection without semifinite perfection is $Π_{2}^{0}$ -complete, with hardness on a family of commuting-perfect games all having $ω_{q} = 1$ . The two languages semifinite but not spatial and semifinite but not finite-entropy spatial are $D_{2} (Σ_{2}^{0})$ -complete, also with no finite-host perfection. Every nonempty directional difference among the six models in Theorem 14.1 is complete for its displayed class.

Theorem C (zero-error communication)

For finite rational classical channels, ${Z E}_{q s}$ and ${Z E}_{f i n S}$ are $Σ_{2}^{0}$ -complete. Moreover, there are a finite rational classical channel $N$ and an integer $m$ for which ${Z E}_{q s} (N, m)$ holds, and every normal spatial $m$ -message zero-error resource has infinite marginal entropy on both sides.

Theorem D (the entanglement spectrum)

For every fixed computable $0 < α < 1$ , perfect play with $T r h^{α} < \infty$ , denoted $𝒫_{α}$ , is $Σ_{2}^{0}$ -complete. With $𝒫_{0}$ denoting finite rank, $𝒫_{1}$ finite entropy and $𝒫_{n o r m a l}$ normal perfection, they form the strict ladder $𝒫_{0} ⊊ 𝒫_{a} ⊊ 𝒫_{b} ⊊ 𝒫_{1} ⊊ 𝒫_{n o r m a l}$ for $0 < a < b < 1$ ; all Rényi orders above one collapse to normal perfection. One computable hardness family has a single perfect witness with all positive moments finite on every YES input, value one on every input, and no finite-dimensional perfect instance. Every nonempty difference between distinct positive computable rungs is $D_{2} (Σ_{2}^{0})$ -complete; a positive rung minus finite rank is $Σ_{2}^{0}$ -complete. For a perfect witness with marginal $h$ , its critical index is $α_{c} (h) = \inf {α > 0 : T r h^{α} < \infty}$ . Put $c (G) = \inf α_{c} (h)$ , the infimum over the marginals $h$ of all perfect spatial witnesses for $G$ . The possible values of $c (G)$ (an infimum, attained by the realizing games) are exactly the right-c.e.-in- $0^{'}$ reals in $[0, 1]$ , already among games with finite-entropy perfect strategies.

Here $ω_{q}$ is the finite-dimensional value, and ${Z E}_{t} (N, m)$ is the existence of a code that sends one of $m$ messages through the channel $N$ , used once, with zero error, helped by entanglement of model $t$ : normal spatial (qs) or spatial with finite entropy (finS). Corollary 3.6, the entropy busy beaver: with $m_{*} (G)$ the least integer $m$ such that $G$ has perfect play of entropy at most $m$ , and $B (n)$ the largest finite $m_{*} (G)$ over games of bit length at most $n$ , there is no total $0^{'}$ -computable upper bound on $B$ , $B \equiv_{T} 0^{″}$ , and $B$ eventually strictly dominates every total $0^{'}$ -computable function. Corollary 3.7 proves the same profile for the least Schmidt stratum. The body also proves exact Bell attainment $Σ_{2}^{0}$ -complete (Theorem 8.1) and the commuting zero-error row $Π_{1}^{0}$ -complete (Theorem 17.2).

Precursor preprintsconsolidated into this paper, which supersedes them

3 Nov 2026Perfect play with spatial quantum strategies is Σ⁰₂-completeSeth Douglas and Nidhal Mghirbi · version 1.1.0 · all versions doi:10.5281/zenodo.23910986
3 Nov 2026Perfect play has different arithmetical complexity in semifinite and type III algebrasSeth Douglas and Nidhal Mghirbi · version 1.0.0 · all versions doi:10.5281/zenodo.23925091
3 Nov 2026One-shot zero-error communication with normal entanglement is Σ⁰₂-completeSeth Douglas and Nidhal Mghirbi · version 1.0.0 · all versions doi:10.5281/zenodo.23924868

Their pages stay online with their versions, DOIs, files and BibTeX. They are not counted as separate works.

Questionson the index

Answered How hard is it to decide whether a finite game has a perfect spatial quantum strategy?

Labelsverification, Lean, peer review and novelty, as Method describes them

Verification: The derivations of the completion of the semifinite-but-not-spatial cells, the Rényi ladder, the nested assembly and the capacity boundary produced with one model family, and refutation-first checks by a second model family, which reconstructed the operator arguments and complexity reductions and checked the proofs presented here; finite checks in eight suites, with exact rational or symbolic checks kept apart from floating-point ones, both full-game dry counts recomputed by separate counters from the producer’s emitted polynomials, and the parity graph’s theta witness, independence number, block code and complete Schrijver symmetry decomposition recomputed in an independent exact implementation.
Lean: Lean kernel-checks the 601 listed proof roots for the concrete row-game construction, selected actual-support and matrix-unit arguments, bridge/refinement and row-algebra steps, fixed-n=4 application syntax, word-coordinate and scalar Fock-entropy calculations, local clock/reader implications, elementary winning-functional identities, and the good-primitive-phase lemma for every prime. Only propext, Classical.choice and Quot.sound occur as solution axioms. Theorem A and the complete compiler, extraction and reduction are not Lean-checked. Two independent kernel replays, by Lean’s checker and the independent nanoda checker, accept the package. Lean source
Peer review: Not yet.
Novelty: New, with named prior work. Earlier versions of Theorems A, B and C, of Theorems 3.1 and 8.1, of the trace-class correspondence, of the summability threshold, of the commuting row and of the I-only and infinite-entropy-only classifications appeared in the authors’ three preprints, which this paper consolidates and supersedes; apart from those, the paper knows of no prior statement of these results, and Theorem D and the completion of the semifinite-but-not-spatial cells are new here. The $Π_{1}^{0}$ -completeness of commuting perfection is known from Slofstra and from Mousavi, Nezhadi and Yuen; what is new in Theorem B is that every fixed type-III subtype has exactly that language. The other known rows of its table are due to Ji, Natarajan, Vidick, Wright and Yuen (finite-dimensional perfection, $Σ_{1}^{0}$ ) and Mousavi, Nezhadi and Yuen (value one, $Π_{2}^{0}$ ). The growth of the entropy busy beaver (Corollary 3.6) is the profile of Radó’s busy beaver function relativized to the halting problem, the “super Busy Beaver” of Aaronson’s The Busy Beaver Frontier, where Beeping Busy Beavers give an earlier natural example of this growth; what is new is that a resource of perfect play realizes it. The bridge geometry is Mančinska’s flagged magic-square construction, and the game-to-channel correspondence extends hers from finite dimension to trace-class operators; the operator characterization of entanglement-assisted zero-error codes is due to Cubitt, Leung, Matthews and Winter. The compiler extends the authors’ entropy-game paper; the standard-form reduction, the commuting bridge and the expected-inclusion transfer come from the authors’ type-games paper, whose Theorem 7.6 left open the question that the type rows complete. The group embeddings go back to Higman, in Chiodo’s effective form, and subtype transfer uses the flow-of-weights theory of Connes and Takesaki and an argument of Haagerup and Musat.

As the paper states, the finite computations do not prove infinite-dimensional existence, compactness, arbitrary-normal soundness, the group embedding theorems, type-III classification or hardness by sampling; those conclusions rest on the written proofs and the cited theorems. The Lean core checks the listed local constructions and implications, not Theorem A.

Every check here is internal. How we check results.

Label checked 4 November 2026.

Versionsone, each with its own DOI

Every archived version, newest first. Dates are Zenodo publication dates. All versions: 10.5281/zenodo.23962889, which always resolves to the newest.
Version	Date	DOI	Notes
1.0.0	4 Nov 2026	10.5281/zenodo.23962890	PDF hosted here.

Paper, code and links

PDF

papers/trace-quantifier-v1.0.0.pdf, version 1.0.0, 1,671,898 bytes, 117 pages.

SHA-256 cb58a517447565d1b47a13506a8eca2907242813b3713455b505ea8b32005930

Of paper/main.pdf, 1,671,898 bytes, in the Zenodo archive; identical in the repository at that commit. The same file is hosted here: papers/trace-quantifier-v1.0.0.pdf.

DOI

10.5281/zenodo.23962890; all versions 10.5281/zenodo.23962889

Code

github.com/Apsiape/perfect-play-arithmetical-hierarchy

Lean

Lean source

Commit

623a029bbff404182a33be1a5f107ad721600234

The commit archived on Zenodo (Apsiape/perfect-play-arithmetical-hierarchy, tag v1.0.0). The main branch has since recorded the DOI.

Licence

Paper and documentation CC BY 4.0; Lean sources and scripts MIT or Apache 2.0, at your option.

Page checked against the paper, its release repository, the Zenodo record and the release notes of the tag v1.0.0 on 4 November 2026.

Corrections

None so far.

All corrections, and what counts as one.

Cite

@misc{douglas2026tracequantifier,
  author  = {Douglas, Seth and Mghirbi, Nidhal},
  title   = {A trace costs one quantifier: the exact complexity of perfect play in nonlocal games},
  year    = {2026},
  version = {1.0.0},
  doi     = {10.5281/zenodo.23962890},
  url     = {https://doi.org/10.5281/zenodo.23962890}
}

trace-quantifier.bib All papers as BibTeX