通过线性系统博弈给出的 Tsirelson 问题的显式反例
An Explicit Counterexample to Tsirelson's Problem via a Linear System Game
浏览论文内容
中文总结 AI 辅助
该论文构造了一个显式二元线性系统博弈，证明有限维量子关联闭包与交换算子关联集合不同，从而为 Tsirelson 问题近似形式提供了具体反例，并精确计算了经典值。
中文摘要 AI 辅助
我们构造了一个显式的二元线性系统博弈，它将有限维量子关联集合的闭包 \(C_{qa}\) 与交换算子关联集合 \(C_{qc}\) 区分开来。该博弈允许一个完美的交换算子策略，而 \(C_{qa}\) 中的每个关联的成功概率都严格小于 1。这为 Tsirelson 问题的近似形式提供了一个具体的反例。定义该系统包含 \(1{,}417{,}152\) 个方程和 \(1{,}889{,}684\) 个变量，每个方程恰好有三个非零系数，且右侧只有一个非零项。我们还精确计算了经典值。完整系统在 Lean~4 中指定，分离性和精确经典值使用 Mathlib 进行了形式化验证。
英文摘要
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.
发表机构
- Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）
- University of Chinese Academy of Sciences（中国科学院大学）
- Tencent Hunyuan（腾讯混元）
- Academy of Mathematics and Systems Science, Chinese Academy of Science（中国科学院数学与系统科学研究院）
机构由 AI 辅助整理，请以论文原文为准。
