← All papers
First page of The I3322 quantum value is attained spatially but not in finite dimension

The I3322 quantum value is attained spatially but not in finite dimension

Seth Douglas

quant-ph Sep 3, 2026 · v2
A Lean 4 kernel of 27 theorems, using standard axioms only, machine-checks the quarter-ceiling chain, the band algebra and the combinatorial lower-bound cores. The full analytic proof is not formalized.
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.

Pál and Vértesi conjectured that the quantum supremum S of the I3322 Bell functional is not attained by any finite-dimensional strategy, and they asked for an analytical proof.

The proof uses critical Bellman storage functions, exact rational endpoint margins, spectral transport and disintegration over orbit measures. Together these show that finite-dimensional strategies are capped strictly below S, while a spatial strategy on l^2(Z)⊗l^2(Z) attains S. A weighted-flow argument establishes the dimension-complexity rate. Exact arithmetic certificates, plus a minimal Lean 4 kernel, check specified numerical, scalar and combinatorial core facts.

No finite-dimensional strategy attains S, including mixed states and POVMs, but a spatial strategy does. Hence C_q(3,3;2,2) is not closed. The local dimension needed to come within ε of S is Θ(log(1/ε)), with constructive upper bound D(ε) ≤ 23.90 log(1/ε) for sufficiently small ε.