5 Parallel repetition
This chapter states the parallel repetition theorems available for gap amplification in the compression procedure (Section 6.5). It has two parts. Section 5.1 states direct (unanchored) parallel repetition in value form, for entangled and for commuting-operator strategies, together with Lin’s tracial density theorem. These theorems are formalized: two external Lean developments proving them are vendored into this repository, and the section records their statements in the vocabulary of Section 2 together with the bridges connecting the two. Sections 5.2–5.4 state the anchored, entanglement-preserving theorem of Bavarian, Vidick and Yuen [ 7 ] used in [ 1 ] : repeating the anchored version of a game amplifies the completeness-soundness gap while preserving entanglement lower bounds. That theorem is a blueprint-only external result, and it is no longer on the path to the main theorem: the pipeline of Section 6 is stated in value form and uses the direct theorems (Remark 5.9). The anchored sections are kept as the record of the entanglement-form route of [ 1 ] , whose remaining interest is the entanglement-requirement corollaries (Remark 6.8). Section 5.2 collects the background results the anchored proof relies on — entropy inequalities, Uhlmann’s theorem — most of which are natural QuantumLib content, and some of which already exist there. Section 5.3 defines the anchoring transformation and states the theorem, and Section 5.4 decomposes the proof into its main steps.
5.1 Direct parallel repetition
The \(n\)-fold direct repetition of a game asks \(n\) independent question pairs at once and accepts if all \(n\) answer pairs are accepted. Two recent Lean developments prove that the value of the repeated game decays exponentially in \(n\), for every game, with no anchoring and at a rate depending only on the gap \(1 - \mathrm{val}(\mathfrak {G})\) and on the size of the answer alphabets: one for tensor-product (entangled) strategies, by OpenAI [ 30 ] , and one for commuting-operator strategies [ 31 ] , the latter building on the former and on Lin’s tracial density theorem [ 9 ] . Both are vendored into this repository (MIPRE/Background/Repetition/, with provenance recorded in the README.md of each directory) and connected to the definitions of Section 2 by explicit bridges; the statements below are the bridged forms. The commuting-operator theorem is recorded now, although only the entangled one enters \(\mathrm{MIP}^*= \mathrm{RE}\), because it is the form needed for the commuting-operator counterpart \(\mathrm{MIP}^{\mathrm{co}}= \mathrm{coRE}\) [ 10 ] (Remark 8.5).
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.
The entangled theorem is stated for the quantum value of Definition 2.9, whose strategies are bipartite. The commuting-operator theorem needs the bipartite counterpart of the commuting value, which Section 2 defines in synchronous (tracial) form only (Definition 2.11); the two are related by Lemma 5.4.
[\(\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.
Comments.
As in Definition 2.9, the formalization takes the real part of the (real, nonnegative) probability. The Hilbert space of a strategy lives in the lowest universe, as in the vendored development; this is no restriction for the suprema, which are bounded by \(1\). The notation \(\omega ^{\mathrm{co}}\) follows [ 31 ] and keeps the bipartite value apart from the tracial value \(\mathrm{val}^{\mathrm{co}}\) of Definition 2.11.
[\(\bullet \bullet \) medium] [\(\uparrow \) QuantumLib]
[\(\uparrow \) QuantumLib] For every synchronous game \(\mathfrak {G}\), \(\mathrm{val}^{\mathrm{co}}(\mathfrak {G}) \leq \omega ^{\mathrm{co}}(\mathfrak {G})\).
Let \((\mathscr {A}, \tau , M)\) be a commuting strategy (Definition 2.5) and let \(\mathcal{H}= L^2(\mathscr {A}, \tau )\) be the completion of \(\mathscr {A}\) for the inner product \(\langle a, b \rangle = \tau (a^* b)\), with the class of \(1\) as the unit vector \(\xi \). Left multiplication \(\pi (a) : b \mapsto ab\) and right multiplication \(\rho (a) : b \mapsto ba\) extend to bounded operators on \(\mathcal{H}\) (for \(\rho \) this uses traciality: \(\left\| {ba} \right\| ^2 = \tau (a^* b^* b a) = \tau (b^* b\, a a^*) \leq \left\| {a} \right\| ^2 \left\| {b} \right\| ^2\)), commute with each other, and satisfy \(\rho (p)^* = \rho (p^*)\) (again by traciality) so that \(\rho \) maps projections to projections. Setting \(E^x_a = \pi (M^x_a)\) and \(F^y_b = \rho (M^y_b)\) gives a commuting-operator strategy with \(\langle \xi | E^x_a F^y_b |\xi \rangle = \langle 1, M^x_a M^y_b \rangle = \tau (M^x_a M^y_b)\), hence with the same value as \((\mathscr {A}, \tau , M)\). Taking suprema yields the claim.
Comments.
This is the direction needed to apply Theorem 5.5 to the tracial value used in the pipeline: a bound on \(\omega ^{\mathrm{co}}(\mathfrak {G}^n)\) is a bound on \(\mathrm{val}^{\mathrm{co}}(\mathfrak {G}^n)\). The reverse comparison (from \(\omega ^{\mathrm{co}}\) to \(\mathrm{val}^{\mathrm{co}}\), which is false in general and true up to error for synchronous games) is the commuting-operator analogue of Theorem 3.3, proved by Lin [ 9 ] ; it is part of the transport discussed in Section 1.3 and not of this section. The Lean statement of this lemma and its GNS construction are a sub-project of their own.
[\(\bullet \bullet \bullet \) hard] [\(\uparrow \) QuantumLib]
[\(\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})\),
This is the main theorem of [ 31 ] (Theorem 7.1 there), whose Lean proof is vendored at MIPRE/Background/Repetition/CommutingRepetition/. The bridge identifies a game of Definition 2.1 with the game of the vendored development having the \(\{ 0, 1\} \)-valued payoff \(D\), a commuting-operator strategy of Definition 5.2 with a strategy of the vendored development (field by field, so that the two suprema defining the value range over the same set of numbers), and the two direct repetitions with each other. When \(\varepsilon = 0\) and \(\left\vert {\mathcal{A}} \right\vert = \left\vert {\mathcal{B}} \right\vert = 1\) the formalization reads the quotient as \(0\) and the bound is trivial.
[\(\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})\),
This is the main theorem of Chapter 6 of [ 30 ] , whose Lean proof is vendored at MIPRE/Background/Repetition/TenProofs/. Its entangled value is defined with a density matrix on the product of two finite sets and POVMs; Lemma 5.7 identifies it with \(\mathrm{val}^*\) (Definition 2.9), after which the two direct repetitions are literally the same construction. The Lean proof is complete modulo that lemma.
[\(\bullet \bullet \) medium] [\(\uparrow \) QuantumLib]
[\(\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})\).
A tensor-product strategy (Definition 2.3) is a strategy of the second kind, with \(S_\textsc{A}= \{ 1, \ldots , d_\textsc{A}\} \), \(S_\textsc{B}= \{ 1, \ldots , d_\textsc{B}\} \), \(\rho = |\psi \rangle \langle \psi |\) and projective measurements, which gives \(\mathrm{val}^*\leq \mathrm{val}^*_{\mathrm{POVM}}\). Conversely, given a strategy of the second kind, purify \(\rho \) on a reference system placed on Bob’s side (Bob’s POVM acts as the identity on it), then dilate the two POVMs to projective measurements on enlarged spaces (Naimark); neither step changes the outcome probabilities or the tensor-product structure, and reindexing the finite sets by initial segments of \(\mathbb {N}\) yields a tensor-product strategy with the same value.
Comments.
The lemma is the only piece of the entangled bridge that is stated but not yet proved in Lean; it is a general fact of independent interest. The vendored definition of the entangled value has the strategy’s two finite sets as arbitrary types in the lowest universe, and the bridge reindexes them.
[\(\bullet \bullet \bullet \) hard] [\(\uparrow \) QuantumLib]
[\(\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 \).
This is Theorem 3.2 of [ 9 ] , as formalized in [ 31 ] (the density programme of the vendored development, Tracial/Density/Main.lean). The statement above is that of the vendored development, in its own vocabulary — its tracially embeddable correlations have the shape of Lin’s Definition 3.1, with Bob’s measurement taken in the commutant of the left action; restating it through the definitions of Section 2 is pending.
Source.
Direct parallel repetition for entangled strategies is Chapter 6 of OpenAI’s Ten advances [ 30 ] , with the Lean proof in the accompanying repository; for commuting-operator strategies it is [ 31 ] , whose proof reduces to the tracially embeddable case by Theorem 5.8 and then rounds by adapting the argument of [ 30 ] . Earlier value-form theorems cover restricted classes of games or give polynomial rates; the anchored theorem of Section 5.3 is the one used in [ 1 ] . The rates \(\varepsilon ^{13}\) and \(\varepsilon ^{7}\) are those of the sources; any polynomial rate suffices for the pipeline.
Comments.
Both vendored developments are sorry-free and use only the standard axioms; the file MIPRE/Background/Repetition/Axioms.lean guards the axioms of the bridged commuting-operator theorem and of Theorem 5.8 (the entangled theorem joins it once Lemma 5.7 is proved). Vendoring is done by scripts/vendor-repetition.py, never by hand; the copies are read-only and the only local changes are recorded in each directory’s README.md. Nothing outside MIPRE/Background/Repetition/ refers to the vendored namespaces.
Theorems 5.6 and 5.5 are statements about values, while Theorem 5.22 is a statement about entanglement requirements: the anchored proof extracts from a good strategy for the repeated game a strategy for the original game of no larger dimension, whereas the proofs of the direct theorems round through auxiliary resources (an embezzling state in [ 30 ] , a tracial approximation in [ 31 ] ) and give no control of the dimension. Lin’s proof of \(\mathrm{MIP}^{\mathrm{co}}= \mathrm{coRE}\) [ 10 ] shows that the entanglement clauses of [ 1 ] are dispensable: with completeness and soundness of compression stated in value form (perfect strategies are preserved, value at most \(\frac12\) is preserved), the halting reduction follows from the enumeration of Lemma 3.13 and Kleene’s recursion theorem alone (Lemma 4.11), and gap amplification then needs only a value statement — exactly the theorems of this section, applied to the game as it is, without anchoring. The pipeline of Section 6 is stated in that form (Section 1.3): Theorem 6.5 rests on Theorem 5.6, and Theorem 5.22 with its toolkit (Sections 5.2–5.4) is not on the path to the main theorem; the entanglement clauses are recorded in Remark 6.8. In either form, the transport between bipartite and synchronous strategies (Section 1.3) is the pipeline’s responsibility.
5.2 Background results
The proof of Theorem 5.22 draws on a toolkit of quantum information theory (collected in [ 7 , Section 5.1 ] ) together with two classical probability lemmas of Holenstein. Everything in this subsection is standard and independent of nonlocal games; entries carry the same effort estimates as in Section 3.
Fidelity and Uhlmann’s theorem
[\(\bullet \bullet \) medium] [\(\uparrow \) QuantumLib]
[\(\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] 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
[\(\uparrow \) QuantumLib] For all density matrices \(\rho , \sigma \) on \(\mathbb {C}^d\),
Source.
Uhlmann [ 32 ] ; Fuchs and van de Graaf [ 33 ] . The finite-dimensional statements above are Theorem 9.2.1 and Section 9.3 of [ 35 ] .
Comments.
This is the tool that converts closeness of reduced states into local unitaries: combined with \(\left\| {|\psi \rangle - |\varphi \rangle } \right\| ^2 = 2(1 - \mathrm{Re}\langle \varphi |\psi \rangle )\), Uhlmann’s theorem turns a fidelity lower bound between reduced density matrices into a unitary on the complementary system carrying one purification close to the other. The proof of Lemma 5.24 applies it three times. The finite-dimensional proof is a page of linear algebra (Schmidt decomposition, polar decomposition, Cauchy–Schwarz) and, like everything in this subsection, should be stated for matrices, with no game-theoretic content.
The relative entropy toolkit
[\(\bullet \bullet \) medium] [\(\uparrow \) QuantumLib]
[\(\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 \).
[\(\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] For all density matrices \(\rho , \sigma \) on \(\mathbb {C}^d\),
[\(\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)\).
[\(\uparrow \) QuantumLib] For all tripartite density matrices \(\rho ^{ABC}\), \(I(A : B \, |\, C)_\rho \geq 0\).
Source.
Standard; the statements above are exactly the toolkit collected in [ 7 , Section 5.1 ] , with textbook treatment in [ 35 , Chapter 11 ] . Strong subadditivity is due to Lieb and Ruskai [ 34 ] .
Comments.
Core QuantumLib material, and a substantial part of it already exists there (including strong subadditivity and much of the relative entropy machinery), so the formalization task is largely one of interfacing: fixing a convention for classical-quantum states, conditioning on classical registers, and expectation notation. Strong subadditivity is the only deep theorem in the list; everything else is a page or two of matrix analysis.
Quantum Raz’s lemma
[\(\bullet \) easy] (given the toolkit) [\(\uparrow \) QuantumLib]
[\(\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
Source.
[ 7 , Lemma 5.10 ] ; it is the quantum analogue of the classical lemma at the heart of Raz’s and Holenstein’s proofs of parallel repetition [ 27 , 28 ] . The proof is a page, by induction from the chain rule (Lemma 5.16), item 4 of Lemma 5.14, and strong subadditivity (Lemma 5.17).
Comments.
The information-theoretic heart of the argument. In the application, \(\rho \) is the state of the players’ question tuple together with one player’s entanglement register, conditioned on winning the coordinates in a set \(C\); \(\sigma \) is the corresponding unconditioned (product) state; and the relative entropy between the two is at most \(\log \frac{1}{\Pr (W_C)}\) plus an answer-length term. The lemma then says that most coordinates \(i\) carry almost no information about the entanglement register. Reusable in any parallel-repetition or direct-product argument, hence a prime upstreaming candidate.
Conditioning independent random variables
[\(\bullet \) easy]
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\).
Source.
Holenstein [ 28 ] , Lemma 4.1 and Corollary 4.3; restated in the form used here in [ 7 , Section 4.3 ] .
Comments.
Purely classical probability (the proof is Kullback–Leibler divergence, classical Pinsker, and Jensen); the natural home is Mathlib rather than QuantumLib, which is why the entry carries no upstreaming badge. The argument also uses, silently, the basic calculus of total variation distance: marginalization is contractive, and appending a shared conditional kernel to both distributions preserves the distance.
Finally, the proof freely uses elementary facts about pure states that should be stated once and for all: every bipartite pure state can be brought to the symmetric Schmidt form \(\sum _j \sqrt{\lambda _j} |v_j\rangle |v_j\rangle \) by a local unitary; for unit vectors, \(\left\| {\psi - \varphi } \right\| _1 \leq 2 \left\| { |\psi \rangle - |\varphi \rangle } \right\| \); the trace distance is contractive under measurements; and the “transpose trick” relating operators applied to either half of a state in symmetric Schmidt form. These are one-line lemmas of Mathlib-style linear algebra.
5.3 The anchoring transformation and the theorem
[\(\bullet \) easy] [\(\uparrow \) QuantumLib]
[\(\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] 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.
With probability \(1 - (1 - \alpha )^2\) at least one question is \(\perp \) and the referee accepts regardless of the answers; conditioned on the complement, the question pair is distributed according to \(\mu \) and the predicate is that of \(\mathfrak {G}\). Extending a value-\(p\) strategy for \(\mathfrak {G}\) by a fixed answer on \(\perp \) therefore achieves \(1 - (1 - \alpha )^2 (1 - p)\) in \(\mathfrak {G}_\perp \), and restricting a strategy for \(\mathfrak {G}_\perp \) to the questions of \(\mathfrak {G}\) — same state, same measurements, so the same dimension — inverts the relation. Taking suprema over strategies yields the claim.
The theorem below is the form of the parallel repetition theorem invoked by the compression procedure of [ 1 ] . It is an entanglement statement, not merely a value statement: this is what soundness of the compression recursion requires when it is stated in terms of \(\mathrm{Ent}\) (Remark 6.8); the value-form pipeline of Section 6 uses Theorem 5.6 instead.
[\(\bullet \bullet \bullet \) hard] [\(\uparrow \) QuantumLib]
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
Source.
Bavarian, Vidick and Yuen [ 7 ] ; the entanglement-preserving form quoted here is the one used in [ 1 , Section 10 ] . The paper proves the theorem for a general anchoring parameter \(\alpha \), with an \(\alpha ^{48}\) dependence in the exponent that is absorbed into \(c\) at \(\alpha = \frac12\); passing from \(\mathrm{Ent}(\mathfrak {G}_\perp , 1 - \varepsilon ')\) to \(\mathrm{Ent}(\mathfrak {G}, 1 - \varepsilon )\) costs only the constant factor of Lemma 5.21, likewise absorbed. An alternate proof of the value form of the theorem was given by Jain and Kundu [ 29 ] and may be worth evaluating as a formalization route.
Comments.
Used for gap amplification: after answer reduction the completeness-soundness gap has shrunk to \(1\) vs. \(1 - 1/\mathrm{poly}\), and repetition of the anchored game restores the gap to \(1\) vs. \(\frac12\) while preserving entanglement lower bounds. The proof is information-theoretic and long; axiomatize first. Direct, value-form repetition is formalized (Section 5.1) and has replaced this theorem in the pipeline (Remark 5.9); this theorem is retained for the entanglement form of the argument (Remark 6.8). Two translation points for the formalization: the source works with bipartite tensor-product strategies while \(\mathrm{Ent}\) (Definition 2.12) is defined via synchronous strategies, so the statement must be transported, consistent with the convention of Section 1.3; and the anchored version of a synchronous game is not literally synchronous (it accepts unequal answers on the question pair \((\perp , \perp )\)), which is repaired by fixing a canonical accepted answer on \(\perp \). The exponent \(17\) and the constants are provisional, as per Section 1.4.
5.4 Decomposition of the proof
This subsection records the structure of the proof of Theorem 5.22 following [ 7 ] , at the level of its two main intermediate statements. It is not yet a formalization roadmap, but it identifies where each background result of Section 5.2 enters.
Shape of the argument.
Like all known proofs of parallel repetition, the proof is a rounding argument. Let \(\mathscr {S}\) be a dimension-\(d\) strategy for the repeated game \(\mathfrak {G}_\perp ^{n}\) with value at least \(p\). One shows: if \(p\) is above the threshold of the theorem, then there is a strategy for \(\mathfrak {G}_\perp \) of dimension at most \(d\) with value at least \(1 - \varepsilon \). By Lemma 5.21 this in turn yields a strategy for \(\mathfrak {G}\), still of dimension at most \(d\), with value \(1 - O(\varepsilon )\); the entanglement inequality of the theorem is the contrapositive. Everything hinges on the extracted strategy reusing the same entangled state (suitably measured) and the same measurements (suitably conjugated), so that the dimension does not grow.
A counting argument ( [ 7 , Proposition 6.5 ] ) reduces the problem to a conditional one: there exists a set \(C \subseteq [n]\) of size \(O\bigl(\frac{1}{\varepsilon } \log \frac{1}{\varepsilon \, p}\bigr)\) such that, conditioned on the event \(W_C\) of winning all coordinates in \(C\), a uniformly random other coordinate \(i\) is won with probability at least \(1 - \varepsilon /2\). The players would therefore like to play coordinate \(i\) of \(\mathfrak {G}_\perp ^n\) “conditioned on \(W_C\)”. The obstruction is that neither the conditioned question distribution nor the conditioned post-measurement state is locally sampleable. All error terms are controlled by the single quantity
whose answer-length term is where the parameter \(s\) of Theorem 5.22 enters.
The classical step: dependency-breaking variables.
Following Raz and Holenstein, one introduces for each coordinate \(i \notin C\) a dependency-breaking variable \(\Omega _i = (D_i, M_i)\): \(D_i\) points to one of the two players uniformly at random, and \(M_i\) is a noisy copy of that player’s question, where the noise rate \(\eta = \alpha /2\) is tuned to the anchoring probability so that the marginal of the question pair remains that of \(\mathfrak {G}_\perp \). Conditioned on \(\Omega _i\) the two players’ questions in coordinate \(i\) are independent. Write \(R_{-i}\) for the tuple collecting the \(\Omega _j\) for \(j \notin C \cup \{ i\} \) together with the questions and answers in the coordinates of \(C\): this is the shared classical data that the extracted strategy will (non-uniformly) fix.
[\(\bullet \bullet \) medium]
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)\).
Source.
[ 7 , Lemma 4.6 ] , items condensed; the proof is classical probability from Lemma 5.19.
Comments.
Item 1 says conditioning on \(W_C\) barely disturbs any single coordinate; item 2 says the shared data \(R_{-i}\) can be sampled without knowing the players’ actual questions \((x, y)\) — by pretending both are the anchor — which is the classical half of the correlated sampling problem. This is where anchoring first pays: switching a question to \(\perp \) costs only a factor \(\mathrm{poly}(1/\alpha )\) because every question profile has the anchor in its support.
The quantum step: dependency-breaking states.
The quantum analogue must also “condition the entangled state on \(W_C\)”. For a realization \(r_{-i} = (\omega _{-i}, a_C, b_C)\) of \(R_{-i}\) and questions \(x, y\) for coordinate \(i\), define the dependency-breaking state
where \(A_{\omega _{-i}, x}(a_C)\) denotes the POVM element of the strategy producing answers \(a_C\) in the coordinates of \(C\), averaged over all questions outside coordinate \(i\) consistent with \(\omega _{-i}\) and with \(X_i = x\) (and symmetrically for \(B\)). This is the post-measurement state of \(|\psi \rangle \) given that the answers on \(C\) were \((a_C, b_C)\), as seen when coordinate \(i\) carries \((x, y)\). The extracted strategy would like to hold \(|\tilde\Phi _{r_{-i}, x, y}\rangle \), but the state depends on both questions; the key technical statement is that the players can reach it from the question-independent state \(|\tilde\Phi _{r_{-i}, \perp , \perp }\rangle \) by local unitaries.
[\(\bullet \bullet \bullet \) hard]
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 \).
Source.
[ 7 , Proposition 5.1 ] , proved in Sections 5.2–5.4 there.
Comments.
This is the technical core of the paper, and the second place anchoring pays: the state is moved one question at a time, using the anchor as a “home base” connected to every question (\(\tilde\Phi _{\perp ,\perp } \to \tilde\Phi _{x,\perp } \to \tilde\Phi _{x,y}\)). Each switch is an application of Uhlmann’s theorem (Theorem 5.11, via Lemma 5.12): the required closeness of reduced density matrices comes from quantum Raz’s lemma (Lemma 5.18) applied to the state of questions and one player’s register conditioned on \(W_C\), converted to trace distance by Pinsker’s inequality (Lemma 5.15). A separate argument compares the normalization factors of the unnormalized states (\(\gamma \)-comparison, [ 7 , Lemma 5.17 ] ). The exponent \(\frac{1}{16}\) is an artifact of chaining these approximations and is provisional.
Assembly.
Given Lemmas 5.23 and 5.24, the extracted strategy for \(\mathfrak {G}_\perp \) is: fix (by averaging) a good coordinate \(i\) and realization \(r_{-i}\); share the state \(|\tilde\Phi _{r_{-i}, \perp , \perp }\rangle \); on questions \((x, y)\), apply \(U_{r_{-i}, x}\) and \(V_{r_{-i}, y}\); then measure with the original measurements for coordinate \(i\), conditioned on the fixed answers \((a_C, b_C)\) (a renormalized, “pretty good” version of the strategy’s POVMs). The main lemma of [ 7 , Section 6 ] shows the resulting question–answer distribution is \(O(\delta ^{1/16}/\alpha ^3)\)-close in total variation to \(P_{X_i Y_i A_i B_i | W_C}\), whose winning probability is at least \(1 - \varepsilon /2\) by the counting argument; the parameters of Theorem 5.22 are set so that the total loss is at most \(\varepsilon \). The state and measurements act on the original \(d\)-dimensional spaces, so the extracted strategy has dimension at most \(d\), giving the entanglement form of the theorem.