← 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 · v1
A Lean 4 kernel machine-checks core lemmas: the quarter-ceiling chain, band algebra, and three lower-bound combinatorial cores of the I3322 nonattainment proof.
Let $S$ be the quantum supremum of the $I_{3322}$ Bell functional in the Collins-Gisin normalization (classical bound 0; two-qubit maximum exactly 1/4). From a certified window $S\in(0.2508753845015185,0.250875388108398]$ (independently and more tightly enclosed by Mghirbi's prior certificates) and a certified equality of the tensor-product and commuting-operator suprema, we prove: (i) no finite-dimensional quantum strategy attains $S$ – any finite local dimensions, pure or mixed states, projective or POVM measurements – proving the conjecture of Pal and Vertesi (2010); (ii) $S$ is attained by a spatial strategy on $\ell^2(\mathbb{Z})\otimes\ell^2(\mathbb{Z})$, the infinite-dimensional attainment those authors asserted, on an independent route. So $C_q(3,3;2,2)$ is not closed – the smallest two-outcome bipartite scenario by input count where nonclosure is known – and $C_{qs}(3,3;2,2)\setminus C_q(3,3;2,2)$ is nonempty, settling the attainment question raised by Dykema, Paulsen and Prakash. Nonattainment is proved via a concave critical Bellman storage, exact rational endpoint-exclusion certificates, reflection-gluing and a convex-envelope theorem: finiteness forces an exact maximizer's two equality transports to coincide, capping its value at $1/4<S$. Attainment is proved by disintegrating a commuting maximizer's spectral measure over the orbits of its two response transports, yielding an $\ell^2$ Jacobi eigenvector with inherited normalizability. We also determine the dimension complexity: with $S_d$ the optimum at local dimension $\le d$ and $D(ε)=\min\{d:S-S_d\leε\}$, $D(ε)=Θ(\log(1/ε))$ – the upper half constructively, with $D(ε)\le 23.9010650\log(1/ε)$; the lower half in a certificate chain in the accompanying repository. Cores of both halves are machine-checked in Lean 4.

The I3322 Bell functional has a quantum supremum S whose attainment properties were conjectured by Pál and Vértesi (2010): no finite dimension suffices, but infinite dimension does. Whether the set of finite-dimensional quantum correlations C_q(3,3;2,2) is closed was open.

A certified rational window for S and certified equality of tensor and commuting suprema are used. Nonattainment is proved via a concave critical Bellman storage, exact rational endpoint-exclusion certificates, reflection-gluing, and a convex-envelope theorem forcing equality transports to coincide. Spatial attainment is proved by disintegrating a commuting maximizer's spectral measure over transport orbits, yielding an ℓ²(ℤ) Jacobi eigenvector. Core lemmas are machine-checked in Lean 4 with no sorry and standard axioms.

No finite-dimensional strategy attains S, but a spatial strategy on ℓ²(ℤ)⊗ℓ²(ℤ) does, proving C_q(3,3;2,2) is not closed and C_qs minus C_q is nonempty. The dimension complexity is D(ε)=Θ(log(1/ε)), with D(ε) ≤ 23.9010650·log(1/ε).