The uncomputable price of precision

Douglas, Seth; Mghirbi, Nidhal

doi:10.5281/zenodo.23753741

The uncomputable price of precision

Seth Douglas and Nidhal Mghirbi · version 4.0.0 · Zenodo, 29 October 2026 · 119 pages · doi:10.5281/zenodo.23753741 · PDF

In plain wordsFor some games with simple, fixed rules, the quantum resources needed to play almost perfectly grow at a rate no computer program can work out from the rules.

The resultat three depths

In one sentenceFor some games with fixed, finite rules, the rate at which near-perfect play demands ever larger quantum systems is a number no algorithm can compute from the rules; the possible rates are exactly the numbers that can be computed in the limit.

As the paper states it, in briefFor finite rational constraint-system games of quantum value one, the positive exponents of the least local dimension needed near perfect play are exactly the positive $Δ_{2}^{0}$ reals, with matched distillable-entanglement realizations; the lower and upper exponent pairs are exactly the $(Σ_{2}^{0}, Π_{2}^{0})$ pairs.

For a scientist
One paragraph

For a finite game $G$ of quantum value one, let $D_{G} (ε)$ be the least local dimension of a strategy with loss at most $ε$ , and call ${lim}_{ε ↓ 0} \log_{2} D_{G} (ε) / \log_{2} (1 / ε)$ its dimension exponent. For finite rational Boolean constraint-system games the positive exponents are exactly the positive $Δ_{2}^{0}$ reals, the limits of computable sequences of rationals, and each is matched by the one-way distillable entanglement of the original mixed strategy state. A fixed halting game has exponent $(3 + θ_{K}) / 4$ , Turing-equivalent to the halting set. The lower and upper exponent pairs of one game are exactly the $(Σ_{2}^{0}, Π_{2}^{0})$ pairs, the same classification holds at the power scale in $(0, 1]$ , and some computable whole profiles are realized by no game: classifying endpoints is not realizing profiles. The main proof uses no ${MIP}^{*} = RE$ witness. In the companion reset model, local-reset heat doubles the coefficient while joint-reset heat stays bounded.

For an expert
The main theorems, as stated in the paper (Section 1)

In the paper, $d_{G}^{\to} (ε)$ is the infimum of the one-way distillable entanglement $E_{D}^{A \to B} (ρ_{A B})$ over finite-dimensional strategies of loss at most $ε$ , the state possibly mixed, and $ℬ_{BCS}$ is the set of positive limits ${lim}_{ε ↓ 0} \log_{2} D_{G} (ε) / \log_{2} (1 / ε)$ for finite BCS games with rational question probabilities and quantum value one.

Theorem 1.1 (Complete dimension classification and matched realization)

The positive dimension spectrum is

ℬ_{BCS} = {α > 0 : α is Δ_{2}^{0}} .

For every positive $Δ_{2}^{0}$ real $α$ there is a fixed finite two-player Boolean constraint-system game $G_{α}$ , with rational question probabilities, quantum value one and no finite-dimensional perfect strategy, such that, as $ε ↓ 0$ ,

\log_{2} D_{G_{α}} (ε) = α \log_{2} (1 / ε)

+ o (\log (1 / ε)),

d_{G_{α}}^{\to} (ε) = α \log_{2} (1 / ε)

+ o (\log (1 / ε)) .

Conversely, every finite dimension exponent of a rational finite game is $Δ_{2}^{0}$ whenever its defining limit exists. The usable-entanglement assertion is an inclusion, not a classification of its full spectrum.

Theorem 1.2 (The halting game)

There is a fixed finite two-player Boolean constraint-system game $G_{K}$ , with rational question probabilities, such that $ω_{q} (G_{K}) = 1$ , no finite-dimensional strategy wins perfectly, and

D_{G_{K}} (ε) = ε^{- (3 + θ_{K}) / 4 + o (1)},

θ_{K} = \sum_{e \in K} 4^{- (e + 1)} .

The exponent is Turing-equivalent to $K$ . The sequence $\log D_{G_{K}} (2^{- n}) / n$ has no computable certified rate of convergence.

