3 Background results
This chapter collects theorems that the proof relies on but whose proofs appear in other papers. Each entry gives a full statement, a pointer to the literature, and comments on its role and on formalization. The project may initially assume these as axioms; discharging them are independent sub-projects. Three of these results are larger sub-projects and are developed in their own sections: the computability results in Section 4 and parallel repetition in Section 5; they are included in the summary table below for completeness. The general-purpose quantum information facts feeding the parallel repetition proof (fidelity and Uhlmann’s theorem, a relative entropy toolkit, quantum Raz’s lemma) are collected in Section 5.2 and likewise appear in the table. Statements are given in the form closest to how they will be used; where the source states a bipartite version and the project needs a synchronous one (see Section 1.3), the translation is part of the formalization task and is noted in the comments.
Each entry carries an estimate of the formalization effort: [\(\bullet \) easy] for self-contained arguments of at most a few pages, [\(\bullet \bullet \) medium] for substantial but well-delimited developments, and [\(\bullet \bullet \bullet \) hard] for results whose formalization is a project in itself; [\(\checkmark \) (mostly) in Mathlib] marks statements essentially available in Mathlib. The estimates are for the statement as it will be used (including any synchronous translation) and are of course provisional. Independently of the effort estimate, the [\(\uparrow \) QuantumLib] badge (introduced in Section 2) marks results of general quantum-information interest that are intended to be upstreamed to QuantumLib.
|
Result |
Statement |
Source |
Effort |
|
Gowers–Hatami |
Thm. 3.2 |
||
|
Almost-synchronous correlations |
Thm. 3.3 |
[ 6 ] |
hard |
|
Orthonormalization |
Thm. 3.4 |
[ 5 ] |
medium |
|
Magic Square rigidity |
Thm. 3.5 |
[ 11 ] |
easy |
|
Low individual degree test (classical) |
Thm. 3.7 |
[ 2 ] |
|
|
Low individual degree test (Pauli) |
Thm. 3.8 |
[ 2 ] |
hard |
|
Anchored parallel repetition |
Thm. 5.22 |
[ 7 ] |
hard |
|
Direct parallel repetition (commuting-operator) |
Thm. 5.5 |
[ 31 ] |
|
|
Direct parallel repetition (entangled) |
Thm. 5.6 |
[ 30 ] |
\(^\dagger \) |
|
Tracial density |
Thm. 5.8 |
||
|
Uhlmann, Fuchs–van de Graaf |
medium |
||
|
Relative entropy toolkit |
medium |
||
|
Quantum Raz’s lemma |
Lem. 5.18 |
[ 7 ] |
easy |
|
Holenstein conditioning lemmas |
Lem. 5.19 |
[ 28 ] |
easy |
|
Recursive compression lemma |
Lem. 4.10 |
[ 8 ] |
|
|
Compressibility criterion |
Lem. 4.11 |
[ 10 ] |
|
|
Efficient computability toolkit |
[ 8 ] |
hard |
|
|
Halting undecidability |
Thm. 3.9 |
Mathlib |
|
|
Succinct Cook–Levin |
Thm. 3.10 |
hard |
|
|
Self-dual normal bases |
Lem. 3.11 |
medium |
|
|
Schwartz–Zippel |
Lem. 3.12 |
||
|
Value approximable from below |
Lem. 3.13 |
folklore |
medium |
\(^\dagger \)The Lean proof of Theorem 5.6 is complete modulo Lemma 5.7, which is stated in Lean but not yet proved. Theorem 5.22 and the results of Section 5.2 are no longer on the path to the main theorem (Remark 5.9).
3.1 The Gowers–Hatami theorem
[\(\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 \(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
Let \(L(G, \mathbb {C}^d) \cong \mathbb {C}^{|G| d}\) carry the inner product normalized by \(1/|G|\), let \(V : \mathbb {C}^d \to L(G, \mathbb {C}^d)\) be the map \(u \mapsto (x \mapsto f(x) u)\), and let \(\rho \) be the right regular representation, \((\rho (x) F)(y) = F(yx)\). Then \(V\) is an isometry, and the compression \(V^\dagger \rho (x) V = \mathop{\mathbb {E}}_{y \sim G} f(y)^\dagger f(yx)\) is an average of unitaries, hence has squared Hilbert–Schmidt norm at most \(1\). Moreover \(\mathop{\mathbb {E}}_{x} \mathrm{Re}\, \langle f(x), V^\dagger \rho (x) V \rangle _{hs} = \mathop{\mathbb {E}}_{x, y} \mathrm{Re}\, \langle f(x) f(y), f(xy) \rangle _{hs} \geq 1 - \varepsilon \) by hypothesis, and the claim follows by expanding \(\left\| {f(x) - V^\dagger \rho (x) V} \right\| _{hs}^2\). The construction gives \(d' = |G|\, d\).
Source.
Gowers and Hatami [ 4 ] . A quantitative form suited to applications in nonlocal games, and a version adapted to the tracial setting, is given by de la Salle [ 5 ] and in [ 6 ] .
Comments.
This is the stability result underlying all rigidity (self-testing) arguments in the proof: an approximate representation of the Pauli group \(\mathbb {F}_2^{2k}\) (with its cocycle) is close to an exact one, which forces the presence of EPR pairs. The statement above is fully formalized (statement and proof) in MIPRE/Background/GowersHatami/Basic.lean, following the regular-representation argument sketched in the proof; the intermediate statement, with the exact representation living on the concrete index set \(G \times \{ 1, \dots , d\} \), is MIPRE.gowers_hatami_prod. Two remarks on the statement. (i) It asserts only \(d' \geq d\), with witness \(d' = |G| d\); it does not include the dimension bound \(d' \leq (1 + C\varepsilon ) d\) of [ 4 ] , whose proof goes through the Fourier-analytic route via irreducible representations. Whether the sharper bound is needed downstream (in the Pauli-group application feeding Theorem 3.8) is to be revisited; if so it will be added as a separate strengthening. (ii) In the Lean encoding the isometry is stored as the \(d \times d'\) matrix of its adjoint, so the isometry condition reads \(V V^\dagger = I\) and the compression is written \(V \rho (x) V^\dagger \). The normalized Hilbert–Schmidt norm is the tracial form needed for the synchronous framework [ 5 , 6 ] .
3.2 Almost-synchronous correlations
[\(\bullet \bullet \bullet \) hard] [\(\uparrow \) QuantumLib]
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}\).
Source.
Vidick [ 6 ] , building on [ 17 , 18 ] ; the statement above is the corollary needed here, with constants independent of the game’s size.
Comments.
The proof uses the orthonormalization lemma (Section 3.3) and a rounding argument.
3.3 The orthonormalization lemma
[\(\bullet \bullet \) medium] [\(\uparrow \) QuantumLib]
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 \).
Source.
de la Salle [ 5 ] , which gives a dimension-free bound with explicit constants; earlier versions with worse parameters appear in [ 17 ] and in [ 1 ] .
Comments.
Used constantly: soundness analyses produce POVMs that are only approximately projective, and this lemma replaces them by genuinely projective measurements on the same space, which is what makes the “projective strategies throughout” convention of Section 1.3 viable (avoiding Naimark dilation). The finite-dimensional case suffices for the main theorem and is a clean, self-contained formalization target in linear algebra.
3.4 Magic Square rigidity
[\(\bullet \) easy] [\(\uparrow \) QuantumLib]
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}\).
Source.
Wu, Bancal, McKague and Scarani [ 11 ] ; the game is the Mermin–Peres magic square. The form above is [ 1 , Section 8 ] .
Comments.
This is the elementary seed of all rigidity in the proof: it certifies a single pair of anticommuting observables, which the low individual degree test then amplifies to many qubits. The game is constant-sized, the proof is a page of algebra, and it is an excellent first self-testing target. The synchronous restatement (one measurement family, tracial state) should be derived once and reused as a template for the other rigidity statements.
3.5 The classical low individual degree test
[\(\bullet \bullet \bullet \) hard]
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\).
Comments.
This is Figure 1 of [ 2 ] . The direction \(v\) of the diagonal lines test may be zero, in which case the “line” is the single point \(u\); this degenerate case is part of the test as stated. In the formalization, line questions are the lines themselves, presented canonically (the direction is rescaled so that its first nonzero coordinate is \(1\), and the base point is the point of the line whose corresponding coordinate vanishes), so that the same line asked by two sub-tests is the same question; a line answer is a polynomial in the parameter of that canonical parametrization.
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.
This is Theorem 1.3 of [ 2 ] (thm:main-formal there), whose proof is the MIPStarRE formalization vendored into this repository. The Lean proof translates a strategy for our game into MIPStarRE’s strategy container (the state as a density matrix; the line measurements as coarse-grainings of the measurements at the canonical line questions along the change of parametrization, which makes them covariant under rebasing), shows that MIPStarRE’s failure surrogate is at most the rejection probability \(1 - \mathrm{val}\) (the consistency defect of each branch is at most the rejection probability of that branch, since acceptance forces the coarse-grained answers to agree), applies their main theorem, and reads the resulting measurements back into our vocabulary.
Source.
Ji, Natarajan, Vidick, Wright and Yuen [ 2 ] , Theorem 1.3 (the formal version for general, not necessarily symmetric, strategies). The proof is a formalization by Sirui Lu and collaborators (https://github.com/LionSR/MIPStarRE), vendored into this repository with the authors’ permission at MIPRE/Background/LIDT/MIPStarRE/; the statement above is this project’s own, and is connected to theirs by an explicit bridge.
Comments.
Two hypotheses correct the printed statement, as established by that formalization: the sampling parameter satisfies \(k \geq 400md\) where the paper prints \(k \geq md\), and \(k\) must be positive, since the printed error vanishes at \(k = 0\). The parameter \(k\) remains free: the error carries both a factor \(k^2\) and a term \(e^{-k/(2560000m^2)}\), so no single choice of \(k\) reduces it to a function of \((\varepsilon , m, d, q)\); a corollary in the shape of \(\delta _{qld}\) below is a separate derivation.
3.6 The quantum low individual degree test
[\(\bullet \bullet \bullet \) hard] [\(\uparrow \) QuantumLib]
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}\).
Source.
Ji, Natarajan, Vidick, Wright and Yuen [ 2 ] , which proves quantum soundness of the classical low individual degree test and derives the Pauli basis test; this corrects the analysis of the total degree test relied on in early versions of [ 1 ] . The reduction from the Pauli test to the low individual degree test follows [ 1 , Section 7 ] , with the Magic Square theorem (Theorem 3.5) providing the base anticommutation.
Comments.
This is the largest and hardest imported result: its proof is an induction on the number of variables with a delicate self-improvement argument. It is the workhorse of question reduction (introspection certifies the players’ sampling of their own questions against Pauli basis measurements). Its classical ingredient is now available as Theorem 3.7; what remains is the reduction from the Pauli basis test, which uses Theorem 3.5 for the base anticommutation and Theorem 3.2 and Theorem 3.4 as black boxes, together with a corollary of Theorem 3.7 collapsing the sampling parameter \(k\) into a single error function.
3.7 Undecidability of the halting problem
[\(\checkmark \) (mostly) in Mathlib]
The halting problem is r.e. but not decidable; it is \(\mathrm{RE}\)-complete under many-one (indeed polynomial-time) reductions.
Source.
Turing (1936); in Mathlib as part of the Computability library.
Comments.
Listed to close the dependency graph: combined with the halting reduction (Theorem 6.9) it yields undecidability of approximating the game value, and \(\mathrm{RE}\)-completeness gives \(\mathrm{RE}\subseteq \mathrm{MIP}^*\).
3.8 Cook–Levin and succinct satisfiability
[\(\bullet \bullet \bullet \) hard]
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)\).
Source.
Cook [ 20 ] and Levin for the tableau reduction; Papadimitriou and Yannakakis [ 19 ] for succinct representations and their complexity; the explicit form needed here is [ 1 , Section 10 ] .
Comments.
This is the classical core of answer reduction: the players prove satisfiability of \(\varphi \) (arithmetized over a low-degree extension) instead of sending \((a,b)\). The statement is long but entirely combinatorial. Cook–Levin has been formalized in other proof assistants; a Lean formalization with the explicit-uniformity guarantees above is a substantial but well-specified sub-project.
3.9 Self-dual normal bases
[\(\bullet \bullet \) medium]
blue( Thomas: Is this needed? )
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.
Source.
Combines Shoup’s deterministic irreducible-polynomial construction [ 21 ] , Lenstra’s isomorphism algorithm [ 22 ] , and the classical existence and construction of self-dual normal bases in characteristic \(2\) for odd \(k\); see the discussion in [ 1 , Section 3 ] .
Comments.
Needed so that verifiers can do field arithmetic over \(\mathbb {F}_{2^k}\) using only \(\mathbb {F}_2\)-data (the “downsize” maps), uniformly and deterministically. This is why field sizes are restricted to \(q = 2^k\), \(k\) odd (“admissible”). Self-contained algebra/algorithmics; independent of everything quantum.
3.10 The Schwartz–Zippel lemma
[\(\checkmark \) (mostly) in Mathlib]
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\).
Source.
[ 23 , 24 ] . A version is available in Mathlib (multivariate polynomials over finite fields).
Comments.
Used throughout the low-degree machinery (distance of the Reed–Muller code, soundness of arithmetization). The variant for individual degree should be derived alongside it.
3.11 Approximating the value from below (\(\mathrm{MIP}^*\subseteq \mathrm{RE}\))
[\(\bullet \bullet \) medium]
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}^*\).
Source.
Folklore; see [ 1 , Section 12 ] . Enumerate tensor-product strategies with entries in \(\mathbb {Q}[i]\) and evaluate; density of such strategies among all tensor-product strategies gives completeness of the enumeration.
Comments.
This is the easy inclusion \(\mathrm{MIP}^*\subseteq \mathrm{RE}\) and one half of Theorem 7.3. The commuting-operator analogue (approximating \(\mathrm{val}^{\mathrm{co}}\) from above via the NPA hierarchy [ 25 ] ) is not needed for the main theorem, but becomes relevant for the downstream consequences in Section 8.