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

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 $\mathrm{1,417,152}$ equations in $\mathrm{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.