← All papers
First page of The quantum supremum of the $I_{3322}$ Bell inequality is not attained in finite dimension

The quantum supremum of the $I_{3322}$ Bell inequality is not attained in finite dimension

Jef Pauwels

quant-ph Aug 30, 2026 · v1
The core mathematical proof that the I_3322 quantum supremum is not attained in finite dimension was formalized in Lean 4.
In 2010, Pál and Vértesi found a family of finite-dimensional strategies for the $I_{3322}$ Bell inequality whose optimized values appeared to converge as the local Hilbert-space dimension grew. They conjectured that this limit is the supremum over all finite-dimensional quantum strategies, but that no finite-dimensional strategy attains it. We prove both claims. The proof uses the symmetry of the Bell functional to associate every strategy with a finite matrix of probabilities, one for each pair of spectral subspaces of Alice and Bob. This matrix gives an upper bound on the Bell value, and finite-dimensional strategies built from the repeating structure found by Pál and Vértesi approach it as the dimension grows. If the bound were attained exactly in finite dimension, the optimality conditions would then require a state that cannot be normalized. Consequently, the set of finite-dimensional quantum correlations is not closed in the $(3,3,2,2)$ scenario, the smallest Bell scenario where this can happen. Moreover, approaching the supremum requires unbounded local dimension. The core of the proof was formalized in Lean 4.

For the I_3322 Bell inequality in the (3,3,2,2) scenario, it was conjectured by Pál and Vértesi that the supremum over finite-dimensional quantum strategies exists but is not attained by any finite-dimensional strategy. Whether the set of finite-dimensional quantum correlations is closed at this familiar Bell inequality was open.

The Bell functional's symmetry is used to associate each strategy with a finite matrix of spectral-subspace probabilities that upper-bounds the Bell value. Finite-dimensional Pál–Vértesi chain strategies are shown to approach this bound as dimension grows. An optimality analysis shows that exact attainment would require a non-normalizable state (geometrically growing coefficients), yielding a contradiction. The core of the proof was formalized in Lean 4.

Both conjectured claims are proven: the supremum equals the Pál–Vértesi limit and is not attained in finite dimension. Consequently the finite-dimensional quantum correlation set is not closed in (3,3,2,2), the smallest binary-outcome scenario where nonclosure is possible, and approaching the supremum requires unbounded local dimension.