Dependencies

If the Aldous–Lyons conjecture holds, the sofic value is approximable.

A tailored answer reduction at input level \(5\) refutes the Aldous–Lyons conjecture.

The sofic value of subgroup tests is not approximable, and the Aldous–Lyons conjecture is false.

There is a separable II\(_1\) factor that does not embed into an ultrapower \(\cal {R}^{\omega }\) of the hyperfinite II\(_1\) factor.

From an inhabitant of MIPRE.AnswerReduction 5 alone there is a MIPRE.GapCompression, and consequently Theorem 7.1, Corollary 7.3, Corollary 7.4 and Theorem 7.6 hold with no other hypothesis.

Assume an ambient MIPRE.GapCompression. On the map of Theorem 6.214, the quantum value of the game is also \(1\) when the machine halts on the empty input and at most \(\tfrac 12\) when it does not. Consequently no computable function separates game descriptions of value \(1\) from those of value at most \(\tfrac 12\), for the synchronous value or for the quantum value; every recursively enumerable language is in \(\mathrm{MIP}^*\); and \(\mathrm{MIP}^*= \mathrm{RE}\).

With \(g\) as in Theorem 7.1: if \(\cal {M}\) halts on the empty input then \(\mathrm{val}^*(\mathfrak {G}_{g(\cal {M})}) = 1\), and if \(\cal {M}\) does not halt on the empty input then \(\mathrm{val}^*(\mathfrak {G}_{g(\cal {M})}) \leq \tfrac 12\).

If the seeded CL test is sound in the commuting-operator model (Definition 8.65), then \(\mathrm{MIP}^{\mathrm{co}}= \mathrm{coRE}\).

If the seeded CL test is sound in dyadic pairs (Definition 8.112), then the compression of Corollary 8.44 is sound in \(\omega ^{\mathrm{co}}\) (Definition 8.38), and \(\mathrm{MIP}^{\mathrm{co}}= \mathrm{coRE}\).

If the Pauli basis test is sound in the commuting-operator model (Definition 8.82) and the seeded CL test is sound in the commuting-operator model (Definition 8.65), then \(\mathrm{MIP}^{\mathrm{co}}= \mathrm{coRE}\). The first hypothesis follows from the second (Lemma 8.99), so the second suffices (Corollary 8.100).

Let \(\delta {\gt} 0\), let \(\{ Q_a\} \) be a POVM on \(\mathcal{H}_\textsc{A}\) and \(\{ R_a\} \) a POVM on \(\mathcal{H}_\textsc{B}\) whose inconsistency on the unit vector \(|\psi \rangle \) is at most \(\delta \). Then there is a projective measurement \(\{ P_a\} \) on \(\mathcal{H}_\textsc{A}\) with

that is, \(P_a \otimes I\approx _{\eta _{ortho}(\delta )} Q_a \otimes I\) on \(|\psi \rangle \) with \(\eta _{ortho}(\delta ) = 18\delta \), linear in \(\delta \) as Theorem 3.5 permits.

Let \(M\) be a dyadic pair (Definition 8.107) in a unit state \(\psi \). A POVM \(P\) of either player’s algebra with \(\sum _a \| \pi (P_a)\psi \| ^2 {\gt} 1 - \varepsilon \) is within \(\sum _a \| \pi (P_a - Q_a)\psi \| ^2 {\lt} 9\varepsilon \) of a projective measurement \(Q\) of that algebra.

Let \(M\) be a finite pair (Definition 8.101) in a unit state \(\psi \) whose first player’s operators contain no nonzero abelian projection. A POVM \(P\) of the first player’s algebra with \(\sum _a \| \pi (P_a)\psi \| ^2 {\gt} 1 - \varepsilon \) is within \(\sum _a \| \pi (P_a - Q_a)\psi \| ^2 {\lt} 9\varepsilon \) of a projective measurement \(Q\) of that algebra. The second player’s version is the same statement for the model with the players exchanged.

Let \(q = 2^k\), let \(\{ e_1, \ldots , e_k\} \) be a self-dual basis of \(\mathbb {F}_q\) over \(\mathbb {F}_2\), and let \(\phi : \mathbb {F}_q^M \to \mathbb {F}_2^{M \times k}\) be the relabelling of Lemma 2.36. Then Corollary 3.39 holds with the same \(\delta _{qld}\) and with the register \((\mathbb {C}^q)^{\otimes M}\) read as \(M k\) qubits: the local isometry maps into the register model on \(\mathbb {F}_2^{M \times k}\), item 1 compares with \(|\textsc{EPR}_2\rangle ^{\otimes Mk} \otimes |\textsc{aux}\rangle \), and in item 2 the honest measurement at the outcome \(\phi (u)\), for the genuine answer \(u\), is the qubit Pauli \(X\) measurement \(\sigma ^X_{\phi (u)}\) for the first player and the computational-basis measurement \(\sigma ^Z_{\phi (u)}\) for the second. Indexed by the qubit label \(x \in \mathbb {F}_2^{M \times k}\), the element of the strategy’s measurement compared with the honest one at \(x\) is its element at the valid answer \(\phi ^{-1}(x)\), the Pauli answer that the binary introspection game reads as \(x\); this conclusion in binary coordinates is the form Lemma 6.115 consumes. The Lean proves it for a projective strategy in any bipartite model, the relabelling acting on the register of the ancilla model’s register model after the local isometry; the statement above is its tensor-product instance.

In the setting of Theorem 3.38, suppose in addition that the strategy’s measurements for the questions \((\textsc{Pauli}, W)\) are supported on correctly formatted answers: for both players and both bases, the measurement has no element at an answer that is not of the form \(h \in \mathbb {F}_q^M\). Then for the first player’s \(X\) measurement and the second player’s \(Z\) measurement, the two that introspection uses, item 2 holds with the sum over \(h \in \mathbb {F}_q^M\) taken at the answer \(h\) itself rather than over every answer the game reads as \(h\), with the same local isometry, the same ancilla model and the same \(\delta _{qld}\). The constants \(a\), \(b\) of \(\delta _{qld}\) are fixed once, before the parameters, and at every \(\varepsilon \geq 0\) the error is \(\delta _{qld}(\varepsilon , m, d, q)\). The support hypothesis holds for the restriction to the Pauli basis test (Lemma 6.114) of a strategy of the parsed introspection game whose measurements at the Pauli questions have nonzero elements only at genuine full-register answers. The Lean proves it for a projective strategy in any bipartite model in which the Pauli basis test is sound (Definition 8.82); the statement above is its tensor-product instance.

Kirchberg’s QWEP conjecture fails: there is a C\(^*\)-algebra that is not a quotient of a C\(^*\)-algebra with the weak expectation property; equivalently, \(C^*(F_2) \otimes _{\min } C^*(F_2) \neq C^*(F_2) \otimes _{\max } C^*(F_2)\).

For every test, \(\mathrm{val}_{\mathrm{sof}}(T) \leq \mathrm{val}_{\mathrm{erg}}(T)\), and if the Aldous–Lyons conjecture holds they are equal.

A halting reduction to tailored games makes the sofic value of subgroup tests not approximable; in particular a tailored answer reduction at input level \(5\) does.

Let \(M\) be a finite pair in a unit state, with doubled model \(D(M)\) (Definition 8.122). For self-adjoint \(A_1, \dots , A_m\) in its local algebra \(\cal {P}\) there is a measurement \(T\) in \(\cal {P}\) such that \(Z = \sum _i T_i A_i\) satisfies items 1–3 of Theorem 8.128 in \(\cal {P}\), and so do the images of \(A\), \(T\) and \(Z\) under each placement \(L\) and \(R\). When \(\cal {A}\) and \(\cal {B}\) are star-ordered, the summed form transfers in both directions between \(\cal {A}\) and \(\cal {A}_c\), between \(\cal {B}\) and \(\cal {B}_c\), and between \(\cal {A} \times \cal {B}\) and \(\cal {P}\). So the conclusion of Theorem 8.128 holds in \(\cal {A}\), in \(\cal {B}\) and in \(\cal {A} \times \cal {B}\) themselves.

Let \(\mathfrak {G}\) be a symmetric game with common question marginal \(\nu \), let \(\mathcal{Y}\) and \(\mathcal{B}\) be finite non-empty auxiliary sets, let \(p\) be a distribution on \(\mathcal{X}\times \mathcal{Y}\), and let \(R \geq 1\) satisfy

For each \((x,y)\) let the sets \(g_{xy}(a) \subseteq \mathcal{B}\), \(a \in \mathcal{A}\), be pairwise disjoint (not necessarily exhaustive), and for a POVM \(N^y\) write \(N^y_{g_{xy}(a)} = \sum _{b \in g_{xy}(a)} N^y_b\). Let \(\kappa : [0,1] \to \mathbb {R}_{\geq 0}\) be convex and non-decreasing, and suppose that every symmetric projective maximally entangled (PME) strategy \(T = (|\Phi \rangle , Q)\) for \(\mathfrak {G}\) (so \(|\Phi \rangle \) is maximally entangled), of value \(\omega (T)\), admits complete auxiliary POVMs \(N^y\) with

Then there are universal constants \(C_0, c_0 {\gt} 0\) — supplied by the squared-distance decomposition behind Theorem 3.3 — such that, writing \(e(\delta ) = C_0 \delta ^{c_0}\) and \(s(\delta ) = 2\sqrt{2\delta } + 8\sqrt{e(\delta )}\), every symmetric projective strategy \(\mathscr {S}= (|\psi \rangle , A)\) of value \(\omega \) and synchronicity defect \(\delta = 1 - \mathop{\mathbb {E}}_{x \sim \nu } \sum _a \langle \psi | A^x_a \otimes (A^x_a)^{\mathsf{T}} |\psi \rangle \) admits complete auxiliary POVMs \(M^y\) on its own Bob space with

Two parts of the hypothesis are load-bearing and easy to lose. Symmetric means the Schmidt form \(|\psi \rangle = \sum _j \sqrt{r_j} |j\rangle |j\rangle \) with \(r_j \geq 0\) and Bob’s game measurements the transposes of Alice’s; swap symmetry alone is not a sufficient input. And the conclusion delivers a POVM: it asserts no projectivity, so a consumer needing projective operators must project separately, at its own cost. The Lean proof does not use this corollary, for the reason given at Theorem 3.3.

An answer reduction at input level \(5\) (Definition 9.44) gives a tailored gap compression at level \(7\), hence the halting reduction to tailored games of Definition 9.20 and \(\mathrm{TMIP}^* = \mathrm{RE}\).

There exist finite question and answer sets for which the closure \(C_{qa}\) of the set of finite-dimensional quantum correlations is strictly contained in the set \(C_{qc}\) of commuting-operator correlations.

There is no algorithm that, given a game description \(g\) with the promise that \(\mathrm{val}^{s}(\mathfrak {G}_g) = 1\) or \(\mathrm{val}^{s}(\mathfrak {G}_g) \leq \frac12\), decides which is the case; the same holds with \(\mathrm{val}^*\) in place of \(\mathrm{val}^{s}\) (Corollary 7.3).

The space \(\mathrm{Sub}(F)\) of subgroups of the free group on \(s\) generators is a closed subspace of \(\{ 0,1\} ^F\) with the product topology. An invariant random subgroup is a Borel probability measure on it invariant under conjugation; the finitely described ones are the measures \(\Phi (\sigma )\) of finite actions. The Aldous–Lyons conjecture asserts that for every \(s\) the finitely described IRSs are weak-\(*\) dense in the IRSs.

Let \((\mathcal{H}, \psi , \mathscr {A}, \mathscr {A}_A, \mathscr {A}_B)\) be a bipartite model, \(\alpha \) and \(\beta \) finite sets and \(e \in \mathbb {C}^{\alpha \times \beta }\). The ancilla extension of the model by \(e\) has the Hilbert space \(\mathcal{H}\otimes \mathbb {C}^{\alpha \times \beta }\), the \(\ell ^2\)-sum of \(\alpha \times \beta \) copies of \(\mathcal{H}\); the state \(\psi \otimes e\); the algebra \(M_{\alpha \times \beta }(\mathscr {A})\), acting entrywise; the first player’s algebra \(M_\alpha (\mathscr {A}_A)\), acting as \(X \otimes I_\beta \); and the second player’s algebra \(M_\beta (\mathscr {A}_B)\), acting as \(I_\alpha \otimes Y\). For \(X \in \mathscr {A}_A\) and \(P \in M_\alpha (\mathbb {C})\), \(X \otimes P \in M_\alpha (\mathscr {A}_A)\) is the matrix with entries \(P_{ab} X\), and likewise for the second player.

The structure MIPRE.AnswerReduction is an ambient contract, parametrized by \(\ell \), its output at \(\max \{ \ell + 2, 5\} \) levels. The hypotheses on the input are the budget AnswerReduction.inBudget: sampler and decider runtime coefficients at most \((\lambda n + 1)^\mu \) and \(2^{(\lambda n + 1)^\mu }\), respectively, both at input-size degree \(\mu \), questions of dimension at most the sampler’s bound and answers rejected beyond the decider’s, together with \(\left\vert {\mathcal{D}} \right\vert \leq \sigma \). The complexity clause asks \(\left\vert {\mathcal{S}} \right\vert \leq \sigma \) as well: the output runs the input sampler through the universal machine, whose overhead is polynomial in the size of the program it simulates, and the source’s \(\mathrm{poly}((\lambda n)^\mu , \sigma )\) bounds are silent on that size (the introspective sampler that compression supplies has size polynomial in \(\log \lambda \)). For a universal base polynomial \(P\) and base degree \(d\), the output is within \(P((\lambda n+1)^\mu +\sigma +\lambda +n)^{\mu +1}\) at input-size degree \(d(\mu +1)\), and rejects longer answers. The terms \(\lambda +n\) change nothing for \(\lambda ,\mu \geq 1\) and \(n\geq 2\), where they are at most \(2(\lambda n)^\mu \); they cover the indices where \((\lambda n+1)^\mu \) does not grow with \(n\), at which the output still computes the PCP’s parameters from \(n\) and \(\lambda \). The extra power retains the input sampler’s degree; fixing \(\mu \) in compression leaves a polynomial bound. Its threshold \(C_{\mathrm{ar}}\) plays the role of the source threshold (thm:ar in ld_compiler.tex); an earlier statement here had the value clauses for all \(n\). Its soundness field also explicitly requires \(n\geq 2\), \(\lambda \geq 1\) and \(\varepsilon {\gt}0\). Completeness transfers ambient HasPerfectPCC from input answer cut \(2^{(\lambda n+1)^\mu }\) to the output budget’s answer cut, for \(\lambda ,\mu \geq 1\): the source’s regime, and the one in which \((\lambda n+1)^\mu \geq n+1\), which the PCP’s validity hypothesis \(2\lceil \log n\rceil \leq T\) needs. At \(\lambda =0\) or \(\mu =0\) the PCP’s time bound is a constant and the clause would be false for large \(n\); compression’s \(\lambda \) is at least \(2\) and its \(\mu \) at least \(1\) (Lemma 6.180). Soundness transfers output value greater than \(1-\varepsilon \) to input value at least \(1-\delta (\varepsilon ,n)\) at those cuts, with \(\delta (\varepsilon ,n)=\sigma ^a((\lambda n)^{\mu a}\varepsilon ^b+(\lambda n)^{-\mu b})\), \(a\geq 1\) and \(0{\lt}b\leq 1\). Sampler and decider descriptions are computable in polynomial time; the sampler depends only on the input sampler and the parameters. The composition consumes an instance at \(\ell =5\), which Lemma 6.194 constructs.

[\(\uparrow \) QuantumLib] Let \(G\) be a finite group and \(\varepsilon \in \mathbb {R}\). An \(\varepsilon \)-approximate representation of \(G\) is a function \(f : G \to U(d)\) such that

where \(\langle \cdot , \cdot \rangle _{hs}\) is the normalized Hilbert–Schmidt inner product of Definition 2.25. Since each value of \(f\) is unitary, \(\left\| {f(x) f(y) - f(xy)} \right\| _{hs}^2 = 2 - 2\, \mathrm{Re}\, \langle f(x) f(y), f(xy) \rangle _{hs}\), so the condition is equivalent to the defect form \(\mathop{\mathbb {E}}_{x, y \sim G} \left\| {f(x) f(y) - f(xy)} \right\| _{hs}^2 \leq 2 \varepsilon \).