Theorem 1.3 (Power-scale classification)

For every $Δ_{2}^{0}$ real $β \in (0, 1]$ , one fixed finite rational BCS game of value one, without a finite-dimensional perfect strategy, has matching power exponents

d_{G}^{\to} (ε) = ε^{- β + o (1)},

\log D_{G} (ε) = ε^{- β + o (1)} .

In $(0, 1]$ , the existing power exponents of log dimension, pure original-state entropy and single-copy entanglement of formation are exactly the $Δ_{2}^{0}$ reals. The usable ceiling remains open; an exponent outside that class would force a polynomial formation/distillation gap.

Theorem (Exponent pairs and whole profiles)

The positive finite logarithmic dimension pairs are exactly $0 < L \leq U < \infty$ with $L \in Σ_{2}^{0}$ and $U \in Π_{2}^{0}$ . One fixed rational BCS game realizes each pair with the same original-state usable pair. At the power scale every such pair in $(0, 1]$ is realized, and these conditions classify dimension pairs there. A polynomial-delay pulse word with positive lower one-density and one-count $k$ gives

\log_{2} D_{G} (2^{- n}) = Λ + \frac{m}{2} k (Λ)

+ O (\log n),

Λ = ⌊ n / (2 q) ⌋,

with the same usable profile, for fixed integers $m, q \geq 1$ . Under linear slope bounds, space- $o (n)$ target profiles are realized modulo $o (n)$ , but some computable bounded-increment profiles with any admissible distinct endpoints are not realized by any game modulo $o (n)$ .

The dependencies are substantive: the Boolean correspondence is used as stated from The price of precision, Theorem 4.9; the second, witness-based proof also uses the finite perfect-completeness reduction of ${MIP}^{*} = RE$ . The paper says this is not a self-contained proof of the imported correspondences or complexity theorem.

Questionson the index

Answered Can the rate at which the least dimension grows near perfect play be computed from a finite game’s rules?
Answered Which lower and upper exponents can one fixed game have?
Open Can a finite rational value-one game with no finite-dimensional perfect strategy have dimension exponent zero? left open
Open Is every positive usable-entanglement coefficient of a finite rational game limit-computable? left open
Open Which finite power exponents above one occur for a fixed finite rational game? left open
Open Which positive local-reset heat coefficients occur? left open

How this was checked

Blind audits: Blind audit rounds before each of the four versions.
Verification: Proofs checked by models from two developers
Independent computation: The original construction checked on two independent finite-model engines
Lean: Sections 2 to 10 in progress, not complete; no completed formal verification is claimed.
Peer review: Not yet.

Each check, what it covers, and what it leaves to the written proof.

Each check, what it covers, and what it leaves to the written proof.
Check	Covers	Does not cover
Finite-model audit	Builds the Section 5 operators for a fixed one-counter program at $N = 4, 6, 8$ and checks every defining relation, the required commutations, domains and the decoding and reset identities: 390, 394 and 398 recorded checks.	The arbitrary-state lower bound, which rests on the written proof; the complete compiled game; convergence as $N$ grows.
Independent engine	A separately written engine, built without access to the audit script, with its own three-counter test program: 911, 915 and 919 relations, operator-norm and flat defects, the exact dimension, and ablations showing each fixed reading is forced.	The arbitrary-state lower bound, the tracial forcing argument or the compiled game.
Blind audits	Proofs checked by models from two developers; blind audit rounds before each of the four versions.	Errors every reader shares.
Lean	A formalization of Sections 2 to 10 is in progress and not complete.	Sections 11 to 17, the power-scale part and the profile part are not yet formalized. No completed Lean verification is claimed.
Peer review	Not yet.	A preprint on Zenodo.

Check descriptions follow the repository’s anc/README.md and the paper. Every audit here is internal. How we check results.

Label checked 29 October 2026.

Novelty and credit

Novelty: New, with named precedents in form: Meyerovitch; Hochman and Meyerovitch; Sapir, Birget and Rips.

