An Explicit Counterexample to Tsirelson's Problem via a Linear System Game

arXiv:2610.10248 · quant-ph, math.FA, math.OA · Submitted 2026-10-07 · Read on arXiv

quant-ph, math.FA, math.OA

Submitted: 2026-10-07

Updated: 2026-10-08

Comments: 31 pages

Code: https://github.com/leanhnhe091221-boop/explicit-linear-system-game-formali

Project page: https://m-ershov.github.io/Research/EL_n_accepted.pdf

License: http://creativecommons.org/licenses/by/4.0/

The gist: 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.

Terminology

Abstract

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.

Sources

Related papers