An Explicit Counterexample to Tsirelson's Problem via a Linear System Game
π arXiv:2610.10248 Β· π₯ PDF Β· 2026-10-07 Β· quant-ph
Authors: Minbo Gao [arXiv Β· scholar] , Tianshi Yu [arXiv Β· scholar] , Lihong Zhi [arXiv Β· scholar]
π 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 \(1{,}417{,}152\) equations in \(1{,}889{,}684\) 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.