Mousavi, Nezhadi and Yuen proved that deciding whether the quantum value is exactly one is $Π_{2}^{0}$ -complete. The algebraic link between constraint games and operator assignments goes back to Cleve and Mittal, and for linear systems to Cleve, Liu and Slofstra; Slofstra and Vidick introduced the hyperlinear profile. Mančinska and Vidick, Ji, Leung and Vidick, and Coladangelo gave important growth examples. The conjugacy gadgets in the compiler are those of Fanizza, Kroell, Mehta, Paddock, Rochette, Slofstra and Zhao, and the paper says their credit is essential. Meyerovitch’s entropy-dimension classification is the exact precedent in form; Hochman and Meyerovitch, and Sapir, Birget and Rips, are precedents in form; the invariants here are fixed-game precision costs.

Recordevery version

27 Oct 2026Version 1.0.0doi:10.5281/zenodo.23701734
28 Oct 2026Version 2.0.0doi:10.5281/zenodo.23717986
28 Oct 2026Version 3.0.0doi:10.5281/zenodo.23736188
29 Oct 2026Version 4.0.0, the current versiondoi:10.5281/zenodo.23753741

Dates are Zenodo publication dates. No correction has been needed so far; each version added results. All corrections

Versionsfour, each with its own DOI

Every archived version, newest first. Dates are Zenodo publication dates. All versions: 10.5281/zenodo.23701733, which always resolves to the newest.
Version	Date	DOI	Notes
4.0.0	29 Oct 2026	10.5281/zenodo.23753741	PDF hosted here.
3.0.0	28 Oct 2026	10.5281/zenodo.23736188
2.0.0	28 Oct 2026	10.5281/zenodo.23717986
1.0.0	27 Oct 2026	10.5281/zenodo.23701734	Titled “A nonlocal game whose dimension exponent is uncomputable”.

Paper, code and links

PDF

papers/uncomputable-price-v4.0.0.pdf, version 4.0.0, 1,402,612 bytes, 119 pages.

SHA-256 47fc33b7183b47111b0da29a8f5ccd7ef8d0e7cd30976eebebd231919e1fc315

Of paper/main.pdf, 1,402,612 bytes, in the Zenodo archive; identical in the repository at that commit. The same file is hosted here: papers/uncomputable-price-v4.0.0.pdf.

DOI

10.5281/zenodo.23753741; all versions 10.5281/zenodo.23701733

Code

github.com/Apsiape/uncomputable-dimension-exponent

Commit

cbcc4dfe30fec755cca56ce21ed917df5da89e0f

The commit archived by Zenodo (Apsiape/uncomputable-dimension-exponent, tag v4.0.0).

Verify

From a clone of the repository. The README builds the paper; anc/README.md runs the two finite-model programs (PowerShell, one numerical thread).

python paper/build.py

$env:OMP_NUM_THREADS='1'
$env:OPENBLAS_NUM_THREADS='1'
python anc/audit/check_models.py --depths 4 6 8

cd verify
python -u run_e2.py 8

The independent engine at $N = 8$ took about 141 s and 656 MB on the authors’ machine.

Lean, in detail

Sections 2 to 10 in progress, not complete; no completed formal verification is claimed.

Licence

Text, LaTeX and documentation CC BY 4.0; scripts MIT or Apache 2.0, at your option.

Page checked against the paper, the release repository and the Zenodo record on 30 October 2026.

Corrections

None so far.

All corrections, and what counts as one.

Cite

BibTeX built from the repository’s CITATION.cff, which cites the all-versions DOI.

@misc{douglas2026uncomputable,
  author  = {Douglas, Seth and Mghirbi, Nidhal},
  title   = {The uncomputable price of precision},
  year    = {2026},
  version = {4.0.0},
  doi     = {10.5281/zenodo.23701733},
  url     = {https://doi.org/10.5281/zenodo.23701733},
  note    = {Preprint. Lean formalization of Sections 2--10 is in progress and not complete}
}

uncomputable-price.bib All papers as BibTeX