\(1 - e_{xa} = \sum _{a' \neq a} e_{xa'} - (\sum _{a'} e_{xa'} - 1) \in M\), and \(e - e^2 = e(1 - e)e + (1 - e)e(1 - e) \in M\), so \(1 - g^2 \in M\) for every variable \(g\) and, telescoping, \(1 - w^* w \in M\) for every word \(w\). Then \((1 + \left\vert {\alpha } \right\vert ^2) \cdot 1 + \alpha w + (\alpha w)^* = (1 + \alpha w)^*(1 + \alpha w) + \left\vert {\alpha } \right\vert ^2 (1 - w^* w)\), and the anti-hermitian part of a monomial lies in \(M\). On a strategy the relations evaluate to \(0\), \(\langle \psi , s^* g s \psi \rangle = \langle s\psi , g\, s\psi \rangle \geq 0\) for positive \(g\), and anti-hermitian operators have imaginary expectations.

A cone state is hermitian (since \(z - z^*\) and \(i(z + z^*)\) are anti-hermitian), vanishes on \(I\) (since \(\pm j, \pm i j \in I \subseteq M\)) and is positive on \(s^* s\) and \(s^* g s\). The GNS construction completes \(P\) for the seminorm \(\mathrm{Re}\, L(a^* a)^{1/2}\); left multiplication by a variable \(g\) is a contraction because \(a^*(1 - g^2) a \in M\), and extends to a positive operator on the completion. The normalizations and the cross-commutation hold because the corresponding vectors are null, and the class of \(1\) is a unit vector.

A cone state is determined by its values on words. The set of those value families that are cone states is closed in the product topology, since each condition involves finitely many words, and lies in the product of closed unit disks, since \(2 \cdot 1 + \alpha w + (\alpha w)^* \in M\) for \(\left\vert {\alpha } \right\vert = 1\) gives \(\left\vert {L(w)} \right\vert \leq 1\). By Tychonoff it is compact, and by Lemma 8.10 its continuous image under \(L \mapsto \mathrm{Re}\, L(e_{xa} f_{yb})\) is \(C_{qc}\).

If \(h = r \cdot 1 - W_\mathfrak {G}\notin M\), the Riesz extension theorem applied to the cone \(M + \mathbb {R}_{\geq 0}(-h)\), with the functional \(t \cdot 1 \mapsto t\) on the span of \(1\), gives a real functional \(L_0 \geq 0\) on \(M\) with \(L_0(1) = 1\) and \(L_0(h) \leq 0\); the Archimedean property supplies both hypotheses. Its complexification \(L_0(z) - i L_0(iz)\) is a cone state, and Lemma 8.10 turns it into a strategy of value \(L_0(W_\mathfrak {G}) \geq r {\gt} \omega ^{\mathrm{co}}(\mathfrak {G})\), a contradiction. The converse is Lemma 8.9, with a strategy supplied by the deterministic one.