A type of the answer-reduced verifier is a pair of an oracularization role and a PCP type. An answer is an answer of its copy’s low-degree test, with one codeword for copies \(1\) to \(5\) and \(m'+6\) codewords for copy \(6\). The oracle answers of the input verifier are never sent. The predicate is the format preamble on both answers, then the five steps of the paper’s decision procedure for both players:

1. equal types have equal answers;

2. the oracle’s \(\mathrm{Point}_6\) answer agrees with an isolated player \(v\)’s \(\mathrm{Point}_v\) answer in component \(v\);

3. an isolated player \(v\)’s input codeword passes the \(m\)-variable test on copy \(v\);

4. between two oracles, copies \(3\), \(4\) and \(5\) pass the consistency check against copy \(6\) and the individual \(m\)-variable test, and copy \(6\) passes the simultaneous test with \(m'+6\) codewords;

5. on an oracle’s \(\mathrm{Point}_6\) question, the point and the answer form a PCP view that the PCP verifier accepts on the input question pair.

The PCP verifier’s decision is a parameter of the predicate.

The decoding of a readable and a linear polynomial at an input question is the table of the readable one on the Boolean cube, cut to the question’s readable length, followed by the linear one’s. The decoded strategy is the strategy for the typed oracularized game of the input, on the state of \(T\), in which an isolated role measures its polynomial measurement and answers the decoding of its two polynomials, read on their slots’ blocks, and the oracle measures its own and answers the pair of decodings of its polynomials in the two roles’ slots.

The honest PCP of an answer pair \((a, b)\) at a question pair \((x, y)\) is \(\mathrm{Induce}\) of the readable tables of the readable parts of \(a, b\) and the linear tables of their linear parts. The honest answer of a tuple of polynomials on the test’s \(M\) variables to a question of the seeded low-degree test is its values at a point, or the coefficients of its restrictions to a line, each field element as its canonical bits, codeword after codeword. At a typed question of role \(r\), to an answer of the oracularized input game, the honest answer is the honest answer of the role’s codewords of the PCP of the oracle’s pair at the questions of its seed, or of an isolated player’s answer paired with itself. The hypotheses under which these PCPs satisfy the checks at every seed are that the parameters fit the lengths of the input game and the constraints its processor outputs on readable answers of at most the readable lengths, and that each seed’s circuit describes the output indicator through the windows of its question pair within a time \(L^*\) meets.

An answer-reduced sampler is a family of CL functions on the typed questions whose questions carry the oracularized input question of the seed’s input part, in the type’s role, and the question of the seeded low-degree test of the seed’s low-degree part. One is the direct sum of the oracularized input sampler and the seeded test’s presentation, downsized along the Shoup basis. The answer-reduced typed game samples a pair of types and a seed and accepts by the typed data. Its honest strategy is the oracularization of the input’s synchronous strategy, pulled back to the typed questions along their roles and oracularized parts and pushed forward along the honest answers.

The index space of the table is \([N] \times [N] \times [D]^3 \times [64]\), the first coordinate fastest, so that for \(N = 2^\ell \) and \(D = 2^{\delta }\) the binary digits of an index are those of its coordinates in turn (II:8453); the last coordinate holds the six signs, one per digit. The table of a triangulated system is the indicator of its decoupled system (Definition 9.94) over the index space, a string of \(64 N^2 D^3\) bits, and five assignments satisfy a table when every equation whose index it contains holds. The check at \((N, D)\) reads the four lengths at the two questions, the constraints that the processor outputs on the readable answers, and the inputs \(a = a^R O\) and \(b = b^R\): the lengths are at most \(N\), \(b\) has \(N\) bits and \(O\) has \(64 N^2 D^3\), the number of constraints times \(2N\), plus \(2N\), is at most \(D\), and \(O\) is the table of the triangulated purified equations, the readable answers cut at the readable lengths. The output indicator of a tailored verifier, at a parameter program giving \((\ell , \delta )\) in unary, is the decider that runs the answer-length calculator four times and the processor once, as the canonical decider does, and then makes the check at \((2^\ell , 2^{\delta })\).

The encoding of a table \(t\) on \(\mathbb {N}\) in \(k\) variables is the multilinear polynomial whose value at the binary digits of \(c {\lt} 2^k\) is \(t(c)\). From Boolean readable tables (the cells of the two readable answers, the table \(O\) and the three witness blocks) and \(\mathbb {F}_2\)-valued linear tables (the cells of the two linear answers and the three copies), the honest PCP of a circuit polynomial \(T\) has the encodings of the tables as its assignments, and as helpers the linear certificates (Lemma 9.107) of the left-hand sides of its checks: of the formula polynomial at degree \(17\), of the system polynomial at degree \(3\), and of \(g(1 - g)\) for each assignment \(g\) at degree \(2\).

An equation over \(\mathbb {F}_2\) is a list of variables and a right-hand side. The purified equation of a constraint \(c\) of the canonical decider at answers \(a^R a^L\), \(b^R b^L\) (eq:purified_equation, II:7762) is the equation on the linear answers, placed in a table of \(2L\) entries (\(a^L\) from \(0\), \(b^L\) from \(L\)), whose right-hand side absorbs the readable answers; a constraint of the wrong length becomes \(0 = 1\). The triangulation of a list of equations (II:7952) replaces \(X_{x_0} + \dots + X_{x_{k-1}} = b\) by \(X_{x_0} = Y_0\), \(Y_{i-1} + X_{x_i} = Y_i\) and \(Y_{k-1} = b\), each row with its own fresh variables, and the extension of an assignment gives \(Y_i\) the partial sum \(\sum _{j \le i} X_{x_j}\), a linear map. The decoupled system (II:8193) on the blocks \(S_A = [\ell _A]\), \(S_B = [\ell _B]\) and three copies \(S_1, S_2, S_3\) of \([\ell ]\) has the equations \(X_A = X^1\), \(X_B = X^1(\ell _A + \cdot )\), \(X^1 = X^2\), \(X^2 = X^3\) and each triangulated equation on the three copies; it is given by the indicator of the equations \(\varepsilon _A X_A(u_A) + \varepsilon _B X_B(u_B) + \sum _i \varepsilon _i X^i(u_i) = \varepsilon _0\) it contains (II:8128), a block of sign \(0\) taking any index.

On \((n, x, y, a^R, b^R)\), with the input verifier’s programs and \((\lambda , \mu , \sigma )\) stored, the processor runs, as stages that keep their input: the routine’s parameter program on \(((\lambda , \mu , \sigma ), n)\); the input sampler, through the universal machine, on the marginal queries of both players at the seeds of \(x\) and \(y\); the routine’s circuit function at each seed, and then the proof check of each question with that circuit’s gates, both on encodings assembled from what the earlier stages output, the input sampler’s questions and the readable answers read as bit strings, so that both run on encodings on every input; and finally the program of Lemma 9.150. No stage decodes a program from data. Its program is computed from the input programs and \((\lambda , \mu , \sigma )\) in polynomial time.

The presented answer-reduced game is the game that the typed data of Definition 9.114 presents on the detyped game of a family of CL functions on the typed questions, with answers bounded by \(B\). A tailored verifier meets it at \(n\) along a bijection of the detyped questions with its questions at \(n\) in the sense of Definition 9.136.

For a parameter routine, an input tailored verifier and \((\lambda , \mu , \sigma )\), the output verifier has the answer-reduced sampler, the answer-length calculator of Lemma 9.144 and the linear-constraints processor of Definition 9.151.

A parameter routine runs in polynomial time when there are \(c\), \(m\) and \(e\) such that, for every \(W \geq (\lambda n + 1)^\mu + \sigma + \lambda + n\) and every \(X \geq 1\), its parameter program halts on \(((\lambda , \mu , \sigma ), n)\) with the parameters within \((c (W + 1)^m X^e)^{\mu + 1}\) steps.

For constants \(E_1, E_2, c_0\) and \((\lambda , \mu , \sigma )\), at the index \(n\), with \(Q = (\lambda n + 1)^\mu \) the input’s budget: the window width \(\ell = Q\); the copy width \(\Delta = (\mu + 2)(Q + 4)\); the table width \(o = 2\ell + 3\Delta + 6\); the description time \(T = 2^K\), \(K = E_1 (\mu + 1)(o + Q + 4)\); the size bound \(\sigma ' = c_0 + 5\sigma + 4(\ell + \Delta ) + 8\) of the output indicator’s program; the witness width \(r\) and the gate count \(s\) the window describer of Lemma 9.98 gives at \((n, T, Q, \sigma ')\); the selector width \(j = \lceil \log _2 (m + 1) \rceil \), \(m\) the PCP’s variable count; the degree \(d = 17\); and the field width \(t = E_2 (j + r + Q + 1)\).

Let \(\ell , \delta , r, s\) be the exponents of the table size and of the copy size, the width of the witness indices and the number of gates, let \(|S_0| = 2\ell + 3\delta + 6\), and let \(m = 2(\ell + 1) + (|S_0| + 1) + 3r + 6 + s\). A PCP over a field \(\mathbb {F}\) consists of eleven assignments, polynomials \(g_A, g_B\) on \(\ell \) variables, \(g_O\) on \(|S_0|\) and three \(g_{W,k}\) on \(r\) (readable), \(g_{La}, g_{Lb}\) on \(\ell \) and three \(g_{L,k}\) on \(\delta \) (linear), and of helpers: \(\alpha ^R_X\) on the \(m\) variables, \(\alpha ^L_X\) on \(|S_0|\), and for each assignment a \(\beta _X\) on its variables. At a point \(p \in \mathbb {F}^m\), for the circuit polynomial \(T\), it passes the formula check when

the system check when, at \(x = p_O\),

and the assignment check of each assignment \(g\) when \(g(1 - g) = \sum _X x_X (1 - x_X)\, \beta _X\) at the point \(x\) of its block. It satisfies the checks identically when each holds at every point of its own space, and it has degree \(d\) when all its polynomials have individual degree at most \(d\).

For PCP parameters \((q,m,d,m',s)\), the typed PCP sampler has the eighteen types \(\mathrm{Point}_i,\mathrm{ALine}_i,\mathrm{DLine}_i\), \(i=1,\ldots ,6\), on the space

over \(\mathbb {F}_q\), of dimension \(10m+2s+16\). Copy \(i\leq 5\) is the seeded CL test of Definition 3.13 in \(m\) variables on its own point, coordinate and direction registers. Copy \(6\) is the test in \(m'=5m+5+s\) variables whose point and direction registers are the concatenations of the five copies’ registers with the auxiliary ones. Each type is presented as a three-level CL function (seed, then direction, then the point register), exact on the whole space. Its full evaluation is the seeded question of its copy, and a uniform vector carries a uniform sample of each copy. The \(i\)-th block of copy \(6\)’s point, in the block order of the PCP, is copy \(i\)’s point: this overlap is what the consistency tests compare.

The block of the seed register a direction is drawn from is read off the seed by a selector \(\chi :\mathbb {F}_q\to [m]\). The test’s own selector numbers the field by an enumeration no program computes, so the presentation takes any selector with blocks of size \(q/m\) (the effective one reads the seed’s high bits), together with a permutation of the seeds carrying it to the test’s; the permutation is used only in the analysis, where a uniform seed stays uniform under it.

The parameters of the answer-reduced verifier at an index are, in unary, the field width \(t\), the selector width \(j\), \(M = 2^j\), the degree \(d\), the four dimensions of the PCP of Definition 9.103, and data for the circuits. A parameter routine consists of the parameters at each \((\lambda , \mu , \sigma )\) and index, with \(m \leq M\); a closed program computing them from \(((\lambda , \mu , \sigma ), n)\); and a polynomial-time circuit function, giving from the input verifier’s programs, \((\lambda , \mu , \sigma )\), \(n\), the parameters and the two questions of a seed a well-formed circuit with the PCP’s numbers of inputs and gates. The program followed by the projection to \((t, j)\) is a parameter routine of the low-degree half.

A parameter routine of the low-degree half is a family of parameters \(t, j\) at each \((\lambda , \mu , \sigma )\) and index, with a polynomial-time map from \((\lambda , \mu , \sigma )\) to a closed program computing them at each index. The answer-reduced typed sampler at \((\lambda , \mu , \sigma )\) puts the oracularized input sampler and the directly answered low-degree half of Lemma 9.140 side by side; its CL functions are the answer-reduced family of Definition 9.121. The answer-reduced sampler is the typed sampler detyped along the complete graph with loops, of level \(\max (\ell + 1, 3) + 2\). Its program is computed from the input sampler’s and \((\lambda , \mu , \sigma )\) in polynomial time.

The common index \(\xi \) is the full uniform oracle seed. Both questions \((x_A,x_B)\) and every auxiliary oracle coordinate are functions of \(\xi \). Indexed measurements and all subsequent averages retain \(\xi \). The image pair \((x_A,x_B)\) is not substituted as an index without proving injectivity or specifying its conditional seed distribution. In the Lean the typed seed is an ordered pair of roles with one common uniform seed (SeededGame.typedSeedEquiv), and every average in the soundness proof is a sum over that seed (one_sub_povmValue_typed).

A PCP (Definition 9.103) has a slot for each of its polynomials, readable or linear, with its block: the injection of the polynomial’s variables into the PCP’s. The codewords of the oracle are all the slots, the readable ones first (the paper’s count of eq:def_heartsuit, readable and linear); those of Alice are \(g_A\) and \(g_{L_a}\), those of Bob \(g_B\) and \(g_{L_b}\). The thirteen checks at a point read only the values of the slots there; they split into the readable checks, the formula check and the readable assignment checks, and the linear checks, the system check and the linear assignment checks. From polynomials on \(N \geq m\) variables, one per slot, the PCP of the polynomials reads each on its slot’s block.

At a role \(r\) with \(k_r\) codewords, \(\delta _r(\varepsilon ) = \delta _{\mathrm{sim}}(q, M, d, k_r, \varepsilon )\) is the error of the seeded test’s soundness. When the test is sound in the model, \(G^\textsc{A}_{r,y}\) and \(G^\textsc{B}_{r,y}\) are the projective measurements, in the two players’ algebras, of \(k_r\)-tuples of polynomials of individual degree at most \(d\) in \(M\) variables that the test’s soundness gives for the per-role strategy at a role \(r\) and an oracularized question \(y\); \(G^\textsc{A}_r\) and \(G^\textsc{B}_r\) are those at \(y_r(z)\).

At the seed \((z, w) \in Z \times W\), the typed question of type \((r, \tau )\) carries the oracularized input question \(y_r(z)\) of the role \(r\) at \(z\) and the seeded test’s question of type \(\tau \) of the sample the registers \(w\) carry. The per-role strategy of \(T\) at a role \(r\) and an oracularized question \(y\) is the strategy for the seeded low-degree test, with one codeword per slot of the role, that plays \(T\) at the typed questions carrying \(y\) and reads the role’s codewords off its answers. The failure of \(T\) at a pair of types and a seed is its failure at the two typed questions they determine.

Fix \(q = 2^t\), \(M = 2^j\) dividing \(q\), a degree \(d\), a PCP layout with \(m \leq M\) variables, the dimension \(r\) of the input sampler at the index, a seed selector of the low-degree test (Definition 3.13), and a circuit polynomial \(T_z\) for each \(z \in \mathbb {F}_2^r\). The types are \(\{ A, B, O\} \times \{ \mathrm{Point}, \mathrm{ALine}, \mathrm{DLine}\} \); a question carries an element of \(\mathbb {F}_2^r\) and, over \(\mathbb {F}_2\) through the Shoup basis, a question of the seeded low-degree test on \(M\) variables. An answer is a codeword for each of its role’s slots, readable first: one field element at a point, the \(d + 1\) or \(Md + 1\) coefficients of a polynomial at an axis-parallel or a diagonal line, each element as its \(t\) canonical bits. The constraints at two typed questions are linear in the answer bits, with coefficients read off the questions and the readable answers:

1. at one role, the seeded low-degree test on the role’s codewords;

2. at one low-degree type, an isolated role and the oracle, the isolated codewords are the oracle’s in the same slots;

3. at an axis-parallel line in the direction \(i\), the codewords whose blocks miss \(i\) have their coefficients \(1, \dots , d\) zero;

4. at the oracle’s point \(p\) with seed \(z\), the thirteen checks of the PCP against \(T_z\) at the first \(m\) coordinates of \(p\): the readable checks as a readable guard, and the linear checks as linear equations, the system check’s coefficients read off \(g_O(p)\) and the linear assignment checks linear because \(g \mapsto g(1 - g)\) is additive in characteristic two.

The typed answer-reduced game at one index has the types (role, PCP type), fifty-four of them, on the complete type graph with loops. Its CL function at a type is the product of two parts on disjoint coordinates, both padded to \(\max \{ \ell +1,3\} \) levels:

• the oracularized sampler’s function of the role;

• the PCP presentation of the PCP type, downsized to \(\mathbb {F}_2\) along the Shoup polynomial basis of \(\mathbb {F}_q\), whose coordinates are the bits the PCP verifier reads.

The coordinates of the PCP part are numbered in three runs: the concatenated point register of the sixth copy, its concatenated direction register, and the six seeds; each copy of the test is then a contiguous run of the first two with its own seed. A question carries the oracularized question in the first part and the downsized PCP question in the second, the latter as the Shoup bits of its coordinates in that order. An answer is written as its field elements’ bit blocks, serialized, and parsed back with the count and block length its type prescribes; an answer of the right format parses back from its encoding. The predicate rejects a failed parse and otherwise applies Definition 6.175 to the decoded questions. Its game check runs the PCP verifier on the input question pair and the view read off the \(\mathrm{Point}_6\) question and answer.

The test associated with a tailored game has a generator \(J\) and one generator for each variable of each vertex, and one challenge per question pair, with the pair’s weight. A subgroup \(H\) passes the challenge at \((x, y)\) when: \(J \notin H\), \(J^2 \in H\) and \(J\) commutes in \(H\) with the variables at \(x\) and \(y\) (Check 1); the variables are involutions and those at a vertex commute (Check 2); each readable variable \(X\) has \(X \in H\) or \(J X \in H\), which reads off a value \(r\) of the readable variables (Check 3); and the word \(J^{c_J} \prod X^{c}\) of every constraint \(c \in L_{xy}(r)\) lies in \(H\) (Check 4). It is written as one clause per readable value \(r\), and the constraint words are deduplicated, which bounds their number by \(2^{2\Lambda + 1} + 1\). An action passes Checks 1–3 everywhere when \(J\) is a fixed-point-free involution commuting with the variables, these are involutions commuting at each vertex, and each readable variable acts at every point as the identity or as \(J\).

A bipartite model consists of a complex Hilbert space \(\mathcal{H}\), a vector \(\psi \in \mathcal{H}\), a unital \(*\)-algebra \(\mathscr {A}\) over \(\mathbb {C}\) represented on \(\mathcal{H}\) by a unital \(*\)-homomorphism \(\pi : \mathscr {A}\to B(\mathcal{H})\), and two unital \(*\)-algebras \(\mathscr {A}_A\) and \(\mathscr {A}_B\) over \(\mathbb {C}\) with unital \(*\)-homomorphisms \(\pi _A : \mathscr {A}_A \to \mathscr {A}\) and \(\pi _B : \mathscr {A}_B \to \mathscr {A}\) such that \(\pi _A(a)\) and \(\pi _B(b)\) commute for all \(a \in \mathscr {A}_A\) and \(b \in \mathscr {A}_B\). The first player’s operators are elements of \(\mathscr {A}_A\), the second player’s elements of \(\mathscr {A}_B\), and a state quantity of \(a\) is computed on the vector \(\pi (\pi _A(a))\psi \). That \(\psi \) is a unit vector is a hypothesis of each statement that needs it, not part of the model. It has two instances.

1. The tensor-product model of a vector \(\psi \in \mathbb {C}^{d_A} \otimes \mathbb {C}^{d_B}\) has \(\mathscr {A}= M_{d_A d_B}(\mathbb {C})\) acting on \(\mathbb {C}^{d_A} \otimes \mathbb {C}^{d_B}\), \(\mathscr {A}_A = M_{d_A}(\mathbb {C})\), \(\mathscr {A}_B = M_{d_B}(\mathbb {C})\), \(\pi _A(X) = X \otimes I\) and \(\pi _B(Y) = I\otimes Y\). Its products and sums are the matrix ones, so the matrix calculus is the model’s with nothing to translate.

2. The commuting-operator model of a commuting-operator strategy \((\mathcal{H}, \psi , E, F)\) has \(\mathscr {A}= B(\mathcal{H})\), \(\mathscr {A}_A\) the commutant of the \(F^y_b\) and \(\mathscr {A}_B\) the commutant of \(\mathscr {A}_A\), with the inclusions. They commute by construction and contain the \(E^x_a\) and the \(F^y_b\). A commutant contains the square roots of its positive elements, so positivity in \(\mathscr {A}_A\) and in \(\mathscr {A}_B\) is positivity in \(B(\mathcal{H})\), which is what the measurements of the analyses need.

For a \(*\)-ring \(R\) ordered by its cone of sums of elements \(z^* z\), the \(n \times n\) matrices over \(R\) are ordered in the same way: \(X \leq Y\) when \(Y - X\) is a sum of matrices \(Z^* Z\). When \(R\) is proper, \(z^* z = 0\) only for \(z = 0\), the relation is antisymmetric, since an element of the cone has nonnegative diagonal entries and a vanishing diagonal entry kills its row and its column, and the matrices over \(R\) are proper again. \(C^*\)-algebras and their \(*\)-subalgebras are proper, and so are the complex matrices; on those the order used is the positive semidefinite one. This is what lets the players’ algebras of an ancilla extension (Definition 8.51) carry POVMs, over and over as registers are adjoined.

The canonical decider of a tailored verifier with answer-length calculator \(\cal {L}\) and linear-constraints processor \(\cal {P}\) is the program that, on \((n, x, y, a, b)\), runs \(\cal {L}\) on \((n, x, \kappa )\) and on \((n, y, \kappa )\) for both kinds \(\kappa \) of variables, then \(\cal {P}\) on \((n, x, y, a^R, b^R)\), where \(a^R\) and \(b^R\) are the first \(\ell ^R(x)\) bits of \(a\) and the first \(\ell ^R(y)\) bits of \(b\), and accepts when \(\left\vert {a} \right\vert = \ell ^R(x) + \ell ^L(x)\), \(\left\vert {b} \right\vert = \ell ^R(y) + \ell ^L(y)\), and every constraint \(c\) that \(\cal {P}\) outputs has the length of \((a, b, 1)\) and satisfies \(\langle c, (a, b, 1)\rangle = 0\) over \(\mathbb {F}_2\). It is a sequence of steps, each of which runs one of the two programs on an input computed in polynomial time from the state and pushes the output onto the state, followed by the check, computed in polynomial time.

Let \(V = \mathbb {F}^n\) with its standard basis. Two complements of a subspace \(S \leq V\) are needed, and they are different.

The orthogonal complement \(S^\perp = \{ u : u \cdot v = 0 \text{ for all } v \in S\} \) for the standard dot product. Over a finite field it need not be a complement of \(S\): \(\mathrm{span}\{ (1,1)\} \) over \(\mathbb {F}_2\) is orthogonal to itself.

The canonical complement, which is one. Write \(u_j = \dim \bigl(S \cap \mathrm{span}\{ \hat e_i : i \geq j\} \bigr)\); the pivot set of \(S\) is \(J = \{ j : u_{j+1} {\lt} u_j\} \), and the canonical complement of \(S\) is \(\mathrm{span}\{ \hat e_j : j \notin J\} \). The canonical linear map with kernel \(S\) is the projector onto the canonical complement parallel to \(S\). Finally, for a linear map \(L\), \(L^\perp \) is the canonical linear map with kernel \((\ker L)^\perp \).

Let \(V = \mathbb {F}^n\) for a finite field \(\mathbb {F}\) and \(n \geq 0\). A register subspace of \(V\) is the span of a subset of the standard basis; for a register subspace \(W\) and \(x \in V\), \(x^W\) denotes the projection of \(x\) onto \(W\) along the complementary register subspace. For \(\ell \geq 0\), the \(\ell \)-level conditionally linear (CL) functions on \(V\) are defined inductively: the only \(0\)-level CL function is the zero function on \(V\); for \(\ell \geq 1\), an \(\ell \)-level CL function is a function \(L : V \to V\) of the form

for complementary register subspaces \(V = V_1 \oplus V_{{\gt}1}\), a linear map \(L_1 : V_1 \to V_1\), and, for each \(v\) in the range of \(L_1\), an \((\ell -1)\)-level CL function \(L_{{\gt}1,v}\) on \(V_{{\gt}1}\). A CL distribution is the distribution of \((L^\textsc{A}(x), L^\textsc{B}(x))\) for uniformly random \(x \in V\) and CL functions \(L^\textsc{A}, L^\textsc{B}\) on \(V\).

A commuting-operator strategy \(\mathscr {S}= (\mathcal{H}, \psi , E, F)\) is projective if every \(E^x_a\) and every \(F^y_b\) is idempotent. Being positive, they are then orthogonal projections, and every measurement of the strategy is projective.

[\(\uparrow \) QuantumLib] A commuting-operator strategy for \(\mathfrak {G}\) consists of a Hilbert space \(\mathcal{H}\) (a complete inner product space over \(\mathbb {C}\), of any dimension), a unit vector \(|\psi \rangle \in \mathcal{H}\), and POVMs \(\{ E^x_a\} _{a \in \mathcal{A}}\) and \(\{ F^y_b\} _{b \in \mathcal{B}}\) on \(\mathcal{H}\), one for each \(x\) (resp. \(y\)) — each \(E^x_a\) and \(F^y_b\) is a positive bounded operator, \(\sum _a E^x_a = I\) and \(\sum _b F^y_b = I\) — such that \(E^x_a F^y_b = F^y_b E^x_a\) for all \(x, y, a, b\). The players answer \((a, b)\) to questions \((x, y)\) with probability \(\langle \psi | E^x_a F^y_b |\psi \rangle \).

[\(\uparrow \) QuantumLib] The value of a commuting-operator strategy \(\mathscr {S}= (\mathcal{H}, \psi , E, F)\) in \(\mathfrak {G}\) is

and the commuting-operator value \(\omega ^{\mathrm{co}}(\mathfrak {G})\) of \(\mathfrak {G}\) is the supremum of \(\omega ^{\mathrm{co}}(\mathfrak {G}, \mathscr {S})\) over all commuting-operator strategies.

Let \(c\) be a machine code with \(i\) input tapes, \(x = (x_1, \ldots , x_i)\) bit strings and \(y \in \{ 0,1\} ^*\). The code \(c\) produces \(y\) on \(x\) if its run on \(x\) halts with output \(y\) (in some time and space). The budgeted evaluation of \(c\) on \(x\) with budget \(T\) returns the output if \(c\) has halted within \(T\) steps, and a timeout marker otherwise; it is total and executable, and the two notions agree: \(c\) produces \(y\) if and only if some budget suffices to observe it.

[\(\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)\).

The proposition that the set of triples \((d, p, q)\) of a game description \(d\) and \(p, q \in \mathbb {N}\) with \(\omega ^{\mathrm{co}}(\mathfrak {G}_d) {\lt} p/q\) is recursively enumerable, where \(p/0 = 0\): the threshold encoding of Lemma 3.112. Lemma 8.14 proves it; Lemma 8.18 takes it as a hypothesis.

[\(\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})\).

A gap compression (an inhabitant of MIPRE.GapCompression) is sound in the value model \(\omega \) if for every \(\lambda \)-bounded verifier \(\mathsf{V}\) and every \(n \geq C_0\),

at the answer bounds of the soundness clause of Theorem 6.197. That clause is soundness in the model \(\mathrm{val}^*\). Soundness in the model \(\omega ^{\mathrm{co}}\) — the commuting-operator soundness of compression — is the model-\(co\) case of the soundness clause of Lin’s gap compression theorem  [ 13 ] , and the one hypothesis of Theorems 8.42 and 8.43. No completeness clause in the commuting-operator model is asked for. It holds for the compression of Corollary 8.44 (Theorem 8.144).

A language \(L \subseteq \{ 0,1\} ^*\) is in \(\mathrm{coRE}\) if its complement is in \(\mathrm{RE}\).

Fix finite sets \(\mathcal{X}, \mathcal{Y}, \mathcal{A}, \mathcal{B}\). A correlation is a function \(p : \mathcal{X}\times \mathcal{Y}\times \mathcal{A}\times \mathcal{B}\to \mathbb {R}\), written \(p(a,b|x,y)\), and its payoff in a game \(\mathfrak {G}\) on these alphabets is \(\sum _{x,y,a,b} \mu (x,y)\, D(x,y,a,b)\, p(a,b|x,y)\). The set \(C_q\) consists of the correlations \(\langle \psi | A^x_a \otimes B^y_b |\psi \rangle \) of finite-dimensional tensor-product strategies (Definition 2.3); \(C_{qa}\) is its closure in \(\mathbb {R}^{\mathcal{X}\times \mathcal{Y}\times \mathcal{A}\times \mathcal{B}}\); and \(C_{qc}\) consists of the correlations \(\langle \psi | E^x_a F^y_b |\psi \rangle \) of commuting-operator strategies (Definition 5.2). The value of a strategy of either kind is the payoff of its correlation.

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.

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.

Let \(\mathfrak {G}= (\mathcal{X}, \mathcal{Y}, \mathcal{A}, \mathcal{B}, \mu , D)\) be a game and \(n \geq 0\) an integer. The \(n\)-fold direct repetition of \(\mathfrak {G}\) is the game \(\mathfrak {G}^{n}\) with question alphabets \(\mathcal{X}^n\), \(\mathcal{Y}^n\) and answer alphabets \(\mathcal{A}^n\), \(\mathcal{B}^n\), question distribution \(\mu ^{n}(\bar{x}, \bar{y}) = \prod _{i=1}^{n} \mu (x_i, y_i)\), and decision predicate \(D^{n}(\bar{x}, \bar{y}, \bar{a}, \bar{b}) = \bigwedge _{i=1}^{n} D(x_i, y_i, a_i, b_i)\). The direct repetition of a synchronous game is synchronous, with the same data.

[\(\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 \(M\) be a finite pair in a unit state \(\psi \), with commutants \(\cal {A}_c\) and \(\cal {B}_c\) as in Lemma 8.121. Its doubled model \(D(M)\) is the following symmetric model (Definition 8.118). Its local algebra is the C\(^*\)-algebra \(\cal {P} = \cal {A}_c \times \cal {B}_c\), with componentwise operations and order, and its space is \(K = \mathcal{H}\oplus \mathcal{H}\). The state is \(\Psi = (\psi , \psi )/\sqrt{2}\), the first placement is \(L(a, b) = a \oplus b\), and the flip is \(J(\xi , \eta ) = (\eta , \xi )\). The second placement is then \(R(a, b) = b \oplus a\), and \(L(x)\) commutes with \(R(y)\) because \(\cal {A}_c\) commutes with \(\cal {B}_c\).

By Lemma 8.121, \(\cal {P}\) is \(*\)-isomorphic to \(\cal {A} \times \cal {B}\), the product of the players’ algebras, which is how reports/c6b-paper-proofs.md writes the doubled model’s local algebra. The model is built over the commutants because a symmetric model needs a C\(^*\)-algebra, and \(\cal {A}\) and \(\cal {B}\) need not be C\(^*\)-algebras.

A dyadic pair is a finite pair (Definition 8.101) whose two players’ algebras both have unital dyadic matrix units (Definition 8.103); by Theorem 8.106, neither player’s operators then contain a nonzero abelian projection. \(\omega ^{\mathrm{co}}\) is approached in dyadic pairs if for every game \(\mathfrak {G}\) and every \(0 \leq t {\lt} \omega ^{\mathrm{co}}(\mathfrak {G})\) there is a projective strategy for \(\mathfrak {G}\) of value greater than \(t\) in a dyadic pair.

Let \(A\) be a ring with an involution and \(\iota \) a finite set. A family \((e_{ij})_{i, j \in \iota }\) of elements of \(A\) is a system of unital matrix units if \(e_{ij} e_{lm} = \delta _{jl}\, e_{im}\), \(e_{ij}^* = e_{ji}\) and \(\sum _i e_{ii} = 1\). The ring \(A\) has unital dyadic matrix units if for every \(n\) it has a system of unital matrix units indexed by \(\{ 0, 1\} ^n\), of size \(2^n \times 2^n\).

[\(\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 \).

The value of a test \(T\) against a probability measure \(\mu \) on \(\mathrm{Sub}(F)\) is the weighted average over challenges of the measure of the set of subgroups passing the challenge. The ergodic value \(\mathrm{val}_{\mathrm{erg}}(T)\) is its supremum over the invariant random subgroups. A finite action \(\sigma \) gives the measure \(\Phi (\sigma )\), the stabilizer of a uniform point.

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

1. 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)\);

2. the norm of a product state is the product of the norms, so the expanded state is a unit vector when both factors are;

3. 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;

4. 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\| \).

A vector trace on a set \(s\) of bounded operators on a Hilbert space \(\mathcal{H}\) is a finite family of vectors \(g_1, \dots , g_n \in \mathcal{H}\) with \(\sum _k \| g_k\| ^2 = 1\) such that \(\tau (x) = \sum _k \langle g_k, x g_k \rangle \) is tracial on \(s\), \(\tau (xy) = \tau (yx)\) for \(x, y \in s\), and the family separates \(s\): an \(x \in s\) with \(x g_k = 0\) for every \(k\) is zero. On a \(*\)-closed \(s\) the separation is the faithfulness of \(\tau \), since \(\tau (x^* x) = \sum _k \| x g_k\| ^2\). A bipartite model (Definition 8.49) is a finite pair if both players’ representations are injective, the operators of each player are exactly the operators commuting with all of the other player’s, and each player’s operators carry a vector trace. The state is an arbitrary unit vector.

Two features of the class matter for the port of the soundness proof to it. The trace is a finite sum of vector states, so the class is narrower than that of all pairs with faithful normal tracial states; the standard form of a tracial algebra needs one vector, and ancilla extensions, the doubling \(\mathcal{H}\oplus \mathcal{H}\) and amplification by a tracial algebra in standard form (Lemma 8.110) stay in the class, while corners do not. And the class contains type \(\mathrm{I}\) pairs with diffuse centre, such as \(L^\infty [0,1]\) acting on \(L^2[0,1]\), whose projections are all abelian. Orthonormalization is proved only in algebras without abelian projections (Theorem 3.8), so the class the port works in is narrowed to the dyadic pairs (Definition 8.107), which exclude them, and Lemma 8.111 amplifies to reach it.

For \(k\) commuting involutions \(U_1, \dots , U_k\) of a complex \(\ast \)-algebra — the observable form of a measurement with outcomes in \(\mathbb {F}_2^k\) — the representation form is the homomorphism \(\alpha \mapsto U^\alpha = \prod _i U_i^{\alpha _i}\) on \(\mathbb {F}_2^k\), and the projective form is the Fourier transform

The inner product \(\langle \alpha , a\rangle = \sum _i \alpha _i a_i\) is taken over \(\mathbb {F}_2\).

[\(\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).

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).

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\):

1. \(\tau ^W(a) \tau ^W(a') = \tau ^W(a + a')\), so \(\tau ^W(0) = I\) and each family commutes;

2. \(\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;

3. (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:

[\(\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.

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 \).

The introspection verifier’s answers are byte strings: a Pauli answer, or a tuple of self-delimiting fields whose last field may be the input’s answer, of variable length at most \(R\). The tailored question reduction re-encodes them with fixed lengths per label, readable bits first: a Pauli answer is kept, readable when it is a \(Z\)-basis answer and linear otherwise; an Introspect or Sample answer \((y, \alpha )\) becomes \(y\), the input’s readable answer bits padded with zeros to \(R\), and its linear answer bits padded to \(R\), the first two readable; a Read answer \((y, y', \alpha )\) becomes \(y\) and the padded readable bits (readable), then \(y'\) and the padded linear bits (linear); a Hide answer \((y, y', x)\) becomes \(y\) (readable), \(y'\) and \(x\) (linear). The input’s split of its answer into readable and linear bits is that at the question read off the readable register \(y\) (a parameter here). Decoding strips the padding and re-forms the tuple.

The introspection verifier runs the input’s decider at index \(2^n\) on the first \(\dim \) bits of the registers \(y\) of its two Introspect answers, and the honest strategy measures the input’s strategy at the same question; a Read answer is compared with an Introspect answer at the same register, and a Sample answer at the seed \(z\) with one at the register \(L_w(z)\). So the input question at an auxiliary answer is the first \(\dim \) bits of \(y\), or of \(L_w(z)\) at a Sample answer, and the layout splits the input’s answer there by the lengths the input’s answer-length calculator outputs. A Pauli label has \(\mathrm{count} \cdot \mathrm{width}\) answer bits, readable at the \(Z\)-basis Pauli label only.

Fix \(\ell \) and an \(\ell \)-level verifier \(\mathsf{V}\) satisfying the paper’s absolute \(\lambda \)-bound, as distinguished in Remark 6.31. The introspective verifier \(\mathsf{V}^{\textsc{Intro}}\) is the typed verifier whose players sample the conditionally linear question distribution of \(\mathsf{V}_{2^n}\) themselves: the question \(y \in V = \mathbb {F}_q^s\) is not sent to them, but obtained by each player measuring its half of \(Q\) shared EPR pairs in a Pauli basis, and reported back. Its decider runs three kinds of test.

1. a Pauli test, which is the game of Theorem 3.38 on the same EPR pairs, so that the measurements the players use to sample are forced to be genuine Pauli measurements in the low-degree-encoded basis;

2. a sampling test, which forces the reported \(y\) to be distributed as the conditionally linear distribution of \(\mathsf{V}_{2^n}\) rather than as anything else the players might prefer;

3. a hiding test, which forces each player not to learn the parts of the question that the conditional sampling should have hidden from it — the types \(\mathtt{Hide}_1, \ldots , \mathtt{Hide}_\ell \) exist for this, one per level.

It is a \(3\)-level typed verifier, hence \(5\)-level once detyped (Remark 6.9), and that \(5\) is what the compression pipeline consumes. The Lean verifier is the ambient one, built for \(7\)-level inputs (Definition 6.130); its question types include the Introspect and Read types of the source.

The structure MIPRE.Introspection is an ambient contract, parametrized by \(\ell \): the introspective sampler as a function of \(\lambda \) alone with its program computable in polynomial time, the introspective decider’s program as a polynomial-time function of the input programs and \(\lambda \), the packaging as a \(5\)-level normal form verifier on every input, the complexity clauses for every input and index — sampler and decider runtime coefficients at most \((\lambda n + 1)^C\) and \(2^{(\lambda n + 1)^C}\), respectively, both at input-size degree \(C\), and \(\left\vert {\mathcal{D}^{\textsc{Intro}}} \right\vert \leq C(\lambda + 1)^C\) for a constant \(C\), the ambient analogue of \(C_{\mathrm{intro}}\), with the decider rejecting answers longer than \(2^{(\lambda n+1)^C}\). For ambient \(\lambda \)-bounded inputs, completeness transfers HasPerfectPCC from index \(2^n\) at answer cut \((2^n)^\lambda \) to index \(n\) at cut \(2^{(\lambda n+1)^C}\). For \(n\geq 1\), soundness transfers a value greater than \(1-\varepsilon \), for \(\varepsilon {\gt}0\), at the output cut to a value at least \(1-\delta (\varepsilon ,n)\) at the input cut, where \(\delta (\varepsilon ,n)=a((\lambda n)^a\varepsilon ^b+(\lambda n)^{-b})\), \(a\geq 1\) and \(0{\lt}b\leq 1\). The complexity clauses are stated in the vocabulary of resource budgets (MIPRE.Budget, Verifier.Within: the running-time coefficients of sampler and decider and their degree, the question dimension, and the answer length beyond which the decider rejects), which lets the exterior transformations be chained. The composition MIPRE.GapCompression.ofPipeline consumes an instance at \(\ell = 7\). Here \(\lambda \)-boundedness is the ambient definition, not the source absolute-time hypothesis. This definition specifies the contract, without constructing an inhabitant. Since \(\ell \) is fixed by the structure, its polynomial-time construction field does not assert a bound polynomial in binary \(\ell \).

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 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\).

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\).

For \(y \in \{ 0,1\} ^m\) let \(\mathrm{ind}_{m,y}(x) = \prod _{i : y_i = 1} x_i \prod _{i : y_i = 0} (1 - x_i)\), a multilinear polynomial over \(\mathbb {F}_q\) which on the subcube \(\{ 0,1\} ^m\) is \(1\) at \(y\) and \(0\) elsewhere. For \(a \in \mathbb {F}_q^M\), \(M = 2^m\), with coordinates indexed by \(\{ 0,1\} ^m\), the low-degree encoding of \(a\) is \(g_a = \sum _y a_y \mathrm{ind}_{m,y}\); it is multilinear and \(g_a(y) = a_y\). For \(H \subseteq \mathbb {F}_q\) the decoding map \(\mathrm{Coded}_H\) sends a polynomial \(g\) to the vector with \(y\)-coordinate \(g(y)\) if \(g(y) \in H\) and \(0\) otherwise, so that \(\mathrm{Coded}_H(g_a) = a\) for \(a \in H^M\); \(\mathrm{Coded}= \mathrm{Coded}_{\{ 0,1\} }\) is the Boolean decoding map, and \(\mathrm{Coded}(g) \in \{ 0,1\} ^M\) for every \(g\). Being multilinear, \(g_a\) has individual degree at most \(1\) and total degree at most \(m\).

Let \(\mathbb {F}\) be a finite field with \(q\) elements and let \(m \geq 1\) and \(d\) be integers. The \((m,q,d)\)-low individual degree test is the two-player game in which the verifier picks one of the following three sub-tests with probability \(\tfrac 13\) each, having sampled a uniform point \(u \sim \mathbb {F}^m\).

1. Axis-parallel lines test. Sample a uniform direction \(i \sim [m]\) and a uniform role. One player receives the line \(\ell = \{ u + t e_i\} \) and answers a univariate polynomial \(f\) of degree at most \(d\); the other receives \(u\) and answers \(a \in \mathbb {F}\). Accept if \(f(u) = a\).

2. Self-consistency test. Both players receive \(u\) and answer elements of \(\mathbb {F}\). Accept if the answers are equal.

3. Diagonal lines test. Sample a uniform \(j \sim [m]\), a uniform direction \(v \in \mathbb {F}^m\) whose coordinates after the \(j\)-th vanish, and a uniform role. One player receives the line \(\ell = \{ u + t v\} \) and answers a univariate polynomial of degree at most \(md\); the other receives \(u\) and answers \(a \in \mathbb {F}\). Accept if \(f(u) = a\).

For admissible \(q\), positive integers \(m,d,\mathrm{ldc}\) and \(m\mid q\), the seeded CL test is the paper’s typed low-degree game with parameters \((q,m,d,\mathrm{ldc})\). Each ordered pair of types from \(\{ \mathtt{Point},\mathtt{ALine},\mathtt{DLine}\} \) has weight \(1/9\), with question contents sampled from the corresponding CL distribution. Point questions ask for an element of \(\mathbb {F}_q^{\mathrm{ldc}}\). Axis-line questions retain a seed-labelled description \((u_0,s)\) and ask for \(\mathrm{ldc}\) degree-\(d\) polynomials; diagonal-line questions retain \((u_0,s,v)\) and ask for \(\mathrm{ldc}\) degree-\(md\) polynomials. The seed selects the direction class, with leading coordinates of the diagonal direction set to zero. The verifier checks the answer format, equality on identical same-type questions, and evaluation agreement for either line type against a point; the other type pairs impose no further check. In particular, different seed descriptions of the same geometric line remain different questions.

The seeded CL test is sound in dyadic pairs if it is sound (Definition 8.65) in every dyadic pair (Definition 8.107). Dyadic pairs being finite pairs, this is weaker than soundness in every finite pair, so the conditional theorem it feeds (Corollary 8.115) is stronger.

The seeded CL test is sound in the bipartite model if the conclusion of Theorem 3.14 holds for the projective strategies in the model, with the extracted measurements in the players’ algebras: for \(q = 2^k\), \(m \mid q\) and \(d, \mathrm{ldc} \geq 1\), every projective strategy in the model passing the seeded test with \(\mathrm{ldc}\) codewords with probability at least \(1 - \varepsilon \) admits projective measurements \(G^\textsc{A}\) in the first player’s algebra and \(G^\textsc{B}\) in the second’s, of tuples of polynomials of individual degree at most \(d\), whose evaluations at a uniform point are consistent with the other player’s point measurement, and which are consistent with each other, all with error at most \(\delta _{\mathrm{CL}}(\varepsilon , q, m, d, \mathrm{ldc})\). It is sound in the commuting-operator model if it is sound in the model of every commuting-operator strategy (Definition 8.49). A value model \(\omega \) is approached in models where the test is sound if for every game \(\mathfrak {G}\) and every \(0 \leq t {\lt} \omega (\mathfrak {G})\) there is a projective strategy for \(\mathfrak {G}\) of value greater than \(t\) in a bipartite model on a Hilbert space in which the test is sound and which \(\omega \) dominates.

For \(p \in \mathbb {F}_q[x_1, \ldots , x_m]\) and a line \(t \mapsto u_0 + t w\), the restriction of \(p\) to the line is the univariate polynomial \(p|_\ell (t) = p(u_0 + t w)\), obtained by substituting the affine parametrization into \(p\). Its degree is at most the total degree of \(p\), and its coefficients, read at any degree bound \(n\) that the degree does not exceed, evaluate back to \(p(u_0 + t w)\). So the low-degree encoding \(g_h\), being multilinear, restricts to a polynomial of degree at most \(m\) on any line, which fits the degree-\(md\) answer format of Definition 3.13 whenever \(d \geq 1\).

A local isometry from a bipartite model \(M\) to a bipartite model \(M'\) is a linear isometry \(W\) of their Hilbert spaces with, for each player, a non-unital \(*\)-homomorphism \(\Phi \) of the player’s algebra of \(M\) into that of \(M'\), such that \(W\) intertwines the two representations: \(\pi '(\pi '_A(\Phi _A(a)))\, W = W\, \pi (\pi _A(a))\), and likewise for the second player. In the tensor-product model, \(X \mapsto V_A X V_A^\dagger \) for an isometry \(V_A\) is such a \(\Phi _A\), not unital since \(\Phi _A(I) = V_A V_A^\dagger \). Local isometries compose and exchange with the players. A projective measurement \(\{ P_a\} \) of the first player is transported to the projective measurement \(\{ \Phi _A(P_a) + [a = a_0](I- \Phi _A(I))\} \) of \(M'\), the complement of the image added at one fixed outcome \(a_0\), and likewise for the second player. The model \(M\) with its state replaced by a vector \(v\) of its Hilbert space is written \(M^{v}\).

A machine code is first-order data: a header (number of work tapes, alphabet size, number of states, start state) and a dense transition table with one entry per observation, in a fixed canonical order. A well-formed code is interpreted as a multi-input machine, with binary input and output through two reserved alphabet symbols. Codes serialize exactly: the description \(\alpha \in \{ 0,1\} ^*\) of a code has size \(\left\vert {\alpha } \right\vert \), and total decoding interprets every string — \([\alpha ]_i\) denotes the coded machine with \(i\) input tapes described by \(\alpha \), with every malformed string denoting one fixed machine that immediately rejects.

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\).

Let \(P\) be the complex polynomials in noncommuting variables \(e_{xa}\) (\(x \in \mathcal{X}\), \(a \in \mathcal{A}\)) and \(f_{yb}\) (\(y \in \mathcal{Y}\), \(b \in \mathcal{B}\)), with the involution that conjugates coefficients, reverses words and fixes the variables. The relations are \(\sum _a e_{xa} - 1\), \(\sum _b f_{yb} - 1\) and \(e_{xa} f_{yb} - f_{yb} e_{xa}\); \(I\) is the complex span of \(u \rho v\) over relations \(\rho \) and \(u, v \in P\). The cone \(M\) is the set of finite nonnegative real combinations of the elements \(s^* s\), \(s^* e_{xa} s\), \(s^* f_{yb} s\) (\(s \in P\)), of the elements of \(I\), and of the anti-hermitian elements of \(P\). The game polynomial of \(\mathfrak {G}\) is \(W_\mathfrak {G}= \sum _{x,y,a,b} \mu (x,y) D(x,y,a,b)\, e_{xa} f_{yb}\). A cone state is a complex-linear \(L : P \to \mathbb {C}\) with \(L(1) = 1\) and \(\mathrm{Re}\, L(m) \geq 0\) for every \(m \in M\).

A language \(L \subseteq \{ 0,1\} ^*\) is in \(\mathrm{MIP}^{\mathrm{co}}\) if there is a computable map \(g\) from bit strings to game descriptions (Definition 2.43) such that for every string \(z\),

in the bipartite commuting-operator value of Definition 5.3: the class \(\mathrm{MIP}(\omega ^{\mathrm{co}})\) of Definition 8.34. As Definition 2.53, this is the computable class, with no polynomial-time bound on \(g\); the polynomial-time class of Lin’s paper is contained in it, as Lemma 2.54 shows for \(\mathrm{MIP}^*\), and is not formalized.

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 )\):

1. 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\).

2. Completeness. If \(z\in L\) then \(\mathrm{val}^*(\mathfrak {G}_z)=1\).

3. Soundness. If \(z\notin L\) then \(\mathrm{val}^*(\mathfrak {G}_z)\leq \tfrac 12\).

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.

An embedding of bipartite models is a local isometry (Definition 8.69) whose isometry carries the state to the state and whose two homomorphisms are unital: the model form of adjoining registers in fixed vectors. Embeddings have identities, compose and exchange with the players, and every isomorphism is one. A local isometry from \(M\) to \(M'\) is also one from \(M\) to \(M'^{\varphi }\), for every vector \(\varphi \) of the space of \(M'\).

An isomorphism of bipartite models from \(M\) to \(M'\) is a unitary \(W\) of their Hilbert spaces carrying the state of \(M\) to the state of \(M'\), with a \(*\)-algebra isomorphism \(\Phi _A\) of the first player’s algebra of \(M\) onto that of \(M'\) and one \(\Phi _B\) for the second player, the two representations intertwined by \(W\) as in Definition 8.69. Isomorphisms have identities, compose, invert and exchange with the players. An isomorphism is a local isometry whose homomorphisms are unital and whose isometry carries the state to the state; conversely, a local isometry carrying the state to the state, whose isometry has a right inverse and whose homomorphisms have two-sided inverses, is an isomorphism.

A projective strategy for a game \(\mathfrak {G}\) in a bipartite model \((\mathcal{H}, \psi , \mathscr {A}, \mathscr {A}_A, \mathscr {A}_B)\) with a unit state (Definition 8.49) is a projective measurement \(\{ A^x_a\} _a\) in \(\mathscr {A}_A\) for each question \(x\) of the first player and a projective measurement \(\{ B^y_b\} _b\) in \(\mathscr {A}_B\) for each question \(y\) of the second. Its value is the model’s value of the two families, and its conditional failure at \((x, y)\) is the probability of rejection given the question pair. It is played on another game through a map of the questions and a question-dependent coarse-graining of the answers, relabelled along equivalences, or restricted to other questions; a coarse-graining of a projective measurement is projective, so these are projective strategies. The inconsistency of a family \(\{ P^x\} \) in \(\mathscr {A}_A\) and a family \(\{ Q^x\} \) in \(\mathscr {A}_B\) with a common outcome set, on an index weighted by \(\mu \), is \(\sum _x \mu (x) \sum _{a \neq b} \mathrm{Re}\langle \psi , \pi (\pi _A(P^x_a)\pi _B(Q^x_b))\psi \rangle \), Definition 2.37 in the model. A value model \(\omega \) dominates the model if every projective strategy in it has value at most \(\omega \) of its game.

Let \(M\) be a bipartite model, \(e\) a vector on registers \(\alpha \times \beta \) and \(\sigma : \alpha \times \beta \to \alpha ' \times \beta '\) a bijection. The reading of the extension of \(M\) in \(e\) along \(\sigma \) has the Hilbert space, the state and the represented algebra of that extension, with the first player’s algebra \(M_{\alpha '}(\mathscr {A}_A)\) and the second player’s \(M_{\beta '}(\mathscr {A}_B)\) acting through \(\sigma \), reindexing square matrices along a bijection being a unital \(*\)-homomorphism. The registers are regrouped, a register handed across the cut is read by the other player, and nothing happens to the state. The regrouping that hands the first player’s outer register \(\gamma \) to the second player is \(((c, a), b) \mapsto (a, (c, b))\), and the product basis vector of a pair of registers at \((a_0, b_0)\) is written \(|a_0 b_0\rangle \).

A multi-input Turing machine with \(i\) input tapes and \(w\) work tapes has \(i\) two-way read-only input tapes (heads clamped one blank cell beyond either end of the input), \(w\) bidirectional work tapes over an alphabet extended with a blank symbol, and a write-only output stream. A transition may write and move on every work tape, move every input head, emit at most one output symbol, and either continue or halt. Time is counted in steps, and space as the number of work-tape cells visited.

At \(i = 1\) this is exactly the CSLib multi-tape model.

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}\).

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)\} \).

