2 Foundations
This chapter fixes the objects that everything else refers to: games, strategies and values (in the synchronous framework, see Section 1.3), the computability conventions, and normal form verifiers. Definitions here are meant to be final; they are the first formalization targets of the project.
Statements marked [\(\uparrow \) QuantumLib] are general-purpose quantum information content: they are intended to be developed in, or contributed to, the QuantumLib (Lean-QuantumInfo) library rather than to remain specific to this project. The badge marks the general-purpose layer — games, strategies, values, and the rigidity theorems of Section 3 — as opposed to project-specific machinery such as normal form verifiers and the game transformations.
2.1 Games, strategies, and values
Games
[\(\uparrow \) QuantumLib] A two-player one-round game \(\mathfrak {G}\) is a tuple \((\mathcal{X}, \mathcal{Y}, \mathcal{A}, \mathcal{B}, \mu , D)\) where \(\mathcal{X}, \mathcal{Y}\) are finite question alphabets, \(\mathcal{A}, \mathcal{B}\) are finite answer alphabets, \(\mu \) is a probability distribution on \(\mathcal{X}\times \mathcal{Y}\), and \(D : \mathcal{X}\times \mathcal{Y}\times \mathcal{A}\times \mathcal{B}\to \{ 0,1\} \) is the decision predicate (\(1\) = accept).
[\(\uparrow \) QuantumLib] A game is synchronous if \(\mathcal{X}= \mathcal{Y}\), \(\mathcal{A}= \mathcal{B}\), and unequal answers to equal questions are rejected: \(D(x,x,a,b) = 0\) whenever \(a \neq b\). We write a synchronous game as \(\mathfrak {G}= (\mathcal{X}, \mathcal{A}, \mu , D)\).
Strategies
[\(\uparrow \) QuantumLib] A tensor-product strategy for \(\mathfrak {G}\) consists of finite-dimensional Hilbert spaces \(\mathcal{H}_\textsc{A}\), \(\mathcal{H}_\textsc{B}\), a unit vector \(|\psi \rangle \in \mathcal{H}_\textsc{A}\otimes \mathcal{H}_\textsc{B}\), and projective measurements (PVMs) \(\{ A^x_a\} \) on \(\mathcal{H}_\textsc{A}\) and \(\{ B^y_b\} \) on \(\mathcal{H}_\textsc{B}\), one for each \(x\) (resp. \(y\)): each \(A^x_a\) is an orthogonal projection and \(\sum _a A^x_a = I\).
Outcome probabilities are computed using the Born rule: the players answer \((a,b)\) to questions \((x,y)\) with probability \(\langle \psi | A^x_a \otimes B^y_b |\psi \rangle \). Restricting to projective measurements follows [ 1 ] ; by Naimark dilation, allowing general POVMs would define the same quantum value.
[\(\uparrow \) QuantumLib] A synchronous strategy for a synchronous game \(\mathfrak {G}= (\mathcal{X}, \mathcal{A}, \mu , D)\) is a dimension \(d \geq 1\) together with a family of projective measurements (PVMs) \(\{ M^x_a\} _{a \in \mathcal{A}}\) on \(\mathbb {C}^d\), one for each \(x \in \mathcal{X}\): each \(M^x_a\) is an orthogonal projection and \(\sum _a M^x_a = I\).
Outcome probabilities are computed with the tracial state \(\tau (M) = \operatorname{tr}(M)/d\): the players answer \((a,b)\) to questions \((x,y)\) with probability \(\tau (M^x_a M^y_b)\).
[\(\uparrow \) QuantumLib] A commuting strategy for a synchronous game \(\mathfrak {G}= (\mathcal{X}, \mathcal{A}, \mu , D)\) is a unital \(C^*\)-algebra \(\mathscr {A}\) with a tracial state \(\tau \) (a positive linear functional with \(\tau (1) = 1\) and \(\tau (ab) = \tau (ba)\) for all \(a, b \in \mathscr {A}\)), together with a family of projective measurements \(\{ M^x_a\} _{a \in \mathcal{A}}\) in \(\mathscr {A}\), one for each \(x \in \mathcal{X}\): each \(M^x_a\) is a self-adjoint idempotent and \(\sum _a M^x_a = 1\).
Outcome probabilities are computed with \(\tau \): the players answer \((a,b)\) to questions \((x,y)\) with probability \(\tau (M^x_a M^y_b)\), a nonnegative real number since \(\tau (M^x_a M^y_b) = \tau (M^x_a M^y_b M^x_a)\).
A synchronous strategy (Definition 2.4) is exactly the finite-dimensional case \(\mathscr {A}= \mathbb {C}^{d \times d}\), \(\tau = \operatorname{tr}/d\). Via the GNS representation, commuting strategies capture exactly the synchronous commuting-operator correlations of the usual two-prover picture, with Bob’s measurements acting in the commutant on \(L^2(\mathscr {A}, \tau )\) — [ 21 , Theorem 5.5 ] ; see also [ 12 ] and [ 13 , Section 3.4 ] .
[\(\uparrow \) QuantumLib] A synchronous strategy \(\mathscr {S}= (d, M)\) for a synchronous game \(\mathfrak {G}= (\mathcal{X}, \mathcal{A}, \mu , D)\) is PCC (projective, consistent, and commuting, following [ 1 , Section 5.2 ] ) if the measurements associated with any pair of questions asked with positive probability commute: for all \((x, y)\) in the support of \(\mu \),
The paper’s PCC condition applies to a tensor-product strategy on equal local spaces. Besides projectivity and \([A^x_a,B^y_b]=0\) on the support of the question distribution, it requires each measurement separately to be consistent with itself on the state:
These are the conditions of def:consistent-measurement, def:consistent-strategy and def:spcc in the companion games.tex [ 34 ] ; see also [ 1 , Section 5.2 ] . The checked realization in Lemma 2.14 uses \(A=M\) and \(B=M^{\mathsf T}\). It preserves probabilities and gives cross-player consistency, but does not establish the displayed same-measurement identities for arbitrary complex \(M\), nor does commutation of two matrices imply commutation of one with the transpose of the other.
Consequently Definition 2.7 is the current synchronous PCC interface, and using it as an input to the paper’s completeness theorems requires a separate PCC representation bridge. The forward bridge must preserve all probabilities and support commutation while producing a source PCC strategy. A candidate is to realify each complex projector on dimension \(2d\), then use the same real symmetric projectors on both halves of a maximally entangled state. Projectivity, the normalized trace probabilities, the two consistency identities and the symmetry required for SPCC all need verification for that construction; no such bridge is proved here. Any transfer back from source PCC strategies to this synchronous interface also needs its own stated hypotheses and proof. The name PCC in the Lean definition does not discharge either direction. In both interfaces, commutation is required only on question pairs in the support of \(\mu \) and is distinct from the commuting-operator model of Definition 2.5.
Values
[\(\uparrow \) QuantumLib] The value of a tensor-product strategy \(\mathscr {S}= (\mathcal{H}_\textsc{A},\mathcal{H}_\textsc{B},\psi ,A,B)\) in \(\mathfrak {G}\) is
and the quantum value \(\mathrm{val}^*(\mathfrak {G})\) is the supremum of \(\mathrm{val}^*(\mathfrak {G}, \mathscr {S})\) over all tensor-product strategies.
[\(\uparrow \) QuantumLib] The value of a synchronous strategy \(\mathscr {S}= (d, M)\) in \(\mathfrak {G}\) is
and the synchronous value of \(\mathfrak {G}\) is \(\mathrm{val}^{s}(\mathfrak {G}) = \sup _\mathscr {S}\mathrm{val}^{s}(\mathfrak {G}, \mathscr {S})\).
[\(\uparrow \) QuantumLib] The value of a commuting strategy \(\mathscr {S}= (\mathscr {A}, \tau , M)\) in \(\mathfrak {G}\) is
and the commuting value of \(\mathfrak {G}\) is \(\mathrm{val}^{\mathrm{co}}(\mathfrak {G}) = \sup _\mathscr {S}\mathrm{val}^{\mathrm{co}}(\mathfrak {G}, \mathscr {S})\).
Let \(\mathfrak {G}\) be a synchronous game, \(\tau \) a tracial state and \(M\) a family of projective measurements with \(\mathrm{val}^{\mathrm{co}}(\mathfrak {G}, M) = 1\). Then \(\tau (M^x_a M^y_b) = 0\) whenever \(\mu (x,y) {\gt} 0\) and \(D(x,y,a,b) = 0\). In particular a value-\(1\) synchronous strategy has \(\mathrm{Tr}(M^x_a M^y_b) = 0\) at every rejected answer pair of every question pair the verifier asks.
At a fixed question pair the outcome probabilities sum to one, \(\sum _{a,b} \tau (M^x_a M^y_b) = \tau (1) = 1\), and each is nonnegative; this is why the value is at most one. The value is the same sum with the rejected terms deleted, so equality with \(1\) forces each deleted term to vanish, and \(\mu (x,y) {\gt} 0\) cancels.
Comments.
Every completeness argument in the pipeline needs this step — a strategy of value \(1\) does not merely win on average, it assigns probability zero to each rejected answer at each question actually asked — and it was used implicitly inside the proof that the value is at most one, without being available as a lemma. It is stated at the generic tracial level, so it serves synchronous and commuting strategies alike.
Two formalization notes. The instance set of the ambient algebra must be exactly the \([\mathrm{Ring}]\, [\mathrm{StarRing}]\, [\mathrm{Module}\ \mathbb {C}]\) of Definition 2.5: demanding a normed algebra instead sends the elaborator looking for a normed-algebra instance on matrices at every application, which is a whnf timeout. And the application to a synchronous strategy goes through the named value_eq_tracialValue rather than letting the unifier see through SyncStrategy.value, for the same reason.
[\(\uparrow \) QuantumLib] For a game \(\mathfrak {G}\) and \(\nu \in [0,1]\), \(\mathrm{Ent}(\mathfrak {G}, \nu )\) is the least \(d\) such that there exists a synchronous strategy (Definition 2.4) with dimension at most \(d\) achieving value at least \(\nu \) in \(\mathfrak {G}\), and \(\infty \) if no synchronous strategy achieves \(\nu \).
Relationship lemmas
[\(\uparrow \) QuantumLib] For every synchronous game \(\mathfrak {G}\), \(\mathrm{val}^{s}(\mathfrak {G}) \leq \mathrm{val}^*(\mathfrak {G})\).
Given a synchronous strategy \(\{ M^x_a\} \) on \(\mathbb {C}^d\), take the tensor-product strategy with \(\mathcal{H}_\textsc{A}= \mathcal{H}_\textsc{B}= \mathbb {C}^d\), \(A^x_a = M^x_a\), \(B^y_b = (M^y_b)^{\mathsf{T}}\), and \(|\psi \rangle = d^{-1/2}\sum _i |i\rangle |i\rangle \) (in Lean, MIPRE.SyncStrategy.toTensorProductStrategy). On that state \(\langle \psi | M \otimes N |\psi \rangle = \operatorname{tr}(M N^{\mathsf{T}})/d\) (MIPRE.dotProduct_kronecker_maxEntangled), so with \(N = (M^y_b)^{\mathsf{T}}\) the Born-rule probability is \(\tau (M^x_a M^y_b)\) and the values agree (MIPRE.SyncStrategy.value_toTensorProductStrategy). Taking the supremum uses that the quantum value is a supremum over a possibly empty type with bounded range: MIPRE.TensorProductStrategy.value_le_one and MIPRE.quantumValue_nonneg, both proved from the Born rule.
The converse direction — every good tensor-product strategy for a synchronous game whose questions carry proportional weight on the diagonal can be rounded to a good synchronous strategy — is the almost-synchronicity theorem, imported as Theorem 3.3. The hypothesis on the diagonal cannot be dropped: without it the two values are unrelated (Remark 3.4).
[\(\uparrow \) QuantumLib] For every synchronous game \(\mathfrak {G}\), \(\mathrm{val}^{s}(\mathfrak {G}) \leq \mathrm{val}^{\mathrm{co}}(\mathfrak {G})\).
A synchronous strategy \((d, M)\) is a commuting strategy with \(\mathscr {A}= \mathbb {C}^{d \times d}\) and \(\tau = \operatorname{tr}/d\), with the same value (in Lean, MIPRE.SyncStrategy.toCommutingStrategy; the value is preserved by definitional equality).
2.2 Linear constraint system games
A well-studied class of nonlocal games arises from systems of linear equations over \(\mathbb {F}_2\): the referee asks Alice for a satisfying assignment to a randomly chosen equation and Bob for the value of a randomly chosen variable in it, and checks consistency. The Mermin–Peres magic square is the canonical example. The formalization of this subsection was contributed by Sean Perazzolo (MIPRE.LCS); beyond the definitions below it includes observable- and projector-based strategy formalisms and their equivalence, a sum-of-squares decomposition of the loss operators, the extraction of operator identities from perfect play on the EPR state, matrix representations of solution groups, and the magic square as a worked example (MIPRE.LCS.MagicSquare.merminPeresStrategy).
A binary linear constraint system consists of \(r\) equations over \(s\) \(\mathbb {F}_2\)-valued variables, specified by the set \(V_i \subseteq \{ 1, \dots , s\} \) of variables occurring in each equation \(i\) together with a right-hand side \(b \in \mathbb {F}_2^r\); equation \(i\) reads \(\sum _{j \in V_i} x_j = b_i\).
The nonlocal game of an LCS instance. Both players receive questions from the same alphabet — an equation or a variable — and answer in the same alphabet — an assignment to all the variables, or a single bit. The referee samples an equation \(i\) uniformly at random, a uniformly random variable \(j \in V_i\), and a uniform orientation: one player is asked \(i\) and the other \(j\). The player asked the equation answers an assignment \(a\) (only its restriction to \(V_i\) is read), the player asked the variable answers a bit \(c\), and they win if \(\sum _{k \in V_i} a_k = b_i\) and \(a_j = c\). An answer whose shape does not match its question loses, as does an off-support pair \(j \notin V_i\).
Comments.
The orientation is what makes the game symmetric in the players, and it is not cosmetic. A one-directional version — the equation always to Alice, the variable always to Bob — cannot express a statement about both players’ variable observables, which is exactly what the Pauli basis test consumes from the Magic Square (Lemma 3.10): Alice would never receive a variable question, so \(A^{\textsc{Variable}_j}\) would not exist. It also fixes that lemma’s constant, the conditional failures being summed over \(2 \sum _i \left\vert {V_i} \right\vert \) oriented incidences rather than \(\sum _i \left\vert {V_i} \right\vert \) unoriented ones.
The shape and support checks in the decider are the discipline Definition 3.13 learned the hard way: a missing format check made the seeded CL game vacuous and a soundness theorem about it false. The formalization pins each outcome with explicit answers — an accepted pair in each orientation, and one rejected for disagreement, one for parity, one for shape, one for being off support.
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).
An observable in a star-algebra is a self-adjoint element squaring to \(1\). Binary projective measurements and observables are two views of the same data: \(\{ P_0, P_1\} \) gives the observable \(P_0 - P_1\), and an observable \(O\) gives the measurement \(\{ \tfrac 12(1 + O), \tfrac 12(1 - O)\} \).
For an observable \(O\) the family \(a \mapsto \tfrac 12(1 + (-1)^a O)\) is a projective measurement indexed by \(\mathbb {F}_2\), and the correspondence preserves commutation: if \(O_1\) and \(O_2\) commute then so do all of their projectors.
Self-adjointness, idempotence, orthogonality and summation to \(1\) are each a two-line computation from \(O^* = O\) and \(O^2 = 1\); commutation is inherited term by term.
A strategy given by commuting observables, one per variable of an LCS instance, yields a strategy given by genuine projective measurements: for a question consisting of several variables the joint measurement is the product of the corresponding binary projectors, which is projective because the observables commute, and the two players’ measurements commute with each other.
The joint family over an equation’s support is a product of commuting binary projectors, so it is a projective measurement and sums to \(1\) over the outcomes; commutation across players is inherited from commutation of the underlying observables.
The Magic Square is the LCS instance over \(\mathbb {F}_2\) with nine variables in a \(3 \times 3\) grid and six equations, one per row and column, the rows summing to \(0\) and the columns to \(1\). It has no classical solution, since the six equations sum to \(0 = 1\).
There are nine observables on \((\mathbb {C}^2)^{\otimes 2}\), one per cell of the Magic Square, such that the three in each row or column commute and multiply to \(+1\) for a row and \(-1\) for a column. They give a strategy for the Magic Square game of value \(1\) on two EPR pairs.
The grid is the Mermin–Peres square of tensor products of Pauli matrices. That each entry is an observable, and that entries sharing an equation commute, are finite computations on \(4 \times 4\) matrices.
If a bipartite observable strategy for an LCS instance is perfect — its local loss operators annihilate the EPR vector — then the associated LCS game has a tensor-product strategy of value \(1\).
Take both players’ spaces to be \(\mathbb {C}^n\) with the normalized EPR state. The game is symmetric, so each player needs measurements at both kinds of question, and both use the same ones: at an equation, the joint projective measurement of its observables, answered as an assignment extended by zero; at a variable, the binary measurement of its observable. At an equation–variable incidence the accepted Born-rule weight is the EPR expectation of the local winning operator, which is \(1\) because the local loss operator annihilates the EPR vector. The other orientation has the same weight, since \(\langle \Omega , (A \otimes B) \Omega \rangle = \sum _{a,k} A_{ak} B_{ak}\) is symmetric in \(A\) and \(B\) and the decider is symmetric in the players. No transposes are needed.
2.3 Distance measures
[\(\uparrow \) QuantumLib] For matrices \(A, B \in \mathbb {C}^{d \times d}\), let \(\langle A, B \rangle _{hs} = \tau (A^\dagger B)\) and \(\left\| {A} \right\| _{hs}^2 = \tau (A^\dagger A)\), where \(\tau = \operatorname{tr}/d\) is the dimension-normalized trace.
[\(\uparrow \) QuantumLib] Let \(\mu \) be a distribution on a finite set \(\mathcal{X}\), and \(\{ M^x_a\} \), \(\{ N^x_a\} \) families of POVMs. We say \(M\) and \(N\) are \(\delta \)-close, written \(M^x_a \approx _\delta N^x_a\), if \(\mathop{\mathbb {E}}_{x \sim \mu } \sum _a \left\| {M^x_a - N^x_a} \right\| _{hs}^2 \leq \delta \). Since each difference \(M^x_a - N^x_a\) is Hermitian, the summand equals \(\tau ((M^x_a - N^x_a)^2)\).
Let \(\mu \) be a distribution on a finite set \(\mathcal{X}\), let \(|\psi \rangle \in \mathbb {C}^{d_\textsc{A}} \otimes \mathbb {C}^{d_\textsc{B}}\), and let \(\{ A^x\} \), \(\{ B^x\} \) be families of operators on \(\mathbb {C}^{d_\textsc{A}}\). We say \(A\) and \(B\) are \(\delta \)-close on \(|\psi \rangle \), written \(A^x \approx _\delta B^x\) when \(\mu \) and \(|\psi \rangle \) are clear from context, if
equivalently if \(\mathop{\mathbb {E}}_{x\sim \mu } \left\| {((A^x - B^x) \otimes I_\textsc{B})|\psi \rangle } \right\| ^2 \leq \delta \). For families indexed by answers as well, \(\{ A^x_a\} \) and \(\{ B^x_a\} \), the outcome sum sits inside the question average.
Comments.
This is not Definition 2.26, and the difference is not presentational. Definition 2.26 is the normalized Hilbert–Schmidt distance, which is the distance of a synchronous strategy — there the state is the normalized trace itself, which is why MIPRE/Foundations/Closeness.lean is the calculus of that one. The appendix of the Pauli basis test (Section 3.6) works throughout with the state-dependent distance above, on a bipartite state that is fixed by context, and every \(\approx _\delta \) in that section is this one.
Two departures from the paper’s own definition ( [ 34 ] , qld-prelim.tex), both in the direction of a stronger statement. The paper writes \(\leq O(\delta )\) inside the relation; here the relation is an inequality against \(\delta \) and the constants appear in the lemmas that produce them, so Lemma 3.43 preserves \(\delta \) exactly and Lemma 3.44 gives exactly \(\left\vert {\mathcal{A}} \right\vert \delta \). And the paper defines \(\approx _\delta \) only for question-indexed operators, using the answer-indexed form without comment; both are defined here.
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\} \) and \(\{ N^x_a\} \) be families of POVMs with a common question set \(\mathcal{X}\) and a common answer set, the first on \(\mathbb {C}^{d_\textsc{A}}\) and the second on \(\mathbb {C}^{d_\textsc{B}}\). We say they are \(\delta \)-close across the two parties, written \(M^x_a \otimes I\simeq _\delta I\otimes N^x_a\), if
Then, for any two POVMs \(M\) and \(N\) with a common answer set and \(|\psi \rangle \) a unit vector,
twice the probability that the two measurements disagree.
Comments.
This is the \(\simeq _\delta \) of the Pauli appendix, and it is not Definition 2.27: that one compares two families of operators on the same factor, which is what the orthonormalization step of Corollary 3.45 needs, whereas every consistency statement of Lemma 3.46 compares one player’s operator with the other player’s. The paper uses both symbols and says the two are interchangeable up to Fact fact:agreement; the formalization keeps them apart, because the conversion is the factor \(2\) of 1 and it is better spent once than assumed throughout.
Inequality 1 is the whole analytic content of the file (MIPRE/Foundations/CrossConsistency.lean): expand each square, and the two diagonal sums are at most one because a POVM element satisfies \(A^\dagger A = A^2 \leq A\) (POVM.mul_self_le_self) and the elements sum to the identity. No projectivity is used, so the inequality holds for arbitrary POVM strategies. On the paper’s route projectivity arrives only later, through Corollary 3.45; the formalized route assumes it from the start, Theorem 3.38 being stated for projective strategies.
Two things the formalization needs that the paper leaves implicit. First, what a subtest buys is not that its decider equals an agreement predicate but that accepting implies agreeing: a real decider checks the answer formats first and rejects an ill-formatted pair even when the post-processings agree. So the readings that coarse-grain the answers may send an ill-formatted answer anywhere — \(0\), here — and the implication is all one_sub_sum_bornProb_le_condFail asks. Second, “divided by the probability that the subtest is selected” needs no injectivity: the subtests of the Pauli basis test are indexed by the verifier’s content and several contents give the same question pair, a \((\textsc{Pauli}, W)\) question reading none of it, so the hypothesis is a condition on the push-forward (sum_condFail_le_of_pushforward).
xStateDist_obsOf_le is Lemma 3.44 across the two parties, with the same proof and the same factor \(\left\vert {\mathcal{A}} \right\vert \): the appendix needs it to pass from a two-outcome coarse-graining of a point measurement to the \(\pm 1\)-observable it defines, and Definition 2.27’s version compares the wrong pair.
The order reversal, and where the sign comes from. One algebraic rule is proved here rather than inlined at its two uses, because the paper’s own correction note on Lemma 3.48 records two displays that had it backwards. If \(A \otimes I\simeq I\otimes A'\) and \(B \otimes I\simeq I\otimes B'\) then
Bob’s factors in the reverse order, at the sum of the two deviations (xNorm_mul_le_one; xNorm_mul_le carries operator-norm bounds \(K\) and \(L\) in front of them). The proof is the split \(AB \otimes I- I\otimes B'A' = (A \otimes I)(B \otimes I- I\otimes B') + (I\otimes B')(A \otimes I- I\otimes A')\), and the reversal is exactly the step that commutes \(A \otimes I\) past \(I\otimes B'\) to factor the second summand: it puts \(B'\) to the left of \(A'\). Applying it in both orders and cancelling Bob’s two products gives the form the anticommuting case of Lemma 3.48 consumes,
norm_stateVec_anticomm_le: an anticommutation on Bob’s side transfers to Alice’s. The two reversals do not cancel each other, because what sits between them is a sum. Both statements are on the unsquared deviation, since the triangle inequality is what the argument uses; xSqNorm_mul_le_one squares the first at the usual cost of a factor two.
Each operator in sight has to be a contraction, and for the \(\pm 1\)-observable of a two-outcome POVM that is POVM.sub_mul_self_le_one, which needs the observable written as a difference of two POVM elements rather than as the weighted sum \(\sum _a (-1)^a M_a\) that obsOf produces. obs2 is that difference and obsOf_sgn_eq_obs2 identifies the two, so a consumer can quote whichever form its input is stated in.
The swap, and the commutator form. Two more entries serve the appendix’s commutation step. norm_stateVec_comm_le is 3 with a commutator in the middle instead of an anticommutator — the same split, Bob’s two products cancelling either way. And snorm_swapVec_aOp_sub_bOp exchanges the two sides of a cross-party deviation, which is what lets a lemma proved for Alice’s factor be applied to Bob’s: the clean statement is at the level of vectors, \((X \otimes Y)\, \mathrm{swap}|\psi \rangle = \mathrm{swap}\, (Y \otimes X)|\psi \rangle \), and everything else follows by linearity. On the paper’s route Corollary 3.45 produces a projective measurement on Alice’s factor only, so the commutation analysis below is run on Bob’s observables and carried back; that swap is the bridge. The formalized route assumes the first player’s measurements projective from the outset and uses the swap in the same way.
2.4 The expanded state
Let \(|\psi \rangle \) be a state on \(\mathbb {C}^{d_\textsc{A}} \otimes \mathbb {C}^{d_\textsc{B}}\) and \(|e\rangle \) one on \(\mathbb {C}^{a} \otimes \mathbb {C}^{a'}\). The expanded state is \(|\psi \rangle \otimes |e\rangle \), re-bipartitioned so that the first party holds \(\mathbb {C}^{d_\textsc{A}} \otimes \mathbb {C}^{a}\) and the second \(\mathbb {C}^{d_\textsc{B}} \otimes \mathbb {C}^{a'}\): one half of the ancilla goes to each. Then
an operator of product form acts factor by factor, \(\bigl((M \otimes N) \otimes I\bigr)(|\psi \rangle \otimes |e\rangle ) = \bigl((M \otimes I)|\psi \rangle \bigr) \otimes \bigl((N \otimes I)|e\rangle \bigr)\);
the norm of a product state is the product of the norms, so the expanded state is a unit vector when both factors are;
consequently an operator with an inert ancilla has the same state-norm on the expanded state as on the original one: \(\left\| {(M \otimes I_a) \otimes I\, |\hat\psi \rangle } \right\| = \left\| {(M \otimes I_\textsc{B})|\psi \rangle } \right\| \) when \(|e\rangle \) is a unit vector;
and a unitary on the ancilla is invisible: \(\left\| {(M \otimes U) \otimes I|\hat\psi \rangle } \right\| = \left\| {(M \otimes I_a) \otimes I|\hat\psi \rangle } \right\| \).
Comments.
Formalized in MIPRE/Foundations/Expanded.lean. This is the bookkeeping of the appendix’s sec:expanding, isolated from the Pauli test: items 3 and 4 are what let a bound proved before the expansion be used after it, and they are why the expansion stage costs exactly the constant of Lemma 3.48 and nothing more. The re-bipartition is the point — the ancilla halves are split between the parties, which is what makes the ancilla observables tied together — and it is why the statements are about \(|\psi \rangle \otimes |e\rangle \) rather than about a tensor power.
Born probabilities factorize, and that is where data processing lives. The consistency half of the expansion stage is about a measurement of product form, and what it needs is that its Born probabilities split: \(\langle \hat\psi | (M \otimes N) \otimes (M' \otimes N') |\hat\psi \rangle = \langle \psi | M \otimes M' |\psi \rangle \cdot \langle e| N \otimes N' |e\rangle \) (bornProb_expVec_kron; only the ancilla’s two operators need be positive, which is what makes their quadratic form real so the real part of the product splits). POVM.kron is the product measurement, and sum_bornProb_le_map is the data-processing inequality that holds: coarse-graining both players the same way can only increase the probability that they agree.
That last one is stated at the Born level deliberately. The state-dependent distance has no data-processing inequality — NW19 states theirs for \(\simeq _\delta \) and the remark following it gives a counterexample for \(\approx _\delta \) — so every coarse-graining in the appendix is taken on Born probabilities and converted once, at the end, by 1. A formalization that reached for the \(\approx \) form would be proving something false.
2.5 Naimark dilation against a fixed state
Let \(\{ E^x_a\} \) be a family of POVMs on \(\mathbb {C}^d\), indexed by questions \(x\) and outcomes \(a \in \mathcal{A}\). Then there is a family of projective measurements \(\{ P^x_a\} \) on \(\mathbb {C}^d \otimes \mathbb {C}^{\mathcal{A}}\) and a single, question-independent isometry \(V : \mathbb {C}^d \to \mathbb {C}^d \otimes \mathbb {C}^{\mathcal{A}}\), \(|v\rangle \mapsto |v\rangle \otimes |a_0\rangle \), such that \(V^\dagger P^x_a V = E^x_a\) for every \(x\) and \(a\).
The columns of the matrix \(V^x\) whose \((q, j)\) entry is \(\sqrt{E^x}\)-like — concretely, the square root of \(E^x_a\) read off in the \(a\)-th block — form an isometry \(\mathbb {C}^d \to \mathbb {C}^d \otimes \mathbb {C}^{\mathcal{A}}\) compressing the block-diagonal projectors \(\Pi _a = I\otimes |a\rangle \langle a|\) back to \(E^x_a\). Extending each \(V^x\) to a unitary \(U^x\) of the larger space that agrees with it on the \(a_0\)-slice — the completion of an orthonormal family to an orthonormal basis — makes \(P^x_a = (U^x)^\dagger \Pi _a U^x\) projective with the compression along the fixed isometry \(|v\rangle \mapsto |v\rangle \otimes |a_0\rangle \). The question-independence of that isometry is the whole point: the expectations are taken against a shared state, which must not depend on the question.
Comments.
Formalized in MIPRE/Foundations/Dilation.lean, extracted from the repetition development where it was written for lem:povm-value-eq. Its other consumers are Lemma 3.10, which dilates the Magic Square’s six constraint POVMs against one shared ancilla, and Theorem 3.55.
2.6 The commutation analysis
Let \(\{ A_b\} \) and \(\{ C_c\} \) be POVMs on \(\mathbb {C}^{d_\textsc{A}}\) and let \(\{ B_{b,c}\} \) be a projective measurement on \(\mathbb {C}^{d_\textsc{B}}\) with outcomes the pairs, with marginals \(B_b = \sum _c B_{b,c}\) and \(B_c = \sum _b B_{b,c}\). If
then Alice’s two POVMs approximately commute on the state:
Both products reach the same operator on Bob’s factor, \(I\otimes B_{b,c}\). For \(A_b C_c \otimes I\): put \(A_b \otimes I\) in front of \(C\)’s relation, and put \(I\otimes B_c\) in front of \(A\)’s; the two meet at \(A_b \otimes B_c\), and the second step lands on \(I\otimes B_c B_b = I\otimes B_{b,c}\) — which is where projectivity is used, and the only place (IsPVM.marg_mul_marg). For \(C_c A_b \otimes I\), the same two steps in the other order, using \(B_b B_c = B_{b,c}\). Each side is therefore within \(4\delta \) after one triangle inequality, and 4 is one more.
Putting an operator in front costs nothing and adds its index to the sum, which is the paper’s fact:add-a-proj: if \(\sum _i F_i^\dagger F_i \leq I\) then \(\sum _i \left\| {F_i v} \right\| ^2 \leq \left\| {v} \right\| ^2\). For a POVM that hypothesis is \(A_b^2 \leq A_b\) with \(\sum _b A_b = I\), so it needs no projectivity of Alice’s measurements (sum_aOp_conjTranspose_mul_self_le_one).
Comments.
Formalized in MIPRE/Foundations/Commutation.lean. This is the paper’s lem:commutation-analysis (games.tex), and it is the only step of the Pauli appendix that genuinely uses projectivity of a measurement.
Proved for abstract families in one algebra. The two parties enter only through four hypotheses — the two factors commute, and Bob’s two marginals multiply to the joint element in either order — so commutation_analysis_abstract is stated for families in a single matrix algebra and the bipartite version is its instance. That is not tidiness: stating it with \(\otimes \) in the hypotheses made the unifier’s work quadratic in the number of rewrites and the proof timed out; in one algebra it elaborates in seconds.
No square root, and the constant is exact. Every step is a triangle inequality or an operator-norm bound, so \(16\delta \) is what the argument gives. The last step of the appendix’s commuting case is also exact: expanding a two-outcome observable as \(I- 2 M_1\), the commutator of two of them is four times the commutator of the two \(M_1\)’s (obs2_commutator_eq), because the identity commutes with everything — a factor \(16\) in the squared norm and no approximation.
2.7 Attaching a projection, and the pasting lemma
Let \(\{ A_i\} _{i \in \mathcal{A}}\) be a projective measurement and \(\{ B_i\} \) any family of operators on the same space, with \(\sum _i \left\| {(A_i - B_i)|\psi \rangle } \right\| ^2 \leq \delta \). Then for any map \(f : \mathcal{A}\to \mathcal{B}\),
simultaneously over all the fibres of \(f\) — multiplying each element by \(A\)’s own element costs nothing, and neither does summing along a fibre.
Consequently, if \(\{ Q_{a,b}\} \) is a projective measurement on \(\mathbb {C}^{d_\textsc{A}}\) with outcomes pairs, \(\{ Z_b\} \) is a projective measurement on \(\mathbb {C}^{d_\textsc{B}}\), and \(\{ X_a\} \) is any family on \(\mathbb {C}^{d_\textsc{B}}\), then the \(b\)-marginal of \(Q\) inherits \(Q\)’s consistency with the ordered product:
For 5: projectivity gives \(A_i - A_i B_i = A_i (A_i - B_i)\), and the cross terms of one fibre vanish because \(A_i A_{i'} = 0\) for \(i \neq i'\), so the fibre’s squared norm is the sum of its terms’ squared norms. Each term loses only \(A_i \leq I\), and the fibres are disjoint, so the outer sum is absorbed rather than repeated.
For 6, the intermediate operator is \(\sum _b Q_{a,b} \otimes Z_b\). Reaching it from \(\sum _b Q_{a,b} \otimes I\) is exactly the first part, applied along the fibres of the first projection. Reaching \(I\otimes X_a\) from it uses \(\sum _b Z_b = I\) to write the difference as \(\sum _b (I\otimes Z_b)\bigl( Q_{a,b} \otimes I- I\otimes Z_b X_a \bigr)\), whose terms are again mutually orthogonal — which is what makes the sum over the summed-out outcome free rather than a factor \(|\mathcal{B}|\). One triangle inequality joins the two.
Comments.
Formalized in MIPRE/Foundations/Commutation.lean (the fact) and MIPRE/Foundations/Pasting.lean (the marginal step). This is the paper’s lem:cool-closeness-fact in the partition form its round-11 repair gives it, and the partition form is the point: the consumer applies it to the \(q\) fibres of an outcome map at once, and the single-subset form would cost a factor \(q\) there.
Let \(\mu \) be a distribution on questions, \(|\psi \rangle \) a unit vector, and suppose given, for each question:
a projective measurement \(\{ A_{b,a}\} \) on \(\mathbb {C}^{d_\textsc{A}}\) with outcomes pairs in \(\mathcal{A}\times \mathcal{B}\);
a projective measurement \(\{ R_b\} _{b \in \mathcal{A}}\) on \(\mathbb {C}^{d_\textsc{B}}\) — in the application already the coarse-graining of the first family along its own outcome map, which is why only its projectivity appears;
a projective measurement \(\{ G_g\} _{g \in \mathcal{C}}\) on \(\mathbb {C}^{d_\textsc{B}}\), a copy \(\{ G'_g\} \) of it on \(\mathbb {C}^{d_\textsc{A}}\), and an outcome map \(e : \mathcal{C}\to \mathcal{B}\).
Write \(J_{b, a} = \sum _{g \, :\, e(g) = a} G_g R_b G_g\) for the pasted family, which is a POVM. Suppose that
and that the collision term \(\mathop{\mathbb {E}}\sum _b \sum _{g \neq g' \, :\, e(g) = e(g')} \langle \psi | G'_{g'} \otimes G_g R_b G_g |\psi \rangle \) is at most \(\varepsilon \). Then
and hence \(A_{b,a} \otimes I\simeq _{\delta _{\mathrm{pasting}}} I\otimes J_{b,a}\) with \(\delta _{\mathrm{pasting}}\) twice the right-hand side of 8.
Finally, if the question is a pair \((z, y)\) with \(y\) uniform and independent of \(z\), every family above depending on \(z\) alone and only \(e\) on \(y\), and if any two distinct \(g, g'\) satisfy \(e_z(y)(g) = e_z(y)(g')\) for at most an \(\varepsilon (z)\) fraction of the probes \(y\), then the collision term is at most the average of \(\varepsilon (z)\). The dependence on \(z\) is what the consumer needs: for a degenerate line — a direction that is zero, which the seeded test’s diagonal branch does sample — the outcome map separates nothing at all, and what makes the average small is that such lines are rare, not that the bound holds at every question.
The target is the agreement of \(A\) with the sandwich. Two steps reach it. The ordered product \(G_g R_b\) carries all but \(\delta /2 + \sqrt{\delta /2}\): its outer factor sums away against Alice’s second marginal by the second hypothesis, and what is left is Alice’s first marginal against \(I- R_b\), whose Cauchy–Schwarz costs the square root of the first hypothesis. Passing from the ordered product to the sandwich costs one more Cauchy–Schwarz against Bob’s commutator \([R_b, G_g]\), the front factor \(A_{b, e(g)} \otimes G_g\) being a mutually orthogonal family and so a contraction.
So everything reduces to the fine-grained commutator \(\sum _{b, g} \left\| {[R_b, G_g] |\psi \rangle } \right\| ^2\). Its coarse-grained counterpart, with \(G\) replaced by its fibre sums, is at most \(16(\delta + \delta )\) by Lemma 2.31 — read in the mirror, with both families on Bob’s factor and Alice’s joint measurement supplying the operator both products reach. Expanding either commutator, the two diagonal terms are exactly one because \(R\) and \(G\) are projective, so each equals \(2 - 2\Sigma \) for its own overlap \(\Sigma \), and the two off-diagonal terms are complex conjugates. Comparing the two overlaps is the only remaining work, and it passes through the paper’s cloud and strife: replacing Bob’s outer factor by Alice’s copy of it costs \(\sqrt\eta \) on each side — and nothing depending on \(|\mathcal{C}|\), because one factor \(R_b\) stays in front of the deviation, so the sum over \(b\) is absorbed — while the cloud and the strife differ by exactly the collision term.
For the last part, the Born probabilities do not depend on the probe, so the probe average acts on the collision indicator alone; what multiplies it is a POVM’s total mass, which is one.
Comments.
Formalized in MIPRE/Foundations/Pasting.lean. This is NW19’s Fact 4.35, the paper’s lem:pasting-updated (games.tex), at \(k = 2\); the paper’s reduction of general \(k\) to \(k = 2\) is an induction that adds nothing, and the consumer (Lemma 3.58) needs \(k = 2\) only.
Two hypotheses of the paper’s statement are absent, and both are absences rather than gaps. First, the inner family is assumed projective; the paper allows a POVM there, and then the two diagonal sums of the commutator expansion are only approximately one, which is what its appeal to Fact 4.31 of [ 6 ] repairs. With projectivity they are exactly one and that fact is not needed at all — the consumer’s inner family is a line measurement, which is projective. Second, the cross-party self-consistency of \(G\) at the fine level is a hypothesis here, where the paper derives it from the backwards consistency and Alice’s self-consistency and pays a further \(\varepsilon \) for the passage from the fibres to the fine family. The consumer has the fine-level relation directly, as item 1 of Lemma 3.54, so the derivation would be work spent to weaken a hypothesis that is already met. Neither change touches the conclusion.
The collision term is a hypothesis of the abstract lemma and a lemma of its own for the product case. That split is what keeps the analytic core free of the question distribution: the core needs only that the off-diagonal cloud terms are small in total, and the product-distribution bridge (sum_collisionTerm_le) is where uniformity of the probe and the separating property of the outcome map are used.
Constants. \(32\delta \) rather than the \(16\delta \) of Lemma 2.31 because the two marginal hypotheses enter that lemma as a single \(\delta \), here instantiated at their sum. Nothing in the chain is a per-outcome estimate, so no constant depends on \(|\mathcal{C}|\) or on \(|\mathcal{B}|\).
2.8 Generalized Pauli observables
Let \(q = 2^k\) be an admissible field size and let \(n\) be a finite index set, so that \(\mathbb {F}_q^n\) indexes a basis of \((\mathbb {C}^q)^{\otimes n}\). Write \(\operatorname {tr}: \mathbb {F}_q \to \mathbb {F}_2\) for the field trace and, for \(a, b \in \mathbb {F}_q^n\),
The generalized Pauli, or Weyl, observables are
They satisfy, for all \(a, a', b, b' \in \mathbb {F}_q^n\):
\(\tau ^W(a) \tau ^W(a') = \tau ^W(a + a')\), so \(\tau ^W(0) = I\) and each family commutes;
\(\tau ^W(a)^\dagger = \tau ^W(a)\) and \(\tau ^W(a)^2 = I\): each is a self-adjoint involution, hence a \(\pm 1\)-observable and a unitary;
(twisted commutation) \(\tau ^X(a)\, \tau ^Z(b) = (-1)^{\langle a, b \rangle }\, \tau ^Z(b)\, \tau ^X(a)\); so the two commute when \(\langle a, b\rangle = 0\) and anticommute when it is \(1\).
For \(W \in \{ X, Z\} \) define the spectral projectors of the family by Fourier averaging,
For \(W = Z\) these are the projectors onto the computational basis vectors. They form a projective measurement and invert 9:
Finally, for \(v \in \mathbb {F}_q^n\) and \(a \in \mathbb {F}_q\) write \(v \cdot e = \sum _l v_l e_l \in \mathbb {F}_q\) for the pairing before the trace, and define the syndrome projector \(\tau ^W_{[\, \cdot \, v = a]} = \sum _{e \, :\, e \cdot v = a} \tau ^W_e\). Averaging the family along the line \(r \mapsto r v\) recovers it:
Source.
The pinned paper [ 34 ] , preliminaries.tex, sec:generalized-pauli: eq:pauli-fp and its \(\mathbb {F}_q\) analogue, eq:twisted-fq, eq:pauli-product-power, eq:pauli-obs-proj and eq:pauli-inversion-0. The cancellation behind the inversion is the paper’s lem:cancellation (Fact 3.2 of [ 6 ] ).
Comments.
The formalization is MIPRE/Foundations/Weyl.lean. It is the half of the Pauli basis test’s infrastructure that was missing: MIPRE/LCS/Pauli.lean is the \(2 \times 2\) Pauli matrices for the Magic Square, and what the expansion stage of Remark 3.41 and its swap isometry both run on is this \(\mathbb {F}_q\) Weyl system. Three points, two of them restrictions stated so that no later statement is read as more general than it is.
Characteristic two only. The paper gives the construction over \(\mathbb {F}_p\) with phases \(\omega = e^{2\pi i/p}\) and then specializes; this is the \(p = 2\) case throughout, where \(\omega = -1\) and every phase is the real sign MIPRE.sgn. Nothing is lost here: the test’s parameters are admissible by hypothesis, which means \(q = 2^k\), and no consumer instantiates it elsewhere. What it buys is that the operators are self-adjoint involutions rather than order-\(p\) unitaries — so they are genuine \(\pm 1\)-observables, and item 2 above is where the paper needs \((\tau ^W(a))^p = I\).
One matrix, not an iterated Kronecker product. \((\mathbb {C}^q)^{\otimes n}\) is presented as matrices indexed by the functions \(n \to \mathbb {F}_q\), which is \(\mathbb {F}_q^n\), so \(\tau ^W(a)\) is a single matrix and the \(n\)-register statements are the one-register statements with no associativity bookkeeping. The index set \(n\) is an arbitrary finite type rather than \(\{ 1, \ldots , n\} \), which is what lets the test use it at \(n = \{ 0,1\} ^m\) — the indexing of \(\mathbb {F}_q^M\), \(M = 2^m\), that Definition 6.149 already uses.
The cancellation lemma needed a generalization, not a port. The identity behind the inversion in 10 is that a nontrivial sign character of \(\mathbb {F}_q^n\) sums to zero, and that is the index-two kernel of a nonzero \(\mathbb {F}_2\)-linear functional. The repository had that count only for a functional on a field extension (card_filter_ker_mul); the proof uses nothing but the module structure and a vector off the kernel, so it is now stated for any finite \(\mathbb {F}\)-vector space (card_filter_ker_mul’), with the field-extension form as the instance. The paper’s own correction note on lem:cancellation warns that the ambient space must be a subspace over the base field and that the statement is false over a subfield; here the space is all of \(\mathbb {F}_q^n\) over \(\mathbb {F}_2\), so there is nothing to check.
The spectral theory is proved once, for both families. The only properties of a family that 10 and 11 use are the three of IsWeylFamily: it represents the additive group, its operators are self-adjoint, and the identity sits at \(0\). So the projectors are built by 9 from any such family and the statements hold for both, which means the paper’s Fourier transform (eq:fourier-f) conjugating \(\tau ^Z\) into \(\tau ^X\) is not needed to reach the \(X\)-side projectors. That is worth avoiding: the transform carries a \(q^{-1/2}\), and a square root in matrix entries costs far more in Lean than it does on paper.
Two of the identities turn out to need even less. The expansion of an operator in its own projectors, and the line average 11, use no group law at all — they are Fourier inversion on the index group and hold for an arbitrary family. What the group law buys is that the projectors are mutually orthogonal, which is what makes them a measurement rather than a resolution.
Equation 11 is the identity Lemma 3.51 averages to, at \(v = \mathrm{ind}_m(u)\).
On two copies of \((\mathbb {C}^q)^{\otimes n}\),
a unit vector. For any operator \(M\) on one copy,
and the Weyl operators and their spectral projectors are symmetric, so for them the transpose is invisible: the two parties’ operators act identically on the state.
Both facts about the syndrome projectors \(\tau ^W_{[\, \cdot \, v = a]}\) — that they are a projective measurement, and that they transport across the state — hold for the coarse-graining of the eigenbasis measurement along a level set of an arbitrary label, the syndrome being the case of the label \(e \mapsto \langle e, v\rangle \); and coarse-graining such a family again gives the family of the composite label.
Comments.
Formalized in MIPRE/Foundations/WeylEPR.lean. The stabilizer relation of 12 at \(M = \tau ^W(a)\) is what the expansion stage of Remark 3.41 runs on: its expanded state adjoins \(|\textsc{EPR}_q\rangle ^{\otimes M}\) to each player, and the sign \((-1)^{\gamma (\omega )}\) that the strategy’s own observables carry is cancelled against one the ancilla observables carry, for which the two ancilla halves must be tied together.
This is the second dividend of characteristic two, after the operators being involutions. Over \(\mathbb {F}_p\) for odd \(p\) the transpose of \(\tau ^Z(b)\) is \(\tau ^Z(b)\) but its conjugate is \(\tau ^Z(-b)\), and the bookkeeping reappears; here every entry is real and the transpose is the identity map on the whole family, projectors included (stateVec_epr_proj, which needs only that the family is symmetric).
[\(\bullet \) easy]
Let \(q = 2^k\) be an admissible field size, let \(L\) be a finite index set, and let \(\{ e_1, \ldots , e_k\} \) be a self-dual basis of \(\mathbb {F}_q\) over \(\mathbb {F}_2\), with coordinate map \(\kappa \). Then the relabelling
is a bijection, and conjugating by it carries the whole Weyl system over \(\mathbb {F}_q\) on \(L\) registers to the Weyl system over \(\mathbb {F}_2\) on \(L k\) registers: the form \(\langle \cdot , \cdot \rangle \), the two operator families \(\tau ^X\) and \(\tau ^Z\), their spectral projectors, and \(|\textsc{EPR}_q\rangle ^{\otimes L} \mapsto |\textsc{EPR}_2\rangle ^{\otimes L k}\). Such a basis exists whenever \(k\) is odd.
Four steps, one per piece, and only the first uses self-duality. The form transports because \(\operatorname {tr}(x y) = \kappa (x) \cdot \kappa (y)\), which is item 2 of the paper’s lem:downsize_field and is exactly self-duality (MIPRE.LowDegree.trace_mul_eq_dot); summing over the \(L\) registers is trDot_binEquiv. \(\tau ^Z\) transports because its entries are the characters of the form, so it transports as soon as the form does. \(\tau ^X\) transports because \(\phi \) is additive, which is all a shift knows about — no self-duality. The projectors transport because the Fourier average of 9 reindexes along \(\phi \) and the normalization is one cardinality counted on either side. The state transports because both sides are the normalized diagonal and a relabelling preserves the diagonal. Existence of the basis is the existence half of Lemma 3.87.
Comments.
Formalized in MIPRE/Foundations/WeylBinary.lean; this is the paper’s lem:pauli-binary (preliminaries.tex), which is what makes the Pauli basis test a self-test for qubit Pauli observables and \(|\textsc{EPR}_2\rangle \), as its cor:pauli-binary states.
A relabelling, not an isometry. The paper builds an isometry \(\theta : \mathbb {C}^q \to (\mathbb {C}^2)^{\otimes k}\) and states the conclusion as \(\tau ^W_u = \phi ^\dagger (\bigotimes _{i,j} \sigma ^W_{u_{ij}}) \phi \). Here both systems are matrices indexed by a finite set — \(\mathbb {F}_q^L\) on one side, \(\mathbb {F}_2^{L \times k}\) on the other — and \(\phi \) is a bijection of those index sets, so conjugating by the corresponding permutation unitary is Matrix.submatrix along \(\phi \) and no unitary has to be constructed. That is the same simplification as presenting \((\mathbb {C}^q)^{\otimes n}\) as one matrix rather than an iterated Kronecker product, and it is why the four items are four short calculations.
What “these are qubit Paulis” means here. The target is the Weyl system at \(\mathbb {F}= \mathbb {F}_2\) and index set \(L \times k\), whose matrices are indexed by \(\mathbb {F}_2^{L \times k}\) — the computational basis of \((\mathbb {C}^2)^{\otimes L k}\). That the operators really are the tensor products of single-qubit Paulis is then a statement inside that system, and it is checked rather than read off the encoding: the form is the plain dot product (trDot_two, the field trace of a one-dimensional extension being the identity), its character is a product over the qubits (sgn_trDot_two), and each operator’s entries factor accordingly (wZ_two_diag on the diagonal, wX_two_apply everywhere). The paper’s \(\bigotimes _{i=1}^L \bigotimes _{j=1}^k \sigma ^W_{u_{ij}}\) is that factorization.
The oddness of \(k\) is inherited, not needed. Every statement above holds for any self-dual basis, given as a hypothesis; only the existence clause asks \(k\) to be odd, and that is the restriction of Lemma 3.87’s formalized half, not of this lemma. The paper’s admissible sizes satisfy it.
Let \(\mu \) be a distribution on a finite set \(\mathcal{X}\), let \(|\psi \rangle \in \mathbb {C}^{d_\textsc{A}} \otimes \mathbb {C}^{d_\textsc{B}}\), and let \(\{ M^x_a\} \), \(\{ N^x_a\} \) be families of POVMs on the two factors with a common question set \(\mathcal{X}\) and a common answer set. Their inconsistency on \(|\psi \rangle \) is
the probability that the two measurements return different answers. We say \(M\) and \(N\) are \(\delta \)-consistent if their inconsistency is at most \(\delta \).
Comments.
This is Definition 4.8 of [ 2 ] , in the two-space form used by Theorem 3.12. It is a different notion from the POVM distance of Definition 2.26: consistency compares two families across the two factors of the state, whereas \(\approx _\delta \) compares them as operator families.
Definition 2.26 is state-independent, whereas the companion paper’s \(\approx _\delta \) (games.tex) is the state-dependent quantity \(\mathop{\mathbb {E}}_{x \sim \mu } \sum _a \left\| {(M^x_a - N^x_a)|\psi \rangle } \right\| ^2\). For a synchronous strategy the two agree. The state is then the maximally entangled state on \(\mathbb {C}^d \otimes \mathbb {C}^d\), and for it \(\langle \psi | (A^\dagger A) \otimes I |\psi \rangle = \operatorname{tr}(A^\dagger A)/d = \left\| {A} \right\| _{hs}^2\), so Definition 2.26 is the state-dependent distance at the tracial state. Every formalized consumer of Definition 2.26 is synchronous, and the soundness of oracularization (Lemma 6.136) reads it that way. For a general bipartite strategy the two notions differ, so a chapter 3 consumer that is not synchronous will need the state-dependent notion added rather than this one reused.
Let \(\{ O_i\} _{i \in I}\), \(\{ C_i\} _{i \in I}\), \(\{ D_i\} _{i \in I}\) be finite families of projections on \(\mathbb {C}^{d \times d}\) with \(\sum _i \tau (O_i) = 1\) and \(\sum _i \tau (C_i D_i) = 1\). Then
Write \(X_i = (1 - C_i) O_i\) and \(Y_i = (1 - D_i) O_i\), so that \(C_i O_i = O_i - X_i\) and \(D_i O_i = O_i - Y_i\). Since \(1 - C_i\) and \(1 - D_i\) are projections, \(\left\| {X_i} \right\| _{hs}^2 = \tau (O_i (1 - C_i))\) and \(\left\| {Y_i} \right\| _{hs}^2 = \tau (O_i (1 - D_i))\); write \(\beta \) and \(\alpha \) for the two sums, which are therefore nonnegative. Expanding the left-hand side and using \(\sum _i \tau (C_i D_i) = \sum _i \tau (O_i) = 1\),
Since \(O_i\) is a projection, \(\tau (O_i D_i C_i) = \langle D_i O_i, C_i O_i \rangle _{hs} = \langle O_i - Y_i, O_i - X_i \rangle _{hs}\), which expands to \(\tau (O_i) - \tau (O_i(1 - C_i)) - \tau (O_i(1 - D_i)) + \langle Y_i, X_i \rangle _{hs}\). Summing over \(i\), \(\sum _i \tau (O_i D_i C_i) = 1 - \alpha - \beta + \sum _i \langle Y_i, X_i \rangle _{hs}\), and Cauchy–Schwarz followed by the arithmetic–geometric mean inequality gives \(\bigl| \sum _i \langle Y_i, X_i \rangle _{hs} \bigr| \leq \sqrt{\alpha }\sqrt{\beta } \leq (\alpha + \beta )/2\). Hence \(\sum _i \left\| {C_i D_i - O_i} \right\| _{hs}^2 \leq 2(\alpha + \beta ) + (\alpha + \beta )\).
Let \(\{ O_i\} _{i \in I}\), \(\{ C_i\} _{i \in I}\), \(\{ D_i\} _{i \in I}\) be finite families of projections on \(\mathbb {C}^{d \times d}\) with \(\sum _i \tau (O_i) = 1\), and let \(\mathrm{acc} \subseteq I\). Then
This is the measurement-level form of [ 6 , Fact 4.31 ] , in the one direction a soundness argument needs and in the synchronous setting, where \(\tau ((C_iD_i)^\dagger C_iD_i) = \tau (C_iD_i)\) makes the products a measurement on the nose. Put \(w_i = C_iD_i - O_i\). Then \(\tau (C_iD_i) = \left\| {C_iD_i} \right\| _{hs}^2 = \left\| {O_i + w_i} \right\| _{hs}^2 = \tau (O_i) + 2\langle O_i, w_i\rangle _{hs} + \left\| {w_i} \right\| _{hs}^2\). Summing over \(\mathrm{acc}\) and dropping the last term, which is nonnegative,
and Cauchy–Schwarz over the index bounds the last modulus by \(\sqrt{\sum _{i \in \mathrm{acc}} \tau (O_i)} \cdot \sqrt{\sum _{i \in \mathrm{acc}} \left\| {w_i} \right\| _{hs}^2} \leq 1 \cdot \sqrt{\sum _i \left\| {w_i} \right\| _{hs}^2}\).
Comments.
The square root is spent here and nowhere else in the soundness of oracularization; everything before it, including Lemma 2.39, is linear. That is what repair 1 of Remark 6.146 is about.
2.9 Computability conventions
Turing machines are represented by their Gödel numbers; in Lean the intended model is Mathlib’s Nat.Partrec.Code, with \(\phi _e\) the partial function computed by code \(e\) and “\(e\) halts on empty input” meaning \((\texttt{e.eval } 0).\texttt{Dom}\). Running times are counted as in [ 11 ] ; polynomial-time computability of a function of strings and integers means time polynomial in the lengths of the string inputs and in \(\log \) of the integer inputs, unless an integer is explicitly given in unary.
A language \(L \subseteq \{ 0,1\} ^*\) is in \(\mathrm{RE}\) if it is the domain (equivalently, the range) of a partial computable function. The halting problem — the set of \(e\) such that \(\phi _e\) halts on the empty input — is \(\mathrm{RE}\)-complete under many-one reductions.
In Lean (MIPRE.IsRE) membership in \(L\) is Mathlib’s REPred, the domain of a partial computable function; equivalently (MIPRE.isRE_iff), \(L\) is the halting set of a well-scoped program of the ambient model (Section 4.2) on encoded strings, which is the form in which the compressibility criterion (Lemma 4.11) consumes recursive enumerability. The completeness of the halting problem is Theorem 3.79, not part of the definition.
Following [ 11 ] , 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 \). ( [ 11 ] 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.197.)
A game description is a tuple \(g = (n_\mathcal{X}, n_\mathcal{A}, w, \mathrm{acc})\) of two integers, a finite list \(w\) of weighted question pairs, and a finite list \(\mathrm{acc}\) of accepted answer tuples. It determines a synchronous game \(\mathfrak {G}_g\) on question alphabet \(\{ 0, \ldots , n_\mathcal{X}\} \) and answer alphabet \(\{ 0, \ldots , n_\mathcal{A}\} \): the question distribution is \(w\) normalized (a fixed point mass if \(w\) has total weight zero), and the predicate accepts exactly the tuples listed in \(\mathrm{acc}\), except that unequal answers to equal questions always lose. Game descriptions are first-order data and carry a canonical Gödel numbering (GameData in the Lean file).
2.10 Normal form verifiers
Games produced in the proof are presented by pairs of Turing machines: a sampler, generating questions by a rigid linear-algebraic procedure that introspection can certify, and a decider, checking answers.
An \(\ell \)-level sampler (with field size \(2\)) is a Turing machine \(\mathcal{S}\) together with, for each \(n\), a dimension \(s(n)\) and two \(\ell \)-level CL functions \(L^\textsc{A}, L^\textsc{B}\) on \(V = \mathbb {F}_2^{s(n)}\) given with exact decomposition data (Lemma 6.4) such that, writing vectors and register subspaces of \(V\) as bit strings of length \(s(n)\) (coordinates, respectively indicator vectors), for all \(w \in \{ \textsc{A}, \textsc{B}\} \), \(j \in \{ 1, \ldots , \ell \} \) and bit strings \(z, u, y\) of length \(s(n)\):
on input \((n, \mathtt{dimension})\), \(\mathcal{S}\) outputs \(s(n)\);
on input \((n, w, \mathtt{marginal}, j, z)\), it outputs the marginal \(L^w_{\leq j}(z)\);
on input \((n, w, \mathtt{linear}, j, u, y)\), it outputs \(L^w_{j,u}(y)\), provided \(u \in L^w_{{\lt}j}(V)\);
on input \((n, w, \mathtt{factor}, j, u)\), it outputs the factor space \(V^w_{j,u}\), provided \(u \in L^w_{{\lt}j}(V)\);
and \(\mathcal{S}\) halts on every input of the form \((n, \ldots )\), well formed or not; nothing is required of its outputs on other inputs. The distribution of \(\mathcal{S}\) at index \(n\) is the CL distribution \(\mu _n\) of \((L^\textsc{A}(x), L^\textsc{B}(x))\) for uniform \(x \in V\) (Definition 6.1). In the paper’s Turing-machine model, \(\mathsf{TIME}_\mathcal{S}(n)\) denotes the absolute supremum of the running times over all inputs of the form \((n, \ldots )\); totality alone does not make that supremum finite.
Comments.
This follows the query interface of the paper’s def:sampler (linear.tex) [ 34 ] at field size \(2\), the only size the normal form verifiers of this blueprint use; the paper’s samplers over \(\mathbb {F}_{2^t}\) reach this form by downsizing (Section 6.1). Two interface details matter here. The correctness clauses for \(\mathtt{linear}\) and \(\mathtt{factor}\) are imposed only for prefixes in the range of \(L^w_{{\lt}j}\), as the paper’s amended definition states, and are well defined there by Lemma 6.4. The paper additionally requires bounded-prefix format and length checks: after computing \(s(n)\), a sampler inspects only the prescribed prefix of each auxiliary input, rejecting with a fixed default when the format fails. Together with totality, this bounds the paper’s absolute \(\mathsf{TIME}_\mathcal{S}(n)\) uniformly over even malformed or overlong inputs. A total program that scans an ignored, arbitrarily long suffix would not satisfy that source contract.
In Lean the machine is a program of the ambient cost model (Section 2.9), its well-formed input is the pair of \(n\) and a query (Sampler.Query), and Sampler.TimeBoundAt n T k is a relative cost bound: it requires halting within \(T\cdot (\left\vert {d} \right\vert +1)^k\) on every input \((n,d)\), well formed or not. It is a separate predicate, not a bound \(\mathsf{TIME}_\mathcal{S}(n)\leq T\) on the absolute supremum. In particular, neither this predicate nor the totality field supplies the paper’s bounded-prefix contract.
Two departures from the paper are forced here, and both were found by trying to prove the bound for a concrete machine rather than by inspection. First, the paper’s bound is uniform over all inputs, and that reading is not available in the ambient model: a value is inspected in place one node at a time, but a loop carries the rest of a list to its next iteration only by copying it, so no program walks an unbounded list within a cost independent of its length, and a uniform bound is met by no sampler or decider that checks the length of a string against an unbounded \(s(n)\). The running time is therefore bounded by a polynomial in the size of the input. Second, the degree \(k\) of that polynomial has to be carried alongside the coefficient \(T\), because every decider of the pipeline runs another program through the universal machine, whose overhead is a polynomial \(Q\) of degree above one (Cost.Universal.univPoly): a simulated run costing \(T (\left\vert {d} \right\vert +1)^k\) becomes one costing about \(Q(T (\left\vert {d} \right\vert +1)^k)\), of degree \(k \cdot \deg Q\). No fixed degree is closed under the composition the deciders perform; a bounded degree is. Collapsing the two into one parameter — reading the bound as \(T (\left\vert {d} \right\vert +1)^T\) — would also be closed, but then \(\lambda \)-boundedness would allow degree \(n^\lambda \) in the input size, which is not a polynomial-time condition at all and would make Theorem 6.197 assume compression of verifiers its proof cannot compress.
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 if it halts with output \(1\), and rejects otherwise (output \(0\), or a timeout). In the paper, \(\mathsf{TIME}_\mathcal{D}(n)\) denotes the absolute supremum of its running times over all inputs with index \(n\), possibly infinite. In Lean, Decider.TimeBoundAt n T k instead requires halting within cost \(T \cdot (\left\vert {d} \right\vert + 1)^k\) on every input \((n, d)\). This relative bound implies totality at index \(n\), but need not imply finite absolute \(\mathsf{TIME}_\mathcal{D}(n)\), for the reasons given after Definition 2.44.
An ambient normal form verifier is a pair \(\mathsf{V}=(\mathcal{S},\mathcal{D})\) of a sampler over \(\mathbb {F}_2\) and a decider satisfying the extensional condition
This is Verifier.accepts_length; no particular sequence of preliminary checks is part of the structure. For each index \(n\) and independently chosen answer cut \(T\in \mathbb {N}\), the game \(\mathsf{V}_{n,T}\) (Verifier.game n T) has question sets \(\mathcal{X}=\mathcal{Y}=\{ 0,1\} ^{s(n)}\), answer sets consisting of the bit strings of length at most \(T\), the sampler distribution at index \(n\), and decision predicate equal to the decider’s acceptance predicate. Its definition imposes no time-bound hypothesis. We write \(\mathsf{V}_n\) when the answer cut is specified by the surrounding statement.
The condition Verifier.IsSynchronousAt n says that the decider rejects unequal answers to equal questions at index \(n\). Under this condition, Verifier.syncGame n T is the same game as a synchronous game, so its synchronous value is defined (Remark 2.48). The description length is \(\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}\).
The paper’s def:normal-ver requires an operational first step: compute \(s(n)\) and check both question lengths before continuing. Its def:normal-game uses answer strings of length at most the finite absolute time \(\mathsf{TIME}_\mathcal{D}(n)\) (games.tex [ 34 ] ). The dimension check yields \(s(n)\leq \mathsf{TIME}_\mathcal{D}(n)\) in that machine model. These source requirements are not the checked ambient definition above.
Relating executions in the two models and identifying the source answer cut are part of the pending normalization in Remark 2.51. An ambient relative-cost coefficient need not be the source absolute time, and increasing an answer cut may change the value. In the ambient model acceptance is halting with output \(1\); the relative time bound ensures totality with input-dependent budgets. The dimension bound needed by the pipeline is required independently in Definition 2.49.
An earlier arrangement of the pipeline of Section 6 asked two properties of the games it produces, neither of which follows from symmetrizing the players’ roles. The pipeline no longer needs either, its soundness being carried in \(\mathrm{val}^*\) throughout (Remark 6.8); the two are recorded here because they are what a synchronous route would have to establish, and because the second is the reason there is no synchronous route:
Synchronicity: equal questions reject unequal answers, so that \(\mathrm{val}^{s}\) is defined at all. For a game given by a game description this holds by fiat (Definition 2.43); for a game given by a normal form verifier it is a condition on the decider. It would be needed wherever \(\mathrm{val}^{s}\) occurs; direct repetition preserves it, since two unequal answer tuples to equal question tuples differ in some coordinate, where the repeated game rejects.
Common marginals and diagonal weight: the game’s two marginals agree, with common marginal \(\nu \), and the almost-synchronous transport requires \(\mu (x,x)\geq \kappa \nu (x)\) for every \(x\), with the same \(\kappa {\gt} 0\) along the whole recursion. This is the hypothesis of Theorem 3.3, without which the two values of a game are unrelated (Remark 3.4).
The second property is emphatically not one of repeated games: the \(k\)-fold repetition of a game with diagonal weight \(\kappa \) has diagonal weight \(\kappa ^k\). A synchronous route would therefore have to establish it for the constructions of introspection, oracularization and answer reduction — never inheriting it from the game being compressed, and never applying the transport to a repeated game — and in [ 1 ] both properties come from the typed structure of the samplers, which this blueprint does not carry (Section 1.3). Neither is established here, and neither needs to be.
For \(\lambda \in \mathbb {N}\), an ambient normal form verifier \(\mathsf{V}=(\mathcal{S},\mathcal{D})\) is \(\lambda \)-bounded if \(\left\vert {\mathsf{V}} \right\vert \leq \lambda \) and, for every \(n\geq 2\), \(s(n)\leq n^\lambda \) and both programs halt within cost \(n^\lambda (\left\vert {d} \right\vert +1)^\lambda \) on every encoded input \((n,d)\). Equivalently, both Sampler.TimeBoundAt and Decider.TimeBoundAt hold at parameters \((n,n^\lambda ,\lambda )\). The parameter \(\lambda \) controls the coefficient’s growth in \(n\) and bounds the polynomial degree in the auxiliary input size. The dimension bound is a separate clause; neither it nor an absolute-time bound is inferred from the relative cost predicates.
The paper’s def:lambda instead requires \(\mathsf{TIME}_\mathcal{S}(n),\mathsf{TIME}_\mathcal{D}(n)\leq n^\lambda \) in the absolute-time model, for \(n\geq 2\), and \(\left\vert {\mathsf{V}} \right\vert \leq \lambda \) [ 34 ] . The source dimension bound follows from writing the sampler’s output and from the decider’s initial checks. This condition and the marked ambient definition above are different contracts; their comparison requires the normalization obligation below.
The paper’s transformation contracts use absolute simulation budgets and, where stated, standard timeout form. They cannot be applied to Verifier.IsBounded solely by reinterpreting \(\mathsf{TIME}\): even on inputs of size \(O(N^\lambda )\) the relative budget \(N^\lambda (\left\vert {d} \right\vert +1)^\lambda \) can be much larger than \(N^\lambda \). A normalization bridge must supply bounded-prefix behavior and the required timeout form, preserve the sampler distribution and the chosen finite game, and transfer the relevant completeness witnesses. It must keep the original answer cut by rejecting longer answers rather than silently enlarging the alphabet when it increases the simulation budget. Any new absolute bound, for example \(N^{p(\lambda )}\), must then be propagated through the transformation parameters. This is a pending bridge between the source and ambient interfaces; the existing conditional Lean results do not construct it.
A language \(L\subseteq \{ 0,1\} ^*\) is in \(\mathrm{MIP}^*_{1,1/2}(2,1)\), written \(\mathrm{MIP}^*\) here, if there are two machines, a sampler \(\mathcal{S}\) and a decider \(\mathcal{D}\), and a polynomial \(P\) such that for every string \(z\), writing \(B = P(\left\vert {z} \right\vert )\):
Efficiency. On input \(z\) and a uniformly random seed \(r\in \{ 0,1\} ^B\), the sampler halts within time \(P(\left\vert {z} \right\vert +\left\vert {r} \right\vert )\) with a pair \((x,y)\) of strings of length at most \(B\); write \(\mu _z\) for the distribution of \((x,y)\). On input \((z,x,y,a,b)\), the decider halts within time \(P(\left\vert {z} \right\vert +\left\vert {x} \right\vert +\left\vert {y} \right\vert +\left\vert {a} \right\vert +\left\vert {b} \right\vert )\) with a bit \(D_z(x,y,a,b)\), and this bit is \(0\) whenever one of \(x,y,a,b\) is longer than \(B\). The game \(\mathfrak {G}_z\) has the strings of length at most \(B\) as its question and answer alphabets, question distribution \(\mu _z\) and decision predicate \(D_z\).
Completeness. If \(z\in L\) then \(\mathrm{val}^*(\mathfrak {G}_z)=1\).
Soundness. If \(z\notin L\) then \(\mathrm{val}^*(\mathfrak {G}_z)\leq \tfrac 12\).
The paper’s definition (games.tex [ 34 ] ) has the decider run in time \(\mathrm{poly}(\left\vert {z} \right\vert )\) “even for long inputs \(a,b\)”, which its footnote makes precise by having the decider return \(0\) whenever the four strings are too long. In the ambient model a program reads a list only by walking it (the discussion under Definition 2.45), so the time bound is stated in the total input length and the footnote’s clause is a separate requirement; the game on the strings of length at most \(B\) is then the paper’s finite game, and the two readings define the same class. A randomized machine is a deterministic program with an explicit uniform seed of the length \(B\) of its time bound, and for the same reason the sampler’s time is bounded by \(P\) in its total input length \(\left\vert {z} \right\vert + \left\vert {r} \right\vert = \left\vert {z} \right\vert + B\): a program cannot read a seed of length \(B\) within time \(B\), and with \(B\) polynomial in \(\left\vert {z} \right\vert \) the bound is still \(\mathrm{poly}(\left\vert {z} \right\vert )\). In Lean the verifier is a PolyVerifier, the clause is PolyVerifier.Efficient, the game is PolyVerifier.game and the class is MIPRE.MIPStar.
A language \(L\subseteq \{ 0,1\} ^*\) is in the computable class if there exists a computable map \(g\) from bit strings to HaltingGameValue.GameData (Definition 2.43) such that for every string \(z\),
The game \(\mathfrak {G}_{g(z)}\) is the explicit game (g z).game. Computability is the Mathlib Computable predicate; there is no polynomial-time bound on \(g\) in this definition. This is MIPRE.MIPStarComputable, the class used by the checked inclusion in \(\mathrm{RE}\) and by the main theorem in its current form (Theorem 7.6); in Lean it is the class MIPRE.MIPClass of Definition 8.34 at the tensor-product value model.
Given \(z\), run the sampler on every seed of length \(B\) and the decider on every tuple of strings of length at most \(B\), each under the budget the efficiency clause supplies; a run within a known budget is decidable, so the table of \(\mathfrak {G}_z\) is computable from \(z\). It is written as a game description with Alice’s questions and Bob’s tagged apart (the description format forces unequal answers to equal questions to lose, and \(\mathfrak {G}_z\) is a general bipartite game), and the tagged game has the value of \(\mathfrak {G}_z\) (quantumValue_doubled). In Lean: PolyVerifier.tab, tab_computable and quantumValue_tab. The inclusion in \(\mathrm{RE}\) is then Lemma 7.5.
Definition 2.52 is the paper’s \(\mathrm{MIP}^*_{1,1/2}(2,1)\) up to the readings of the time bounds recorded after it. The checked halting reduction (Theorem 6.214) has two forms. Along the criterion route it supplies its game as an explicit description computed with no time bound — the tabulation of a verifier at a level exponential in the machine’s size, whose questions no polynomial-time sampler can write down — which is what the computable class of Definition 2.53 asks for. Along the paper’s route it supplies the verifier \(\mathsf{V}^{\mathsf{halt}}\) at the fixed level \(C\) with \(\lambda = \mathrm{poly}(\left\vert {\cal {M}} \right\vert )\) (Lemma 6.210), played on input \(z\) by a polynomial-time sampler and decider, which is what Definition 2.52 asks for; so Theorem 7.6 holds for both classes (MIPRE.Halting.mipstar_eq_re, MIPRE.Halting.mipstarComputable_eq_re), and Lemma 2.54 is the inclusion of the first in the second. General bipartite games must be represented in GameData with value-preserving transport; merely forcing unequal answers to equal questions to lose can destroy a perfect strategy, which is why both tabulations tag the two players’ questions apart.