I3322量子值在空间上达到但不在有限维度中达到
The I3322 quantum value is attained spatially but not in finite dimension
浏览论文内容
中文总结 AI 辅助
该论文证明I3322贝尔泛函的量子上确界在无限维空间策略中达到但任何有限维策略均无法达到，并给出维度复杂度为对数阶，解决了Pal-Vertesi猜想及Dykema等人提出的达到问题。
中文摘要 AI 辅助
设$S$为Collins-Gisin归一化下$I_{3322}$贝尔泛函的量子上确界（经典界为0；两量子比特最大值为精确的1/4）。从认证窗口$S\in(0.2508753845015185,0.250875388108398]$（由Mghirbi先前的证书独立且更紧地包围）以及张量积与交换算子至上确界的认证相等性，我们证明：(i) 没有任何有限维量子策略能达到$S$——任何有限局域维度、纯态或混合态、投影或POVM测量——证明了Pal和Vertesi（2010）的猜想；(ii) $S$由$\ell^2(\mathbb{Z})\otimes\ell^2(\mathbb{Z})$上的空间策略达到，即这些作者所断言的无限维达到，且采用独立路径。因此$C_q(3,3;2,2)$不是闭的——这是按输入计数已知非闭的最小双输出二分场景——且$C_{qs}(3,3;2,2)\setminus C_q(3,3;2,2)$非空，解决了Dykema、Paulsen和Prakash提出的达到问题。非达到性通过凹临界贝尔曼存储、精确有理端点排除证书、反射粘合和凸包络定理证明：有限性迫使精确最大化器的两个等式输运重合，将其值限制在$1/4<S$。达到性通过将交换最大化器的谱测度分解到其两个响应输运的轨道上证明，产生具有继承可归一化性的$\ell^2$雅可比特征向量。我们还确定了维度复杂度：设$S_d$为局域维度$\le d$时的最优值，$D(\epsilon)=\min\{d:S-S_d\le\epsilon\}$，则$D(\epsilon)=\Theta(\log(1/\epsilon))$——上半部分为构造性的，$D(\epsilon)\le 23.9010650\log(1/\epsilon)$；下半部分在随附仓库的证书链中。两半部分的核心均在Lean 4中进行了机器验证。
英文摘要
Let $S$ be the common tensor-product and commuting-operator supremum of the $I_{3322}$ Bell functional in the Collins-Gisin normalization. Starting from a certified value window and Bellman/path equivalence, we prove that no finite-dimensional quantum strategy attains $S$, whereas a spatial strategy on $\ell^2(\mathbb{Z})\otimes\ell^2(\mathbb{Z})$ does. The finite-dimensional statement includes mixed states and binary POVMs. Consequently $C_q(3,3;2,2)$ is not closed and $C_{qs}(3,3;2,2)\setminus C_q(3,3;2,2)$ is nonempty. We also establish the dimension complexity $D(ε)=Θ(\log(1/ε))$: approaching $S$ requires and suffices local dimension logarithmic in inverse error. The constructive upper bound is $D(ε)\le 23.9010650\log(1/ε)$ for all sufficiently small $ε$, with natural logarithms; the lower constants are existential. The proofs use critical Bellman storage, spectral transport and normalizable orbit measures. A finite weighted-flow argument supplies the unrestricted quantitative lower bound without identifying distinct joint spectral components. This revision replaces an unsupported step in the earlier lower argument and records additional proof corrections. Prior numerical certification and independent concurrent attainment results are credited. Exact arithmetic and Lean 4 check specified numerical, scalar and finite accounting facts; the complete analytic proof is not formalized.
