Let \((\mathscr {A}, \tau , M)\) be a commuting strategy (Definition 2.5) and let \(\mathcal{H}\) be the completion of \(\mathscr {A}\) for the semi-inner product \(\langle a, b \rangle = \tau (a^* b)\), with the class of \(1\) as the unit vector \(\xi \). A tracial state is Hermitian, \(\tau (a^*) = \overline{\tau (a)}\), by polarization of its positivity at \(1 + a\) and \(1 + ia\). Left multiplication \(\pi (p) : b \mapsto pb\) and right multiplication \(\rho (p) : b \mapsto bp\) by a projection \(p\) are contractions for the semi-norm, hence extend to \(\mathcal{H}\). For \(\rho \) this uses the trace: \(\tau ((bp)^*(bp)) = \tau (b^* b p)\) and \(\tau (b^* b) - \tau (b^* b p) = \tau ((b(1-p))^*(b(1-p))) \geq 0\). Both are symmetric and positive for the form; for \(\rho \), \(\tau ((bp)^* c) = \tau (b^* c p)\) and \(\tau (b^* b p) = \tau ((bp)^*(bp))\). Left and right multiplications commute, by associativity, and each family sums to the identity. Setting \(E^x_a = \pi (M^x_a)\) and \(F^y_b = \rho (M^y_b)\) gives a commuting-operator strategy with \(\langle \xi | E^x_a F^y_b |\xi \rangle = \tau (1^* M^x_a M^y_b) = \tau (M^x_a M^y_b)\), hence with the same value as \((\mathscr {A}, \tau , M)\). Taking suprema yields the claim. No norm on \(\mathscr {A}\) is used.

This is the main theorem of  [ 32 ] (Theorem 7.1 there), whose Lean proof is vendored at MIPRE/Background/Repetition/CommutingRepetition/. The bridge identifies a game of Definition 2.1 with the game of the vendored development having the \(\{ 0, 1\} \)-valued payoff \(D\), a commuting-operator strategy of Definition 5.2 with a strategy of the vendored development (field by field, so that the two suprema defining the value range over the same set of numbers), and the two direct repetitions with each other. When \(\varepsilon = 0\) and \(\left\vert {\mathcal{A}} \right\vert = \left\vert {\mathcal{B}} \right\vert = 1\) the formalization reads the quotient as \(0\) and the bound is trivial.

This is the main theorem of Chapter 6 of  [ 31 ] , whose Lean proof is vendored at MIPRE/Background/Repetition/TenProofs/. Its entangled value is defined with a density matrix on the product of two finite sets and POVMs; Lemma 5.7 identifies it with \(\mathrm{val}^*\) (Definition 2.9), after which the two direct repetitions are literally the same construction.

A tensor-product strategy (Definition 2.3) is a strategy of the second kind, with \(S_\textsc{A}= \{ 1, \ldots , d_\textsc{A}\} \), \(S_\textsc{B}= \{ 1, \ldots , d_\textsc{B}\} \), \(\rho = |\psi \rangle \langle \psi |\) and projective measurements, which gives \(\mathrm{val}^*\leq \mathrm{val}^*_{\mathrm{POVM}}\).

Conversely, given a strategy of the second kind, purify \(\rho \) on a reference system placed on Bob’s side, where Bob’s effects act as \(B^y_b \otimes I\), so that the bipartite structure survives; then dilate the two POVM families to projective measurements on one extra register each, and reindex the two finite sets by initial segments of \(\mathbb {N}\). Neither step changes an outcome probability, so the result is a tensor-product strategy of the same value.

The dilation is the only delicate point, and the reason is that the shared state may not depend on the questions while the dilating isometry does. Writing \(A^x_a = (K^x_a)^\dagger K^x_a\), the isometry \(V_x : v \mapsto \sum _a (K^x_a v) \otimes |a\rangle \) satisfies \(V_x^\dagger (I\otimes |a\rangle \langle a|) V_x = A^x_a\); extending each \(V_x\) to a unitary \(U_x\) of \(\mathbb {C}^{S_\textsc{A}} \otimes \mathbb {C}^{\mathcal{A}}\) and setting \(P^x_a := U_x^\dagger (I\otimes |a\rangle \langle a|) U_x\) gives projective measurements all of which are compressed back to the POVMs by the same, question-independent isometry \(v \mapsto v \otimes |a_0\rangle \), so that the single state \(|\psi \rangle \otimes |a_0\rangle \otimes |b_0\rangle \) works for every question. In Lean the extension is Mathlib’s completion of an orthonormal family to an orthonormal basis, and only the factorization \(A^x_a = (K^x_a)^\dagger K^x_a\) is used, not a matrix square root, which Mathlib does not have. The nonemptiness of \(\mathcal{A}\) and \(\mathcal{B}\) needed to choose \(a_0\) and \(b_0\) is derived, not assumed: \(\mu \) is a probability distribution, so some question is asked, and a POVM on a space carrying a state has a nonempty outcome set.

The normalized trace on \(\mathbb {C}^{d^k}\) of a tensor product is the product of the normalized traces on \(\mathbb {C}^d\) (the trace of a product of two projections being real), and the distribution and predicate of \(\mathfrak {G}^{k}\) are products, so each summand of the value of \(\mathscr {S}^{\otimes k}\) is the product over the coordinates of the corresponding summands of the value of \(\mathscr {S}\), and the sum over \(k\)-tuples of questions and answers is the \(k\)-th power of the sum. Commutation is coordinatewise, on the support of the product distribution, which is the product of the supports. For the doubled reading, the strategy on the doubled repetition is the tensor power relabeled along \((t, \bar{x}) \mapsto ((t, x_i))_i\), which is injective and covers the support of the doubled repeated distribution.

Theorem 5.6 at \(\varepsilon ' = 1 - \mathrm{val}^*(\mathfrak {G}) \geq \varepsilon \): there are at most \(3^{B+1}\) strings of length at most \(B\), so \(\log (\left\vert {\mathcal{A}} \right\vert \left\vert {\mathcal{B}} \right\vert ) \leq 2(B + 1) \log 3\), and \(\varepsilon ' \leq 1 \leq B + 1\), so the denominator is at most \((B + 1)(1 + 2 \log 3)\); the exponent is monotone in the gap, so the bound at \(\varepsilon '\) implies the one at \(\varepsilon \). Take \(c' = c / (1 + 2 \log 3)\). This is the form in which the soundness clause of Theorem 6.196 consumes the theorem.

This is Theorem 3.2 of  [ 12 ] , as formalized in  [ 32 ] (the density programme of the vendored development, Tracial/Density/Main.lean). The statement above is that of the vendored development, in its own vocabulary — its tracially embeddable correlations have the shape of Lin’s Definition 3.1, with Bob’s measurement taken in the commutant of the left action; restating it through the definitions of Section 2 is pending.