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

Abstract

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.

The paper addresses the Pál–Vértesi conjecture that the quantum supremum of $I_{3322}$ is approached by their increasing-dimensional family but attained by no finite-dimensional strategy. It proves both statements: the supremum over arbitrary finite-dimensional states and binary measurements equals the supremum of the finite Pál–Vértesi family, numerically estimated near $0.25087538$, and every finite-dimensional strategy has strictly smaller value. It also proves the exact two-qubit maximum $1/4$. The upper-bound argument uses a party-swap/outcome-flip symmetry, optimizes the third measurements through a trace norm, and applies Jordan decomposition to the first two measurements. This associates each strategy with a finite joint distribution over spectral labels and an explicit upper-bound functional. A combinatorial construction approximates that functional by weighted averages of finite Pál–Vértesi chains. For nonattainment, equality conditions for a finite distribution produce a square-summable auxiliary chain; stationarity then forces geometric growth, yielding a contradiction. The core results are formalized in Lean 4, excluding the reduction from mixed states and POVMs. Consequently, finite-dimensional quantum correlations are not closed in $(3,3,2,2)$, the smallest binary-outcome scenario permitting nonclosure. Approaching the supremum requires unbounded local dimension: every fixed dimension cutoff has a strict gap. The paper does not determine whether an infinite-dimensional tensor-product strategy attains the supremum, whether the commuting-operator value is larger, or a closed-form value. Exact dimension-restricted thresholds beyond qubits, convergence rates, and rigidity of near-optimal strategies remain open.