A tailored verifier \(\mathsf{V}\) is the normal form verifier (Definition 2.46) with the sampler of \(\mathsf{V}\) and the decider that checks that both questions have the length the sampler gives them and then runs the canonical decider of \(\mathsf{V}\) through the universal machine (Verifier.ofSamplerDecider, Remark 6.204).

The one-sided extension of a bipartite model \(M\) by a finite register \(T\) in a basis state \(t_0\) adjoins \(T\) to the first player only: the first player’s algebra becomes \(M_T(\mathscr {A}_A)\), the second player’s is unchanged, and the state is \(\psi \otimes e_{t_0}\). The inert embedding of \(M\) into it carries \(a\) to \(a \otimes I\). Local isometries extend along registers, and extending a register model on one side is, up to exchanging the two layers of block matrices, the register model of the extension.

A seeded game is a finite seed space \(V\), two question maps \(L^\textsc{A}, L^\textsc{B}: V \to V\) and a decision predicate \(D\); the game it presents is the law of \((L^\textsc{A}(z), L^\textsc{B}(z))\) for a uniform seed \(z\), with predicate \(D\). Its oracularization is the synchronous game on questions \(\mathcal{T}^\textsc{Orac}\times V\), \(\mathcal{T}^\textsc{Orac}= \{ \textsc{O}, \textsc{A}, \textsc{B}\} \), and answers either a pair (from an oracle) or a single answer (from an isolated player), in which the verifier draws the ordered pair of roles and the seed uniformly, gives an oracle the seed \(z\) itself and an isolated player of role \(v\) the question \(L^v(z)\), and accepts when: each answer’s shape matches its player’s role; each oracle’s pair of answers is accepted by \(D\) at the pair of questions its seed determines; equal roles carry equal answers; and each oracle’s component for the other player’s role agrees with that player’s answer.

