PreprintCC BY 4.0arXiv
An Explicit Counterexample to Tsirelson's Problem via a Linear System Game
Abstract
We construct an explicit binary linear system game that separates Cqa, the closure of the set of finite dimensional quantum correlations, from Cqc, the set of commuting operator correlations. The game admits a perfect commuting operator strategy, while every correlation in Cqa has a success probability strictly less than 1. This provides a concrete counterexample to Tsirelson's problem in its approximation form. The defining system has 1417152 equations in 1889684 variables, with exactly three nonzero coefficients per equation and a single nonzero entry on the right hand side. We also compute the classical value exactly. The complete system is specified in Lean 4, and the separation and exact classical value are formalized using Mathlib.
Related
- Fermions and the Tsirelson Problem in Real Quantum Theory
- Stochastic linear-quadratic control problem for regime-switching jump-diffusion system and its application to finance
- An explicit counterexample to the Hinrichs--Vybiral conjecture
- An Explicit Polynomial Counterexample to Connes' Embedding Conjecture
- An explicit rational lemniscate counterexample with certified separators
BibTeX
@misc{gao2026explicit,
title = {{An Explicit Counterexample to Tsirelson's Problem via a Linear System Game}},
author = {Minbo Gao and Tianshi Yu and Lihong Zhi},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.10248},
eprint = {2610.10248},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.10248},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - An Explicit Counterexample to Tsirelson's Problem via a Linear System Game
AU - Minbo Gao
AU - Tianshi Yu
AU - Lihong Zhi
PY - 2026
DA - 2026/10/08
PB - arXiv
DO - 10.48550/arxiv.2610.10248
UR - https://arxiv.org/abs/2610.10248
AB - We construct an explicit binary linear system game that separates C_qa, the closure of the set of finite dimensional quantum correlations, from C_qc, the set of commuting operator correlations. The game admits a perfect commuting operator strategy, while every correlation in C_qa has a success probability strictly less than 1. This provides a concrete counterexample to Tsirelson's problem in its approximation form. The defining system has 1417152 equations in 1889684 variables, with exactly three nonzero coefficients per equation and a single nonzero entry on the right hand side. We also compute the classical value exactly. The complete system is specified in Lean 4, and the separation and exact classical value are formalized using Mathlib.
ER -