- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
There is a separable II\(_1\) factor (indeed, a tracial von Neumann algebra generated by finitely many projections) that does not embed into an ultrapower \(\cal {R}^{\omega }\) of the hyperfinite II\(_1\) factor.
Kirchberg’s QWEP conjecture fails: there is a C\(^*\)-algebra that is not a quotient of a C\(^*\)-algebra with the weak expectation property; equivalently, \(C^*(F_2) \otimes _{\min } C^*(F_2) \neq C^*(F_2) \otimes _{\max } C^*(F_2)\).
There exist finite question and answer sets for which the closure \(C_{qa}\) of the set of finite-dimensional quantum correlations is strictly contained in the set \(C_{qc}\) of commuting-operator correlations.
There is no algorithm that, given a game description \(g\) with the promise that \(\mathrm{val}^{s}(\mathfrak {G}_g) = 1\) or \(\mathrm{val}^{s}(\mathfrak {G}_g) \leq \frac12\), decides which is the case.
[\(\uparrow \) QuantumLib] Let \(\mathfrak {G}= (\mathcal{X}, \mathcal{Y}, \mathcal{A}, \mathcal{B}, \mu , D)\) be a game and \(0 {\lt} \alpha {\lt} 1\). The \(\alpha \)-anchored version of \(\mathfrak {G}\) is the game \(\mathfrak {G}_\perp \) with question alphabets \(\mathcal{X}\cup \{ \perp \} \) and \(\mathcal{Y}\cup \{ \perp \} \) and the same answer alphabets, in which the referee samples \((x, y) \sim \mu \) and then, independently for each player, replaces that player’s question by the anchor symbol \(\perp \) with probability \(\alpha \); the decision predicate accepts whenever either question is \(\perp \), and otherwise applies \(D\). Unless indicated otherwise, \(\mathfrak {G}_\perp \) denotes the \(\frac12\)-anchored version.
[\(\uparrow \) QuantumLib] Let \(G\) be a finite group and \(\varepsilon \in \mathbb {R}\). An \(\varepsilon \)-approximate representation of \(G\) is a function \(f : G \to U(d)\) such that
where \(\langle \cdot , \cdot \rangle _{hs}\) is the normalized Hilbert–Schmidt inner product of Definition 2.19. Since each value of \(f\) is unitary, \(\left\| {f(x) f(y) - f(xy)} \right\| _{hs}^2 = 2 - 2\, \mathrm{Re}\, \langle f(x) f(y), f(xy) \rangle _{hs}\), so the condition is equivalent to the defect form \(\mathop{\mathbb {E}}_{x, y \sim G} \left\| {f(x) f(y) - f(xy)} \right\| _{hs}^2 \leq 2 \varepsilon \).
Let \(V = \mathbb {F}_q^s\) and \(\ell \geq 1\). An \(\ell \)-level conditionally linear (CL) function on \(V\) is defined recursively: a \(1\)-level CL function is a linear map \(L : V \to V\); an \(\ell \)-level CL function is given by a direct sum decomposition \(V = V_1 \oplus V_{{\gt}1}\), a linear map \(L_1\) on \(V_1\), and, for each value \(u\) of \(L_1\), an \((\ell -1)\)-level CL function \(L^{u}_{{\gt}1}\) on \(V_{{\gt}1}\); it maps \(z = z_1 + z_{{\gt}1}\) to \(L_1(z_1) + L^{L_1(z_1)}_{{\gt}1}(z_{{\gt}1})\). A CL distribution is the distribution of \((L^\textsc{A}(z), L^\textsc{B}(z))\) for uniformly random \(z \in V\) and CL functions \(L^\textsc{A}, L^\textsc{B}\).
[\(\uparrow \) QuantumLib] A commuting-operator strategy for \(\mathfrak {G}\) consists of a Hilbert space \(\mathcal{H}\) (a complete inner product space over \(\mathbb {C}\), of any dimension), a unit vector \(|\psi \rangle \in \mathcal{H}\), and POVMs \(\{ E^x_a\} _{a \in \mathcal{A}}\) and \(\{ F^y_b\} _{b \in \mathcal{B}}\) on \(\mathcal{H}\), one for each \(x\) (resp. \(y\)) — each \(E^x_a\) and \(F^y_b\) is a positive bounded operator, \(\sum _a E^x_a = I\) and \(\sum _b F^y_b = I\) — such that \(E^x_a F^y_b = F^y_b E^x_a\) for all \(x, y, a, b\). The players answer \((a, b)\) to questions \((x, y)\) with probability \(\langle \psi | E^x_a F^y_b |\psi \rangle \).
[\(\uparrow \) QuantumLib] The value of a commuting-operator strategy \(\mathscr {S}= (\mathcal{H}, \psi , E, F)\) in \(\mathfrak {G}\) is
and the commuting-operator value \(\omega ^{\mathrm{co}}(\mathfrak {G})\) of \(\mathfrak {G}\) is the supremum of \(\omega ^{\mathrm{co}}(\mathfrak {G}, \mathscr {S})\) over all commuting-operator strategies.
Let \(c\) be a machine code with \(i\) input tapes, \(x = (x_1, \ldots , x_i)\) bit strings and \(y \in \{ 0,1\} ^*\). The code \(c\) produces \(y\) on \(x\) if its run on \(x\) halts with output \(y\) (in some time and space). The budgeted evaluation of \(c\) on \(x\) with budget \(T\) returns the output if \(c\) has halted within \(T\) steps, and a timeout marker otherwise; it is total and executable, and the two notions agree: \(c\) produces \(y\) if and only if some budget suffices to observe it.
[\(\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)\).
[\(\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})\).
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\).
Let \(\mathfrak {G}= (\mathcal{X}, \mathcal{Y}, \mathcal{A}, \mathcal{B}, \mu , D)\) be a game and \(n \geq 0\) an integer. The \(n\)-fold direct repetition of \(\mathfrak {G}\) is the game \(\mathfrak {G}^{n}\) with question alphabets \(\mathcal{X}^n\), \(\mathcal{Y}^n\) and answer alphabets \(\mathcal{A}^n\), \(\mathcal{B}^n\), question distribution \(\mu ^{n}(\bar{x}, \bar{y}) = \prod _{i=1}^{n} \mu (x_i, y_i)\), and decision predicate \(D^{n}(\bar{x}, \bar{y}, \bar{a}, \bar{b}) = \bigwedge _{i=1}^{n} D(x_i, y_i, a_i, b_i)\). The direct repetition of a synchronous game is synchronous, with the same data.
[\(\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)\).
[\(\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 \).
[\(\uparrow \) QuantumLib] The fidelity between positive semidefinite matrices \(\rho , \sigma \) on \(\mathbb {C}^d\) is \(F(\rho , \sigma ) = \left\| {\sqrt{\rho }\sqrt{\sigma }} \right\| _1\), where \(\left\| {A} \right\| _1 = \operatorname{tr}\sqrt{A^\dagger A}\) denotes the trace norm.
[\(\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).
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).
[\(\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.
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 \).
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 \).
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\).
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\).
Let \(\mathbb {F}\) be a finite field with \(q\) elements and let \(m \geq 1\) and \(d\) be integers. The \((m,q,d)\)-low individual degree test is the two-player game in which the verifier picks one of the following three sub-tests with probability \(\tfrac 13\) each, having sampled a uniform point \(u \sim \mathbb {F}^m\).
Axis-parallel lines test. Sample a uniform direction \(i \sim [m]\) and a uniform role. One player receives the line \(\ell = \{ u + t e_i\} \) and answers a univariate polynomial \(f\) of degree at most \(d\); the other receives \(u\) and answers \(a \in \mathbb {F}\). Accept if \(f(u) = a\).
Self-consistency test. Both players receive \(u\) and answer elements of \(\mathbb {F}\). Accept if the answers are equal.
Diagonal lines test. Sample a uniform \(j \sim [m]\), a uniform direction \(v \in \mathbb {F}^m\) whose coordinates after the \(j\)-th vanish, and a uniform role. One player receives the line \(\ell = \{ u + t v\} \) and answers a univariate polynomial of degree at most \(md\); the other receives \(u\) and answers \(a \in \mathbb {F}\). Accept if \(f(u) = a\).
A machine code is first-order data: a header (number of work tapes, alphabet size, number of states, start state) and a dense transition table with one entry per observation, in a fixed canonical order. A well-formed code is interpreted as a multi-input machine, with binary input and output through two reserved alphabet symbols. Codes serialize exactly: the description \(\alpha \in \{ 0,1\} ^*\) of a code has size \(\left\vert {\alpha } \right\vert \), and total decoding interprets every string — \([\alpha ]_i\) denotes the coded machine with \(i\) input tapes described by \(\alpha \), with every malformed string denoting one fixed machine that immediately rejects.
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\).
A multi-input Turing machine with \(i\) input tapes and \(w\) work tapes has \(i\) two-way read-only input tapes (heads clamped one blank cell beyond either end of the input), \(w\) bidirectional work tapes over an alphabet extended with a blank symbol, and a write-only output stream. A transition may write and move on every work tape, move every input head, emit at most one output symbol, and either continue or halt. Time is counted in steps, and space as the number of work-tape cells visited.
At \(i = 1\) this is exactly the CSLib multi-tape model.
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}\).
[\(\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 \),
[\(\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.
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.
[\(\uparrow \) QuantumLib] For positive semidefinite \(\rho , \sigma \) on \(\mathbb {C}^d\), the relative entropy is \(D(\rho \, \| \, \sigma ) = \operatorname{tr}\bigl(\rho (\log \rho - \log \sigma )\bigr)\) if the support of \(\rho \) is contained in that of \(\sigma \), and \(+\infty \) otherwise; the relative min-entropy is \(D_\infty (\rho \, \| \, \sigma ) = \min \{ \lambda : \rho \leq 2^\lambda \sigma \} \), and \(+\infty \) if no such \(\lambda \) exists. For a bipartite state \(\rho ^{AB}\) the mutual information is \(I(A : B)_\rho = D(\rho ^{AB} \, \| \, \rho ^A \otimes \rho ^B)\), and for a tripartite state \(\rho ^{ABC}\) the conditional mutual information is \(I(A : B \, |\, C)_\rho = I(A : BC)_\rho - I(A : C)_\rho \).
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\).
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).
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.)
[\(\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)\).
[\(\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] 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] 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] For every game \(\mathfrak {G}\) and \(0 {\lt} \alpha {\lt} 1\),
Moreover the relation holds at the level of strategies, without change of dimension: extending a strategy for \(\mathfrak {G}\) by arbitrary answers on \(\perp \), or restricting a strategy for \(\mathfrak {G}_\perp \) to the original questions, translates value \(p\) in one game into value \(1 - (1-\alpha )^2 (1 - p)\) in the other. The same relation holds for the classical value.
For each arity \(i\) there are a machine code \(U\) with \(i + 2\) input tapes and a polynomial \(P\) such that on input \((\alpha ;\, T \text{ in binary};\, x)\), the machine \(U\) always halts within \(P(\left\vert {\alpha } \right\vert + T)\) steps, outputting the canonically encoded budgeted evaluation of \([\alpha ]_i\) on \(x\) with budget \(T\).
Exact decoding inverts encoding, distinct codes have distinct descriptions, and every description accepted by the exact decoder is the canonical encoding of the code it parses to.
Compositional, from paired prefix and soundness lemmas for each field of the description format.
Let \(A, B \subseteq \{ 0,1\} ^*\) be languages with distinguished elements \(y_{\mathrm{yes}} \in A\) and \(y_{\mathrm{no}} \in B\), and suppose that the complement of \(B\) is recursively enumerable: there is a program \(S\) that halts on input \(x\) if and only if \(x \notin B\). Suppose there is a polynomial-time computable function \(\textsc{Compr}: \{ 0,1\} ^* \times \mathbb {N}\to \{ 0,1\} ^*\) such that whenever \(\hat{x}\) is a succinct description (Definition 2.23) of a string \(x\) and \(y = \textsc{Compr}(\hat{x}, n)\):
if \(x \in A\) then \(y \in A\), and
if \(x \in B\) then \(y \in B\).
Then there is a polynomial-time computable function \(g\) reducing the halting problem to \((A, B)\): for every Turing machine \(e\), if \(\phi _e\) halts on the empty input then \(g(e) \in A\), and otherwise \(g(e) \in B\).
Fix a strategy for \(\mathfrak {G}_\perp ^{n}\), a set \(C \subseteq [n]\) with \(\Pr (W_C) {\gt} 0\), and let \(\delta \) be as in 1 and \(m = n - \left\vert {C} \right\vert \). Then, writing \(\mathop{\mathbb {E}}_{i}\) for the expectation over a uniform \(i \notin C\):
\(\mathop{\mathbb {E}}_{i} \, \left\| { P_{\Omega _i X_i Y_i | W_C} - P_{\Omega _i X_i Y_i} } \right\| \leq \sqrt{\delta }\);
\(\mathop{\mathbb {E}}_{i} \, \left\| { P_{X_i Y_i}\, P_{R_{-i} | X_i = \perp , Y_i = \perp , W_C} - P_{X_i Y_i}\, P_{R_{-i} | X_i, Y_i, W_C} } \right\| = O\bigl( \sqrt{\delta } / \alpha ^2 \bigr)\).
[\(\uparrow \) QuantumLib] For all density matrices \(\rho , \sigma \) on \(\mathbb {C}^d\),
Write \(\left\| {P - Q} \right\| \) for the total variation distance between distributions. Let \(U = (U_1, \ldots , U_m)\) be independent random variables and \(W\) an event with \(\Pr (W) {\gt} 0\). Then
More generally, let \(T, V\) be random variables such that \(P_{TUV} = P_T \prod _i P_{U_i | T} \cdot P_{V | TU}\) (the \(U_i\) are independent conditioned on \(T\)). Then
where \(\cal {V}\) is the support of \(V\).
For every polynomial-time computable \(f : \{ 0,1\} ^* \to \{ 0,1\} ^*\) there is a program \(e\) with \(\phi _e = \phi _{f(e)}\) and the runtime of \(e\) polynomially bounded in terms of that of \(f(e)\). (This is the direction used by Lemma 4.10; [ 8 ] states the runtimes as polynomially equivalent, and the converse direction would require a simulator that is never faster than the simulated program.)
In the setting above there exist, for every \(i \notin C\), \(r_{-i}\), \(x\) and \(y\), unitaries \(U_{r_{-i}, x}\) on the first player’s space and \(V_{r_{-i}, y}\) on the second player’s space such that
where \((x, y)\) is distributed according to the question distribution of \(\mathfrak {G}_\perp \).
[\(\uparrow \) QuantumLib] Let \(\mathrm{val}^*_{\mathrm{POVM}}(\mathfrak {G})\) be the supremum of the winning probabilities \(\sum _{x,y,a,b} \mu (x,y)\, D(x,y,a,b)\, \operatorname{tr}\bigl( (A^x_a \otimes B^y_b)\, \rho \bigr)\) over all finite sets \(S_\textsc{A}\), \(S_\textsc{B}\), density matrices \(\rho \) on \(\mathbb {C}^{S_\textsc{A}} \otimes \mathbb {C}^{S_\textsc{B}}\) and POVMs \(\{ A^x_a\} \) on \(\mathbb {C}^{S_\textsc{A}}\), \(\{ B^y_b\} \) on \(\mathbb {C}^{S_\textsc{B}}\). Then \(\mathrm{val}^*_{\mathrm{POVM}}(\mathfrak {G}) = \mathrm{val}^*(\mathfrak {G})\).
[\(\uparrow \) QuantumLib] For all density matrices \(\rho , \sigma \) on \(\mathbb {C}^d\),
[\(\uparrow \) QuantumLib] Let \(\rho = \rho ^{X_1 \cdots X_n A}\) and \(\sigma = \sigma ^{X_1} \otimes \cdots \otimes \sigma ^{X_n} \otimes \sigma ^A\) be states with \(X = X_1 \cdots X_n\) classical in both. Then
Let \(f : \{ 0,1\} ^* \to \mathbb {N}\cup \{ \infty \} \) be a function and \(A \subseteq \{ x : f(x) {\lt} \infty \} \) a nonempty language. Suppose there is a polynomial-time computable function \(\textsc{Compr}: \{ 0,1\} ^* \times \mathbb {N}\to \{ 0,1\} ^*\) such that whenever \(\hat{x}\) is a succinct description (Definition 2.23) of a string \(x\) and \(y = \textsc{Compr}(\hat{x}, n)\):
\(f(y) \geq \max \{ f(x), n \} \), and
if \(x \in A\) then \(y \in A\).
Then there is a polynomial-time computable function \(g\) reducing the halting problem to \(A\): for every Turing machine \(e\), if \(\phi _e\) halts on the empty input then \(g(e) \in A\), and otherwise \(f(g(e)) = \infty \).
[\(\uparrow \) QuantumLib] For all density matrices on finite-dimensional spaces, with subsystems as indicated:
(Nonnegativity) \(D(\rho \, \| \, \sigma ) \geq 0\);
(Monotonicity under partial trace) \(D(\rho ^{X} \, \| \, \sigma ^{X}) \leq D(\rho ^{XY} \, \| \, \sigma ^{XY})\);
(Composition with the min-entropy) if \(D(\rho \, \| \, \sigma ) \leq \lambda _1\) and \(D_\infty (\sigma \, \| \, \tau ) \leq \lambda _2\) then \(D(\rho \, \| \, \tau ) \leq \lambda _1 + \lambda _2\);
(Mutual information minimizes over product states) for all density matrices \(\sigma ^A\), \(\tau ^B\), \(D(\rho ^{AB} \, \| \, \sigma ^A \otimes \tau ^B) \geq I(A : B)_\rho \).
[\(\uparrow \) QuantumLib] Let \(\rho = \sum _x P(x) |x\rangle \langle x| \otimes \rho _x\) and \(\sigma = \sum _x Q(x) |x\rangle \langle x| \otimes \sigma _x\) be classical-quantum states. Then
where \(D(P \, \| \, Q)\) is the Kullback–Leibler divergence. In particular, for a classical-quantum state \(\rho ^{XE}\), \(I(X : E)_\rho = \mathop{\mathbb {E}}_{x} \, D(\rho ^E_x \, \| \, \rho ^E)\).
Let \(f \neq g : \mathbb {F}_q^m \to \mathbb {F}_q\) be polynomials of total degree at most \(d\). Then \(\Pr _{x \sim \mathbb {F}_q^m}[ f(x) = g(x) ] \leq d/q\).
There is a deterministic algorithm that, given an odd integer \(k {\gt} 0\), outputs in time \(\mathrm{poly}(k)\) a self-dual normal basis of \(\mathbb {F}_{2^k}\) over \(\mathbb {F}_2\) together with its multiplication tables.
There is a polynomial-time computable \(s\) such that \(\phi _{s(e,x)}(y) = \phi _e(x, y)\) for all \(e, x, y\), with the runtimes of \(e\) and \(s(e,x)\) polynomially equivalent.
[\(\uparrow \) QuantumLib] For all tripartite density matrices \(\rho ^{ABC}\), \(I(A : B \, |\, C)_\rho \geq 0\).
[\(\uparrow \) QuantumLib] For every synchronous game \(\mathfrak {G}\), \(\mathrm{val}^{s}(\mathfrak {G}) \leq \mathrm{val}^{\mathrm{co}}(\mathfrak {G})\).
[\(\uparrow \) QuantumLib] For every synchronous game \(\mathfrak {G}\), \(\mathrm{val}^{s}(\mathfrak {G}) \leq \mathrm{val}^*(\mathfrak {G})\).
[\(\uparrow \) QuantumLib] For every synchronous game \(\mathfrak {G}\), \(\mathrm{val}^{\mathrm{co}}(\mathfrak {G}) \leq \omega ^{\mathrm{co}}(\mathfrak {G})\).
For each arity \(i\) there are a machine code \(U\) with \(i + 1\) input tapes and a polynomial \(P\) such that for all \(\alpha \in \{ 0,1\} ^*\), all inputs \(x\) and all \(y\): \(U\) on \((\alpha ; x)\) produces \(y\) if and only if \([\alpha ]_i\) on \(x\) produces \(y\); and whenever \([\alpha ]_i\) halts on \(x\) within \(t\) steps, \(U\) halts on \((\alpha ; x)\) within \(P(\left\vert {\alpha } \right\vert + t)\) time and space.
There is a program \(u\) and a polynomial \(p\) such that \(\phi _u(e, x) = \phi _e(x)\) for all \(e, x\), with \(\mathrm{runtime}(u, (e,x)) \leq p\bigl(\left\vert {e} \right\vert , \left\vert {x} \right\vert , \mathrm{runtime}(e, x)\bigr)\).
The set \(\{ (g, p) : g \text{ a game description}, p \in \mathbb {Q}, \mathrm{val}^{s}(\mathfrak {G}_g) {\gt} p \} \) is recursively enumerable, and likewise for \(\mathrm{val}^*\).
There are universal constants \(C {\gt} 0\) and \(0 {\lt} c \leq 1\) such that for every synchronous game \(\mathfrak {G}\),
More precisely, every tensor-product strategy for \(\mathfrak {G}\) with value \(1 - \varepsilon \) is, up to local isometries, well-approximated on average by a convex combination of synchronous strategies each of value at least \(1 - C\varepsilon ^{c}\).
There is a polynomial-time Turing machine \(\mathsf{ComputeAnsRedVerifier}\) that on input \((\mathsf{V}, \lambda , \mu , \sigma )\), for \(\mathsf{V}\) an \(\ell \)-level normal form verifier with \(\left\vert {\mathcal{D}} \right\vert \leq \sigma \), \(\mathsf{TIME}_\mathcal{S}(n) \leq (\lambda n)^\mu \) and \(\mathsf{TIME}_\mathcal{D}(n) \leq (2^{\lambda n})^\mu \) for \(n \geq 2\), outputs a \(\max \{ \ell + 2, 5\} \)-level normal form verifier \(\mathsf{V}^{\mathsf{ar}}\) with \(\mathsf{TIME}_{\mathcal{S}^{\mathsf{ar}}}(n), \mathsf{TIME}_{\mathcal{D}^{\mathsf{ar}}}(n) = \mathrm{poly}\bigl( (\lambda n)^\mu , \sigma \bigr)\), whose sampler depends only on \((\mathcal{S}, \lambda , \mu , \sigma )\), and such that for some \(\delta (\varepsilon , n) = \sigma ^a \bigl( (\lambda n)^{\mu a} \varepsilon ^b + (\lambda n)^{-\mu b} \bigr)\) (universal constants \(a, b\)) and all \(n\):
(Completeness) If \(\mathsf{V}_n\) has a value-\(1\) symmetric PCC strategy then \(\mathsf{V}^{\mathsf{ar}}_n\) has a value-\(1\) PCC strategy.
(Soundness) If \(\mathrm{val}^{s}(\mathsf{V}^{\mathsf{ar}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^{s}(\mathsf{V}_n) \geq 1 - \delta (\varepsilon , n)\).
There exists a universal constant \(c {\gt} 0\) such that for every two-player game \(\mathfrak {G}\), all positive integers \(k\), all \(0 {\lt} \varepsilon \leq 1\), and all \(p\) satisfying
where \(s\) is the bit-length of the players’ answers in \(\mathfrak {G}\) and \(\mathfrak {G}_\perp \) is the anchored version of \(\mathfrak {G}\) (Definition 5.20, with \(\alpha = \frac12\)), it holds that
There is a universal constant \(C_0 {\gt} 0\) and a polynomial-time Turing machine \(\mathsf{Compress}\) that on input \((\mathsf{V}, \lambda )\) outputs a \(9\)-level normal form verifier \(\mathsf{V}^{\textsc{Compr}}= (\mathcal{S}^{\textsc{Compr}}, \mathcal{D}^{\textsc{Compr}})\) with \(\mathsf{TIME}_{\mathcal{S}^{\textsc{Compr}}}(n), \mathsf{TIME}_{\mathcal{D}^{\textsc{Compr}}}(n) = \mathrm{poly}(n, \lambda )\), where \(\mathcal{S}^{\textsc{Compr}}\) is independent of \(\mathsf{V}\) and computable from \(\lambda \) in time \(\mathrm{polylog}(\lambda )\). If moreover \(\mathsf{V}\) is a \(\lambda \)-bounded \(9\)-level normal form verifier, then for all \(n \geq C_0\) and \(N = 2^n\):
(Completeness) If \(\mathsf{V}_N\) has a value-\(1\) PCC strategy, then so does \(\mathsf{V}^{\textsc{Compr}}_n\).
(Soundness) If \(\mathrm{val}^{s}(\mathsf{V}_N) \leq \tfrac 12\) then \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Compr}}_n) \leq \tfrac 12\).
[\(\uparrow \) QuantumLib] There is a universal constant \(c {\gt} 0\) such that for every game \(\mathfrak {G}\) with nonempty alphabets and every integer \(n \geq 1\), writing \(\varepsilon = 1 - \omega ^{\mathrm{co}}(\mathfrak {G})\),
[\(\uparrow \) QuantumLib] There is a universal constant \(c {\gt} 0\) such that for every game \(\mathfrak {G}\) with nonempty answer alphabets and \(\mathrm{val}^*(\mathfrak {G}) {\lt} 1\), and every integer \(n \geq 1\), writing \(\varepsilon = 1 - \mathrm{val}^*(\mathfrak {G})\),
Let \(G\) be a finite group and \(f : G \to U(d)\) an \(\varepsilon \)-approximate representation of \(G\). Then there exist \(d' \geq d\), an isometry \(V : \mathbb {C}^d \to \mathbb {C}^{d'}\), and a representation \(\rho : G \to U(d')\) such that
There is a computable (indeed polynomial-time) map \(\cal {M}\mapsto \mathfrak {G}_{\cal {M}}\) from Turing machines to synchronous game descriptions, with games given by normal form verifiers satisfying the efficiency requirements of Definition 2.29, such that:
if \(\cal {M}\) halts on the empty input then \(\mathrm{val}^{s}(\mathfrak {G}_\cal {M}) = 1\), witnessed by a PCC strategy;
if \(\cal {M}\) does not halt on the empty input then \(\mathrm{val}^{s}(\mathfrak {G}_\cal {M}) \leq \tfrac 12\).
The halting problem is r.e. but not decidable; it is \(\mathrm{RE}\)-complete under many-one (indeed polynomial-time) reductions.
There is a polynomial-time Turing machine \(\mathsf{ComputeIntroVerifier}\) that on input \((\mathsf{V}, \lambda , \ell )\) returns a \(5\)-level normal form verifier \(\mathsf{V}^{\textsc{Intro}}= (\mathcal{S}^{\textsc{Intro}}, \mathcal{D}^{\textsc{Intro}})\) with \(\mathsf{TIME}_{\mathcal{S}^{\textsc{Intro}}}(n) = \mathrm{poly}(n, \lambda , \ell )\), \(\mathsf{TIME}_{\mathcal{D}^{\textsc{Intro}}}(n) = \mathrm{poly}(2^{\lambda n}, \ell )\) and \(\left\vert {\mathcal{D}^{\textsc{Intro}}} \right\vert = \mathrm{poly}(\lambda , \ell )\), such that for every \(\lambda \)-bounded \(\ell \)-level verifier \(\mathsf{V}\) there is a function \(\delta (\varepsilon , n) = a\bigl( (\lambda n)^a \varepsilon ^b + (\lambda n)^{-b} \bigr)\) (constants \(a, b\) depending only on \(\ell \)) with, for all \(n\):
(Completeness) If \(\mathsf{V}_{2^n}\) has a value-\(1\) PCC strategy, so does \(\mathsf{V}^{\textsc{Intro}}_n\).
(Soundness) If \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Intro}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^{s}(\mathsf{V}_{2^n}) \geq 1 - \delta (\varepsilon , n)\).
Let
Let \(\mathscr {S}= (|\psi \rangle , A, B)\) be a tensor-product strategy for the \((m,q,d)\)-low individual degree test that succeeds with probability at least \(1 - \varepsilon \), and let \(k\) be an integer with \(k \geq 400md\) and \(k {\gt} 0\). Then there exist projective measurements \(G^\textsc{A}= \{ G^\textsc{A}_g\} \) on Alice’s space and \(G^\textsc{B}= \{ G^\textsc{B}_g\} \) on Bob’s space, both with outcomes the polynomials \(g\) in \(m\) variables of individual degree at most \(d\), such that, writing \(\delta = \delta _{lidt}(\varepsilon , m, d, q, k)\) and letting \(u \sim \mathbb {F}^m\) be uniform:
Alice’s point measurement \(A^u\) and the evaluation \(G^\textsc{B}_{[g(u) = \cdot ]}\) are \(\delta \)-consistent;
the evaluation \(G^\textsc{A}_{[g(u) = \cdot ]}\) and Bob’s point measurement \(B^u\) are \(\delta \)-consistent;
\(G^\textsc{A}\) and \(G^\textsc{B}\) are \(\delta \)-consistent.
There is a computable map \(g\) from Turing machines to game descriptions such that for every Turing machine \(\cal {M}\):
(Completeness) if \(\cal {M}\) halts on the empty input, then \(\mathrm{val}^{s}(\mathfrak {G}_{g(\cal {M})}) = 1\);
(Soundness) if \(\cal {M}\) does not halt on the empty input, then \(\mathrm{val}^{s}(\mathfrak {G}_{g(\cal {M})}) \leq \tfrac 12\).
Let \(\mathscr {S}= (|\psi \rangle , A, B)\) be a strategy that succeeds in the Magic Square game \(\mathfrak {G}^{\mathrm{MS}}\) with probability \(1 - \varepsilon \). Then there exist local isometries \(\phi _\textsc{A}: \mathcal{H}_\textsc{A}\to (\mathbb {C}^2)^{\otimes 2} \otimes \mathcal{H}_{\textsc{A}''}\), \(\phi _\textsc{B}: \mathcal{H}_\textsc{B}\to (\mathbb {C}^2)^{\otimes 2} \otimes \mathcal{H}_{\textsc{B}''}\) and a state \(|\textsc{aux}\rangle \in \mathcal{H}_{\textsc{A}''} \otimes \mathcal{H}_{\textsc{B}''}\) such that
and, writing \(\tilde A = \phi _\textsc{A}A \phi _\textsc{A}^\dagger \), the observables for the questions \(\textsc{Variable}_1\) and \(\textsc{Variable}_5\) satisfy \(\tilde A^{\textsc{Variable}_1}_b \approx _{\sqrt\varepsilon } \sigma ^X_b \otimes I\) and \(\tilde A^{\textsc{Variable}_5}_b \approx _{\sqrt\varepsilon } \sigma ^Z_b \otimes I\) on \(|\textsc{EPR}_2\rangle ^{\otimes 2} \otimes |\textsc{aux}\rangle \) (and symmetrically for \(\tilde B\)). In particular the corresponding \(\pm 1\)-observables approximately anticommute: \(\tilde A^{\textsc{Variable}_1} \tilde A^{\textsc{Variable}_5} \approx _{\sqrt\varepsilon } - \tilde A^{\textsc{Variable}_5} \tilde A^{\textsc{Variable}_1}\).
There is a polynomial-time Turing machine \(\mathsf{ComputeOracleVerifier}\) mapping a normal form verifier \(\mathsf{V}= (\mathcal{S}, \mathcal{D})\) to a normal form verifier \(\mathsf{V}^{\textsc{Orac}}\) such that, for some \(\delta (\varepsilon ) = \mathrm{poly}(\varepsilon )\) and all \(n\):
(Completeness) If \(\mathsf{V}_n\) has a value-\(1\) PCC strategy then \(\mathsf{V}^{\textsc{Orac}}_n\) has a value-\(1\) symmetric PCC strategy.
(Soundness) If \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Orac}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^{s}(\mathsf{V}_n) \geq 1 - \delta (\varepsilon )\).
(Complexity) The sampler of \(\mathsf{V}^{\textsc{Orac}}\) depends only on \(\mathcal{S}\), with \(\mathsf{TIME}\) within a constant factor and the same number of levels.
There is a universal constant \(C {\gt} 0\) such that the following holds. Let \((\cal {M}, \tau )\) be a von Neumann algebra with a normal faithful tracial state (for the finite-dimensional case, \(\cal {M} = M_d(\mathbb {C})\) with the normalized trace). Let \(\{ M_a\} _{a \in \mathcal{A}}\) be a POVM in \(\cal {M}\) that is \(\varepsilon \)-nearly projective:
Then there is a projective measurement \(\{ P_a\} _{a \in \mathcal{A}}\) in \(\cal {M}\) with
The same holds, on average, for a family \(\{ M^x_a\} \) indexed by \(x \sim \mu \).
There are universal constants \(b, c, c' {\gt} 0\) and a polynomial-time Turing machine \(\mathsf{ComputeRepeatedVerifier}\) that on input \((\mathsf{V}, \lambda , \tau )\) outputs a normal form verifier \(\mathsf{V}^{\textsc{Rep}}\) whose game \(\mathsf{V}^{\textsc{Rep}}_n\) is the \(k(n)\)-fold direct repetition (Definition 5.1) of \(\mathsf{V}_n\), with \(k(n) = (\lambda n)^{(1 + c')\tau }\), such that if \(\mathsf{V}\) is \(\ell \)-level then \(\mathsf{V}^{\textsc{Rep}}\) is \(\ell \)-level with \(\mathsf{TIME}_{\mathcal{S}^{\textsc{Rep}}}(n) = O(k(n) \mathsf{TIME}_\mathcal{S}(n))\) and \(\mathsf{TIME}_{\mathcal{D}^{\textsc{Rep}}}(n) = O\bigl(k(n) \max (\mathsf{TIME}_\mathcal{D}(n), (\lambda n)^\tau )\bigr)\), the sampler of \(\mathsf{V}^{\textsc{Rep}}\) depends only on \((\mathcal{S}, \lambda , \tau )\), and for all \(n\):
(Completeness) If \(\mathsf{V}_n\) has a value-\(1\) PCC strategy and \(\mathsf{TIME}_\mathcal{D}(n) \leq (\lambda n)^\tau \), then \(\mathsf{V}^{\textsc{Rep}}_n\) has a value-\(1\) PCC strategy.
(Soundness) For all \(\varepsilon {\gt} 0\), if \(\mathrm{val}^{s}(\mathsf{V}_n) \leq 1 - \varepsilon \) and \(\mathsf{TIME}_\mathcal{D}(n) \leq (\lambda n)^\tau \), then \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Rep}}_n) \leq \exp \bigl( -c\, \varepsilon ^{b}\, k(n) / (\lambda n)^{\tau } \bigr)\); in particular \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Rep}}_n) \leq \frac12\) whenever \(\varepsilon \geq (\lambda n)^{-\tau }\), for \(c'\) large enough and \(n \geq 2\).
There exists a function
for universal constants \(a \geq 1\) and \(0 {\lt} b {\lt} 1\) such that the following holds. For all admissible parameter tuples \(\mathsf{qldparams}= (q, m, d)\) and all strategies \(\mathscr {S}= (|\psi \rangle , A, B)\) for the game \(\mathfrak {G}^{\textsc{Pauli}}_{\mathsf{qldparams}}\) that succeed with probability at least \(1 - \varepsilon \), there exist local isometries \(\phi _\textsc{A}, \phi _\textsc{B}\) mapping into \(\mathcal{H}' \otimes (\mathbb {C}^q)^{\otimes M}\) with \(M = 2^m\), and a state \(|\textsc{aux}\rangle \), such that \(\left\| {\phi _\textsc{A}\otimes \phi _\textsc{B}|\psi \rangle - |\textsc{aux}\rangle \otimes |\textsc{EPR}_q\rangle ^{\otimes M}} \right\| \leq \delta _{qld}\), and for \(W \in \{ X, Z\} \) the measurements for the questions \((\textsc{Pauli}, W)\) are \(\delta _{qld}\)-close to the Pauli basis measurements \(\tau ^W_u\), \(u \in \mathbb {F}_q^M\), acting on \(|\textsc{EPR}_q\rangle ^{\otimes M}\).
There is an explicit synchronous game \(\mathfrak {G}^{\textsc{Sep}}\) with \(\mathrm{val}^*(\mathfrak {G}^{\textsc{Sep}}) \leq \frac12\) and \(\mathrm{val}^{\mathrm{co}}(\mathfrak {G}^{\textsc{Sep}}) = 1\).
There is a polynomial-time algorithm that, given a decider \(\mathcal{D}\), an index \(n\), a time bound \(T\) (in binary) and strings \(x, y\), outputs a succinct description (in the sense of Definition 2.23, via Boolean formulas) of a 3SAT instance \(\varphi \) of size \(2^{\mathrm{poly}(\log T)}\) such that \(\varphi \) is satisfiable if and only if there exist strings \(a, b\) of length at most \(T\) with \(\mathcal{D}(n, x, y, a, b) = 1\) within \(T\) steps; moreover satisfying assignments of \(\varphi \) encode the computation tableau together with \((a,b)\).
[\(\uparrow \) QuantumLib] Let \(\mathcal{X}\) and \(\mathcal{A}\) be finite nonempty sets. Call a correlation \(q(a, b \mid x, y)\) on question alphabets \(\mathcal{X}, \mathcal{X}\) and answer alphabets \(\mathcal{A}, \mathcal{A}\) tracially embeddable if there are: a unital \(*\)-algebra \(\mathscr {A}\) over \(\mathbb {C}\) with a tracial state \(\tau \) (\(\tau (1) = 1\), \(\tau (ab) = \tau (ba)\), \(\tau (a^*) = \overline{\tau (a)}\)); a Hilbert space \(\mathcal{H}\) with a linear map \(\iota : \mathscr {A}\to \mathcal{H}\) of dense range satisfying \(\langle \iota a, \iota b \rangle = \tau (a^* b)\), on which \(\mathscr {A}\) acts on the left by bounded operators \(L(a)\) with \(L(a)\, \iota b = \iota (ab)\); a positive element \(\sigma \in \mathscr {A}\) with \(\tau (\sigma ^* \sigma ) = 1\); POVMs \(\{ E^x_a\} _{a} \subseteq \mathscr {A}\) of positive elements summing to \(1\); and POVMs \(\{ G^y_b\} _{b}\) of positive bounded operators on \(\mathcal{H}\) summing to \(I\) and commuting with \(L(\mathscr {A})\), such that
Then every commuting-operator correlation \(p(a, b \mid x, y) = \langle \psi | E^x_a F^y_b |\psi \rangle \) on these alphabets (Definition 5.2) is an \(\ell ^1\)-limit of tracially embeddable correlations: for every \(\delta {\gt} 0\) there is a tracially embeddable \(q\) with \(\sum _{x, y, a, b} \left\vert {p(a, b \mid x, y) - q(a, b \mid x, y)} \right\vert {\lt} \delta \).
[\(\uparrow \) QuantumLib] Let \(|\psi \rangle , |\varphi \rangle \in \mathcal{H}_A \otimes \mathcal{H}_B\) be unit vectors and let \(\rho , \sigma \) denote their reduced density matrices on \(\mathcal{H}_A\). Then there exists a unitary \(V\) on \(\mathcal{H}_B\) such that