Oracularization is sound in the value model \(\omega \) if \(\omega \) has three properties of \(\mathrm{val}^*\) that the value transfers of Theorem 6.133 use: the monotonicity of item 1 of Lemma 8.59; the game-level soundness of oracularization, that \(\omega \) of the oracularization of a seeded game above \(1 - \varepsilon \) puts \(\omega \) of its game at least \(1 - 24\sqrt\varepsilon \); and the detyping restriction of item 2 of Lemma 8.59, between the values of the typed and the detyped finite games.

Let \(\mathsf{V}\) be a normal form verifier with at least one level, \(n\) an index, \(B\) a parse cut and \(T\) an answer cut, and let \(L^\textsc{A}, L^\textsc{B}\) be the CL functions of its sampler at \(n\). The typed oracularized game of \(\mathsf{V}_n\) is the finite typed game, in the sense of Definition 6.10, on the complete type graph with loops over \(\mathcal{T}^\textsc{Orac}= \{ \textsc{O}, \textsc{A}, \textsc{B}\} \). Its CL functions are the identity for the type \(\textsc{O}\), as a CL function with the levels of \(\mathsf{V}\), and \(L^\textsc{A}\), \(L^\textsc{B}\) for the types \(\textsc{A}\), \(\textsc{B}\), the same for both players; its answers are the bit strings of length at most \(T\). Its predicate parses each answer by the type of the player who gave it: an oracle’s must be the serialization of a pair of strings of length at most \(B\), an isolated player’s a single string of length at most \(B\). It rejects when a parse fails, and otherwise decides as the oracularization (Definition 6.134) of the seeded game \((L^\textsc{A}, L^\textsc{B}, D)\), where \(D\) is the predicate of \(\mathsf{V}_n\) on answers of length at most \(B\).

