The I3322 quantum value is attained spatially but not in finite dimension
Seth Douglas
quant-ph
Sep 3, 2026 · v1
TL;DR
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.
Abstract
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.
Problem
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.
Approach
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.
Results
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/ε).