An explicit nonlocal game of quantum value one that needs exponential entanglement

As the paper states it, in briefA binary linear system game with 1687 equations in 1993 variables, of quantum value one, in which winning with probability $1-\epsilon$ needs entanglement entropy ${\epsilon }^{-1+o(1)}$, hence local dimension $\exp ({\epsilon }^{-1+o(1)})$; the exponent is sharp.

• Answered How much entanglement can an explicit game of quantum value one force?

Independent computation

Exact certificates for the four computational statements, each re-checked by a separately written program in anc/.

In Lean

Theorem A (conditional on the published perfect tensor-strategy implication) and Theorems C, D, E and F checked in Lean 4, standard axioms only; independent fresh build and two kernel replays of the release.

Lean

Theorem A, conditional on the published implication from perfect tensor-product strategies, and Theorems C, D, E and F formalized in Lean 4; the release was rebuilt from scratch and replayed by Lean's checker and the independent nanoda checker. Source and recorded axioms in the repository. Lean source

Peer review

Not yet.

Every check here is internal. How we check results.

Label checked 2 November 2026.

Novelty

New. For explicit games of quantum value one, the best previous lower bound was polynomial in $1/\epsilon$. The same tools give sharp rates for the CHSH($n$) games and the game of Slofstra and Vidick.

PDF

papers/explicit-game-v1.1.0.pdf, version 1.1.0, 1,246,081 bytes, 93 pages.

SHA-256 9b7793fe0474706173d8e3c25d4d5174cc4eca6d1dc5251e97583c42288fd8fc

DOI

10.5281/zenodo.23878232; all versions 10.5281/zenodo.23697254

Code

github.com/Apsiape/explicit-game-exponential-entanglement

Lean

Lean source

None so far.

All corrections, and what counts as one.

@misc{mghirbi2026explicitgame,
  author  = {Mghirbi, Nidhal and Douglas, Seth},
  title   = {An explicit nonlocal game of quantum value one that needs exponential entanglement},
  year    = {2026},
  version = {1.1.0},
  doi     = {10.5281/zenodo.23878232},
  url     = {https://doi.org/10.5281/zenodo.23878232}
}

explicit-game.bibAll papers as BibTeX