The structure MIPRE.Oracularization, parametrized by \(\ell \), specifies the typed oracularized verifier of an \((\ell + 1)\)-level normal form verifier. Its sampler is the typed sampler of Lemma 6.141, so the oracle form of the sampler is definitional. Its fields specify the decider: a typed decider over \(\mathcal{T}^\textsc{Orac}\) of the programs of the input sampler and decider and of an index routine supplying a parse cut \(B(n)\) and a simulation budget \(K(n)\). The decider halts on every input, and its program is a polynomial-time function of the three programs. It accepts only answers that the bit-string predicate of Definition 6.139 accepts at the cut \(B(n)\): this is the oracle form of the decider. It accepts every such answer within an answer cut \(T\) once \(K(n) \geq c(W + 1)^m(Z + 1)^{e(k + 1)}\), where \(W\) bounds the running-time coefficients of the input verifier at \(n\), \(k\) is their degree, and \(Z\) is the sum of the description lengths of the input programs, the sizes of \(B(n)\) and \(n\), the dimension \(s(n)\) and \(T\). It runs within \(c'(W' + 1)^{m'}(\left\vert {d} \right\vert + 1)^{e'}\) on inputs \((n, d)\), where \(W'\) bounds \(K(n)\), \(B(n)\), the index routine’s running time at \(n\), the description lengths of the three programs and \(n\).

[\(\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 \),

A value model \(\omega \) dominates the POVM strategies of a bipartite model if every pair of families of POVMs in the players’ algebras has value at most \(\omega \) of the game. It is approached by projective strategies if, for every game \(\mathfrak {G}\) and every \(0 \leq t {\lt} \omega (\mathfrak {G})\), some projective strategy for \(\mathfrak {G}\) in a model on a Hilbert space that \(\omega \) dominates has value greater than \(t\).

A bipartite model \(M'\) reduces to \(M\) if every POVM strategy in \(M'\), for every game, has value at most that of some POVM strategy in \(M\). A model over an algebra \(\mathscr {A}_B\) is a bipartite model whose second player’s algebra is \(\mathscr {A}_B\), packed with its first player’s algebra and its represented algebra, the former ordered and proper; its one-sided extension is again one. The game with the players exchanged asks the second player the first question.

At stage \(t\) take the words of length at most \(t+2\) in the first \(n+t\) letters, and the grid points of weight \(M = P \cdot 2^t\) on its \(P\) patterns. A grid point is feasible when every pattern of positive weight is locally closed (contains the empty word, closed under cancelling a pair, deleting a letter beyond the \(n\) generators, and \(u, v \mapsto u v^{-1}\) within the stage) and conjugation by each generator moves it by at most \(4P\) in \(\ell ^1\). The upper value at stage \(t\) is the best value of a feasible point, plus \(2/2^t\), rounded up to a multiple of \(2^{-t}\). This replaces the paper’s pseudo IRS polytope and its linear program by an exhaustive search over a grid, with the invariance relaxed to absorb rounding.

[\(\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.

Let \(\mathsf{qldparams}= (q, m, d)\) be admissible: \(q\) an admissible field size and \(m \mid q\). Write \(M = 2^m\) and let \(\omega = (u_X, u_Z, r_X, r_Z) \in (\mathbb {F}_q^m)^2 \times \mathbb {F}_q^2\). The Pauli basis test \(\mathfrak {G}^\textsc{Pauli}_\mathsf{qldparams}\) is the two-player game with the following twenty-six question types,

where \(\mathcal{T}^\mathrm{MS}\) is the six constraints and nine variables of the Magic Square (Definition 2.22).

Question distribution. The verifier draws an ordered pair of types uniformly among those adjacent in the type graph \(G^\textsc{Pauli}\) — each non-loop edge contributing two ordered pairs and each self-loop one — and independently \(u_X, u_Z, v \in \mathbb {F}_q^m\), \(s \in \mathbb {F}_q\) and \(r_X, r_Z \in \mathbb {F}_q\) uniformly. The edges of \(G^\textsc{Pauli}\) are: a self-loop at every type; \((\mathtt{ALine}, W)\) and \((\mathtt{DLine}, W)\) each to \((\mathtt{Point}, W)\); \((\mathtt{Point}, W)\) to \((\textsc{Pauli}, W)\); \((\mathtt{Point}, W)\) to \((\mathtt{Pair}, W)\) to \(\mathtt{Pair}\); \((\mathtt{Point}, X)\) to \(\mathtt{Variable}_1\) and \((\mathtt{Point}, Z)\) to \(\mathtt{Variable}_5\); and the eighteen incidences of the Magic Square, \(\mathtt{Constraint}_i\) to \(\mathtt{Variable}_j\) for \(j\) in the support of equation \(i\). So there are thirty non-loop edges and eighty-six ordered pairs, each of weight \(1/86\).

Question content. A type \((\mathtt{Point}, W)\) receives \(u_W\); \((\mathtt{ALine}, W)\) receives \((u_0, s)\) with \(u_0 = L^{\mathrm{Ln}}_{e_i}(u_W)\) and \(i = \chi (s)\); \((\mathtt{DLine}, W)\) receives \((u_0, s, v')\) with \(v' = \pi _{i-1}(v)\) and \(u_0 = L^{\mathrm{Ln}}_{v'}(u_W)\) — all three exactly as in Definition 3.13; \((\textsc{Pauli}, W)\) receives nothing; and each of \(\mathtt{Pair}\), \((\mathtt{Pair}, W)\), \(\mathtt{Constraint}_i\) and \(\mathtt{Variable}_j\) receives \(\omega \).

Answer format. An element of \(\mathbb {F}_q\) for \((\mathtt{Point}, W)\); a polynomial of degree at most \(d\) for \((\mathtt{ALine}, W)\) and at most \(md\) for \((\mathtt{DLine}, W)\); an element of \(\mathbb {F}_q^M\) for \((\textsc{Pauli}, W)\); a pair \((\beta _X, \beta _Z) \in \mathbb {F}_2^2\) for \(\mathtt{Pair}\); a single bit for \((\mathtt{Pair}, W)\) and for \(\mathtt{Variable}_j\); and a triple \((\alpha _{v_1}, \alpha _{v_2}, \alpha _{v_3}) \in \mathbb {F}_2^3\), indexed by the three variables of the equation in order, for \(\mathtt{Constraint}_i\).

Decision. The verifier first checks that both answers have the format their question’s type prescribes, and rejects if not. It then applies, with \(\gamma (\omega )\) as in Lemma 3.42 and \(g_h\) the low-degree encoding of Definition 6.149:

1. equal types: accept iff the two answers agree;

2. \((\mathtt{Point}, W)\) against \((\mathtt{ALine}, W)\) or \((\mathtt{DLine}, W)\): accept iff the seeded CL decider of Definition 3.13 at \((q, m, d, 1)\) accepts;

3. \((\mathtt{Point}, W)\) against \((\textsc{Pauli}, W)\): accept iff \(g_{a_{\bar w}}(x_w) = a_w\);

4. \((\mathtt{Pair}, W)\) against \(\mathtt{Pair}\): accept iff \(a_w = \beta _W\) or \(\gamma (\omega ) \neq 0\);

5. \((\mathtt{Point}, W)\) against \((\mathtt{Pair}, W)\): accept iff \(\operatorname {tr}(a_w r_W) = a_{\bar w}\) or \(\gamma (\omega ) \neq 0\);

6. \(\mathtt{Constraint}_i\) against \(\mathtt{Variable}_j\): accept iff \(\gamma (\omega ) = 0\), or \(j\) occurs in equation \(i\), the triple \(a_w\) satisfies that equation, and its entry at \(j\) is \(a_{\bar w}\);

7. \((\mathtt{Point}, W)\) against \(\mathtt{Variable}_j\): accept iff \(\gamma (\omega ) = 0\), or \(j = 1\), \(W = X\) and \(\operatorname {tr}(a_w r_X) = a_{\bar w}\), or \(j = 5\), \(W = Z\) and \(\operatorname {tr}(a_w r_Z) = a_{\bar w}\);

each in both orientations, and accepts on any type pair no rule names.

Let \(\cal {N}\) be a bipartite model and \(I\) a finite set, the register of the analysis (\(I = \mathbb {F}_q^{\{ 0,1\} ^m}\), so that \(\mathbb {C}^I = (\mathbb {C}^q)^{\otimes M}\)). Let \(T\) be the ancilla of the projective dilation of Lemma 8.77 for POVMs whose outcomes are the answers of the seeded CL test at \((q, 4m, d, 1)\), with \(K + 1\) Kraus terms, and \(t_0 \in T\) its reference state, at the zero answer. The registers are named as in the paper: \(A\) is the first player’s own space, \(A'\) and \(A''\) the two halves of an EPR pair on \(I\), and \(E_A\) a copy of \(T\); likewise \(B\), \(B'\), \(B''\) and \(E_B\) for the second player. Every model below depends on the padding size \(K\).

1. The padded model is the register model of \(\cal {N}\) on \(I\) (Definition 8.72) extended by \(E_A\) for the first player and \(E_B\) for the second, in the basis state \(|t_0\rangle \otimes |t_0\rangle \) (Definition 8.51). Up to the associativity of extensions it is the extension of \(\cal {N}\) by the registers \((E_A, A')\) and \((E_B, A'')\) in the unit vector \(|t_0 t_0\rangle \otimes |\textsc{EPR}_I\rangle \), so the seeded CL test is sound in it (Definition 8.65) whenever it is sound in every extension of \(\cal {N}\) by a unit vector, and then also in the padded model of \(\cal {N}\) with the players exchanged.

2. The physical model is the extension of \(\cal {N}\) in which each player holds three registers, \((A'', E_A, A')\) and \((B'', E_B, B')\), in the physical state: each player’s own EPR pair, \((A'', A')\) and \((B'', B')\), and the two padding registers in \(|t_0\rangle \otimes |t_0\rangle \). The physical state is a unit vector, symmetric under the exchange of the two players’ blocks, and each pair satisfies the mirror identity: an operator \(P\) on the near half \(A'\) acts on the state as \(P^{\mathsf T}\) on the far half \(A''\), whatever the other player applies, and likewise for \(B'\) and \(B''\).

3. The first cut is the physical model read (Definition 8.88) with the first player’s far half \(A''\) handed to the second player: the same Hilbert space, state and representation, the first player’s operators being those of \((E_A, A')\) and the second player’s those of \((A'', B'', E_B, B')\). The second cut is the first cut of \(\cal {N}\) with the players exchanged, a reading of the same state.

4. The padded model and the register model embed in the first cut, along embeddings \(j_1\) and \(\iota _1\) (Definition 8.90), local isometries that carry the state to the state and keep both units: \(\iota _1\) is the inert extension of the register model by \(|t_0 t_0\rangle \) followed by \(j_1\), and it sends a first-player operator \(Z\) of \(A'\) to \(I_{E_A} \otimes Z\).

5. Item 1’s cut is the register model on \(I\), its pair being \((A'', B'')\), of the extension of \(\cal {N}\) by the padded registers \((E_A, A')\) and \((E_B, B')\). Regrouping the physical registers into it is a local isometry (Definition 8.69) from the physical model, with no condition on the state.

6. The physical model of \(\cal {N}\) with the players exchanged is the physical model of \(\cal {N}\) with the players exchanged: the exchange of the two blocks of registers is an isomorphism of models between them (Definition 8.85), the identity on the players’ algebras, because the physical state is symmetric.

An ancilla model is a bipartite model on a Hilbert space, with a unit state and with ordered, proper player algebras (Definition 8.68); every such model is one. An extraction at error \(\delta \), for a projective strategy of the Pauli basis game \(\mathfrak {G}^{\textsc{Pauli}}_{(q,m,d)}\) in a bipartite model \(M\), is an ancilla model \(N\) and a local isometry of \(M\) into the register model of \(N\) on \(\mathbb {F}_q^{\{ 0,1\} ^m}\) that carries the state of \(M\) within \(\delta \) of the state \(|\textsc{EPR}_q\rangle ^{\otimes 2^m} \otimes \psi _N\) of the register model, and carries each player’s \((\textsc{Pauli}, W)\) measurement, read as cube data, within \(\delta \) of the honest Pauli projectors on that player’s register, in summed squared state norm, for both bases \(W\). An extraction at one error is one at every larger error. The Pauli basis test is sound in \(M\), with the value model \(\omega \), if for every field \(\mathbb {F}_q\) of characteristic two, every \(m \geq 1\) dividing \(q\) and every \(d \geq 1\), every projective strategy in \(M\) failing the test with probability at most \(\varepsilon \) has an extraction at the error \(\delta _{qld}(\varepsilon , m, d, q)\) of Theorem 3.38 whose ancilla model \(\omega \) dominates (Definition 8.78). That error is, in Lean, the function qldErr the proof of the theorem produces, at most the closed form of the theorem when \(\varepsilon \leq 1\) (Lemma 3.78). Soundness in \(M\) is the conclusion of Theorem 3.38 for the projective strategies in \(M\), and that theorem proves it in every model with ordered, proper player algebras in which the seeded low-individual-degree test is sound in every extension by a unit vector and whose extensions, in every unit state, \(\omega \) dominates. The test is sound in the commuting-operator model if it is sound, with \(\omega ^{\mathrm{co}}\), in the model of every commuting-operator strategy. A value model is approached in models where the test is sound if, for every game \(\mathfrak {G}\) and every \(0 \leq t {\lt} \omega (\mathfrak {G})\), some projective strategy for \(\mathfrak {G}\) in a model on a Hilbert space in which the test is sound with \(\omega \) has value greater than \(t\).

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.

The register model of a bipartite model \(N\) on a finite register \(I\) is its ancilla extension by the maximally entangled vector \(|\mathrm{EPR}_I\rangle \): each player holds a copy of \(I\), and the state is \(|\mathrm{EPR}_I\rangle \otimes \psi _N\). In the tensor-product model of a vector \(\xi \) it is the tensor-product model of the register state \(|\mathrm{EPR}_I\rangle \otimes |\xi \rangle \). Relabelling the register, splitting it as a product, extending it by a spectator factor and exchanging the players are local isometries between register models.

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.

Let \(K / \mathbb {F}\) be a finite extension of finite fields, \(q = \left\vert {\mathbb {F}} \right\vert \). A basis \((e_i)\) of \(K\) over \(\mathbb {F}\) is self-dual when its Gram matrix for the trace form is the identity, \(\mathrm{tr}_{K / \mathbb {F}}(e_i e_j) = \delta _{ij}\), and normal when its vectors are the Frobenius orbit \(\alpha , \alpha ^q, \alpha ^{q^2}, \ldots \) of a single element \(\alpha \in K\).

A signed permutation of a finite set \(\Omega \) is a permutation \(\sigma \) of \(\Omega \) with a sign \((-1)^{s(j)}\) at each point: the permutation \(\pm j \mapsto \pm (-1)^{s(j)} \sigma (j)\) of the signed set \(\Omega _\pm = \{ \pm \} \times \Omega \), which commutes with the sign flip. They form a group, the semidirect product of \(\mathrm{Sym}(\Omega )\) and \(\mathbb {F}_2^\Omega \) (II:1057), which contains the sign flip \(-I\), the \(\pm 1\) diagonals, and, for two sets, the products \(g \times h\) acting on \((\Omega \times \Omega ')_\pm \) (II:3062). The matrix of a signed permutation is that of its action on the anti-symmetric functions in the basis \(B^-\) (II:1049), the signed permutation matrix \(e_j \mapsto (-1)^{s(j)} e_{\sigma (j)}\).

The sofic value is approximable when a computable function \(f\) of a test \(T\) and \(k \in \mathbb {N}\) satisfies \(|\mathrm{val}_{\mathrm{sof}}(T) - f(T, k)/(k+1)| \leq 1/(k+1)\) for all \(T\) and \(k\).

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).

The soundness clause of introspection, of answer reduction or of parallel repetition in the value model \(\omega \) is that stage’s soundness clause (Definitions 6.130 and 6.193, Theorem 6.196) with the value \(\mathrm{val}^*\) replaced by \(\omega \) on both sides, at the same parameters, error functions and answer bounds. In the model \(\mathrm{val}^*\) it is the stage’s own clause.

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.

A subgroup test over the free group \(F\) on \(n\) generators is a finite list of weighted challenges, each a finite list \(K\) of words and a decision on the subsets of \(K\), here in disjunctive normal form over the literals “the \(i\)-th word of \(K\) lies in (or out of) the subgroup”. A finite action \(\sigma \) of \(F\) on a set of size \(N \geq 1\) gives the finitely described IRS \(\Phi (\sigma )\), the stabilizer of a uniform point; its value against the test is the probability that the stabilizer passes a challenge drawn with probability proportional to its weight. The sofic value of the test is the supremum of the values of finite actions.

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 Boolean circuit \(C\) with three inputs of length \(m\) and three single-bit inputs succinctly describes the 3SAT formula on the \(2^m\) variables \(x_0, \ldots , x_{2^m - 1}\) whose clauses are the \(x_{i_1}^{o_1} \vee x_{i_2}^{o_2} \vee x_{i_3}^{o_3}\) with \(C(i_1, i_2, i_3, o_1, o_2, o_3) = 1\), integers presented to the circuit in binary ( [ 1 , Definition of succinct descriptions of 3SAT formulas, Section 10 ] ). A decoupled 5SAT formula has five blocks of variables and clauses with one literal from each block, evaluated on five separate assignments; a circuit with two inputs of length \(\ell \), three of length \(r\) and five single-bit inputs succinctly describes one in the same way. Such a circuit describes the decider \(\mathcal{D}\) on \((n, x, y)\) at time \(T\) if, for all \(a, b \in \{ 0,1\} ^{2^\ell }\), some three assignments complete \((a, b)\) to a satisfying tuple exactly when \(a\) and \(b\) are the two-bit tape encodings (\(0 \mapsto 00\), \(1 \mapsto 01\), blank \(\mapsto 10\)) of strings of length at most \(T\) on which \(\mathcal{D}\) accepts \((n, x, y, \cdot , \cdot )\) within \(T\) steps. Circuits have fan-in and fan-out at most two and a terminal output gate, and their size is the number of gates.

A vector state on a Hilbert space \(K\) is a unit vector \(\Psi \in K\), with the expectation \(\mathrm{ev}(X) = \mathrm{Re}\, \langle \Psi , X \Psi \rangle \) of a bounded operator \(X\) on \(K\). A symmetric model over a C\(^*\)-algebra \(\cal {P}\) consists of a vector state \(\Psi \) on \(K\), a unital \(*\)-homomorphism \(L : \cal {P} \to B(K)\), the first player’s placement, and a linear isometry \(J\) of \(K\) onto itself with \(J^2 = 1\) and \(J \Psi = \Psi \), such that \(L(x)\) commutes with \(J L(y) J\) for all \(x, y \in \cal {P}\). The flip is the \(*\)-automorphism \(X \mapsto J X J\) of \(B(K)\), and the second player’s placement is \(R = \mathrm{flip} \circ L\), so that \(L(x)\) and \(R(y)\) commute.

The vendored proof of Theorem 3.14 works with a state on \(\mathbb {C}^\iota \otimes \mathbb {C}^\iota \): its local operators are the \(\iota \times \iota \) matrices, its joint operators those of the tensor product, and its placements \(A \mapsto A \otimes I\) and \(A \mapsto I\otimes A\). A symmetric model replaces them by \(\cal {P}\), \(B(K)\), \(L\) and \(R\), and the Kronecker product \(A \otimes B\) by \(L(A)\, R(B)\). Measurements are generic over the ring of operators, local ones in \(\cal {P}\) and joint ones in \(B(K)\). A quantity that uses only the state, not the placements, belongs to the vector state, so that it applies as well to a state on one space, tensored with an ancilla, or reduced.

[\(\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)\).

[\(\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] 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})\).

\(\mathsf{V}\) is \(\lambda \)-bounded when, for every \(n \geq 2\), the sampler’s dimension and the running times of the three programs are at most \(n^\lambda \) — the running times read as in Definition 2.49, at degree \(\lambda \) in the size of the input — the lengths \(\cal {L}\) outputs are at most \(n^\lambda \), and \(\left\vert {\mathsf{V}} \right\vert \leq \lambda \). The answer-length calculator outputs in unary, as in the paper, but its running time is bounded relative to the size of its input, which is not bounded by \(n^\lambda \); so the running time does not bound the lengths by \(n^\lambda \), and that bound is a clause of its own. A verifier is within a budget at index \(n\) when the same quantities are bounded by the budget’s.

A tailored gap compression at level \(\ell \) is a polynomial-time procedure that maps a tailored verifier and \(\lambda \) to a tailored verifier whose sampler and answer-length calculator depend on \(\lambda \) only, the calculator halting on every question of the sampler, with running times, dimension and lengths at most a polynomial in \(n + \lambda \), such that for every \(\lambda \)-bounded input and every \(n \geq C_0\): a perfect ZPC strategy for \(\mathsf{V}_{2^n}\) gives one for \(\mathsf{V}'_n\); and \(\mathrm{val}^*(\mathsf{V}_{2^n}) \leq \frac12\) implies \(\mathrm{val}^*(\mathsf{V}'_n) \leq \frac12\).

Typed tailored data on a finite set of types \(T\) fixes, for each type, the numbers of readable and of linear answer bits, and, for each pair of typed questions, a list of controlled linear constraints. Its detyping is the tailored game on the detyped questions (a graph view followed by a content register, Lemma 6.13) in which a question has the lengths of the type its graph view decodes to, for either player, and none when it decodes to none; and a pair of questions has the typed constraints when the two views are Alice’s and Bob’s views of an edge, and no constraint otherwise. Answers are decoded and encoded through the type of their question.

A tailored game on a finite question set \(X\) is a distribution \(\mu \) on \(X \times X\) together with, at each question \(x\), a set \(S_x = S_x^R \cup S_x^L\), a disjoint union, of \(\ell ^R(x)\) readable and \(\ell ^L(x)\) linear formal variables, and, for each pair of questions \((x, y)\) and each assignment \(\gamma ^R\) of the readable variables at \(x\) and \(y\), a finite list \(L_{xy}(\gamma ^R)\) of vectors over the disjoint union \(S_x \cup S_y \cup \{ J\} \), the controlled linear constraints. The answer at \(x\) is an assignment \(a \in \mathbb {F}_2^{S_x}\), readable bits first. The canonical decider (II:1757–1787) accepts \((a, b)\) at \((x, y)\) when every \(c \in L_{xy}(a^R, b^R)\) satisfies \(\langle c, (a, b, 1)\rangle = 0\) over \(\mathbb {F}_2\), the coordinate \(J\) being set to \(1\); the empty list accepts every answer pair, and the list \(\{ J\} \) rejects every one. The tailored game defines a game (Definition 2.1) with answers the bit strings of bounded length, those of the wrong length losing, and its quantum value \(\mathrm{val}^*\). Its doubled game asks \((\mathsf{false}, x)\) and \((\mathsf{true}, y)\) with the weight of \((x, y)\) and no weight elsewhere; it is again a tailored game.

A tailored game description lists the number of vertices, the readable and linear lengths at each vertex, the question weights, and the controlled linear constraints as entries \((x, y, \gamma ^R, c)\), read as \(c \in L_{xy}(\gamma ^R)\). It denotes a synchronous game in the sense of Definition 2.43: questions are vertices, answers bit vectors of the maximal length that vanish beyond the vertex’s length, the weights are normalized as there, and acceptance is the canonical decider’s, unequal answers at a loop losing. ZPC strategies are Definition 9.4’s, the generators beyond a vertex’s length acting as the identity. These definitions are written on top of Mathlib alone, in MIPRE/TailoredGameValue.lean, beside the standalone statement of Theorem 7.1, whose game value they reuse.

Let a tailored gap compression be given, with compressed sampler \(\cal {S}^\lambda \) and answer-length calculator \(\cal {L}^\lambda \), a machine \(\cal {M}\), a search program \(\cal {S}'\) and a parameter \(\lambda \). The tailored halting verifier \(\mathsf{V}^{\cal {M},\lambda } = (\cal {S}^\lambda , \cal {L}^\lambda , \cal {P}^{\cal {M},\lambda })\) has for linear-constraints processor the efficient Kleene fixed point of the map that sends a processor \(\cal {P}\) to the program which, on \((n, x, y, a^R, b^R)\):

1. outputs the empty list of constraints if \(\cal {M}\) halts on the empty input within \(\lceil \log _2 (n+1) \rceil \) steps;

2. otherwise outputs the list \(\{ J\} \) if \(\cal {S}'\) halts on the description of \((\cal {S}^\lambda , \cal {L}^\lambda , \cal {P})\) within the same budget;

3. otherwise runs the compressed processor of \((\cal {S}^\lambda , \cal {L}^\lambda , \cal {P})\) on the input.

Items 1 and 3 are the paper’s map \(F\) (II:1900), the empty list accepting and \(\{ J\} \) rejecting every answer pair; item 2 is the search branch of the paper route of Theorem 6.214, which supplies the base case that the value form of compression lacks.

The proposition that the halting problem reduces to tailored games: the statement of Theorem 9.21, written in MIPRE/TailoredGameValue.lean on top of Mathlib alone. It is a definition, so that the conditional theorem proving it from a compression (Theorem 9.37) can name it while Theorem 9.21 awaits that compression.

A tailored verifier \(\mathsf{V}\) meets a tailored game \(G\) on questions \(X\) at an index \(n\) along a bijection \(e\) from \(X\) to the questions of \(\mathsf{V}\) at \(n\) when its sampler’s distribution at \(n\) is \(G\)’s weights along \(e\), its answer-length calculator outputs \(G\)’s readable and linear lengths at every question \(e(x)\), and its linear-constraints processor outputs \(G\)’s constraints at every pair \((e(x), e(y))\) and pair of readable answers.

A tailored game description presents a tailored game along a bijection of its vertices with the game’s questions when the weights, the numbers of readable and linear variables at each vertex, and the constraints at every pair of vertices and every readable part of the right length are the game’s.

The \(k\)-fold product of a tailored game \(\mathfrak {G}\) asks \(k\)-tuples of questions with the product distribution \(\prod _i \mu (x_i, y_i)\). The variables at \(\bar{x}\) are those of its coordinates, the readable ones first, as a tailored answer must have them: the readable variables of \(x_1, \ldots , x_k\) in this order, then their linear variables, so that \(\ell ^R(\bar{x}) = \sum _i \ell ^R(x_i)\) and \(\ell ^L(\bar{x}) = \sum _i \ell ^L(x_i)\). The constraints at \((\bar{x}, \bar{y})\) are those of every coordinate, each written over all the variables with zero coefficients outside its coordinate. A constraint is cut into its five blocks of coefficients — readable and linear at \(x_i\), readable and linear at \(y_i\), affine — by prefixes and suffixes, each put at its coordinate’s place among the variables of its kind; the blocks partition the constraint whatever its length, so a constraint of the wrong length pads to a vector of the wrong length, which the canonical decider rejects, as it rejects the constraint in its coordinate. No length is tested, so a program computes the padding as defined.

The repeated answer-length calculator, on \((n, x, \kappa )\) with the input sampler and calculator stored, asks the sampler for the dimension \(s\), computes \(k = k(n)\), cuts \(x\) into its \(k\) blocks of \(s\) bits, runs the input calculator on every block at both kinds, and outputs the concatenation of the outputs at the kind \(\kappa \). The repeated linear-constraints processor, on \((n, x, y, a^R, b^R)\), does the same for both questions, cuts \(a^R\) and \(b^R\) into the coordinates’ readable answers by the lengths it obtained, runs the input processor on every coordinate, and outputs every coordinate’s constraints padded as in Definition 9.47. Both are fixed programs with the input programs stored; every stage between the calls to the input programs is a polynomial-time function, and the calls go through one loop running a stored program on every element of a list through the universal machine.

The repeated verifier of \(\mathsf{V}\) at \((\lambda , \tau )\) has the repeated sampler of Theorem 6.196, \(k(n) = 2^{\tau (\left\vert {\lambda } \right\vert + \left\vert {n} \right\vert )}\) independent copies of \(\mathsf{V}\)’s, and two programs \(\cal {L}\) and \(\cal {P}\). Call a question of the \(n\)-th game good when \(\mathsf{V}\)’s answer-length calculator halts at each of its coordinates. The programs meet the specification at \(n\) when \(\cal {L}\) outputs at a good question the sums of the coordinates’ lengths and halts at no other question, and \(\cal {P}\), at good questions and readable answers of the right lengths, halts exactly when \(\mathsf{V}\)’s linear-constraints processor halts on every coordinate, and then outputs the constraints of the \(k(n)\)-fold product of \(\mathsf{V}_n\).

Let \(C = \max \{ C_0, 2\} \). A program \(\cal {S}'\) meets the search specification when, on the description of every \(\lambda \)-bounded tailored verifier \((\cal {S}^\lambda , \cal {L}^\lambda , \cal {P})\), it halts exactly when \(\mathrm{val}^*\) of that verifier at the level \(C\) exceeds \(\frac12\).

Question reduction (II:5712), answer reduction (II:6883) and parallel repetition (II:11103) for tailored verifiers, each in value form, with the parameters, budgets and soundness losses of the corresponding contracts of the existing pipeline (Definitions 6.130 and 6.193, Theorem 6.196): tailored verifiers in and out, the output’s answer-length calculator part of the data, completeness read in perfect ZPC strategies, and repetition’s soundness loss depending on a bound on the input’s lengths in place of a parse length.

The tabulation of a tailored verifier at index \(n\), under the budget \(T \cdot (\left\vert {d} \right\vert + 1)^k\), is the tailored game description whose vertices are the doubled questions \(\{ 0, 1\} \times \mathbb {F}_2^{s(n)}\), whose weights count the points of \(\mathbb {F}_2^{s(n)}\) landing on each pair of tagged marginals, and whose lengths and constraints are what the answer-length calculator and the linear-constraints processor output, each program run under the budget. On a description string, the verifier is \((\cal {S}^\lambda , \cal {L}^\lambda , \cal {P})\) for the string’s parameter \(\lambda \) and processor \(\cal {P}\), and the budget is \(n^\lambda \cdot (\left\vert {d} \right\vert +1)^\lambda \).

A tailored normal form verifier \(\mathsf{V}= (\cal {S}, \cal {L}, \cal {P})\) is a conditionally linear sampler \(\cal {S}\) (Definition 2.44), an answer-length calculator \(\cal {L}\), which on \((n, x, \kappa )\) outputs, in unary, the number of readable (\(\kappa = R\)) or linear (\(\kappa = L\)) variables at the question \(x\), and a linear-constraints processor \(\cal {P}\), which on \((n, x, y, a^R, b^R)\) outputs the list \(L_{xy}(a^R, b^R)\); the paper’s fourth machine, the canonical decider, is the same for every verifier (Definition 9.15). The outputs are read totally, so that none is malformed: a length as the length of the output’s spine, a list of constraints elementwise. The \(n\)-th game \(\mathsf{V}_n\) is the tailored game on the sampler’s questions that the programs compute, a question or pair at which a program does not halt rejecting every answer. \(\mathsf{V}\) has a perfect ZPC strategy at \(n\) when the doubled game of \(\mathsf{V}_n\) has one (Remark 9.5).

[\(\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.

A language \(L \subseteq \{ 0,1\} ^*\) is in the computable class \(\mathrm{TMIP}^*\) if there is a computable map \(g\) from bit strings to tailored game descriptions such that for every string \(z\): if \(z \in L\), then \(g(z)\) has a perfect ZPC strategy; if \(z \notin L\), then \(\mathrm{val}^*(g(z)) \leq \frac12\). As for Definition 2.53, there is no polynomial-time bound on \(g\).

A language \(L \subseteq \{ 0,1\} ^*\) is in \(\mathrm{TMIP}^*\) if there are three machines, a sampler, an answer-length calculator and a linear-constraints processor, and a polynomial \(P\), such that for every string \(z\), writing \(B = P(\left\vert {z} \right\vert )\):

1. Efficiency. The sampler is as in Definition 2.52: on \(z\) and a uniform seed \(r \in \{ 0,1\} ^B\) it halts within time \(P(\left\vert {z} \right\vert + \left\vert {r} \right\vert )\) with a pair of strings of length at most \(B\); write \(\mu _z\) for their distribution. On \((z, x, \kappa )\) the calculator, and on \((z, x, y, a^R, b^R)\) the processor, halt within time \(P\) of the total input length. The tailored game \(\mathfrak {G}_z\) has the strings of length at most \(B\) as its questions, the distribution \(\mu _z\), the lengths the calculator outputs and the constraints the processor outputs, read as for a tailored normal form verifier (Definition 9.13).

2. Completeness. If \(z \in L\), the doubled game of \(\mathfrak {G}_z\) has a perfect ZPC strategy.

3. Soundness. If \(z \notin L\), then \(\mathrm{val}^*(\mathfrak {G}_z) \leq \frac12\).

A typed decider receives \((n,t,x,u,y,a,b)\); a timeout rejects regardless of the output tape. A typed normal verifier is over \(\mathbb {F}_2\) and first uses the sampler’s dimension query to check \(t,u\in T\) and \(|x|=|y|=s(n)\). In timeout-counter form, its bound dominates this preliminary computation. For finite decider runtime the answer alphabet consists of strings of length at most \(\mathsf{TIME}_D(n)\), and the decision predicate is total. In the ambient model there is no timeout counter: totality is a hypothesis on the typed decider, supplied by the clock of Lemma 6.23, and the answer bound is the executable inner and outer cut of Lemma 6.21.

Let \(G=(T,E)\) be a finite undirected type graph with \(m_G\geq 1\) edges and \(k_G\) loops. Sample an ordered adjacent type pair uniformly from its \(2m_G-k_G\) possibilities, and independently a common uniform \(z\in \mathbb {F}_{q(n)}^{s(n)}\). Output \(((t,L_t^\textsc{A}(z)),(u,L_u^\textsc{B}(z)))\). A typed sampler exposes dimension, marginal, level-linear and factor-support queries for each type. It computes the prescribed bounds before parsing auxiliary inputs, inspects at most the bound plus one symbol per component, and halts with a fixed default on malformed input. Computing the bounds is charged in its runtime. Linear and factor-query correctness is required only on valid prefix images; image membership is not a parsing obligation. No field-size query is implicit in this interface. In the ambient model a typed sampler is binary, and bounded-prefix parsing is replaced by halting on every input together with a polynomial budget (TypedSampler.TimeBoundAt); linear and factor correctness are required on valid prefixes, as here.

A value model \(\omega \) assigns to every finite game \(\mathfrak {G}\) a real number \(\omega (\mathfrak {G})\) such that \(\mathrm{val}^*(\mathfrak {G}) \leq \omega (\mathfrak {G}) \leq 1\), and such that \(\omega \) is invariant under relabeling of the four alphabets, monotone in the decision predicate, zero on a game that rejects everything, unchanged by padding the answer alphabets with always-rejected answers, and unchanged by the doubling of the question set. The two models are \(\mathrm{val}^*\) (Definition 2.9) and \(\omega ^{\mathrm{co}}\) (Definition 5.3), and every statement below in a model \(\omega \) is one theorem in Lean, instantiated twice. The value of \(\mathsf{V}_n\) in the model is \(\omega (\mathsf{V}_n)\), at an answer bound. The model is r.e. from below if the set of triples \((d, p, q)\) with \(p/q {\lt} \omega (\mathfrak {G}_d)\) is recursively enumerable, in the threshold encoding of Lemma 3.112, and r.e. from above if the set with \(\omega (\mathfrak {G}_d) {\lt} p/q\) is: \(\mathrm{val}^*\) is r.e. from below (Lemma 3.112) and \(\omega ^{\mathrm{co}}\) from above (Lemma 8.14), and neither has the other direction, by the two theorems themselves. A halting reduction of \(\mathrm{RE}\) shape to \(\omega \) is a computable map from machines to game descriptions with \(\omega = 1\) on the machines that halt on the empty input and \(\omega \leq \frac12\) on the others; the \(\mathrm{coRE}\) shape is the reverse. The class \(\mathrm{MIP}(\omega )\) is the set of languages \(L\) for which some computable map \(g\) from strings to game descriptions has \(\omega (\mathfrak {G}_{g(z)}) = 1\) for \(z \in L\) and \(\omega (\mathfrak {G}_{g(z)}) \leq \frac12\) for \(z \notin L\); \(\mathrm{MIP}^*\) of Definition 2.53 is \(\mathrm{MIP}(\mathrm{val}^*)\).

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.

A signed permutation matrix on \(\mathbb {C}^m\) is a matrix \(e_j \mapsto (-1)^{s(j)} e_{\sigma (j)}\) for a permutation \(\sigma \) of \(\{ 1, \dots , m\} \) and signs \(s\): the action of a signed permutation of \(\{ \pm \} \times \{ 1, \dots , m\} \) on the anti-symmetric functions, in their standard basis. A permutation strategy for a tailored game assigns to each variable \(X\) at each question \(x\) an observable \(U(x, X)\) on \(\mathbb {C}^m\) that is a signed permutation matrix and an involution, the observables at a question commuting with each other; its measurement at \(x\) is the Fourier transform

and its value is \(\sum _{x, y} \mu (x, y) \sum _{a, b} \mathrm{tr}(P^x_a P^y_b)/m\) over the accepted \((a, b)\). It is Z-aligned when the observables of readable variables are diagonal, and commutes along edges when \(U(x, X)\) and \(U(y, Y)\) commute whenever \(\mu (x, y) {\gt} 0\). A ZPC strategy is a Z-aligned permutation strategy commuting along edges, and it is perfect when its value is \(1\).

A permutation strategy for a tailored game (signed permutation observables, involutions commuting at each vertex, diagonal at the readable variables, the identity beyond each vertex’s length) need not commute along edges; its Fourier-transform measurements still form a synchronous strategy, with the same value, so its value is at most the game’s synchronous value.

Let \(\mathrm{ind}_m(x) \in \mathbb {F}_q^M\), \(M = 2^m\), be the vector \((\mathrm{ind}_{m,y}(x))_y\) of the indicator polynomials of Definition 6.149 evaluated at a point \(x \in \mathbb {F}_q^m\), and call a tuple \(\omega = (u_X, u_Z, r_X, r_Z) \in (\mathbb {F}_q^m)^2 \times \mathbb {F}_q^2\) anticommuting if

the inner product being the one of \(\mathbb {F}_q^M\), and commuting otherwise. The two cases partition the sample space. If \(m \geq 1\) and \(d \geq 1\) then a uniformly random \(\omega \) is anticommuting with probability at least \((1 - 3md/q)/2\), and commuting with probability at least \((1 - 3md/q)/2\).

For every \(k \geq 1\) there is a field of size \(2^k\) together with a \(k\)-bit representation of its elements admitting a left inverse; that is, MIPRE.SAT.BinField \(k\) is inhabited.

Let \(\mathcal{H}\) be a Hilbert space and \(\iota \), \(\alpha \), \(\beta \) finite sets.

1. An operator \(T\) on \(\mathcal{H}\otimes \mathbb {C}^\iota \) is the operator of the matrix of its compressions \(T_{ij}\), from the \(j\)-th copy of \(\mathcal{H}\) to the \(i\)-th; the matrix of the operator of a matrix is that matrix; and \(T\) commutes with the operator of a matrix of operators exactly when the matrix of \(T\) commutes with that matrix.

2. A matrix over a ring commutes with the constant diagonal matrix of an element \(f\) exactly when its entries commute with \(f\). An \((\alpha \times \beta )\)-matrix commuting with every \(I_\alpha \otimes E_{bb'}\) is \(X \otimes I_\beta \), and symmetrically. The matrix units of a register are generated by its diagonal projections and the projection \(|u\rangle \langle u|\) onto its uniform superposition: \(E_{bb'} = |\beta |\, E_{bb} |u\rangle \langle u| E_{b'b'}\).

3. Consequently, if \(\beta \) is nonempty and an operator \(T\) on \(\mathcal{H}\otimes \mathbb {C}^{\alpha \times \beta }\) commutes with \(f \otimes I\) for every \(f\) in a set \(s\) of operators and with every \(I_\alpha \otimes E_{bb'}\), then \(T = X \otimes I_\beta \) with every entry of \(X\) commuting with \(s\); and symmetrically for the other register. The matrices of one register act injectively when the other is nonempty, and both registers of a unit vector are nonempty.

An element commuting with a \(*\)-closed set lies in its commutant, and \(\{ P, I- P\} \) is a projective measurement for every orthogonal projection \(P\).

Let \(\mathscr {A}\) and \(\cal {B}\) be tracial algebras in standard form, and suppose that \(\cal {B}\) has unital dyadic matrix units (Definition 8.103).

• (A) For every vector \(\psi \), the standard-form model of \(\mathscr {A}\otimes \cal {B}\) — the commutant \(\cal {N}\) of its right action and the commutant \(\cal {N}'\) of \(\cal {N}\), as the players’ algebras, in the state \(\psi \) — is a dyadic pair (Definition 8.107).

• (T) A tracial strategy \((\sigma , E, F)\) in \(\mathscr {A}\) gives the tracial strategy \((\sigma \otimes 1, E \otimes 1, F \otimes 1)\) in \(\mathscr {A}\otimes \cal {B}\), with the same correlation.

Consequently, for every game with nonempty alphabets and every \(\lambda {\lt} \omega ^{\mathrm{co}}\), there is a tracial strategy of winning probability greater than \(\lambda \) whose standard-form model is a dyadic pair in every state.

In the ancilla extension by \(e\) of a bipartite model:

1. for \(X \in \mathscr {A}_A\), \(Y \in \mathscr {A}_B\) and positive semidefinite \(P \in M_\alpha (\mathbb {C})\) and \(Q \in M_\beta (\mathbb {C})\), the Born probability of \((X \otimes P, Y \otimes Q)\) is the model’s Born probability of \((X, Y)\) times \(\mathrm{Re}\langle e, (P \otimes Q) e\rangle \);

2. an operator with an inert ancilla keeps its norm up to the norm of \(e\): \(\| \pi (X \otimes I)(\psi \otimes e)\| = \| e\| \, \| \pi (X)\psi \| \), for either player;

3. \(\| \psi \otimes e\| = \| \psi \| \, \| e\| \);

4. if \((P_i)_i\) is a projective measurement in \(\mathscr {A}_A\) and \((Q_k)_k\) one in \(M_\alpha (\mathbb {C})\), then \((P_i \otimes Q_k)_{(i,k)}\) is a projective measurement in \(M_\alpha (\mathscr {A}_A)\).

Adjoining an inert ancilla in a unit vector \(e\), relabelling the registers of an ancilla extension along bijections, reading an extension of an extension as the extension by the product registers, and exchanging the players of an extension are local isometries between ancilla extensions of a model that carry the state exactly to the state.

The ambient contract MIPRE.AnswerReduction 5 is inhabited.

If \(L\leq B\) and \(s+1\leq B\), then \(L(s+1)^\mu \leq B^{\mu +1}\). Consequently the ambient answer-reduction contract retains the input sampler’s degree in its output budget: a universal base polynomial is raised to \(\mu +1\), and the base output degree is multiplied by \(\mu +1\). This arithmetic bound does not construct the answer-reduction program or its clock.

For each seed, extract the input and proof polynomial PVMs, averaged with the source’s conditional question laws. One common family \(G_i\) can be used on both copies, for \(i=1,\ldots ,5\). To derive this, choose one side’s LDT output, use swap invariance of the state to transport its point relation, then point self-consistency and polynomial separation to obtain cross-copy consistency; average the resulting errors using Jensen. Identical point operators alone do not make the two existential LDT outputs identical. The resulting evaluation and full-polynomial consistency error is denoted \(\kappa =O(\sqrt E+\rho )\) with \(E,\rho \) as below. The Lean keeps one extracted family per player, \(G^A_i\) and \(G^B_i\), with their consistency, rather than a single common family; the errors are averaged over the seed by concavity of \(\varepsilon \mapsto \varepsilon ^{b'}\). It extracts in a bipartite model in which the seeded test is sound (Definition 8.65), a hypothesis the tensor-product model satisfies by the theorem itself (Lemma 8.66).

A perfect PCC input witness gives a perfect typed answer-reduction witness, using the complete honest proof tuple and one combined measurement rule on both players. All queried formats are satisfied; mismatched proof branches use a whole legal zero tuple. Apply detyping completeness, including its identical-operator property, to obtain the exterior PCC witness. In the ambient form, for \(\lambda ,\mu \geq 1\): an input within inBudget \(\lambda \) \(\mu \) \(n\) with \(\left\vert {\mathcal{D}} \right\vert \leq \sigma \) and a value-\(1\) PCC strategy at the answer cut \(2^{(\lambda n+1)^\mu }\) gives the answer-reduced verifier a value-\(1\) PCC strategy at the answer cut \(32(k+1)(m'+7)^2\), and so at the output bound. Two hypotheses on the PCP decider are used: its field is the Shoup field the sampler downsizes along (ShoupField), and, for the output bound, its parameters are polynomial in \((\log n,\log T,Q,\sigma )\) (ParamsBound, as in Lemma 6.179).

With the parameter and timeout hypotheses of Theorem 6.192, construct the typed oracle verifier and the PCP verifier. Downsize the PCP sampler using its explicit field routine before taking the direct sum with the binary oracle sampler. This yields a common binary ambient space and \(\max \{ \ell ,3\} \) typed levels, hence \(\max \{ \ell +2,5\} \) levels after detyping. The compiled timeout and actual runtimes have the claimed polynomial bounds. Format checks include all proof coefficients and answer components. In the ambient model, for a PCP decider whose parameters are polynomial in \((\log n,\log T,Q,\sigma )\): the output’s programs are polynomial-time functions of the input programs and \((\lambda ,\mu ,\sigma )\), and for a polynomial \(P\) and degree \(d\) depending only on the PCP, an input within the budget of Definition 6.193 with \(|S|,|D|\le \sigma \) gives an output within \(P((\lambda n+1)^\mu +\sigma +\lambda +n)^{\mu +1}\) at input-size degree \(d(\mu +1)\) that rejects answers longer than its cut \(32(k+1)(m'+7)^2\).

Let \(P\) be a projective measurement on \(\mathbb {C}^m\). A bit of its outcome that is a function of some Z-bits of \(P\) (bits whose observables are diagonal signed permutations) is a Z-bit. A bit that is, for each value of those Z-bits, an \(\mathbb {F}_2\)-affine function of some X-bits of \(P\) (bits whose observables are signed permutations) is an X-bit. The answer bits of the synchronous strategy of a permutation strategy are X-bits, and Z-bits below the readable length.

Under the hypotheses of Definition 9.116, the input game accepts an oracle’s decoded pair whenever its polynomials are block-local and pass densely. So at a seed, the decoded strategy fails each of the nine ordered pairs of roles at most as often as an oracle’s outcome is not block-local or does not pass densely, plus the disagreements of the polynomial measurements its two answers are decoded from.

If \(q \geq 2 (M + 1) d\) and \(q \geq 2 m (5 + 6 (d + 1))\), the decoded strategy fails the typed oracularized game of the input with probability at most

which is strictly increasing in \(\theta \geq 0\) and at least \(\theta \).

Decode the polynomial strategy to the oracle strategy, applying the length-\(B_D(n)\) prefix cutoff to each original answer. It preserves the simulated decider’s output both before and after the oracle construction, and makes every decoded answer pass its bounded parser. Check all three oracle subtests. Group malformed or failed decodings into fixed legal outcomes so measurements remain complete. The final conversion to the input game yields deficit \(O(\delta _3^{1/4})\). The Lean decodes without the sandwich and without a cutoff. An oracle measures the complete \(J\) and answers the pair decoded from its first two answer polynomials, read on their blocks; an isolated player measures its own copy’s \(G\) and answers the decoded polynomial. The decoder returns the answer of length at most \(2^{(\lambda n+1)^\mu }\) whose answer vector the polynomial’s Boolean values are. No truncation is needed: the PCP’s soundness gives accepted answers of length at most \(T\), and an input within its budget rejects answers longer than \(2^{(\lambda n+1)^\mu }\), so accepted answers already fit its alphabet, where the answer vector determines them. The oracle’s game check fails only where \(J\)’s outcome is not placed on its blocks, or the PCP check rejects it at half the points; each ordered pair of roles fails at most by a game check and the disagreement of the polynomials. The decoded POVM strategy fails the typed oracularized game with probability at most \(6\) times the combined error. Its measurements are coarse-grainings of the extracted projective ones, so it is a projective strategy in the model with no dilation, and oracularization soundness (one square root) gives \(\omega (\mathsf{V}_n)\geq 1-24\sqrt{7\, \mathrm{err}}\) in every value model \(\omega \) in which oracularization is sound (Definition 8.60) and which dominates the model (Definition 8.62); in particular \(\mathrm{val}^*(\mathsf{V}_n)\).

There is \(E_{2,0}\) such that for constants with \(E_2 \geq E_{2,0}\) the field-size conditions of Theorem 9.154 hold, and there are \(a \geq 1\) and \(C\) with \(24 \sqrt{e(16^9 \varepsilon )} \leq \delta (\varepsilon , n)\), \(\delta \) the loss of the answer reduction contract with \(b = c_{\mathrm{LD}}/2\), or \(\delta \geq 1\), for \(n \geq \max (C, 2)\), \(\lambda , \sigma \geq 1\).

Put \(L=(\lambda n)^\mu \), \(\rho =m'd/q\) and \(E=\delta _{\mathrm{CL}}(\theta ,q,m',d,m'+6)\) for the source parameter routine. The comparison with the smaller-\(m\) LDT error uses its field-error floor \(E{\gt}4^{-b'}/L\) and the bound \(a'(dm)^{a'}2^{-b'md}\leq C/L\) for sufficiently large \(n\), with \(m\geq \lambda \mu n\) and \(d=7\). Here \(a',b'\) are the fixed seeded-LDT constants; the polynomial prefactor is absorbed into the exponential. It does not reverse the exponential inequality when \(m'\geq m\). The quantitative chain is

Choose a universal final exponent strictly below \(\min \{ b'/16,1/16\} \) and enlarge the polynomial coefficient and threshold to absorb every constant. This gives the displayed error of Theorem 6.192. When that error is at least one the value conclusion is trivial; the nontrivial regime also justifies the small-error inequalities above.

In the Lean, without the sandwich, the chain has one square root, from oracularization, and the exponent is \(b=b'/2\). The field term \(q^{-b'}\) of the low-degree test has the prefactor \(a'(7m'(m'+6))^{a'}\), polynomial in \(m'\) of degree about \(2a'\), and is controlled by a hypothesis on the PCP decider, FieldLarge: for every exponent \(e\), past a threshold on \(Q\), its field has at least \((8(Q+1)m')^{e}\) elements; it is used at \(e=40000(3\lceil a'\rceil +4)\), and a field of \(2^{O(\log ^2(Qm'))}\) elements satisfies it. Theorem 6.164 does not carry the paper’s lower bound on \(q\) (eq:pcp-q-choice); this is it, beside ParamsBound and ShoupField. The term \(2^{-b'md}\) uses \(m\geq Q\), from \(2^m\geq 2T\), and the threshold on \(n\); \(\mu =0\) and \(\varepsilon \geq 1\) are trivial, the loss being at least \(1\) there. The constants are explicit, \(a\) a function of the parameter polynomial alone and the threshold the larger of the two above, and the assembly is stated for a projective strategy in a bipartite model in which the seeded test is sound (val_ge_of_arStrategy), for every value model in which oracularization is sound and which dominates the model; the clause in \(\mathrm{val}^*\) is its tensor-product case, and the clause in \(\omega ^{\mathrm{co}}\) (Theorem 8.67) the commuting-operator case, at the same constants.

Let \(\Delta \) be at least the number of equations times \(N = \ell _A + \ell _B\). A solution \(f\) gives the solution \((f, f(\ell _A + \cdot ), \mathrm{ext}\, f, \mathrm{ext}\, f, \mathrm{ext}\, f)\) of the decoupled triangulated system on \(\ell = N + \Delta \), and the first two blocks of any solution, glued, solve the equations. For the canonical decider (claim:properties_of_L*, item 2): if the game accepts answers of the right lengths, the extension of the table of their linear parts solves the decoupled triangulated purified system, the last three blocks linear in the linear answers with coefficients depending only on the readable ones; and if five assignments solve that system, the game accepts the readable answers completed by the first two blocks, read at the linear lengths.

A field equation \(E(z) = c\) over \(\mathbb {F}_q\), linear in the answer bits \(z \in \mathbb {F}_2^N\), gives \(t\) constraints: for each \(s {\lt} t\), the \(s\)-th coordinates of \(E\) at the \(N\) unit vectors, then that of \(c\). A program computing the Shoup bits of \(E(z)\) at every \(z\) of length \(N\), and one computing those of \(c\), therefore give a program computing the constraints, which runs the first on the unit vectors and transposes; likewise for an indexed list of equations. A field element of the answer bits is a window of \(t\) bits. Sums, products, \(0\), \(1\), \(g (1 - g)\), indexed sums and comparisons of programs computing field elements in their Shoup bits compute the corresponding sums, products, constants and comparisons.

Embed each of the five scalar polynomial alphabets into the full individual-degree-\(d\) alphabet on \(m'\) variables by zero-projector extension. Use the \((m'+1)\)-tuple of constraint polynomials as a sixth alphabet; the complete \(J\) now has literally the product of the six alphabets as outcomes. For either scalars or tuples, unequal outcomes agree at a uniform point with probability at most \(\rho =m'd/q\): one unequal component witnesses the tuple bound, with no tuple-length factor. Apply Lemma 6.170 with the full seed as index and the evaluation point uniform independently of it. Reverse the six-index order so the constraint-tuple marginal of \(J\) is innermost. The resulting giant sandwich has error \(\delta _3=O(\sqrt{\kappa +\rho })=O((\sqrt E+\rho )^{1/2})\). The Lean proof does not use this lemma. The oracle there measures the complete \(J\) itself, and what the sandwich provides is replaced by a Schwartz–Zippel comparison: the \(i\)-th component of \(J\)’s outcome agrees at a uniform point with the placement on its block of the other player’s \(G_i\) outcome, except with probability \(O(E+\theta )\), and two distinct individual-degree-\(d\) polynomials agree there with probability at most \(\rho \). So \(J\)’s outcome is placed on its blocks, and equal to the placed \(G_i\) outcome, except with probability \(O(E+\theta +\rho )\).

Conditioning the typed success estimate on each checked type pair gives the global PCP subtests with \(O(\theta )\) failure, averaged over uniform \(\xi \) and the prescribed PCP seed. Retain the joint proof-tuple format, individual proof-line formats, and all identical-question equality subtests. No low-degree theorem is applied to line–point success alone.

The answer bits of an isolated player’s honest answer are X-bits of the input strategy’s measurement at its question, and its readable answer bits are Z-bits; the same holds of the oracle’s honest answer and the input strategy’s measurements at both questions of its seed, jointly.

At two typed questions read off one seed, honest answers to answers of the oracularized input game that its predicate accepts pass the four checks of the answer-reduced predicate, for a degree \(d \geq 17\).

Let the circuit of a seed be the window describer’s description of the output indicator at the constant parameters \((\ell , \Delta )\), through the windows \(\ell + 1, \ell + 1, o + 1\), at \((n, T, Q, \sigma ')\), padded to \(s\) gates. If \(E_1 \geq 2E\) and \(c_0\) is the constant of Lemma 9.163, then for every input tailored verifier within the input budget of answer reduction at \(n\), with \(|\mathsf{V}| \leq \sigma \) and \(\lambda , \mu \geq 1\), the hypotheses of Definition 9.116 hold at the description time \(T\).

The check is a polynomial-time function of its input, and decides the check of Definition 9.99. The output indicator accepts \((n, x, y, a, b)\) exactly when the answer-length calculator gives the four lengths, the processor gives the constraints on the cut readable answers, and the check passes. If the two programs halt within \(T (|d| + 1)^k\) on every input \((n, d)\), the output indicator halts on \((n, x, y, a, b)\) within an explicit bound, polynomial in \(T\), in the size of the input and in the time bound of the check, and so accepts what it accepts within that bound.

(1) On readable answers of the readable lengths, padded with zeros to \(N\) bits, the check passes for \(O\) the table, when the lengths are at most \(N\) and \(D\) is large enough; and \(O\) is the only string it accepts after them. (2) When the check passes on the lengths and constraints of the game at \((x, y)\), five assignments satisfying the table held by \(a\) give answers that the game accepts: the readable answers completed by the first two blocks, read at the linear lengths. (3) Answers of the right lengths that the game accepts give the satisfying 5-tuple \(\mathsf{Extend}\) of the table, the last three blocks linear in the linear answers.

The table is the output of the loops over the coordinates, the signs outermost and the first coordinate innermost. If \(N {\gt} 0\), \(2N \le D\) and the triangulated equations are below \(D\), five assignments satisfy the table exactly when they satisfy the decoupled system.

The two input-codeword tests, conditioned on their respective typed questions, have \(O(\theta )\) failure on the required seeded point/line laws. The distributions are conditioned before averaging over \(\xi \), and include answer formats and equality tests. These supply both input evaluation relations consumed by the individual-polynomial extraction.

For a selector computed by the introspection stage’s selector program, a program computes the constraints of the low-degree checks at two questions of one role from the parameters, the types, the two questions’ low-degree bits and the layout of the answers: the equations that two answers agree codeword by codeword, each the difference of two windows, and the equations that the line polynomials at the line parameter are the point values, by Horner’s rule.

Represent a vector of the registers \(\mathbb {F}_q^{D}\) of the seeded low-degree test, \(D = 2M + 1\), by its coordinates’ Shoup bits, \(t\) per coordinate: three runs of \(t\)-bit blocks, \(M\) for the point, \(M\) for the direction and one for the seed. On such bits, the run functions of the MIP* answer reduction’s stage program, on one copy of the test at offset \(0\) and length \(M\), return the bits of the answers of the test’s presentation to its marginal, linear-map and factor queries. So for parameters \(t \geq 1\) and \(j \leq t\) at every index, computed by a closed program, the presentation, downsized along the Shoup basis, is a sampler answered directly by a polynomial-time function of the parameters.

The answer-length calculator at \((\lambda , \mu , \sigma )\), on \((n, x, \kappa )\), runs the routine’s parameter program on \(((\lambda , \mu , \sigma ), n)\) as a stage, then decodes the graph view of \(x\) with \(\kappa \) into the two factors of a length by a finite table and multiplies them with \(t\) in unary, an undecodable view giving \(0\). It halts on every input, at a detyped question it outputs the readable and the linear lengths of the presented answer-reduced game, and its program is computed from \((\lambda , \mu , \sigma )\) in polynomial time.

The answer-length calculator halts on every input. For a parameter routine in polynomial time, it runs at \(n\), on every input \((n, d)\), within \((C (W + 1)^M X^E)^{\mu + 1}\) for every \(X {\gt} |d|\) and \(W \geq (\lambda n + 1)^\mu + \sigma + \lambda + n\), and the lengths it outputs are at most \((C (W + 1)^M)^{\mu + 1}\), for \(C\), \(M\) and \(E\) depending only on the routine.

For every \(m\) and \(d\) there is a linear map \(f \mapsto (c_i(f))_i\) from polynomials in \(m\) variables over a field to \(m\)-tuples of polynomials of individual degree at most \(d\) such that \(f = \sum _i c_i(f) X_i (1 - X_i)\) whenever \(f\) has individual degree at most \(d\) and vanishes on \(\{ 0, 1\} ^m\).

At every index and every pair of detyped questions and readable answers, the processor halts with the presented answer-reduced game’s constraints.

A program decodes, by a finite table, the edge on which the graph views of two detyped questions lie, checks that the readable answers have their questions’ readable lengths, and on the edge’s pair of types concatenates the low-degree checks at one role, the consistency checks at one low-degree type, the indifference checks of both answers, and the proof checks of the oracle point answers, the last given as its input. When the proof checks given are those of the two questions at the circuits of their seeds, it outputs the presented answer-reduced game’s constraints at the two questions.

For a parameter routine in polynomial time there are \(C\), \(M\) and \(E\) such that, for every \(W \geq (\lambda n + 1)^\mu + \sigma + \lambda + n\), every input verifier with \(|\mathsf{V}| \leq \sigma \) whose sampler runs within \((\lambda n + 1)^\mu (|d| + 1)^\mu \) at \(n\), and every input \((n, d)\) and \(X {\gt} |d|\), the processor halts within \((C (W + 1)^M X^E)^{\mu + 1}\) steps.

A readable polynomial of the honest PCP depends only on the readable answers; a linear one is, the readable answers fixed, \(\mathbb {F}_2\)-affine in the linear answers. Alice’s polynomials depend only on her question and answer, when that answer carries its readable part and the part fits the table, and Bob’s only on his; so they are the oracle’s in the same slots. The PCP has individual degree at most \(17\), and under the hypotheses of Definition 9.116 the PCP of an answer pair the input game accepts satisfies the thirteen checks identically.

\(m {\lt} 2^j\); once \(E_2 \geq 1\), \(1 \leq t\) and \(j \leq t\); once \(E_1 \geq 1\), \(Q \leq K\) and \(o \leq K\).

Over a field of characteristic two, the honest PCP has degree \(17\) and its assignment checks hold identically. For the circuit polynomial of a well-formed circuit with the PCP’s inputs, its formula check holds identically when the window tables, \(\pi \cdot t(u)\) at the index of parity \(\pi \) and cell \(u\), and the witness tables satisfy the formula that the circuit describes; its system check holds identically when the linear tables satisfy the system that the table \(O\) holds.

Let a circuit describe the output indicator \(L^*\) of a tailored verifier \(\mathsf{V}\) at \((n, x, y)\) through windows of index lengths \(\ell + 1\), \(\ell + 1\) and \(|S_0| + 1\), the parameter program giving \((\ell , \delta )\) at \(n\). To answers \(a^R a^L\) and \(b^R b^L\) at \((x, y)\) associate the readable tables of the readable answers padded with zeros to \(2^\ell \) bits, of the table \(O\) of the decoupled triangulated purified system, and of witnesses of the formula for their windows, which depend only on \(a^R, b^R\); and the linear tables \(\mathsf{Extend}(a^L, b^L)\), which are \(\mathbb {F}_2\)-linear in \(a^L, b^L\). If the game \(\mathsf{V}_n\) accepts the answers, the lengths fit \(2^\ell \) and \(2^\delta \), the programs of \(\mathsf{V}\) halt at \(x\) and \(y\), and \(L^*\) accepts the padded strings within the describer’s time, then the honest PCP of these tables satisfies the thirteen checks identically.

The readable part of the honest PCP, the readable assignments and their helpers, depends only on the readable tables. Its linear part is \(\mathbb {F}_2\)-affine in the linear tables: the linear assignments and their helpers are additive, and the helpers of the system check affine. The tables of the encodings on the cube are the encoded tables.

The thirteen checks pass at a point exactly when thirteen polynomials vanish there, of individual degree at most \(d_T + 6(d + 1)\) for a PCP of degree \(d\) and a circuit polynomial of individual degree \(d_T\). A PCP of degree \(d\) over \(\mathbb {F}_q\) passing the checks on a set of points of density more than \(m (d_T + 6(d + 1))/q\) has all thirteen polynomials zero, and so satisfies the checks identically.

Over a field of characteristic two, let a PCP satisfy the checks identically for the circuit polynomial of a well-formed circuit with the PCP’s inputs. Then every assignment is \(0\) or \(1\) on the Boolean cube; the tables of \(g_{La}\), \(g_{Lb}\) and the \(g_{L,k}\) satisfy the system that the table of \(g_O\) holds; and the tables of the windows, \(\pi \cdot g(u)\) at the index of parity \(\pi \) and cell \(u\) for \(g = g_A, g_B, g_O\), with the tables of the \(g_{W,k}\), satisfy the decoupled 6SAT formula that the circuit describes.

The sandwiched polynomial measurements define the intermediate strategy on the same state. Transfer acceptance through the complete tuple \(J\), including its constraint polynomials and tested formats, to obtain success \(1-O(\sqrt{\delta _3})\). The proof uses the full-tuple relations of Lemma 6.186, not independently chosen evaluations. The Lean proof does not use this lemma: its decoded strategy (Lemma 6.189) measures \(J\) and the extracted \(G_i\) directly.

A program computes, from the parameters, the offset and length of the answer bits, the coordinates of a point \(p\), the oracle’s readable answer and the gates of a well-formed circuit with the PCP’s numbers of inputs and gates, the constraints of the proof check of the oracle’s point answer: the readable checks of Lemma 9.148 as a guard, then the system check and the five linear assignment checks at \(p\), as field equations in the answer bits.

A program computes, from the coordinates of a point \(p \in \mathbb {F}_q^m\) and the gates of a well-formed circuit with \(n_{\mathrm{in}}\) inputs and \(s\) gates, \(n_{\mathrm{in}} + s = m\), the value at \(p\) of the circuit’s polynomial. A program computes, from the parameters, the coordinates of \(p\), the oracle’s readable answer and the gates of such a circuit with the PCP’s numbers of inputs and gates, whether the readable values the answer decodes to pass the formula check and the six assignment checks at \(p\).

A constraint holds of answers of the right lengths exactly when its purified equation holds of the table of their linear parts. So a tailored game accepts \((a^R a^L, b^R b^L)\) at \((x, y)\) exactly when the purified equations of \(L_{xy}(a^R, b^R)\) hold of the table.

For constants with \(E_2 \geq 1\) the parameters of Definition 9.160 form a parameter routine: a closed program computes them from \(((\lambda , \mu , \sigma ), n)\) in polynomial time in the sense of Definition 9.155, and the circuit function computing the padded descriptions of Lemma 9.164 is a polynomial-time function. Its circuits satisfy the honest PCPs’ hypotheses for every input within the input budget.

Along the numbering of the detyped coordinates, the answer-reduced sampler’s question distribution at \(n\) is the detyped game’s, and so the presented answer-reduced game’s weights.

The output sampler is determined by \((S,\lambda ,\ell ,\mu ,\sigma )\), independent of the input decider’s code. The typed oracle sampler uses only \(S\); PCP parameters use only the supplied numerical bounds; downsizing uses their explicit field routine; and detyping’s sampler uses only its sampler and fixed graph. This supplies the source premise used by compression’s sampler-independence argument (ledger node \(1.5.1\)). The already checked conditional compression theorem keeps its existing Lean proof and premises.

For a parameter routine in polynomial time there are \(C\), \(M\) and \(E\) such that, for every \(W \geq (\lambda n + 1)^\mu + \sigma + \lambda + n\) and every input sampler \(S\) with \(|S| \leq W\) running within \((\lambda n + 1)^\mu (|d| + 1)^\mu \) at \(n\), the answer-reduced sampler runs within \((C (W + 1)^M)^{\mu + 1} (|d| + 1)^{E (\mu + 1)}\) at \(n\); and when the dimension of \(S\) at \(n\) is at most \(W\), the answer-reduced sampler’s dimension at \(n\) is at most \((C (W + 1)^M)^{\mu + 1}\).

Let \(k\geq 0\). Let \(x\) be drawn from a distribution \(\mu \) on a finite set \(\mathcal{X}\) and, independently of \(x\), let \(y\) be drawn from a distribution \(\nu \) on a finite set \(Y\) (uniform in the source). For each \(i\leq k\) let \(\cal {G}_i\) be a finite family of functions on \(Y\), any two distinct elements of which agree at \(y\sim \nu \) with probability at most \(\varepsilon \). Let \(|\psi \rangle \in \mathbb {C}^{d_\textsc{A}}\otimes \mathbb {C}^{d_\textsc{B}}\) be a unit vector, let \(\{ A^x_{g_1,\ldots ,g_k}\} \) be a projective measurement on \(\mathbb {C}^{d_\textsc{A}}\) with outcomes in \(\cal {G}_1\times \ldots \times \cal {G}_k\), and for each \(i\) let \(\{ G^{i,x}_g\} _{g\in \cal {G}_i}\) be a projective measurement on \(\mathbb {C}^{d_\textsc{B}}\). Suppose that for every \(i\) the evaluated \(i\)th coordinate of \(A\) and the evaluated \(G^{i,x}\) disagree with probability at most \(\delta \):

Define the POVM \(C^x_{g_1,\ldots ,g_k}=G^{k,x}_{g_k}\ldots G^{2,x}_{g_2}G^{1,x}_{g_1} G^{2,x}_{g_2}\ldots G^{k,x}_{g_k}\), the last index outermost. Then the evaluated tuples disagree with probability at most \(2\sqrt{2}\, k\, (\delta +\varepsilon )^{1/2}\):

Combined with 1, the evaluated tuples are \(4\sqrt{2}\, k\, (\delta +\varepsilon )^{1/2}\)-close across the parties in the sense of Definition 2.28.

Use the simultaneous theorem at \((q,m',d,m'+6)\) to obtain a projective measurement \(J\) of the entire tuple \((f_1,\ldots ,f_5,c_0,\ldots ,c_{m'})\). Write \(M_i\) for individual point measurements, and \(M_6\) for the complete proof-tuple point measurement. With seed averaging understood, retain all five relations: \(M_i(y_i)\) is cross-party consistent with the \(i\)th evaluation coordinate of \(M_6(z)\) for \(i=3,4,5\) with error \(O(\theta )\); \(M_i(y)\) is consistent with \(G_i\) evaluated at \(y\); the two copies of \(G_i\) are consistent; \(M_6(z)\) is consistent with \(J\) evaluated at \(z\); and the two copies of the complete \(J\) are consistent. The last four errors are \(O(\kappa )\). Include player mirrors of the first, second and fourth. Individual evaluations without a projective complete-tuple output do not suffice for the next lemma.

Programs compute, from the parameters and the layout of the answers, the constraints of the consistency checks, that the isolated player’s two codewords are the oracle’s codewords in the same slots; and those of the indifference checks at an axis-parallel line, that the coefficients \(1, \ldots , d\) of the codewords whose blocks miss the direction the seed selects vanish.

The checks of a PCP at a point hold exactly when the checks on its slot values there do, which are the readable checks and the linear checks; the readable checks read only readable values. If each of a family of polynomials on \(N\) variables depends only on the image of its slot’s block, then the slots of the PCP of the polynomials, renamed back, are the polynomials: its values are theirs, and its degree is at most theirs. A readable slot sits among the oracle’s readable codewords.

An outcome of the oracle’s polynomial measurement at a seed passes densely if its evaluations pass the thirteen checks of the seed’s circuit on more than a fraction \(m (5 + 6 (d + 1)) / q\) of the points of \(\mathbb {F}_q^M\). If \(q \geq 2 m (5 + 6 (d + 1))\), the outcomes of \(G^\textsc{A}_\textsc{O}\) that do not pass densely weigh, summed over the seeds, at most \(|Z| (2\, \delta _\textsc{O}(9\theta ) + 162\, \theta )\).

Let \(\varepsilon _{r,y}\) be the failure of the per-role strategy at \((r, y)\). The evaluations of \(G^\textsc{B}_{r,y}\) at a uniform point are inconsistent with Alice’s point answers of the per-role strategy, those of \(G^\textsc{A}_{r,y}\) with Bob’s, and \(G^\textsc{A}_{r,y}\) with \(G^\textsc{B}_{r,y}\), each at most \(\delta _r(\varepsilon _{r,y})\); and \(\sum _{z} \delta _r(\varepsilon _{r, y_r(z)}) \leq |Z|\, \delta _r(9 \theta )\).

An outcome of the oracle’s polynomial measurement is block-local if each codeword’s polynomial involves only the variables of its slot’s block. If \(q \geq 2 (M + 1) d\), the outcomes of \(G^\textsc{A}_{\textsc{O}}\) that are not block-local weigh, summed over the seeds, at most \(2M |Z| (12\, \delta _\textsc{O}(9\theta ) + 1782\, \theta )\).

Two measurements of tuples of polynomials of individual degree at most \(d\) in \(M\) variables disagree at most as often as their evaluations at a uniform point do, plus \(M d / q\). So for an isolated role \(r\), \(\sum _z \mathrm{dis}(G^\textsc{A}_r, \mathrm{res}_r G^\textsc{B}_\textsc{O}) \leq |Z|\, e_r(\theta )\), and the same with the players exchanged, where \(e_r(\theta ) = 11 (\delta _r(9\theta ) + 81\theta + \delta _\textsc{O}(9\theta )) + M d / q\).

Write \(\mathrm{ev}_w\) for evaluation at the point the registers \(w\) carry, and \(\mathrm{res}_r\) for the restriction of the oracle’s tuple to the slots of an isolated role \(r\). Summed over the seeds:

1. at one pair of types, if the typed data’s acceptance forces two readings of the two answers to agree, their disagreement is at most \(81 |Z| |W| \theta \); the consistency check at the point questions of an isolated role and the oracle forces the role’s point values to be the oracle’s in the role’s slots;

2. \(\mathrm{ev}_w G^\textsc{B}_r\) disagrees with Alice’s point values at most \(|Z| |W| \delta _r(9\theta )\), \(\mathrm{ev}_w G^\textsc{A}_r\) with Bob’s likewise, and \(G^\textsc{A}_r\) with \(G^\textsc{B}_r\) at most \(|Z| \delta _r(9\theta )\);

3. for an isolated role \(r\), \(\mathrm{ev}_w G^\textsc{A}_r\) disagrees with \(\mathrm{ev}_w \mathrm{res}_r G^\textsc{B}_\textsc{O}\) at most \(11 |Z| |W| (\delta _r(9\theta ) + 81 \theta + \delta _\textsc{O}(9\theta ))\), and the same with the players exchanged.

The failure \(\theta \) is the average of \(T\)’s failure over the \(81\) pairs of types and the seeds, so its failures at any set of pairs of types sum, over the seeds, to at most \(81 |Z| |W| \theta \). At two typed questions of one role and one oracularized question, the typed data’s low-degree check is the test’s predicate on the role’s codewords, and the per-role strategies’ failures at \(y_r(z)\) sum over \(z \in Z\) to at most \(9 |Z| \theta \).

Let \(g\) be a polynomial in \(n\) variables of individual degree at most \(d\) over a field with \(q\) elements, with a nonzero coefficient on a monomial containing \(X_i\). Then \(g(u + t e_i) \neq g(u)\) for at least \(q^n (q - (n + 1) d)\) of the pairs \((u, t) \in \mathbb {F}_q^n \times \mathbb {F}_q\).

An exterior strategy with deficit \(\varepsilon _{\mathrm{out}}\) gives a typed strategy with deficit \(\theta =16^{|T^{\mathrm{ar}}|}\varepsilon _{\mathrm{out}}\) on the same state. Symmetrize the typed strategy for its symmetric game; do not assume the detyped question law is symmetric. The soundness proof then works with projective, well-formatted measurements and a swap-invariant state. All type-pair conditioning costs are constants since \(T^{\mathrm{ar}}\) is fixed. The Lean does not symmetrize: it keeps the two families of measurements of a projective strategy in a bipartite model (Definition 8.62), of which a tensor-product strategy is the case of its tensor-product model, and derives every relation for each ordered pair of players from the ordered type pair that carries it, the type graph being complete.

For answers of their types’ lengths, the constraints at a pair of typed questions hold exactly when the four checks hold of the field elements the answers carry: when the roles agree, the seeded low-degree test accepts the two answers read as answers of the test; when the low-degree types agree, the isolated codewords are the oracle’s in the same slots; each answer at an axis-parallel line is indifferent along it; and each oracle point answer passes the thirteen checks at its point.

If the equations have at most \(N\) variables, all below \(N\), the extension of a solution solves the triangulated system; a solution of the triangulated system solves the equations. Five assignments solve the decoupled system exactly when the first two agree with the first copy, the three copies agree on \([\ell ]\), and the triangulated equations hold on the three copies.

For a PCP decider and parameters \((\lambda ,\mu ,\sigma )\), and an \((\ell +1)\)-level input verifier \((S,D)\), there is a typed decider on the types of Definition 6.176, computed from the programs of \(S\) and \(D\) and \((\lambda ,\mu ,\sigma )\), which halts on every input and, on the bits of any two questions of that game and any two answers, accepts exactly when that game’s predicate does, with the game check run at \(\mathrm{pcpparams}(n,T,Q,\sigma )\), \(Q=(\lambda n+1)^\mu \), \(T=2^{(Q+5)(\mu +1)}\). Under the hypotheses of Lemma 6.177, and \(|D|\le W\), it runs within \((C(W+1)^M(|d|+1)^E)^{\mu +1}\) on every input \((n,d)\) whose two questions have oracle halves of length at most \(W\) — as the questions the detyping compiler hands it have.

For a PCP decider and parameters \((\lambda ,\mu ,\sigma )\), and an \((\ell +1)\)-level input sampler \(S\), there is a typed sampler with \(\max \{ \ell +1,3\} \) levels on the types of Definition 6.176 whose typed CL functions are that game’s, with the PCP parameters \(\mathrm{pcpparams}(n,T,Q,\sigma )\), \(Q=(\lambda n+1)^\mu \), \(T=2^{(Q+5)(\mu +1)}\), and with the seed selectors reading the high bits of the seed. Its program is computed from the program of \(S\) and \((\lambda ,\mu ,\sigma )\) alone. If the PCP’s parameters are polynomial in \((\log n,\log T,Q,\sigma )\) and \(S\) runs within \(Q(|d|+1)^\mu \) at \(n\), it runs within \((C(W+1)^M)^{\mu +1}(|d|+1)^{E(\mu +1)}\) for universal \(C,M,E\) and any \(W\) above \(Q\), \(\lambda \), \(\sigma \), \(n\) and \(|S|\).

There is a polynomial-time algorithm that, on window lengths \(\ell _a, \ell _b, \ell _c\) in unary and the inputs \((\mathcal{D}, n, T, Q, \sigma , x, y)\) of Theorem 3.83, outputs a circuit with inputs of lengths \(\ell _a\), \(\ell _b\), \(\ell _c\), three of length \(r_0 = O(\log T + \log \sigma )\), with \(2^{r_0} \geq 4T\), and six single bits, describing a decoupled 6SAT formula on blocks of \(2^{\ell _a}\), \(2^{\ell _b}\), \(2^{\ell _c}\) and three times \(2^{r_0}\) variables. On valid inputs with \(\ell _a, \ell _b, \ell _c \le r_0\) the circuit has at most \(s_0 = \mathrm{poly}(\log n, \log T, Q, \sigma )\) gates, and if moreover \(2^{\ell _a} + 2^{\ell _c} \le 2T\) and \(2^{\ell _b} \le 2T\), then three tables \(A, B, C\) complete to a satisfying assignment exactly when the decider accepts, within cost \(T\), strings \(a, b\) of length at most \(T\) such that \(A\) and \(C\) are the consecutive windows of lengths \(2^{\ell _a}\) and \(2^{\ell _c}\) at the start of the tape encoding of \(a\), and \(B\) is the first \(2^{\ell _b}\) bits of that of \(b\). The parameters \(r_0, s_0\) are computable in time polynomial in the bit lengths of \(n, T, Q, \sigma \).

A perfect ZPC strategy of a tailored game lifts to an action of value \(1\) against the associated test: on twice the points, \(J\) swapping the copies and each variable acting by its signed permutation.

For an action passing Checks 1–3 everywhere, a point passes the challenge at \((x, y)\) exactly when the constraint words of the entries whose readable part is the point’s readable value fix it; and there are at most \(2^{\ell (x) + \ell (y) + 1} + 1\) constraint words.

In the associated test every generator has significance at most a bound \(S(\Lambda )\) of order \(\Lambda 4^{\Lambda }\), and the variables at a vertex \(x\) at most \(S(\Lambda )\) times the weight of the question pairs containing \(x\).

The map from a tailored game description to the description of its associated test is primitive recursive.