Soundness: every word acts as a contraction, so on every strategy \(2 N^2 \kappa (r - \text{value}) \geq \mathrm{Re} \langle \psi , (T + T^*)\psi \rangle \) is at least the dominance margin of \(T + T^*\), uniformly over strategies. Completeness: take \(\omega ^{\mathrm{co}}(\mathfrak {G}) {\lt} r' {\lt} r\); Theorem 8.12 writes \(\kappa (r \cdot 1 - W_\mathfrak {G}) = \varepsilon \cdot 1 + \sum _i \sigma _i^* g_i \sigma _i + \sum _t c_t w_t \rho _t w'_t + a\) with \(\varepsilon = \kappa (r - r') {\gt} 0\) and \(a\) anti-hermitian, which symmetrization removes. Rounding the coefficients of the \(\sigma _i\) at scale \(N\) and the \(c_t\) at scale \(N^2\) changes \(T + T^*\) by \(O(N)\) in the \(\ell ^1\) norm of coefficients (submultiplicative and star-invariant), against a constant term \(2N^2\varepsilon \).

The certificates of Lemma 8.13 at \(\kappa = q\, W_g\), where \(W_g\) is the total weight of \(g\), have integer data: \(\kappa (p/q \cdot 1 - W_{\mathfrak {G}_g}) = p W_g \cdot 1 - q \sum \mathrm{wt}(x,y)[D]\, e_{xa} f_{yb}\). The checker computes \(T + T^*\) on lists of monomials with coded Gaussian-integer coefficients, merges equal words, tests dominance, and rejects \(q = 0\) and malformed letters or relation indices; it is primitive recursive, and a certificate passes exactly when \(\omega ^{\mathrm{co}}(\mathfrak {G}_g) {\lt} p/q\). Enumerating certificates gives the semidecider.

\(E^x_a F^y_b\) is the product of two commuting positive operators, hence positive, which gives nonnegativity; the sum over \(a, b\) is \(\langle \psi , \psi \rangle = 1\). On \(\mathbb {C}^{d_A} \otimes \mathbb {C}^{d_B}\) the operators \(A^x_a \otimes I\) and \(I\otimes B^y_b\) are commuting projections with the same Born probabilities. The payoff is linear, hence continuous, so the bound \(\mathrm{val}^*(\mathfrak {G})\) on \(C_q\) passes to its closure.

If \(\omega ^{\mathrm{co}}(\mathfrak {G}_d) \leq \mathrm{val}^*(\mathfrak {G}_d)\) for every \(d\), the two values agree on every described game, since \(\mathrm{val}^*\leq \omega ^{\mathrm{co}}\). Then \(\cal {M}\) fails to halt exactly when \(\omega ^{\mathrm{co}}(\mathfrak {G}_{g(\cal {M})}) {\lt} \frac34\), so non-halting is the pullback of an r.e. relation along a computable map, hence r.e., which it is not (Theorem 3.79). So some \(d\) has \(\mathrm{val}^*(\mathfrak {G}_d) {\lt} \omega ^{\mathrm{co}}(\mathfrak {G}_d)\), and some commuting-operator strategy has value above \(\mathrm{val}^*(\mathfrak {G}_d)\); its correlation is in \(C_{qc}\), and its payoff exceeds the bound \(\mathrm{val}^*(\mathfrak {G}_d)\) that holds on \(C_{qa}\) (Lemma 8.16). With \(C_{qc}\) closed, \(C_{qa} \subseteq C_{qc}\), and the inclusion is strict.

Lemma 8.18, with the halting reduction of Corollary 7.3, the upper semidecider of Lemma 8.14, and the closedness of \(C_{qc}\) in every finite scenario (Lemma 8.11).

Let \(g\) be the computable map of Corollary 7.3, from machines to game descriptions, with \(\mathrm{val}^*(\mathfrak {G}_{g(\cal {M})}) = 1\) when \(\cal {M}\) halts on the empty input and \(\mathrm{val}^*(\mathfrak {G}_{g(\cal {M})}) \leq \frac12\) otherwise. By Lemma 8.14 at \(p = q = 1\), the set of machines \(\cal {M}\) with \(\omega ^{\mathrm{co}}(\mathfrak {G}_{g(\cal {M})}) {\lt} 1\) is recursively enumerable. Kleene’s recursion theorem therefore gives a machine \(\cal {M}_{\textsc{Sep}}\) that halts on the empty input exactly when \(\omega ^{\mathrm{co}}(\mathfrak {G}_{g(\cal {M}_{\textsc{Sep}})}) {\lt} 1\). Put \(\mathfrak {G}^{\textsc{Sep}} = \mathfrak {G}_{g(\cal {M}_{\textsc{Sep}})}\).

If \(\cal {M}_{\textsc{Sep}}\) halted, then \(\mathrm{val}^*(\mathfrak {G}^{\textsc{Sep}}) = 1\), so \(\omega ^{\mathrm{co}}(\mathfrak {G}^{\textsc{Sep}}) = 1\) by \(\mathrm{val}^*\leq \omega ^{\mathrm{co}}\) (Lemma 8.16), and \(\cal {M}_{\textsc{Sep}}\) would not halt. So \(\cal {M}_{\textsc{Sep}}\) does not halt. Hence \(\mathrm{val}^*(\mathfrak {G}^{\textsc{Sep}}) \leq \frac12\), and \(\omega ^{\mathrm{co}}(\mathfrak {G}^{\textsc{Sep}})\) is not below \(1\), so it equals \(1\).

For the correlation: the payoff is continuous, and \(C_{qc}\) is compact (Lemma 8.11) and nonempty, so the payoff attains its maximum on \(C_{qc}\) at some \(p\). That maximum is \(\omega ^{\mathrm{co}}(\mathfrak {G}^{\textsc{Sep}}) = 1\), since every commuting-operator strategy has value equal to the payoff of its correlation. Payoffs on \(C_{qa}\) are at most \(\mathrm{val}^*(\mathfrak {G}^{\textsc{Sep}}) \leq \frac12\) (Lemma 8.16), so \(p \notin C_{qa}\).

Let \(z \mapsto \mathfrak {G}_z\) witness \(L \in \mathrm{MIP}(\omega )\). Under the promise, \(z \notin L\) if and only if \(\omega (\mathfrak {G}_z) {\lt} 1\). The set of game descriptions \(d\) with \(\omega (\mathfrak {G}_d) {\lt} 1\) is recursively enumerable, at \(p = q = 1\), and the complement of \(L\) is its preimage under the computable map \(z \mapsto \mathfrak {G}_z\). For \(\omega ^{\mathrm{co}}\) the semidecider is Lemma 8.14; Lin’s proof runs the NPA hierarchy here  [ 13 ] , and the Lean runs the sum-of-squares certificates of Lemma 8.13. The same argument at the threshold \(\frac12\), for a model r.e. from below, is Lemma 7.5.

The soundness chain of Theorem 6.197 (Remark 6.203), read in \(\omega \): the three clauses, used contrapositively, through the same margins (Lemmas 6.201 and 6.202). Nothing else in the chain depends on the model: between the stages’ answer bounds it passes by the value of a verifier whose decider rejects every answer beyond a bound, which is the same at every larger bound in every model. The soundness clause of Theorem 6.197 is the case \(\omega = \mathrm{val}^*\).

The compressed verifier is within its budget, so its value at the answer bound of Definition 8.38 is its value at the bound of Lemma 8.40, which that lemma bounds.

The halting reduction of Theorem 6.214 in a value model \(\omega \), with the direction of the semidecider reversed. Lemma 4.12 is run with three classes of strings, each read as a normal form verifier as in Theorem 6.214 and with the same answer bounds:

• \(A(n)\): the verifier is \(n\)-bounded, rejects every answer longer than the bound, and \(\omega (\mathsf{V}_n) \leq \frac12\) — the class \(B\) of Theorem 6.214 in the model \(\omega \). It contains the trivially rejecting string \(y_{\mathrm{no}}\) of that theorem, whose game has value \(0\) in every model, and the compressor of that theorem preserves it by soundness in the model, through the class transfer of Theorem 6.214 read in \(\omega \): the described verifier rejects beyond its answer bound, so raising the bound keeps the value; freezing keeps it; soundness carries it through compression; and the output’s decider accepts what the compressed decider accepts.

• \(B_0(n)\): the class \(A\) of Theorem 6.214 — \(n\)-bounded, rejecting long answers, with a perfect PCC strategy. It contains \(y_{\mathrm{yes}}\), and the compressor preserves it by the tensor completeness of Theorem 6.197.

• \(B_1(n)\): the strings whose tabulated game at level \(n\) (the game description of Theorem 6.214, item 2) does not have \(\omega {\lt} 1\). It contains \(B_0(n)\), because a perfect PCC strategy gives \(\mathrm{val}^*= 1\) and every model dominates \(\mathrm{val}^*\); its complement is recursively enumerable by the upper semidecider of the model, at \(p = q = 1\), composed with the computable tabulation.

The criterion gives a polynomial-time \(g\) with \(g(\cal {M}) \in A\) at the start level when \(\cal {M}\) halts and \(g(\cal {M}) \in B_1\) otherwise. The game of \(\cal {M}\) is the tabulation of \(g(\cal {M})\) at that level. In the first case it has \(\omega (\mathsf{V}_n) \leq \frac12\), the tabulation having the value of the verifier’s game in every model at every bounded string, which is item 2 of Theorem 6.214 read in \(\omega \); in the second it does not have \(\omega {\lt} 1\), so \(\omega = 1\). No perfect strategy of the model is constructed. At \(\omega = \omega ^{\mathrm{co}}\) this is Lin’s verifier sequence  [ 13 ] , with the compressor’s preservation of the accepting game read as tensor completeness, and with Lemma 8.14 in place of the NPA hierarchy.

\(\mathrm{MIP}(\omega ) \subseteq \mathrm{coRE}\) is Lemma 8.37. For the converse, the complement of a co-r.e. language many-one reduces to halting on the empty input (Theorem 3.79; in Lean MIPRE.Halting.exists_code_halts_of_isRE, applied to the complement), and composing with the map of Theorem 8.42 sends the members of \(L\), whose machines do not halt, to games of value \(1\) and the non-members to games of value at most \(\frac12\). This is the argument of Theorem 7.6 with the two verdicts exchanged, and in Lean the two are the same theorem in the two shapes.

Build the gap compression of Theorem 6.197 from the introspection, which is sound in \(\omega ^{\mathrm{co}}\) by Theorem 8.84, the answer reduction, which is sound in \(\omega ^{\mathrm{co}}\) by Theorem 8.67, and the parallel repetition of Theorem 8.56, which is sound in \(\omega ^{\mathrm{co}}\): it is the compression of Theorem 6.198 with the number of repetitions chosen against the smaller of the two repetition constants. It is sound in \(\omega ^{\mathrm{co}}\) by Theorem 8.41, and the argument of Theorem 8.43, which uses of the compression only its soundness in \(\omega ^{\mathrm{co}}\) and its tensor completeness, applies to it.

Let \(s_a = \sqrt{E_a}\), by the continuous functional calculus: it is self-adjoint, \(\sum _a s_a^2 = I\), and it commutes with every operator that commutes with \(E_a\). Write operators on \(\mathcal{H}\otimes \mathbb {C}^n\) as \(n \times n\) matrices of operators on \(\mathcal{H}\), so that composition and the adjoint are the matrix product and the conjugate transpose. Let \(W\) be the \(\mathcal{A}\times \mathcal{A}\) matrix whose column \(a_0\) is \((s_a)_a\) and whose other columns vanish. Then \(W^* W\) is the matrix unit at \((a_0, a_0)\), so \(W W^* W = W\) and \(W\) is a partial isometry. The block matrix

is unitary, by the identities \(W(I- W^* W) = 0\) and \((I- W W^*) W = 0\) and their adjoints. Let \(Q_a\) be the diagonal projection onto the two copies of the coordinate \(a\), and put \(P_a = U^* Q_a U\). These are projections summing to \(I\), and the entry of \(P_a\) at the first copy of \((a_0, a_0)\) is \(s_a s_a = E_a\), which is item 1. Every entry of \(U\) is a polynomial in the \(s_b\), and so commutes with \(c\) as soon as \(c\) commutes with every \(E_b\), which is item 2.

For the strategy, take \(c = F^y_b\). The correlation at \((x, y)\) is \(\langle \iota \psi | P_a (F^y_b \otimes I) |\iota \psi \rangle = \langle \psi | \iota ^* P_a \iota F^y_b |\psi \rangle \), because \((F^y_b \otimes I) \iota = \iota F^y_b\), and item 1 makes it \(\langle \psi | E^x_a F^y_b |\psi \rangle \). At \(x' \neq x\) both operators are amplified, and \(\iota \) is an isometry. The amplification \(c \mapsto c \otimes I\) is a unital \(*\)-homomorphism, so it preserves positivity, sums to \(I\), commutation and idempotence. For the second player, exchange the players, which transposes the correlation because the two players’ operators commute.

Dilate the first player’s questions one at a time by Lemma 8.47, then the second player’s. Each step keeps the correlation and every projectivity already obtained, and makes one more measurement projective. A question has an answer, since its POVM sums to \(I\) on a nonzero space, so the lemma applies. The value is the payoff of the correlation, and it lies in \([0, 1]\), as does \(\omega ^{\mathrm{co}}(\mathfrak {G})\) (Lemma 8.16), which gives the supremum and the strategy of value greater than \(t\). A tensor-product strategy (Definition 2.3) measures \(A^x_a \otimes I\) and \(I\otimes B^y_b\) with \(A^x_a\) and \(B^y_b\) projections.

The \(E^x_a\) lie in the commutant of the \(F^y_b\), and are positive and sum to \(I\) there because they are and do in \(B(\mathcal{H})\); the same holds for the \(F^y_b\) in the commutant of that commutant. The model’s Born probability at \((E^x_a, F^y_b)\) is \(\mathrm{Re}\langle \psi , E^x_a F^y_b \psi \rangle \), the correlation, and the value is the same sum of payoffs against the same probabilities.

The operator of \((X \otimes P)(Y \otimes Q)\) acts on \(\psi \otimes e\) entrywise, as \(\pi (XY)\) on \(\psi \) and as \(P \otimes Q\) on \(e\), so its quadratic form is \(\langle e, (P \otimes Q) e\rangle \langle \psi , \pi (XY) \psi \rangle \). The first factor is real when \(P\) and \(Q\) are positive semidefinite, and the real part of the product then splits: item 1. Items 2 and 3 are item 1 with \(P = Q = I\), and item 4 is a computation in the entries.

A \(*\)-homomorphism of star-ordered algebras preserves positivity, sums and commutation, and the model’s Born probability of \((M^x_a, N^y_b)\) is the correlation of the strategy at \((x, y, a, b)\). For the converse, take a projective strategy of value above \(t\) (Theorem 8.48) and read its measurements in its model (Lemma 8.50). Its operators are projections summing to \(I\), hence mutually orthogonal: conjugating \(\sum _c P_c = I\) by \(P_a\) makes the compressions \(P_a P_c P_a = (P_c P_a)^*(P_c P_a)\), \(c \neq a\), positive operators summing to \(0\), so each vanishes, and then \(P_c P_a = 0\) by the C\(^*\)-identity. The equations of a projective measurement hold in the commutants because they hold in \(B(\mathcal{H})\), which the inclusions reflect.

Theorem 5.5 at \(\varepsilon ' = 1 - \omega ^{\mathrm{co}}(\mathfrak {G}) \geq \varepsilon \), through the arithmetic of Lemma 5.9: its exponent is \(\varepsilon '^7\), and \(\varepsilon ^{13} \leq \varepsilon ^7 \leq \varepsilon '^7\) because \(\varepsilon \leq \varepsilon ' \leq 1\). Take \(c'' = c / (1 + 2 \log 3)\) for the constant \(c\) of Theorem 5.5. The bound decreases as the constant grows.

The value of \(\mathsf{V}^{\textsc{Rep}}_n\) is the value of the repeated game in every model: the proof of Theorem 6.196 identifies the two games up to an equivalence of the questions and the padding of the answers by always-rejected ones, and a value model is invariant under both (Definition 8.34). So soundness in a model is the repetition bound in that model. Lowering the constant of the procedure keeps every clause, the bound being antitone in the constant; the procedure at \(\min (c', c'')\) is the same verifier. The main theorem keeps the constant \(c'\), so \(\mathrm{MIP}^*= \mathrm{RE}\) does not depend on Theorem 5.5.

Fix a seed \(z\) and write \(O\) for the first player’s measurement at \((\textsc{O}, z)\), \(O^\textsc{A}_u\) and \(O^\textsc{B}_v\) for its sums over the answers whose Alice, respectively Bob, component is \(u\), respectively \(v\), \(C\) for the first player’s measurement at \((\textsc{A}, L^\textsc{A}(z))\), and \(P\), \(Q\) for the second player’s at \((\textsc{A}, L^\textsc{A}(z))\) and \((\textsc{B}, L^\textsc{B}(z))\). In the model’s algebra, \(\pi _A(C_u)\pi _B(Q_v) - \pi _A(O^\textsc{A}_u O^\textsc{B}_v) = X_1 + X_2 + X_3\), where

because the two players’ operators commute. The front factors are projective measurements, so summed over their outcome they cost nothing, and each of the three deviations is the cross-party inconsistency of one role pair — \((\textsc{A}, \textsc{A})\), \((\textsc{O}, \textsc{A})\), \((\textsc{O}, \textsc{B})\) — at which acceptance forces the two answers compared to agree, so by the estimate of Definition 2.28 each is at most twice that pair’s conditional failure. So \(\delta _z = \sum _{u,v} \| \pi (\pi _A(C_u)\pi _B(Q_v) - \pi _A(O^\textsc{A}_u O^\textsc{B}_v))\psi \| ^2\) is at most \(6\) times the sum of the three conditional failures. Both \(\{ \pi _A(C_u)\pi _B(Q_v)\} \) and \(\{ \pi _A(O^\textsc{A}_u O^\textsc{B}_v)\} \) are projective measurements indexed by pairs, the second because distinct outcomes of \(O\) are orthogonal, and on the pairs of isolated answers the input predicate accepts at \((L^\textsc{A}(z), L^\textsc{B}(z))\) the second carries at least the oracle’s acceptance probability at \((\textsc{O}, \textsc{O})\). The vector form of Lemma 2.40 then puts the conditional value of the extracted families at the seed at least one minus the conditional failure at \((\textsc{O}, \textsc{O})\) minus \(2\sqrt{\delta _z}\). The four role pairs used are distinct and each carries a ninth of the question weight, so their conditional failures average to at most \(9\varepsilon \) in total, and with Cauchy–Schwarz taking the average inside the square root the value is at least \(1 - 9\varepsilon - 2\sqrt{54\varepsilon } \geq 1 - 24\sqrt\varepsilon \). Nothing here uses a dimension: projectivity is a hypothesis, and in the commuting-operator model it is supplied by Lemma 8.54. The matrix analysis of Lemma 6.137 is this one in the tensor-product model.

For \(\varepsilon \leq 1\), Lemma 8.54 gives a commuting-operator strategy whose measurements are projective in its model and whose model value exceeds \(1 - \varepsilon \). Lemma 8.57 in that model gives families of value at least \(1 - 24\sqrt\varepsilon \) in the game of \(S\), and those families are a commuting-operator strategy (Lemma 8.54). For \(\varepsilon {\gt} 1\) the bound is negative.

Item 1: at each question pair the coarse-grained families accept a superset of the outcome pairs, with the same Born probabilities summed over the fibres. Item 2 is the proof of Lemma 6.26, which uses of a strategy only its conditional failures, their nonnegativity and the averaging identity of a sampled game, all of which hold for families in a model. For the values, apply each item in the model of every strategy of the first game and take the supremum; for item 2 the transfer is affine, \(v \mapsto 1 - 16^{|T|}(1 - v)\), and passes to the supremum. In \(\omega ^{\mathrm{co}}\) the model is the strategy’s own and the output families are a commuting-operator strategy (Lemma 8.54).

In \(\mathrm{val}^*\) the three properties are Lemma 6.137 and the value forms of Lemma 8.59; in \(\omega ^{\mathrm{co}}\) they are Lemma 8.58 and the same value forms. The two clauses are then the proofs of Lemma 6.140 and of Theorem 6.133, read in \(\omega \): the typed game’s value is at most the oracularization’s, by the monotonicity and the equality of the two distributions; the game-level soundness bounds the input verifier; and the detyped verifier’s game is the finite detyped game up to the numbering of its coordinates (Lemma 6.22), on which the detyping restriction gives the typed game at least \(1 - 16^3\varepsilon \). The tensor-product clauses of Theorem 6.133 are the case \(\omega = \mathrm{val}^*\).

Each statement is its matrix counterpart for tensor-product strategies, whose proof uses of a strategy only its Born probabilities, their nonnegativity and their normalization, which hold in the model (Lemma 8.54).

The measurements of a tensor-product strategy are projective, the matrix algebras are the players’ algebras of its model and the value is computed by the same Born rule. For \(\omega ^{\mathrm{co}}\), both statements are Lemma 8.54.

A projective strategy in that model is a tensor-product strategy (Lemma 8.64), to which Theorem 3.14 applies; its extracted measurements are projective measurements in the matrix algebras, and the matrix inconsistencies it bounds are the model’s.

Let \(\omega \) of the answer-reduced verifier exceed \(1 - \varepsilon \), with \(\mu \geq 1\) and \(\varepsilon {\lt} 1\); otherwise the loss is at least \(1\). The output verifier rejects answers longer than the answer cut, so \(\omega \) at the cut exceeds \(1 - \varepsilon \), and the hypothesis gives a projective strategy of value greater than \(1 - \varepsilon \) for the game at the cut, in a model where the test is sound and which \(\omega \) dominates. The analysis of Lemma 6.190, which is stated for a projective strategy in any such model, gives \(\omega (\mathsf{V}_n) \geq 1 - \delta (\varepsilon , n)\) at the constants of the clause in \(\mathrm{val}^*\), which are explicit. For \(\omega ^{\mathrm{co}}\), oracularization is sound (Theorem 8.61), and Lemma 8.64 gives, below \(\omega ^{\mathrm{co}}\), a projective strategy in the model of a commuting-operator strategy, which \(\omega ^{\mathrm{co}}\) dominates.

Every quantity is a quadratic form of a product of represented operators on the state, and intertwining moves \(W\) past each factor; \(W\) preserves inner products. The transported effects are the images of orthogonal projections summing to \(\Phi _A(I)\), completed by the orthogonal projection \(I- \Phi _A(I)\), and the complement annihilates the image of \(W\).

Each is a permutation of the copies of \(\mathcal{H}\) in the \(\ell ^2\)-sums, which acts on the players’ operators entrywise.

The mirror identity is \((P \otimes I)|\mathrm{EPR}_I\rangle = (I\otimes P^{\mathsf T}) |\mathrm{EPR}_I\rangle \) in the ancilla factor. The others are the lemma on moving registers, with \(|\mathrm{EPR}_{J \times R}\rangle = |\mathrm{EPR}_J\rangle \otimes |\mathrm{EPR}_R\rangle \) and the invariance of \(|\mathrm{EPR}\rangle \) under relabelling.

The \(\ell ^2\)-sum of copies of \(\mathbb {C}^{d_A \times d_B}\) is \(\mathbb {C}^{(\alpha \times d_A) \times (\beta \times d_B)}\), and block matrices of matrices are matrices on the products of the indices.

The state has one nonzero component, in the copy \(t_0\), so every operator acts on it through its column \(t_0\).

In a star-ordered ring a nonnegative element is a finite sum of elements \(z^* z\), so each POVM is a Kraus family \(\{ Z^x_{a,i}\} \) with \(\sum _{a,i} (Z^x_{a,i})^* Z^x_{a,i} = I\); pad the number of terms to a common bound. The Halmos unitary of its Naimark column dilates it to orthogonal projections; coarse-grained over \(i\), they compress at the fixed basis vector to \(Q^x_a\). Neither finite dimension nor a square root is used; the matrix proof’s unitary extension needed both.

In the tensor-product model, the Naimark dilation of each party’s measurements makes the strategy projective on registers extended by the answer sets, at the same value. In a model on a Hilbert space a POVM strategy is a commuting-operator strategy. The approximations are Lemma 8.64.

On the one-sided extension, the Born probability of a pair of POVMs is that of the \((t_0, t_0)\) entries (Lemma 8.76), and the diagonal blocks of a POVM in \(M_T(\mathscr {A}_A)\) form a POVM in \(\mathscr {A}_A\). The rest is a composition.

This is Theorem 3.38 at the tensor-product model of \(\psi \), with \(\omega = \mathrm{val}^*\). An extension of that model by registers in a unit vector \(e\) is, by an isomorphism of models, the tensor-product model of the expanded vector \(e \otimes \psi \) (Lemma 8.87), in which the seeded test is sound (Lemma 8.92): that is the first hypothesis. For the second, the same isomorphism, with the state of the extension replaced by a unit vector \(v\) and that of the tensor-product model by the image of \(v\), is a local isometry whose homomorphisms are unital and which carries the state to the state, so the extension in the state \(v\) reduces to the tensor-product model of a unit vector (Lemma 8.81), whose POVM strategies \(\mathrm{val}^*\) dominates (Lemma 8.79). For the approximations, a tensor-product strategy of value near \(\mathrm{val}^*\) is a projective strategy of its own tensor-product model, of the same value, and the commuting-operator strategies play that part for \(\omega ^{\mathrm{co}}\) (Lemma 8.64).

Let the value of the output verifier exceed \(1 - \varepsilon \), with \(\varepsilon {\lt} 1\); otherwise the loss is at least \(1\). The output rejects answers beyond its cutoff and agrees with the reference verifier, so the value of the reference game at the cutoff exceeds \(1 - \varepsilon \), and a projective strategy of value above \(1 - \varepsilon \) for it exists in a model where the Pauli basis test is sound. Restricted to the typed raw game, decoded to the canonical game and restricted to the Pauli block, it stays in that model, where the test supplies the extraction; the analysis of Lemma 6.111, stated for a strategy in any model, then bounds the value of the padded source game in every value model dominating the ancilla model, and removing the padding, which needs the approximation by projective strategies, bounds the source verifier’s value. The constants are those of the clause in \(\mathrm{val}^*\), which is the case of \(\mathrm{val}^*\) (Lemma 8.83 and Lemma 8.79).

An isomorphism is a local isometry carrying the state to the state, so the first statements are Lemma 8.70; a \(*\)-isomorphism preserves positivity, sums, products and adjoints, hence POVMs and projective measurements. The value and the inconsistency are sums of Born probabilities. Exchanging the players exchanges the two factors of each Born probability, which commute.

The local isometries of Lemmas 8.71 and 8.74 carry the state to the state and have inverses of the same kind. The algebra isomorphisms are three: the one-by-one matrices over an algebra are the algebra; relabelling the rows and columns of square matrices along a bijection is a \(*\)-algebra isomorphism; and so is applying a \(*\)-isomorphism to the entries. A relabelling of the factors of a tensor-product model permutes the coordinates of \(\mathbb {C}^{d_A \times d_B}\).

An operator of an extension acts entrywise on the copies of the Hilbert space, and a reading permutes the copies, so items 1 to 3 compare entries of block matrices; in item 3 the reindexing of the \(\ell ^2\)-sum carries the state to the state and has the inverse reindexing. In item 4 the state has one nonzero component, at \((a_0, b_0)\), so a product of the two players’ operators acts on it through the entry at \((a_0, b_0)\) of each.

Item 1 is Lemma 8.70, the homomorphisms being unital so that pushed-forward POVMs are POVMs; the isometry intertwines each product of the two players’ operators with the product of their images. In item 2 the conditions on the state are those of Lemmas 8.71 and 8.89. In item 3, \((\pi _A(U)\pi _B(V))^*\pi _A(U)\pi _B(V) = I\) because \(U^*U = I\), \(V^*V = I\) and the two players’ operators commute, which also gives the intertwining; \(UU^* = I\) and \(VV^* = I\) make the conjugations unital.

Every subtest is written in both orientations, and agreement is symmetric. Along an isomorphism a projective strategy is pushed forward with its value, the measurements extracted for its image are pulled back along the inverse, and the three inconsistencies are carried over (Lemma 8.86). In the exchanged model a projective strategy is one of the model for the game with the players exchanged, which is the seeded game itself, with the same value; the measurements extracted for it serve exchanged, with the first two inconsistencies exchanged and the third symmetric. Lemma 8.66 is the tensor-product case on numbered factors, and the others follow by numbering the factors and, for an extension, by the isomorphism with the tensor-product model of the expanded vector (Lemma 8.87); an extension of the exchanged model is the exchanged extension in the exchanged vector, read backwards.

A vector of \(\mathcal{H}\otimes \mathbb {C}^\iota \) is the sum of its embedded coordinates, so an operator is determined by its compressions, and composition is the matrix product of the compressions. Commuting with \(I_\alpha \otimes E_{bb'}\) moves the blocks of a matrix: the block at \((b, b')\) is the block at \((b_0, b_0)\) when \(b = b'\) and vanishes otherwise. The identity for the matrix units is a computation with \(|u\rangle \langle u|\), all of whose entries are \(1/|\beta |\). Item 3 combines the two previous items through the operators of matrices.

An operator commuting with the second player’s operators commutes with \(F^y_b \otimes I\) and with the register’s diagonal and uniform projections, hence with its matrix units, so it is \(X \otimes I_\beta \) with the entries of \(X\) in the commutant \(\mathscr {A}_A\) of the \(F^y_b\) (Lemma 8.93); conversely every such operator commutes with them. That algebra contains \(M_\alpha (\mathbb {C}) \otimes I\) and \(\mathscr {A}_A \otimes I\), so the same lemma, for the register \(\alpha \), makes its commutant \(\{ I_\alpha \otimes Y : Y \in M_\beta (\mathscr {A}_A')\} \), and \(\mathscr {A}_A'\) is \(\mathscr {A}_B\) by definition. Both identifications are the representations of the extension, so the identity of the space intertwines them, and it carries the state to the state.

The extension is isomorphic to the model of a commuting-operator strategy (Lemma 8.94), in which the test is sound by hypothesis, and soundness passes along isomorphisms (Lemma 8.92).

The action is the entrywise inclusion of the scalars followed by the action of operator matrices (Lemma 8.47), a composite of unital \(*\)-homomorphisms. The formulas are the matrix product in the register’s coordinates, and in an extension both players’ scalar matrices act on the copies of the Hilbert space alone.

Item 1: distinct outcomes of a projective measurement are orthogonal, so the cross terms vanish. Item 2 telescopes the deviation and applies the Cauchy–Schwarz inequality against the constant one, item 3 the triangle inequality over the outcomes and then the same inequality. In item 4 the difference splits into two terms, each with the deviation on one side, and each is bounded by the Cauchy–Schwarz inequality against a vector of norm at most one. Item 5 is the triangle inequality through \(0\), and a projective measurement on a unit vector has summed squared state norm one.

Item 1 expands the squared norms of the transform into a double sum over the family, of which the orthogonality of the characters keeps the diagonal. In item 2, two distinct points lie in a common fibre for a fraction \(1/q\) of the coefficients \((\alpha , \beta )\), so the average is the sum of the squared norms plus \(1/q\) times the off-diagonal sum, which the zero-sum hypothesis makes \(-1/q\) times the diagonal; the formal proof writes the indicator of a fibre as an average of the characters of item 1. Item 3 applies item 2 to the vectors \(\pi (T)\psi \); for the cross-party deviations, the differences of the two families’ operators sum to \(I- I= 0\).

Theorem 3.38 in the model of a commuting-operator strategy, with \(\omega = \omega ^{\mathrm{co}}\). Its first hypothesis, the soundness of the seeded test in every extension of that model by a unit vector, is Lemma 8.95. Its second, that \(\omega ^{\mathrm{co}}\) dominates the POVM strategies of every such extension in every unit state, holds because \(\omega ^{\mathrm{co}}\) dominates the POVM strategies of every model on a Hilbert space with a unit state (Lemma 8.79).

The Pauli basis test is then sound in the commuting-operator model (Lemma 8.99), so both hypotheses of Corollary 8.44 hold.

Let the registers be \(\alpha \) and \(\beta \). The first player’s operators of the extension are the \(X \otimes I_\beta \) for matrices \(X\) over the first player’s operators, and the second player’s the \(I_\alpha \otimes Y\). An operator commuting with every \(I_\alpha \otimes Y\) commutes with the matrix units of the second register and with the amplifications of the second player’s operators, so it is an \(X \otimes I_\beta \) whose entries commute with the second player’s operators (Lemma 8.93), and these entries are the first player’s operators; symmetrically for the second player. If \(g_1, \dots , g_n\) is a vector trace of the first player’s operators, the vectors \(\left\vert {\alpha } \right\vert ^{-1/2}\, g_k \otimes e_i \otimes e_{b_0}\), for \(k \leq n\), \(i \in \alpha \) and a fixed \(b_0 \in \beta \), give \(X \otimes I_\beta \) the normalized trace \(\left\vert {\alpha } \right\vert ^{-1} \sum _i \tau (X_{ii})\). It is tracial because \(\tau \) is, and the family separates because \(X \otimes I_\beta \) kills the vector of \((k, i)\) only if \(X_{ji} g_k = 0\) for every \(j\). Exchanging the players exchanges the conditions.

Each clause is a direct computation. A unital \(*\)-homomorphism preserves products, adjoints, finite sums and the unit. In the opposite ring \(e_{ji}^{\mathrm{op}} e_{ml}^{\mathrm{op}} = (e_{ml} e_{ji})^{\mathrm{op}} = \delta _{jl}\, e_{mi}^{\mathrm{op}}\). Diagonal matrices multiply entrywise, and the adjoint of a diagonal matrix is the diagonal of the adjoints. Products are computed componentwise, which is why the two systems must share an index: indexing dyadic units by \(\{ 0, 1\} ^n\) is what makes the product clause need no reindexing. The full proof is reports/c6b-paper-proofs.md, Section 3, Lemma 5.

\(p_k\) is a projection, \(x_k p_k x_k = 1 - p_k\) by anticommutation, and so \(p_k x_k p_k = x_k (1 - p_k) p_k = 0\). Hence \(u^{(k)}_{ab} u^{(k)}_{cd} = x_k^a\, p_k x_k^{b + c} p_k\, x_k^d\) is \(u^{(k)}_{ad}\) if \(b = c\) and \(0\) otherwise, \((u^{(k)}_{ab})^* = u^{(k)}_{ba}\), and \(u^{(k)}_{00} + u^{(k)}_{11} = p_k + (1 - p_k) = 1\). Units at distinct sites commute, so the relations of the product system follow site by site, by induction on \(n\). The construction is that of reports/c6b-paper-proofs.md, Section 3.8.

The tool is a Cauchy–Schwarz inequality in a commutative corner: for operators \(x, y\) with \(\alpha = x^* x\), \(\beta = y^* y\) and \(\gamma = x^* y\), if \(\alpha \) commutes with \(\beta \) and \(\beta \) with \(\gamma \), then \(\gamma \gamma ^* \leq \alpha \beta \). For \(\varepsilon {\gt} 0\) the operator \(b = \beta + \varepsilon \) is invertible and positive and commutes with \(\alpha \), \(\gamma \) and \(\gamma ^*\); with \(z = x b - y \gamma ^*\), \(b (\alpha b - \gamma \gamma ^*) = z^* z + \varepsilon \gamma \gamma ^* \geq 0\), so \(\alpha b - \gamma \gamma ^* \geq 0\), and \(\varepsilon \to 0\) gives the claim, the positive cone being closed.

For (K1), fix \(i_0 \in \iota \) and put \(w_i = f_{i_0 i}\, p\) and \(a_{ij} = w_i^* w_j = p f_{ij} p\). The \(a_{ij}\) commute pairwise because \(p\) is abelian, \(\sum _i a_{ii} = p\), and \(a_{ij} a_{ij}^* \leq a_{ii} a_{jj}\) by the corner inequality. The operator \(X = \sum _i w_i w_i^*\) is self-adjoint and \(f_{i_0 i_0} X = X = X f_{i_0 i_0}\); by traciality \(\tau (X) = \tau (p)\) and \(\mathrm{Re}\, \tau (X^2) = \sum _{i, j} \mathrm{Re}\, \tau (a_{ij} a_{ij}^*) \leq \mathrm{Re}\, \tau (p)\), and \(\tau (f_{ii}) = \tau (f_{i_0 i_0})\) for every \(i\), so \(\tau (f_{i_0 i_0}) = 1/\left\vert {\iota } \right\vert \). With \(t = \mathrm{Re}\, \tau (p) \geq 0\), the positivity of \((X - c f_{i_0 i_0})^* (X - c f_{i_0 i_0}) = X^2 - 2cX + c^2 f_{i_0 i_0}\) for real \(c\) gives \(0 \leq t - 2ct + c^2/\left\vert {\iota } \right\vert \), and \(c = \left\vert {\iota } \right\vert \, t\) gives \(t (1 - \left\vert {\iota } \right\vert \, t) \geq 0\). For (K2), \(2^n t \leq 1\) for every \(n\), so \(t = 0\); and \(\tau (p) = \tau (p^* p) = \sum _k \| p g_k\| ^2\), so \(p\) kills every \(g_k\) and vanishes, the family separating \(s\). For (K\('\)), the first player’s operators are the image of a \(*\)-homomorphism, hence closed under products and adjoints; they carry the vector trace of the finite pair, and contain the images of the units (Lemma 8.104). The second player’s case is the first for the model with the players exchanged, again a finite pair (Lemma 8.102). No comparison theory and no centre-valued trace is used. The full proof is reports/c6b-paper-proofs.md, Section 3, Theorems K and K\('\) (Lemmas 1–4 and 6).

Exchanging the players exchanges the two conditions. The players’ algebras of an extension are the matrix algebras \(M_\alpha (\mathscr {A}_A)\) and \(M_\beta (\mathscr {A}_B)\) (Definition 8.51), in which the scalar diagonals of the model’s units are units (Lemma 8.104), and the extension is a finite pair (Lemma 8.102). The last claim is Theorem 8.106 on each side. The full proof is reports/c6b-paper-proofs.md, Section 3, Theorem Cl (Lemma 7).

\(\tau (W_g) = 1\) if \(g = 0\) and \(0\) otherwise, so \(\tau (W_g W_h)\) and \(\tau (W_h W_g)\) both vanish unless \(h = g\), where the two products agree: \(\tau \) is tracial on a spanning set, hence on \(\cal {P}\). The vectors \(W_g \delta _0 = \delta _g\) span a dense subspace. \(J\) is an involutive antiunitary with \(J(a \delta _0) = a^* \delta _0\), from which the formula for the right action and its commutation with the left action follow on that dense subspace. Finally \(X_k = W_g\) for \(g\) the pair \((1, 0)\) at site \(k\), and \(Z_k = W_g\) for \((0, 1)\) at site \(k\), are self-adjoint symmetries that anticommute at one site and commute at distinct sites, by the values of \(\omega \); so Lemma 8.105 gives units in \(\cal {P}\) itself, not only after representation. No closure is taken: the interface asks only for a \(*\)-algebra. The candidates and the choice are in reports/c6b-paper-proofs.md, Section 3.8.

For (A): the elements \(1 \otimes f_{ij}\), for units \(f\) of \(\cal {B}\), are unital dyadic matrix units of \(\mathscr {A}\otimes \cal {B}\), the image of those of \(\cal {B}\) under the unital \(*\)-homomorphism \(b \mapsto 1 \otimes b\). The left action maps \(\mathscr {A}\otimes \cal {B}\) into \(\cal {N}\), and the right action maps its opposite algebra into \(\cal {N}'\), both as unital \(*\)-homomorphisms, so both players’ algebras have units (Lemma 8.104). The model is a finite pair: the trace vector is tracial on \(\cal {N}\) and, through the conjugation \(J\) of the standard form, on \(\cal {N}'\), and it separates both, being cyclic for the left and for the right actions. So it is a dyadic pair, and so are its ancilla extensions with nonempty registers, which is how Lemma 8.111 uses it (Lemma 8.108). For (T): \(a \mapsto a \otimes 1\) is a unital \(*\)-homomorphism, so it maps sums of squares to sums of squares and keeps the measurements’ sums equal to \(1\), and the trace of \(\mathscr {A}\otimes \cal {B}\) restricts to that of \(\mathscr {A}\) on \(\mathscr {A}\otimes 1\), since \(\tau (a \otimes b) = \tau (a) \tau (b)\) and \(\tau (1) = 1\); so the normalization of the density and the correlation \(\mathrm{Re}\, \tau (\sigma ^* E^x_a \sigma F^y_b)\) are unchanged. The consequence is the vendored strict form of Lin’s tracial density for game values (Theorem 5.10), followed by (T) and (A). The full proof is reports/c6b-paper-proofs.md, Section 3, Theorems A and T (Lemmas 8 and 9).

If an alphabet is empty, \(\omega ^{\mathrm{co}}(\mathfrak {G}) = 0\) and there is nothing to prove. Otherwise the vendored development’s strict form of Lin’s tracial density for game values gives a tracially embeddable strategy (Theorem 5.10) of winning probability greater than \(t\): a tracial algebra \(\mathscr {A}\) in standard form on \(L^2(\mathscr {A}, \tau )\), a density \(\sigma \), and the two players’ POVMs acting on the left and on the right, in the state \(\iota \sigma \). Amplified by the twisted Pauli algebra (Lemma 8.109), it keeps its winning probability, and its standard-form model — the commutant \(\cal {N}\) of the right action and its commutant \(\cal {N}'\), as the players’ algebras — is a dyadic pair in every state (Lemma 8.110). The left action lies in \(\cal {N}\) and the right action in \(\cal {N}'\), so the strategy is a POVM strategy in this model, of the same value. Each player’s POVMs dilate to projective measurements in the matrices over the player’s algebra, compressed to one basis vector (Lemma 8.77); in the ancilla extension at that basis vector they form a projective strategy of the same value (Lemma 3.66), and the extension is a dyadic pair (Lemma 8.108). Before the amplification the model is only a finite pair, whose algebras may have abelian projections; that is the reason for it (reports/c6b-paper-proofs.md, Section 3.7).

\(\omega ^{\mathrm{co}}\) is then approached by projective strategies in dyadic pairs, where the test is sound, and it dominates every model on a Hilbert space (Lemma 8.64). So Theorem 8.67 applies.

Theorem 3.38 applies in each dyadic pair approaching \(\omega ^{\mathrm{co}}\), with \(\omega = \omega ^{\mathrm{co}}\). Its first hypothesis holds because an extension of a dyadic pair by a unit vector has nonempty registers and so is a dyadic pair (Lemma 8.108), in which the seeded test is sound. Its second holds because \(\omega ^{\mathrm{co}}\) dominates the POVM strategies of every model on a Hilbert space in a unit state (Lemma 8.79).

\(\omega ^{\mathrm{co}}\) is approached in dyadic pairs (Lemma 8.111). Introspection is sound in \(\omega ^{\mathrm{co}}\) as soon as \(\omega ^{\mathrm{co}}\) is approached by projective strategies of models in which the Pauli basis test is sound (Theorem 8.84), which Lemma 8.114 then provides. Answer reduction is sound in \(\omega ^{\mathrm{co}}\) by Theorem 8.113, and parallel repetition is (Theorem 8.56). So the compression of Corollary 8.44 is sound in \(\omega ^{\mathrm{co}}\), which gives \(\mathrm{MIP}^{\mathrm{co}}= \mathrm{coRE}\).

The first player’s operators are the commutant of the second player’s, so they form a von Neumann algebra, with no bicommutant theorem; the vector trace of the finite pair is a faithful tracial vector functional on it, and the model’s state is a vector state. Theorem 3.8 applies, and its projective measurement, which lies in the first player’s operators, pulls back to the first player’s algebra by injectivity.

Neither player’s operators contain a nonzero abelian projection (Lemma 8.108), so Corollary 8.116 applies to the first player, and to the second in the model with the players exchanged, which is again a dyadic pair. This is the form the orthonormalization sites of the port call, with no hypothesis beyond the class (reports/c6b-paper-proofs.md, Section 3.7).

\(J\) is isometric and fixes \(\Psi \), so \(\langle \Psi , J X J \Psi \rangle = \langle J \Psi , J X \Psi \rangle = \langle \Psi , X \Psi \rangle \). The flip carries \(L(x)\) to \(R(x)\) by definition, and \(R(x)\) to \(L(x)\) because \(J^2 = 1\); so it carries \(L(x)\, R(y)\) to \(R(x)\, L(y)\), which is \(L(y)\, R(x)\) because the two placements commute. The vendored development takes these facts as hypotheses of a symmetric strategy — the swap fixes the state’s density, and the state is permutation invariant — and here they are theorems of the model, so the ported statements drop those hypotheses (planning/c6b-plan.md, “Port conventions”).

The proof is the vendored one, MIPStarRE.LDT.CommutativityPoints.commutativityPoints in MIPRE/Background/LIDT/MIPStarRE/LDT/CommutativityPoints/, rewritten over the symmetric model declaration by declaration (planning/c6b-plan.md, milestone M1 and “Port conventions”). A uniformly random pair of points has the law of two points sampled on a random diagonal line, so it suffices to compare the two orders of the product for points \(u\) and \(v\) on a shared diagonal line \(\ell \). By the diagonal-line test, the point measurement \(A^u\) placed by \(L\) is within \(2 \gamma m\), in averaged squared state-dependent distance, of the line measurement of \(\ell \) evaluated at \(u\) and placed by \(R\). Multiplying such an approximation by a family \(C\) with \(\sum _c C_c^* C_c \leq 1\) keeps its error, so four replacements carry \(L(A^u_a A^v_b)\) to the product of the line measurement’s two evaluations, placed by \(R\), and from there to \(L(A^v_b A^u_a)\); the two evaluations commute, being post-processings of one projective measurement. The triangle inequality for the squared distance loses a factor \(2\), which gives \(2 (2 \gamma m + 2 \gamma m) = 8 \gamma m\) for each half and \(2 (8 \gamma m + 8 \gamma m) = 32 \gamma m\) in all. The Cauchy–Schwarz inequalities behind these steps are those of the vector state read as a state model (Definition 8.49). The flip of the model is never used. The answer-valued variant has the same proof; it is ported as a separate statement, as the vendored development states it and its consumers use it.

The first player’s operators commute with the second player’s and with their adjoints, so they lie in \(\cal {A}_c\). The commutant clause of a finite pair says that an operator commuting with the second player’s operators is one of the first player’s, so they are all of \(\cal {A}_c\); and the representation is injective, so \(a \mapsto \pi (\pi _A(a))\) is bijective onto \(\cal {A}_c\). A commutant is norm closed, and it is star-ordered because a positive element of it is the square of its square root, which commutes with everything the element commutes with. A \(*\)-homomorphism between star-ordered rings is monotone, and both the isomorphism and its inverse are \(*\)-homomorphisms, so the two orders agree (reports/c6b-paper-proofs.md, Section 5.6, Lemma 13). The second player’s statements are the first player’s for the model with the players exchanged.

An operator on \(\mathcal{H}\oplus \mathcal{H}\) that commutes with \(R(0, 1) = 1 \oplus 0\) is block diagonal. Its first block commutes with \(\cal {B}_c\), so it lies in \(\cal {A}_c\), and its second block lies in \(\cal {B}_c\) in the same way. So an operator commuting with every \(R(y)\) is an \(L(x)\), and symmetrically. The trace vectors are \((g_k, 0)/\sqrt{2}\) and \((0, h_l)/\sqrt{2}\), for the trace vectors \(g_k\) of \(\tau \) and \(h_l\) of \(\sigma \). Traciality and separation hold blockwise. A block-diagonal operator is positive exactly when each block is, which gives item 2 together with Lemma 8.121. The dyadic matrix units of \(\cal {A}\) and of \(\cal {B}\) transfer to \(\cal {A}_c\) and \(\cal {B}_c\), and pair componentwise into units of \(\cal {P}\). For item 4, \(L\) is an injective \(*\)-homomorphism of C\(^*\)-algebras, so it preserves spectra and commutes with the functional calculus. The first player’s operators of \(M\) are a closed commutant, which contains the functional calculus of each of its self-adjoint elements (reports/c6b-paper-proofs.md, Section 4, Theorem A and Proposition H).

\(L(x) R(y) = x^1 y^2 \oplus y^1 x^2\), because \(y^1 \in \cal {A}_c\) and \(x^2 \in \cal {B}_c\) commute. The vector state \(\Psi = (\psi , \psi )/\sqrt{2}\) averages the two blocks. In the defect the maximum with \(0\) is inactive on both sides, since the summands are Born probabilities of positive elements, so the defect is the sum of the off-diagonal Born probabilities, and that sum halves too. The two defects of \(M\) are nonnegative and average to at most \(\sigma \), so each is at most \(2\sigma \) (reports/c6b-paper-proofs.md, Section 4, Theorems C and E).

The players’ operators of \(D(M)\) are the block-diagonal operators \(u \oplus v\) with \(u\) and \(v\) in the players’ operators of \(M\) (Lemma 8.123). A projection \(p \oplus q\) there is abelian exactly when \(p\) and \(q\) are, since its corner is the product of theirs. For a dyadic pair, neither player’s operators contain a nonzero abelian projection (Lemma 8.108) (reports/c6b-paper-proofs.md, Section 4, Theorem F).

Each failure probability of \(S_D\) is a bipartite consistency defect of \(D(M)\) between two paired families, so it is the average of the two two-space defects of \(M\) (Lemma 8.124). The paired families have the families of \(S\) as components. The failure probability of \(S\) is the mean of the three role averages, which are nonnegative, so each is at most \(3\varepsilon \) (reports/c6b-paper-proofs.md, Section 4, Theorem D).

Complete \(X\) to a positive operator valued measurement by one further outcome, \(1 - X_{\mathrm{total}}\). In any symmetric model, \(1 - \sum _o \| L(\tilde X_o) \Psi \| ^2\) for the completion \(\tilde X\) is at most twice the defect of \(X\), using \(\| R(y) \Psi \| = \| L(y) \Psi \| \) and the Cauchy–Schwarz inequality for \(\langle \Psi , L(y) R(y) \Psi \rangle \); so it is less than \(3 \min (\eta , 1)\). The doubled model is a finite pair without abelian projections (Lemmas 8.123 and 8.125), so Corollary 8.116 gives a projective measurement \(Q\) of the first player’s algebra of \(D(M)\) within \(9 \cdot 3 \min (\eta , 1)\) of \(\tilde X\). Dropping the added outcome gives \(P\), and \(27 \min (\eta , 1) \leq 100 \eta ^{1/4}\) (reports/c6b-paper-proofs.md, Section 4, Theorem G). The case \(\eta = 0\) is excluded because the hypothesis of Corollary 8.116 is strict.

The measurements of \(\cal {M}\) form a weak-operator compact set, and \(f(T) = \sum _i \mathrm{Re}\, \tau (T_i A_i)\) is weak-operator continuous, being a finite sum of matrix coefficients. So \(f\) has a maximizer \(T\). Perturbing \(T\) toward a single outcome \(h\) by \(T'_i = K T_i K + \delta _{ih}(1 - K^2)\), with \(K = 1 - \varepsilon P\) for \(0 \leq P \leq 1\) in \(\cal {M}\), expands \(f(T')\) exactly to second order in \(\varepsilon \). Maximality then gives the first-order condition \(\mathrm{Re}\, \tau (P A_h) \leq \mathrm{Re}\, \tau (P Z)\) for all such \(P\). Let \(W = \frac{1}{2}(Z + Z^*)\), and let \(N\) be the negative part of \(W - A_h\), which lies in \(\cal {M}\). The condition at \(P = N / (1 + \| N\| )\) gives \(\mathrm{Re}\, \tau (N^2) \leq 0\), since \(N (W - A_h) = -N^2\); so \(N = 0\) by faithfulness, and \(A_h \leq W\). Then \(\mathrm{Re}\, \tau (T_h (W - A_h)) \geq 0\) for every \(h\), with sum \(\mathrm{Re}\, \tau (W - Z) = 0\), and faithfulness of \(\tau \) makes each product vanish: \(W T_h = A_h T_h\). Summing over \(h\) gives \(W = Z^*\), hence \(Z = W\) (reports/c6b-paper-proofs.md, Section 5, Theorem 10 and Corollary 11). The weak-operator compactness of the unit ball is that of the vendored orthonormalization development.

In a product with componentwise operations and order, the summed form holds exactly when it holds in each factor. Theorem 8.128 solves it in \(\cal {A}_c\) and in \(\cal {B}_c\), and the pair of solutions solves it in \(\cal {P}\), with \(Z = \sum _i T_i A_i\). A \(*\)-homomorphism between star-ordered rings that preserves and reflects nonnegativity is injective and an order embedding, so it carries the summed form both ways. This applies to \(L\) and \(R\) (Lemma 8.123) and to the isomorphisms of Lemma 8.121 (reports/c6b-paper-proofs.md, Section 5, Corollary 12 and Lemma 13). Neither a trace on the doubled algebra nor its commutant is used.

The proofs are the vendored ones, in MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/, rewritten over the symmetric model declaration by declaration (planning/c6b-plan.md, milestone M3 and “Port conventions”). Each estimate is a Cauchy–Schwarz inequality for the vector state read as a state model (Definition 8.49), \(|\mathrm{ev}(X^* Y)|^2 \leq \mathrm{ev}(X^* X)\, \mathrm{ev}(Y^* Y)\), applied question by question and averaged with \(\mathop{\mathbb {E}}_x \sqrt{f} \leq \sqrt{\mathop{\mathbb {E}}_x f}\), which needs the total weight to be at most \(1\). The Kronecker identities of the vendored proofs are the commutation of \(L(x)\) with \(R(y)\) and the multiplicativity of \(L\) and \(R\). Swap symmetry enters items 2 and 3 through \(\mathrm{ev}(L(x)) = \mathrm{ev}(R(x))\) (Lemma 8.119): it expands \(\| (L(x) - R(x)) \Psi \| ^2 = 2 (\mathrm{ev}(L(x^2)) - \mathrm{ev}(L(x)\, R(x)))\) for self-adjoint \(x\). The vendored statements assume it, with the normalization of the state; here both are theorems of the model.

The vendored proof, MIPStarRE.LDT.ExpansionHypercubeGraph.localToGlobal, realizes the family as a block matrix and traces the scalar inequality \(g P_\perp \leq \Delta \) against the state’s density, where \(\Delta \) is the Laplacian of the hypercube graph, \(P_\perp \) the projection onto the vectors of mean zero and \(g = 1/(m q^m)\) its spectral gap. A vector state has no density; here the inequality is read through Gram positivity instead. For a positive semidefinite scalar matrix \(Q\) indexed by the points, \(\mathrm{Re} \sum _{u, v} Q_{u v} \langle A^v \Psi , A^u \Psi \rangle \geq 0\), because \(Q\) is a sum of matrices \(s^* s\), for which the sum is \(\sum _k \| \sum _u s_{k u} A^u \Psi \| ^2\). At \(Q = \Delta - g P_\perp \), which is positive semidefinite (the scalar spectral estimate, imported from the vendored development), this reads \(g \cdot q^m V_{\mathrm{glob}} \leq V_{\mathrm{loc}}\): the sum at \(\Delta \) is the local variance \(V_{\mathrm{loc}}\), the sum at \(P_\perp \) is \(\sum _u \| (A^u - \mathop{\mathbb {E}}_v A^v) \Psi \| ^2 = q^m V_{\mathrm{glob}}\), and \(g q^m = 1/m\) (planning/c6b-plan.md, milestone M5). The expectations are those of the vector state read as a state model (Definition 8.49). The matrix realization of the vendored development is not ported.

The proof is the vendored one, MIPStarRE.LDT.Test.mainFormalStep5_selfConsistency_ofExpansionBound in MIPRE/Background/LIDT/MIPStarRE/LDT/Test/SchwartzZippelStep.lean, rewritten over the symmetric model (planning/c6b-plan.md, milestone M4). Evaluating at \(u\) leaves the totals unchanged and adds to the matched mass the pairs \(g \neq h\) with \(g(u) = h(u)\), so

Two distinct polynomials of individual degree at most \(d\) in \(m\) variables agree on at most a fraction \(md/q\) of the points, by the Schwartz–Zippel bound of the vendored classical layer, which is imported; and the \(\mathrm{ev}(L(G_g)\, R(H_h))\) are nonnegative, \(L(G_g)\) and \(R(H_h)\) being commuting positive operators, with sum at most \(1\). The definitions ported with this step (the restricted strategies of the main induction step, the slice families with their completeness, consistency, strong self-consistency and boundedness, and the statements of the induction step) are definitions, without proofs.

The proof is the vendored one, MIPStarRE.LDT.GlobalVariance.globalVarianceOfPoints in MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/, rewritten over the symmetric model (planning/c6b-plan.md, milestone M6). Six comparisons carry \(W^u_g\) to \(W^v_g\) along an edge, each an averaged squared distance: the self-consistency test (\(2\delta \)), the axis-parallel test (\(2\varepsilon \)), the Schwartz–Zippel bound for the line through \(u\) and \(v\) (\(md/q\), twice), and the first two undone at \(v\) (\(2\varepsilon \), \(2\delta \)); the triangle inequality for six steps loses a factor \(6\). The global bound is Lemma 8.131 for the family \(u \mapsto W^u_g\), which costs the factor \(m\), with \(6 (4\varepsilon + 4\delta + 2md/q) \leq 24 (\varepsilon + \delta + md/q)\). The vendored proof evaluates these variances on the weighted state \(R(\sqrt{G_g})\, \rho \, R(\sqrt{G_g})\), which is not normalized; a vector state has no density, so here they are the variances of the weighted family on \(\Psi \) itself, the same numbers. The consistency relations are used in both orders, which in a symmetric model is a theorem (Lemma 8.119).

The proof is the vendored one, MIPStarRE.LDT.Commutativity.comMain in MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/, rewritten over the symmetric model (planning/c6b-plan.md, milestone M7). It first bounds the commutators of the evaluated slice measurements \(G^x_{[g(u) = a]}\) and \(G^y_{[h(v) = b]}\), on average over two points \((u, x)\) and \((v, y)\), by \(48\, m (\gamma ^{1/2} + \eta ^{1/2})\): a chain of comparisons, each a Cauchy–Schwarz estimate for the vector state, inserts the point measurements next to the slice measurements by consistency, exchanges the two points by the commutativity of points (Lemma 8.120) and removes them again, the boundedness controlling the mass that \(G^x\) loses. It then passes from the evaluated to the full slice measurements: two distinct polynomials agree at a random point with probability at most \(md/q\), so the evaluation loses at most that collision mass, and the closeness estimates of Lemma 8.130 turn the bound into the displayed one, with its fourth roots. Where the vendored proof uses the permutation invariance of the state, the port uses \(\mathrm{ev}(L(x)) = \mathrm{ev}(R(x))\) (Lemma 8.119).

The vendored proof, in MIPRE/Background/LIDT/MIPStarRE/LDT/MakingMeasurementsProjective/, passes from consistency to an almost projective measurement and rounds that to a projective one in finite dimension, through a Naimark dilation, a spectral truncation and a reduction of rank. The first half is ported (planning/c6b-plan.md, milestone M8): by the Cauchy–Schwarz inequality for the vector state, \(\mathrm{cons}(A, B) \leq \eta \) gives \(1 - \sum _a \| L(A_a) \Psi \| ^2 \leq 2 \eta \), which is less than \(3 \min (\eta , 1)\). The second half is replaced: Corollary 8.116, applied to \(A\), gives a projective measurement \(P\) with \(\sum _a \| L(A_a - P_a) \Psi \| ^2 {\lt} 27 \min (\eta , 1) \leq 84\, \eta ^{1/4}\), which is item 1. Item 2 is Theorem 8.127, in the form stated there for any symmetric model whose bipartite reading is such a finite pair. Item 3 is the same estimate in the two-space model, where Corollary 8.117 applies to either player with no further hypothesis, and \(27 \min (\eta , 1) \leq 100\, \eta ^{1/4}\). The case \(\eta = 0\) is excluded because the hypothesis of Corollary 8.116 is strict.