2 Foundations
This chapter fixes the objects that everything else refers to: games, strategies and values (in the synchronous framework, see Section 1.3), the computability conventions, and normal form verifiers. Definitions here are meant to be final; they are the first formalization targets of the project.
Statements marked [\(\uparrow \) QuantumLib] are general-purpose quantum information content: they are intended to be developed in, or contributed to, the QuantumLib (Lean-QuantumInfo) library rather than to remain specific to this project. The badge marks the general-purpose layer — games, strategies, values, and the rigidity theorems of Section 3 — as opposed to project-specific machinery such as normal form verifiers and the game transformations.
2.1 Games, strategies, and values
Games
[\(\uparrow \) QuantumLib] A two-player one-round game \(\mathfrak {G}\) is a tuple \((\mathcal{X}, \mathcal{Y}, \mathcal{A}, \mathcal{B}, \mu , D)\) where \(\mathcal{X}, \mathcal{Y}\) are finite question alphabets, \(\mathcal{A}, \mathcal{B}\) are finite answer alphabets, \(\mu \) is a probability distribution on \(\mathcal{X}\times \mathcal{Y}\), and \(D : \mathcal{X}\times \mathcal{Y}\times \mathcal{A}\times \mathcal{B}\to \{ 0,1\} \) is the decision predicate (\(1\) = accept).
[\(\uparrow \) QuantumLib] A game is synchronous if \(\mathcal{X}= \mathcal{Y}\), \(\mathcal{A}= \mathcal{B}\), and unequal answers to equal questions are rejected: \(D(x,x,a,b) = 0\) whenever \(a \neq b\). We write a synchronous game as \(\mathfrak {G}= (\mathcal{X}, \mathcal{A}, \mu , D)\).
Strategies
[\(\uparrow \) QuantumLib] A tensor-product strategy for \(\mathfrak {G}\) consists of finite-dimensional Hilbert spaces \(\mathcal{H}_\textsc{A}\), \(\mathcal{H}_\textsc{B}\), a unit vector \(|\psi \rangle \in \mathcal{H}_\textsc{A}\otimes \mathcal{H}_\textsc{B}\), and projective measurements (PVMs) \(\{ A^x_a\} \) on \(\mathcal{H}_\textsc{A}\) and \(\{ B^y_b\} \) on \(\mathcal{H}_\textsc{B}\), one for each \(x\) (resp. \(y\)): each \(A^x_a\) is an orthogonal projection and \(\sum _a A^x_a = I\).
Outcome probabilities are computed using the Born rule: the players answer \((a,b)\) to questions \((x,y)\) with probability \(\langle \psi | A^x_a \otimes B^y_b |\psi \rangle \). Restricting to projective measurements follows [ 1 ] ; by Naimark dilation, allowing general POVMs would define the same quantum value.
[\(\uparrow \) QuantumLib] A synchronous strategy for a synchronous game \(\mathfrak {G}= (\mathcal{X}, \mathcal{A}, \mu , D)\) is a dimension \(d \geq 1\) together with a family of projective measurements (PVMs) \(\{ M^x_a\} _{a \in \mathcal{A}}\) on \(\mathbb {C}^d\), one for each \(x \in \mathcal{X}\): each \(M^x_a\) is an orthogonal projection and \(\sum _a M^x_a = I\).
Outcome probabilities are computed with the tracial state \(\tau (M) = \operatorname{tr}(M)/d\): the players answer \((a,b)\) to questions \((x,y)\) with probability \(\tau (M^x_a M^y_b)\).
[\(\uparrow \) QuantumLib] A commuting strategy for a synchronous game \(\mathfrak {G}= (\mathcal{X}, \mathcal{A}, \mu , D)\) is a unital \(C^*\)-algebra \(\mathscr {A}\) with a tracial state \(\tau \) (a positive linear functional with \(\tau (1) = 1\) and \(\tau (ab) = \tau (ba)\) for all \(a, b \in \mathscr {A}\)), together with a family of projective measurements \(\{ M^x_a\} _{a \in \mathcal{A}}\) in \(\mathscr {A}\), one for each \(x \in \mathcal{X}\): each \(M^x_a\) is a self-adjoint idempotent and \(\sum _a M^x_a = 1\).
Outcome probabilities are computed with \(\tau \): the players answer \((a,b)\) to questions \((x,y)\) with probability \(\tau (M^x_a M^y_b)\), a nonnegative real number since \(\tau (M^x_a M^y_b) = \tau (M^x_a M^y_b M^x_a)\).
A synchronous strategy (Definition 2.4) is exactly the finite-dimensional case \(\mathscr {A}= \mathbb {C}^{d \times d}\), \(\tau = \operatorname{tr}/d\). Via the GNS representation, commuting strategies capture exactly the synchronous commuting-operator correlations of the usual two-prover picture, with Bob’s measurements acting in the commutant on \(L^2(\mathscr {A}, \tau )\) — [ 18 , Theorem 5.5 ] ; see also [ 9 ] and [ 10 , Section 3.4 ] .
[\(\uparrow \) QuantumLib] A synchronous strategy \(\mathscr {S}= (d, M)\) for a synchronous game \(\mathfrak {G}= (\mathcal{X}, \mathcal{A}, \mu , D)\) is PCC (projective, consistent, and commuting, following [ 1 , Section 5.2 ] ) if the measurements associated with any pair of questions asked with positive probability commute: for all \((x, y)\) in the support of \(\mu \),
In [ 1 , Section 5.2 ] a PCC strategy is a tensor-product strategy (Definition 2.3) with \(\mathcal{H}_\textsc{A}= \mathcal{H}_\textsc{B}\) that is projective (all measurements are PVMs), consistent (\(A^x_a \otimes I|\psi \rangle = I\otimes B^x_a |\psi \rangle \) for all \(x, a\)), and commuting (\([A^x_a, B^y_b] = 0\) for all \((x, y)\) in the support of \(\mu \) and all \(a, b\)). In the synchronous framework the first two conditions are automatic: a projective, consistent strategy on a maximally entangled state is exactly a synchronous strategy ( [ 1 , Remark 5.13 ] ; see also [ 18 , Theorem 5.5 ] ), so only the commutation condition remains, and we keep the name PCC for alignment with the paper. The “commuting” in PCC is a condition on question pairs in the support of \(\mu \), unrelated to the commuting (operator) strategies of Definition 2.5. Finally, since a synchronous strategy describes both players by the same family of measurements, symmetry is automatic, and we do not distinguish between the PCC and symmetric PCC (SPCC) strategies of [ 1 ] .
Values
[\(\uparrow \) QuantumLib] The value of a tensor-product strategy \(\mathscr {S}= (\mathcal{H}_\textsc{A},\mathcal{H}_\textsc{B},\psi ,A,B)\) in \(\mathfrak {G}\) is
and the quantum value \(\mathrm{val}^*(\mathfrak {G})\) is the supremum of \(\mathrm{val}^*(\mathfrak {G}, \mathscr {S})\) over all tensor-product strategies.
[\(\uparrow \) QuantumLib] The value of a synchronous strategy \(\mathscr {S}= (d, M)\) in \(\mathfrak {G}\) is
and the synchronous value of \(\mathfrak {G}\) is \(\mathrm{val}^{s}(\mathfrak {G}) = \sup _\mathscr {S}\mathrm{val}^{s}(\mathfrak {G}, \mathscr {S})\).
[\(\uparrow \) QuantumLib] The value of a commuting strategy \(\mathscr {S}= (\mathscr {A}, \tau , M)\) in \(\mathfrak {G}\) is
and the commuting value of \(\mathfrak {G}\) is \(\mathrm{val}^{\mathrm{co}}(\mathfrak {G}) = \sup _\mathscr {S}\mathrm{val}^{\mathrm{co}}(\mathfrak {G}, \mathscr {S})\).
[\(\uparrow \) QuantumLib] For a game \(\mathfrak {G}\) and \(\nu \in [0,1]\), \(\mathrm{Ent}(\mathfrak {G}, \nu )\) is the least \(d\) such that there exists a synchronous strategy (Definition 2.4) with dimension at most \(d\) achieving value at least \(\nu \) in \(\mathfrak {G}\), and \(\infty \) if no synchronous strategy achieves \(\nu \).
Relationship lemmas
[\(\uparrow \) QuantumLib] For every synchronous game \(\mathfrak {G}\), \(\mathrm{val}^{s}(\mathfrak {G}) \leq \mathrm{val}^*(\mathfrak {G})\).
Given a synchronous strategy \(\{ M^x_a\} \) on \(\mathbb {C}^d\), take the tensor-product strategy with \(\mathcal{H}_\textsc{A}= \mathcal{H}_\textsc{B}= \mathbb {C}^d\), \(A^x_a = M^x_a\), \(B^y_b = (M^y_b)^{\mathsf{T}}\), and \(|\psi \rangle = d^{-1/2}\sum _i |i\rangle |i\rangle \); then \(\langle \psi | A^x_a \otimes B^y_b |\psi \rangle = \tau (M^x_a M^y_b)\), so the values agree.
The converse direction — every good tensor-product strategy for a synchronous game can be rounded to a good synchronous strategy — is the almost-synchronicity theorem, imported as Theorem 3.3.
[\(\uparrow \) QuantumLib] For every synchronous game \(\mathfrak {G}\), \(\mathrm{val}^{s}(\mathfrak {G}) \leq \mathrm{val}^{\mathrm{co}}(\mathfrak {G})\).
A synchronous strategy \((d, M)\) is a commuting strategy with \(\mathscr {A}= \mathbb {C}^{d \times d}\) and \(\tau = \operatorname{tr}/d\), with the same value (in Lean, MIPRE.SyncStrategy.toCommutingStrategy; the value is preserved by definitional equality).
2.2 Linear constraint system games
A well-studied class of nonlocal games arises from systems of linear equations over \(\mathbb {F}_2\): the referee asks Alice for a satisfying assignment to a randomly chosen equation and Bob for the value of a randomly chosen variable in it, and checks consistency. The Mermin–Peres magic square is the canonical example. The formalization of this subsection was contributed by Sean Perazzolo (MIPRE.LCS); beyond the definitions below it includes observable- and projector-based strategy formalisms and their equivalence, a sum-of-squares decomposition of the loss operators, the extraction of operator identities from perfect play on the EPR state, matrix representations of solution groups, and the magic square as a worked example (MIPRE.LCS.MagicSquare.merminPeresStrategy).
A binary linear constraint system consists of \(r\) equations over \(s\) \(\mathbb {F}_2\)-valued variables, specified by the set \(V_i \subseteq \{ 1, \dots , s\} \) of variables occurring in each equation \(i\) together with a right-hand side \(b \in \mathbb {F}_2^r\); equation \(i\) reads \(\sum _{j \in V_i} x_j = b_i\).
The nonlocal game of an LCS instance: the referee samples an equation \(i\) uniformly at random, then a uniformly random variable \(j \in V_i\); Alice answers an assignment to the variables, Bob answers a value for \(x_j\), and they win if Alice’s assignment satisfies equation \(i\) and agrees with Bob’s answer on \(x_j\).
The solution group of an LCS instance is the group presented by generators \(g_1, \dots , g_s\) and \(J\) subject to the relations: all generators are involutions, \(J\) is central, variables occurring in a common equation commute, and \(\prod _{j \in V_i} g_j = J^{b_i}\) for each equation \(i\). Operator solutions of the system correspond to representations sending \(J \mapsto -I\) (in Lean, MIPRE.LCS.SolutionGroup.solutionGroupRepresentationOfEPRLoss).
If a bipartite observable strategy for an LCS instance is perfect — its local loss operators annihilate the EPR vector — then the associated LCS game has a tensor-product strategy of value \(1\).
Take both players’ spaces to be \(\mathbb {C}^n\) with the normalized EPR state; Alice measures with the joint projective measurements of her equations and Bob with the binary measurements of his observables. The Born-rule value then equals the EPR expectation of the winning operator, which is \(1\) by hypothesis.
2.3 Distance measures
[\(\uparrow \) QuantumLib] For matrices \(A, B \in \mathbb {C}^{d \times d}\), let \(\langle A, B \rangle _{hs} = \tau (A^\dagger B)\) and \(\left\| {A} \right\| _{hs}^2 = \tau (A^\dagger A)\), where \(\tau = \operatorname{tr}/d\) is the dimension-normalized trace.
[\(\uparrow \) QuantumLib] Let \(\mu \) be a distribution on a finite set \(\mathcal{X}\), and \(\{ M^x_a\} \), \(\{ N^x_a\} \) families of POVMs. We say \(M\) and \(N\) are \(\delta \)-close, written \(M^x_a \approx _\delta N^x_a\), if \(\mathop{\mathbb {E}}_{x \sim \mu } \sum _a \left\| {M^x_a - N^x_a} \right\| _{hs}^2 \leq \delta \). Since each difference \(M^x_a - N^x_a\) is Hermitian, the summand equals \(\tau ((M^x_a - N^x_a)^2)\).
Let \(\mu \) be a distribution on a finite set \(\mathcal{X}\), let \(|\psi \rangle \in \mathbb {C}^{d_\textsc{A}} \otimes \mathbb {C}^{d_\textsc{B}}\), and let \(\{ M^x_a\} \), \(\{ N^x_a\} \) be families of POVMs on the two factors with a common question set \(\mathcal{X}\) and a common answer set. Their inconsistency on \(|\psi \rangle \) is
the probability that the two measurements return different answers. We say \(M\) and \(N\) are \(\delta \)-consistent if their inconsistency is at most \(\delta \).
Comments.
This is Definition 4.8 of [ 2 ] , in the two-space form used by Theorem 3.7. It is a different notion from the POVM distance of Definition 2.20: consistency compares two families across the two factors of the state, whereas \(\approx _\delta \) compares them as operator families.
2.4 Computability conventions
Turing machines are represented by their Gödel numbers; in Lean the intended model is Mathlib’s Nat.Partrec.Code, with \(\phi _e\) the partial function computed by code \(e\) and “\(e\) halts on empty input” meaning \((\texttt{e.eval } 0).\texttt{Dom}\). Running times are counted as in [ 8 ] ; polynomial-time computability of a function of strings and integers means time polynomial in the lengths of the string inputs and in \(\log \) of the integer inputs, unless an integer is explicitly given in unary.
A language \(L \subseteq \{ 0,1\} ^*\) is in \(\mathrm{RE}\) if it is the domain (equivalently, the range) of a partial computable function. The halting problem — the set of \(e\) such that \(\phi _e\) halts on the empty input — is \(\mathrm{RE}\)-complete under many-one reductions.
Following [ 8 ] , a pair \((e, n)\) of a Turing machine \(e\) and integer \(n\) is a succinct description of the string \(x \in \{ 0,1\} ^*\) if \(\left\vert {x} \right\vert \leq 2^n\), the runtime of \(e\) on input \(m\) is at most \((n+1)(\left\vert {m} \right\vert +1)^2\), and \(\phi _e(m)\) equals the \(m\)-th bit of \(x\) for \(m {\lt} \left\vert {x} \right\vert \), and \(2\) for \(m \geq \left\vert {x} \right\vert \). ( [ 8 ] require runtime at most \(n\) on every input; in a model that charges for reading its input this is vacuous for \(\left\vert {m} \right\vert {\gt} n\), and the polynomial slack in \(\left\vert {m} \right\vert \) is what the ambient model’s bit-indexing program achieves. Any fixed polynomial in \(n\) and \(\left\vert {m} \right\vert \) would do, provided the same one is used in Theorem 6.6.)
A game description is a tuple \(g = (n_\mathcal{X}, n_\mathcal{A}, w, \mathrm{acc})\) of two integers, a finite list \(w\) of weighted question pairs, and a finite list \(\mathrm{acc}\) of accepted answer tuples. It determines a synchronous game \(\mathfrak {G}_g\) on question alphabet \(\{ 0, \ldots , n_\mathcal{X}\} \) and answer alphabet \(\{ 0, \ldots , n_\mathcal{A}\} \): the question distribution is \(w\) normalized (a fixed point mass if \(w\) has total weight zero), and the predicate accepts exactly the tuples listed in \(\mathrm{acc}\), except that unequal answers to equal questions always lose. Game descriptions are first-order data and carry a canonical Gödel numbering (GameData in the Lean file).
2.5 Normal form verifiers
Games produced in the proof are presented by pairs of Turing machines: a sampler, generating questions by a rigid linear-algebraic procedure that introspection can certify, and a decider, checking answers.
An \(\ell \)-level sampler with field size \(q(n) = 2\) is a Turing machine \(\mathcal{S}\) that on input \(n\) specifies a linear space \(V = \mathbb {F}_2^{s(n)}\) and a pair of \(\ell \)-level conditionally linear functions \(L^\textsc{A}, L^\textsc{B}\) on \(V\) (Definition 6.1); the question distribution it samples is \(\mu _n = (L^\textsc{A}(z), L^\textsc{B}(z))\) for uniform \(z \in V\). Formally \(\mathcal{S}\) answers dimension, marginal, and linear-evaluation queries as in [ 1 ] ; the precise query interface is fixed in Section 6.1. \(\mathsf{TIME}_\mathcal{S}(n)\) denotes its maximal running time on queries with index \(n\).
A decider is a \(5\)-input Turing machine \(\mathcal{D}\), whose input is interpreted as \((n, x, y, a, b)\) with \(n\) an integer index and \(x, y, a, b\) strings. It accepts (output \(1\)) or rejects. \(\mathsf{TIME}_\mathcal{D}(n)\) denotes its maximal running time over inputs with index \(n\).
A normal form verifier is a pair \(\mathsf{V}= (\mathcal{S}, \mathcal{D})\) of a sampler and a decider. For each \(n\), \(\mathsf{V}\) determines a game \(\mathsf{V}_n\) with question distribution given by \(\mathcal{S}\) at index \(n\) and decision predicate \(D(x,y,a,b) = \mathcal{D}(n,x,y,a,b)\), where answers longer than \(\mathsf{TIME}_\mathcal{D}(n)\) are rejected. Symmetrizing the roles of the two players makes \(\mathsf{V}_n\) a synchronous game; we write \(\mathrm{val}^*(\mathsf{V}_n)\) and \(\mathrm{val}^{s}(\mathsf{V}_n)\) for its values. The description length \(\left\vert {\mathsf{V}} \right\vert = \max \{ \left\vert {\mathcal{S}} \right\vert , \left\vert {\mathcal{D}} \right\vert \} \), and the number of levels of \(\mathsf{V}\) is that of \(\mathcal{S}\).
For \(\lambda \in \mathbb {N}\), a normal form verifier \(\mathsf{V}= (\mathcal{S}, \mathcal{D})\) is \(\lambda \)-bounded if \(\mathsf{TIME}_\mathcal{S}(n), \mathsf{TIME}_\mathcal{D}(n) \leq n^\lambda \) for all \(n \geq 2\), and \(\left\vert {\mathsf{V}} \right\vert \leq \lambda \).
A language \(L\) is in \(\mathrm{MIP}^*\) (more precisely, \(\mathrm{MIP}^*_{1, 1/2}(2,1)\)) if there is a polynomial-time computable map \(z \mapsto \mathfrak {G}_z\) from strings to (descriptions of) games — given by a sampler and decider running in time \(\mathrm{poly}(\left\vert {z} \right\vert )\) — such that \(z \in L\) implies \(\mathrm{val}^*(\mathfrak {G}_z) = 1\) and \(z \notin L\) implies \(\mathrm{val}^*(\mathfrak {G}_z) \leq \frac12\).