Every observable is the identity, which is a signed permutation matrix, diagonal and an involution, and commutes with everything. Each factor \(\frac12(I+ (-1)^{a_X}I)\) is \(I\) at \(a_X = 0\) and \(0\) at \(a_X = 1\), so \(P^x_a\) is \(1\) at \(a = 0\) and \(0\) elsewhere, and the value is \(\sum _{x, y} \mu (x, y) = 1\). This is the case of the halting protocol in which the machine has halted (II:1978), and it shows that the definitions are not vacuous.

Column \(j\) of the matrix of \((\sigma , s)\) has a single nonzero entry, \((-1)^{s(j)}\) in row \(\sigma (j)\). The product of the matrices of \((\sigma , s)\) and \((\tau , t)\) has, in column \(j\), the single entry \((-1)^{s(\tau (j)) + t(j)}\) in row \(\sigma \tau (j)\), which is the group law; and the columns determine \((\sigma , s)\). The adjoint is the matrix of the inverse, so the matrix is unitary, and an involution equals its adjoint. A diagonal one has \(\sigma = I\).

For one involution, \(\frac12(I\pm U)\) are complementary projections. If every element of one projective measurement commutes with every element of another, their products form a projective measurement on the product of the outcome sets; the Fourier transform of \(k + 1\) observables is the product of that of the first and that of the other \(k\), reindexed, which proves the first claim by induction on \(k\). \(U_i\) commutes with the factors of \(P_a\) other than the \(i\)-th, on which it acts as \((-1)^{a_i}\); multiplying over the \(i\) with \(\alpha _i = 1\) gives the eigenvalue relation, and summing it over \(a\) the inverse transform. A product of diagonal matrices is diagonal.

The observable of the coarse-graining is \(\sum _a (-1)^{c + \langle \alpha , a\rangle } P_a = (-1)^c U^\alpha \), by Lemma 9.8. Sums of diagonal matrices are diagonal.

The observables are involutive signed permutation matrices, hence self-adjoint (Lemma 9.7), and Lemma 9.8 applies. If the rejected pairs have \(P^x_a P^y_b = 0\), the accepted pairs carry \(\sum _{a, b} \mathrm{tr}(P^x_a P^y_b)/m = 1\) at each edge. The parity of the number of common ones of two vectors is their inner product. By the eigenvalue relations, \(U^\alpha V^\beta P^x_a P^y_b = (-1)^{\langle \alpha , a\rangle + \langle \beta , b\rangle } P^x_a P^y_b\), as \(V^\beta \) commutes with \(P^x_a\) along an edge; comparing with \((-1)^\gamma P^x_a P^y_b \neq 0\) gives the constraint.

By Lemma 9.10 the measurements are projective and commute along edges; the operators on strings of the wrong length are \(0\), and summing over the strings of length \(\ell (x)\) is summing over \(\mathbb {F}_2^{\ell (x)}\), so the measurement sums to \(I\) and the two values are the same sum, the bipartite decider agreeing with the canonical one on the edges. Doubling a strategy keeps the observables, and the doubled distribution is that of \(G\) on the pairs \(((\mathsf{false}, x), (\mathsf{true}, y))\) and zero elsewhere. The synchronous value bounds the quantum value of the doubled game (Lemma 2.14), which is that of \(G\).

The observables are involutions commuting along each row and each column, the rows multiply to \(I\) and the columns to \(-I\); these are identities in the group of signed permutations of four points, checked by computation, and the matrix map transports them. All variables being linear, Z-alignment is vacuous; an edge joins a constraint to one of its cells, whose observable is one of the constraint’s, so the strategy commutes along edges. The observable of a consistency check is the square of a cell’s observable, \(I\), and that of a row or column check is the product of its three observables, \(I\) or \(-I\) as the parity requires, so every sampled answer pair is accepted by Lemma 9.10. The quantum value is \(1\) by Lemma 9.11.

A run of a sequence of steps is a run of each step, the model being deterministic, and the polynomial-time pieces compute what they are meant to. For the second part: when the five runs halt, their outputs are the lengths and the constraints that \(\mathsf{V}_n\) is read from. When one of them does not halt, \(\mathsf{V}_n\) has at that edge the constraint list \(\{ J\} \), which no answer pair satisfies, and the canonical decider does not halt, which is a rejection.

The question-length check passes at the questions of index \(n\), so acceptance is the canonical decider’s, which is that of \(\mathsf{V}_n\) by Lemma 9.16. The two games have the same distribution and accept the same answer pairs, and every answer pair that \(\mathsf{V}_{n,T}\) accepts has the lengths of \(\mathsf{V}_n\), so is one of the answer pairs of the game of \(\mathsf{V}_n\): enlarging the answer sets by rejected answers changes no value. A perfect ZPC strategy for the doubled game of \(\mathsf{V}_n\) is a perfect PCC strategy for the doubled bipartite game (Lemma 9.11), which, extended by zero to the answers of length at most \(T\), is one for the doubled game of \(\mathsf{V}_{n,T}\).

Theorem 9.37 at the compression of Theorem 9.92, the synchronous value being at most the quantum value; the class theorems for both readings of \(\mathrm{TMIP}^*\) follow.

The processor is the fixed point, so on an input of index \(n\) it outputs what the three branches say. In the first, every constraint list is empty — the answer-length calculator halts at every question of the sampler, which is where its totality is spent — so the game accepts every answer pair of the right lengths, and the deterministic strategy is perfect (Lemma 9.6). In the second, every constraint list holds \(J = 0\), so no answer pair is accepted. In the third, the two verifiers have the same sampler and answer-length calculator, and their processors output the same constraints at index \(n\), so their \(n\)-th games coincide.

The processor is a hardcoding of the fixed point’s program to its own description, of size \(2(\left\vert {\cal {M}} \right\vert + \left\vert {\lambda } \right\vert )\) plus a constant. On \((n, d)\) it runs within the fixed point’s overhead on the hardcoded description, the branch computation, and the universal machine on the compressed processor, whose time is the compression’s \(\mathrm{poly}(n + \lambda )\); together a polynomial in \(n + \left\vert {\cal {M}} \right\vert + \lambda \) times a power of \(\left\vert {d} \right\vert + 1\). The sampler’s and the answer-length calculator’s clauses are the compression’s bounds. Each clause is absorbed into \(n^\lambda \), at degree \(\lambda \), past a threshold on \(\lambda \), and the size into \(\lambda \) once \(\lambda \geq \Lambda _0 + 4\left\vert {\cal {M}} \right\vert \).

Along the levels \(C, 2^C, 2^{2^C}, \dots \), compression carries a perfect ZPC strategy at \(2^n\) down to \(n\), and a value at most \(\frac12\), at every level where neither of the first two branches fires, the verifier then having the compressed verifier’s games (Lemma 9.26); the verifier is \(\lambda \)-bounded by Lemma 9.27. If \(\cal {M}\) halts, the first branch fires from some level on; the search never fires below it, since a firing would put every level below it, the start level among them, at value at most \(\frac12\), while the search fires only when the start level’s value exceeds \(\frac12\); so completeness descends to \(C\). If \(\cal {M}\) does not halt and the value at \(C\) exceeded \(\frac12\), the search would fire from some level on, and soundness would descend from there to \(C\), a contradiction.

The two notions of a synchronous strategy are the same data, and so are their values. The Fourier transform of commuting self-adjoint involutions is a projective measurement (Lemma 9.8), and the observables of a ZPC strategy are involutive signed permutation matrices, which are self-adjoint.

The two games have the same questions and the same distribution, and their answer sets are in bijection along the binary expansion, under which the two predicates agree; the quantum value is invariant under such relabelings.

The two read answers differently: the description reads bit vectors of the largest length that vanish beyond a vertex’s variables, the game bit strings of exactly that length; and the description also rejects unequal answers at a loop. On well-formatted answers the two predicates agree up to the loop condition, and the quantum value sees a predicate only where the distribution has weight. Answers pass from vectors to strings by keeping a vertex’s coordinates and back by padding with zeros, question by question, and decoding answers question by question can only raise a value; so the two values bound each other. For the strategies: an observable equal to the identity leaves the Fourier transform unchanged at an answer whose bit there is \(0\) and annihilates it at the others, so the padded strategy’s measurements are the strategy’s on padded answers and vanish elsewhere, and it has the strategy’s value.

Under its time bound each budgeted run returns the program’s output. The weights are counted as in the tabulation of a normal form verifier (Definition 2.43), the marginals at the sampler’s level being normalized to the dimension, which only matters at level \(0\), where the questions are empty. A vertex’s question is read off its binary expansion, the tag being the lowest bit.

On a string, semidecide \(\mathrm{val}^*{\gt} \frac12\) for the game description of its tabulation at the level \(C\). On the description of a \(\lambda \)-bounded verifier that tabulation presents the doubled game at \(C \geq 2\) (Lemma 9.35), so it has the doubled game’s quantum value, which is the verifier’s value (Lemma 9.33), and the conversion keeps it (Lemma 9.31).

The reduction sends \(\cal {M}\) to the tabulation, at the level \(C\), of the tailored halting verifier \(\mathsf{V}^{\cal {M},\lambda }\) with the search program of Lemma 9.36 and \(\lambda = \Lambda _0 + 4\left\vert {\cal {M}} \right\vert \). That verifier is \(\lambda \)-bounded (Lemma 9.27), so its tabulation presents the doubled game at \(C\) (Lemma 9.35). If \(\cal {M}\) halts, the verifier has a perfect ZPC strategy at \(C\) (Theorem 9.29), which, padded, is one of the tabulation; if not, its value at \(C\) is at most \(\frac12\), and that is the tabulation’s quantum value (Lemma 9.33), which bounds the synchronous value (Lemma 9.30). The map is computable: the processor’s description is a fixed tree around the encodings of \(\cal {M}\) and \(\lambda \), built as the decider’s is for Theorem 6.214, and the tabulation is computable.

A perfect ZPC strategy gives quantum value \(1\) (Lemma 9.30), and the conversion to a game description keeps the quantum value (Lemma 9.31); so a language in \(\mathrm{TMIP}^*\) is in the computable class of Definition 2.53, which is contained in \(\mathrm{RE}\) (Lemma 7.5). The plan had this inclusion by enumerating signed-permutation strategies; the route through the quantum value needs no new semidecider. Conversely, an r.e. language many-one reduces to the halting problem, which reduces to tailored games by Theorem 9.37.

On the input \(z\), tabulate the doubled game of \(\mathfrak {G}_z\): its vertices are the doubled strings of length at most \(B\), its weights those of the tabulation of Definition 2.52’s game (Lemma 2.54), and its lengths and constraints what the calculator and the processor output within the time bound \(P\), as in Lemma 9.35. The table is a computable function of \(z\), and on an efficient input it presents the doubled game of \(\mathfrak {G}_z\), which has no weight on its loops; so it has a perfect ZPC strategy when the doubled game does, and the doubled game’s quantum value, which is \(\mathfrak {G}_z\)’s (Lemma 9.33). So \(L\) is in the computable class, and in \(\mathrm{RE}\) by Theorem 9.39.

Restricting \(\mathfrak {G}'\) to the image of \(e\) does not change its value, its distribution being supported there. The answers of length at most the largest length of \(\mathfrak {G}\) then sit inside those of \(\mathfrak {G}'\), and the canonical decider rejects the longer ones, so the value is \(\mathfrak {G}\)’s. For a ZPC strategy of \(\mathfrak {G}\), pull it back along the inverse of \(e\): its observables on the image of \(e\), and identities elsewhere, where no question is asked. An edge of positive weight has both ends in the image, with the lengths of their preimages and an edge of \(\mathfrak {G}\) between these, on which the two canonical deciders agree; so the pulled-back strategy is a perfect ZPC strategy, by the pull-back of permutation strategies of the repetition phase.

\(\mathrm{TMIP}^* \subseteq \mathrm{RE}\) is Lemma 9.41. Conversely, an r.e. language many-one reduces to halting on the empty input by a polynomial-time map \(z \mapsto \cal {M}_z\), as in Theorem 7.6. The class verifier on \(z\) plays the game of the tailored halting verifier \(\mathsf{V}^{\cal {M}_z, \lambda (z)}\) at the fixed level \(C\), with \(\lambda (z) = \Lambda _0 + 4\left\vert {\cal {M}_z} \right\vert \). Its sampler is that of Lemma 6.213 for the compressed samplers. Its calculator and its processor compute, in polynomial time, the programs of the compressed calculator at \(\lambda (z)\) and of the processor of \(\mathsf{V}^{\cal {M}_z, \lambda (z)}\), and run them on \(C\) and the rest of the input through the universal machine, which halts exactly when the simulated program does, with its output. They run within polynomials in the total input length: the compressed calculator within \(\mathrm{poly}(C, \lambda )\) times a power of the size of its input, and the processor within \(Q(C + \left\vert {\cal {M}} \right\vert + \lambda )\) times one. So the class verifier’s game on \(z\) extends that of \(\mathsf{V}^{\cal {M}_z, \lambda (z)}\) at \(C\) along the embedding of its questions as bit strings, and Lemma 9.42 transfers both clauses of Theorem 9.37 at the level \(C\).

Route A (Remark 9.23). A \(\lambda \)-bounded tailored input has a \(C_0\lambda \)-bounded normal form verifier (Lemma 9.72); with \(M = 2^{C_0 + 1}\), the output at \(\lambda \) is the output tailored verifier of Lemma 9.80 at \(M\lambda \), with the introspection verifier’s sampler and the programs \(\mathrm{L}^{\mathrm{intro}}\) and \(\mathrm{LP}^{\mathrm{intro}}\) at \(M\lambda \), which meet its specification (Lemma 9.88). Soundness is that of Lemma 9.80, with \(a M^a\) in place of \(a\); completeness at \(n \geq 1\) is Lemma 9.81, and at \(n = 0\) the output is empty. The budgets at \(M\lambda \) are budgets at \(\lambda \) (Lemma 9.89).

The output verifier of the routine of Lemma 9.165, at \(E_1 = 2E\), \(E_2 = E_{2,0}\) and \(c_0\) the size constant of the output indicator: its complexity clause is Theorem 9.159, its completeness that of Theorem 9.154 under the honest PCPs’ hypotheses, and its soundness that of Theorem 9.154 with Lemma 9.166; for \(\mu = 0\) the loss is at least \(1\).

A coordinate’s answer is two blocks of the tuple’s answer, its readable bits after the readable bits of the coordinates before it and its linear bits likewise. Cut the tuple’s answers into the thirteen blocks the padding is made of: a constraint of the right length pairs with the whole answers block by block, the zero blocks contributing nothing and the others pairing as the constraint does with the coordinate’s answers; one of the wrong length pads to a vector of the wrong length, and both sides reject. The readable answers of a coordinate are its block of the readable answers of the tuple, so the constraints of the coordinate are evaluated at the right readable answers.

The observable of the variable \((i, v)\) of \(\bar{x}\) is \(1 \otimes \ldots \otimes U(x_i, v) \otimes \ldots \otimes 1\), on the \(k\)-th tensor power of the space. A slot of a signed permutation is a signed permutation, of a diagonal matrix a diagonal matrix, and slots in two different factors commute, so the observables are involutive signed permutations, commuting at each question, diagonal at the readable variables, and commuting along the edges, which are edges in every coordinate. The factors of the Fourier transform at \(\bar{x}\) commute; regrouped by coordinate they give the tensor product of the coordinates’ measurements. In a perfect strategy a rejected pair of answers on an edge has \(P^x_a P^y_b = 0\): its probability is zero, and \(P^x_a P^y_b\), two commuting projections, is its own \(X^* X\). A rejected pair of the product is rejected in some coordinate (Lemma 9.48), and a tensor product with a zero factor is zero, so the power is perfect (Lemma 9.10). For the doubled product, the power of the strategy for the doubled game is read at \((t, \bar{x})\) on the questions \((t, x_1), \ldots , (t, x_k)\), a map of the questions that keeps the lengths, the edges and the constraints.

At good questions the repeated verifier’s game has the lengths and the constraints of the product, up to the blocks of the questions; at any other question it accepts nothing, and neither does the product, a coordinate of whose constraint lists then rejects. For completeness, the doubled product has a perfect ZPC strategy (Lemma 9.49); a perfect strategy is accepted somewhere on every edge, so the questions on an edge are good, and the strategy pulled back along the blocks of the questions, with identity observables at the questions that carry no edge, is perfect for the repeated verifier. For soundness, the repeated verifier’s game accepts, read through the coordinates of its answers, only what the direct repetition of \(\mathsf{V}_n\)’s bipartite game accepts, so its value is at most that game’s: a strategy merged at each question along the map from answers to their coordinates is a strategy of the repetition of at least the same value. The answers of \(\mathsf{V}_n\) have length at most \(2B\), and Lemma 5.9 at length \(2B\) gives the bound, the factor \(2\) absorbed into the constant.

The loop of calls halts with the results of the calls when every call halts, and only then. At a question all of whose coordinates have their lengths, the calculator’s calls all halt and its output has the sum of the lengths; conversely a halting run of the calculator ran the input calculator at both kinds of every coordinate. For the processor, the lengths read off the calculator’s outputs are the coordinates’, so its cuts of \(a^R\) and \(b^R\) are the coordinates’ readable answers, its queries are the coordinates’ and its padding is the product’s.

Every stage between the calls is a polynomial-time function of an input of size polynomial in \(W\) and \(|d|\). Every query to an input program is of size linear in \(|d|\), so a call costs at most the universal machine’s overhead at \(T_D (c|d|)^K \le W^{j} |d|^K\), using \(10^K \le W\), and there are at most \(4k(n)\) calls.

The repeated sampler, and the repeated programs of Definition 9.52, their descriptions computed by the s-m-n map. The complexity clause is Lemma 9.54 with the repeated sampler’s time bound, and completeness and soundness are Theorem 9.51 applied to Lemma 9.53.

The map \(\varepsilon \mapsto \sum _\lambda \varepsilon (\lambda ) P_\lambda \) is multiplicative, so the \(U_i\) are commuting involutions, self-adjoint as their weights are real. Since \(\sum _\lambda P_\lambda = I\), the factor \(\frac12(1 + (-1)^{b} U_i)\) is \(\sum _\lambda \frac12(1 + (-1)^{b + \mathrm{enc}(\lambda )_i}) P_\lambda \), the coarse-graining of \(P\) onto \(\{ \mathrm{enc}(\lambda )_i = b\} \); by multiplicativity the product over \(i\) is the coarse-graining onto the intersection of these sets, by induction on \(k\). The last two claims regroup the sum \(\sum _\lambda \) by the fibres of \(f\), resp. drop the outcomes outside the image of \(f\), which carry zero.

The first two claims are the definitions. The trace form is nondegenerate (a nonzero \(c\) gives a nonzero functional, since the trace is onto), so \(c \mapsto \operatorname{tr}(c \cdot -)\) is an injective linear map between spaces of equal finite dimension over \(\mathbb {F}_2\), hence onto. The observable of the bit \(\operatorname{tr}(c \cdot -)\) is \(\sum _e (-1)^{\operatorname{tr}(c \cdot e)} P_e = W(c)\), the expansion of a Weyl operator in its eigenbasis projectors. The \(Z\)-basis projectors are the diagonal matrix units, so any \(\pm 1\) combination of them is a \(\pm 1\) diagonal.

The controlled sum applies \(U_{f(i)}\) on the second factor of the basis state \((i, a)\), so it is the block-diagonal matrix with blocks \(U_{f(i)}\). The block-diagonal matrix with blocks the matrices of \((\sigma _i, s_i)\) is the matrix of the signed permutation \((i, a) \mapsto (i, \sigma _i(a))\) with signs \(s_i(a)\). The other claims are linearity of the Kronecker product and of relabelling, entry by entry.

The observable is \(\sum _b (-1)^{\mathrm{enc}(b)} \frac12(1 + (-1)^b O)\), a two-term sum. \(X\) is the matrix of the transposition, \(Z\) the diagonal of the signs \((1, -1)\), and the grid is built from them, \(A\) and \(B\) by Kronecker products and products.

The synchronous strategy charges only the strings of length \(\mathrm{len}(x)\), with the Fourier transform of the observables at \(x\); on them the bit observable is \(\sum _v (-1)^{v_j} P^x_v = U(x, j)\) (Lemma 9.8), resp. \(\pm \sum _v P^x_v = \pm I\).

The first claim is post-processing of the answers. For the second, the bit observables are commuting involutions commuting along edges (Lemma 9.56, from PCC), and their measurement at \(x\) is the push-forward of \(S\) along \(\mathrm{enc}\). A perfect PCC strategy has \(M^x_a M^y_b = 0\) for every rejected pair at an edge: the product is a projection, as the two commute, of trace zero. So a pair \((a, b)\) that \(\mathfrak {G}\) rejects has \(P^x_a P^y_b = \sum M^x_{a'} M^y_{b'}\) over the \(a', b'\) encoding to it, each term zero — \(a'\) or \(b'\) outside \(\mathrm{ok}\) carries zero, and otherwise \((a', b')\) is rejected by \(\mathfrak {G}'\), or its encoding would be accepted — and the strategy is perfect by Lemma 9.10.

A view of an edge decodes to the edge’s type, so the lengths and constraints are the typed ones there; off the edges there is no constraint. The two reductions follow case by case on whether the pair of questions is the pair of views of an edge.

The fields of a well-formed tuple are recovered by the parser (pairParts, tripleParts); the re-encoding lays them out at fixed offsets, so cutting at those offsets recovers them, and the first \(s\) bits of a block padded from \(s \le R\) bits are the block.

Lemma 9.61, its acceptance obligations reduced to the edges by Lemma 9.63; the encoded lists have the question’s length, so they are the vectors the permutation strategy reads.

Every call reads only components of the parsed input: \(L\) on \((n, x, \kappa )\) and \((n, y, \kappa )\), \(LP\) on \((n, x, y, a^R, b^R)\), each of size linear in \(|d|\), so each costs at most \(T\, (20|d| + 20)^k\), and so does its output. The polynomial-time steps between them run on states made of the input and these outputs, so their costs are polynomials in \(T(20|d|+20)^k\) and the parse’s cost, a polynomial in \(|n| + |d|\). The domination tools of the repeated programs turn the sum into the stated shape.

The inner product is additive over concatenation, and zero against zeros; the rest is cutting the vectors at the offsets.

The inner product of two windows is the \(\mathbb {F}_2\) sum of the products of their entries. The dual readouts agree exactly when \(x - y\), restricted to \(S\), is orthogonal to the kernel of \(L\); a linear functional vanishing on a spanning list vanishes on the span.

Each rule of the test compares field elements and bits that are \(\mathbb {F}_2\)-linear in the answer bits, with coefficients given by the questions: the evaluation of a line’s polynomial at a parameter, the indicator of a point, the trace. A field equation is its \(k\) coordinate equations. Where a rule rejects on the questions alone, the list is the rejecting constraint; where it accepts on the questions alone, it is empty.

The two deciders accept the same inputs. The wrapper’s cost at an index \(n\) needs the sampler’s bound at \(n\) only; with the canonical decider’s bound of Lemma 9.68, at \(T = n^\lambda \) and exponent \(\lambda \), every term of the wrapper’s cost is dominated by \(n^{A\lambda }\) for a constant \(A\), and the domination tools turn the whole into \(n^{C\lambda }(|d|+1)^{C\lambda }\). The description is that of the wrapper, plus four times that of the length calculator, plus that of the constraint processor, plus a constant.

The projection reads the self-dual coordinates of the field elements of the answer, each a fixed linear function of the \(k\) bits encoding it. The dual readouts agree exactly when the difference is orthogonal to the kernel, as in Lemma 9.70.

A comparison of readable data is a readable condition; one of linear data is a list of linear constraints, bit by bit for an equality of windows, coordinate by coordinate for an equality on a coordinate set, generator by generator for an equality of dual readouts. The input’s answer is compared by its split, readable, and its two windows. The other order swaps the two blocks of every constraint.

Label pair by label pair: the semantic check is the format of the parsed answers (automatic), their equality at equal labels, the Pauli basis test at two Pauli labels and the directed checks in both orders, each of which is one of the families.

At a view decoding to a typed question the detyped measurement is the typed one there; at the other views the detyped tailored game has no answer bits, and the measurement is concentrated on a fixed answer.

By Lemma 9.75 the readable conditions hold and the kernel’s semantic check accepts the parsed answers. The readable conditions are the kernel’s prefix guard and source-output condition, and parsed Pauli answers are formatted, so the kernel’s completeness gives acceptance by the kernel program on the re-encoded answers, which is the typed predicate.

The kernel’s soundness turns acceptance by the kernel program into its semantic check on the decoded answers, which are the parsed encodings; Lemma 9.75 turns that into the constraints. The rest is Lemma 9.76.

The program’s correctness, read in the sampler’s encoding of vectors.

The detyped game is the reference verifier’s along the numbering of the detyped registers, and the reference verifier has the value of the introspection verifier’s output. Its soundness at \(C\lambda \), the identification of the input’s normal form verifier’s value with the input’s, and \(\delta (a, b, C\lambda , n, \varepsilon ) \le \delta (aC^a, b, \lambda , n, \varepsilon )\) for \(a \geq 1\), \(C \geq 1\) and \(\lambda n \geq 1\).

The honest strategy measures in the eigenbases of Weyl operators, in the computational basis, and by controlled sums over a control register; its answer bits are read out linearly or from the computational basis. Each of the three gives signed-permutation bit observables, diagonal for the computational-basis reads, which are the readable bits. The support condition is checked label by label. Then Lemma 9.80.

A bounded program halts within its bound, so the clocked run is the run; a bounded calculator halts at every question, so the constraints are what the processor outputs.

These are the kernel’s own queries and scans, read out rather than compared; the sampler’s program is specified at attained prefixes, which the prefix condition provides.

Every coefficient is an inner product of the generator, restricted to the factor, with a column of the self-dual coordinate map, or a unit vector.

It routes the pair as the kernel does. Each check is affine in the answer bits, so its constraint vector is its values at the zero answer and at the unit vectors, which the kernel’s field programs compute; a field equation gives its \(k\) coordinate constraints.

The lengths are fixed combinations of \(k\), \(2^j k\), \(Q\), \(R\) and \(1\), read from a table over the graph view; \(Q\) and \(R\) are computed in unary.

Unit vectors are shifts of one another, a coordinate set selects among them, and every other list is a concatenation of placed vectors.

A composition of the programs of the previous lemmas, by cases on the finitely many labels; each branch’s output is the corresponding constraint family on the edge, and the costs add.

Bernoulli’s inequality \(C x + 1 \le (x + 1)^C\); for the last, every pair of empty answers is accepted.

As Theorem 6.197: question reduction, then answer reduction at \((\lambda , \mu , \sigma (\lambda ))\), then repetition at \((\lambda , \tau )\), each soundness clause read contrapositively inside the margin the previous stage left (Lemmas 6.201 and 6.202). Three things change. The size parameter \(\sigma (\lambda )\) dominates the three introspective programs, the linear-constraints processor’s by the size clause of question reduction and the other two because they are computed from \(\lambda \) in polynomial time. The compressed answer-length calculator is repetition’s on the answer-reduced sampler and calculator, which depend on \(\lambda \) only. And repetition reads its input’s lengths from the calculator, so \(\tau \) is chosen against a bound \((\lambda n + 1)^\beta \) on the answer-reduced lengths in place of a parse length. Completeness is the three completeness clauses chained, with no answer bound to adjust.

Theorem 9.90 with the question reduction of Theorem 9.45 and the repetition of Theorem 9.55; then Theorems 9.37 and 9.39.

Theorem 9.90 applied to the three stages: question reduction (Theorem 9.45), answer reduction (Theorem 9.46) and parallel repetition (Theorem 9.55).

The inner product of \(c\) with \(a^R a^L b^R b^L 1\) splits over the five windows; the readable windows and the affine coordinate are known, and in characteristic \(2\) they move to the right.

The step equations of a row force the partial sums, by induction along the row, and the last one is the row. For the decoupled system, each kind of equation is one instance of the indicator, and conversely every instance is one of the kinds.

Lemma 9.96: the extension agrees with \(f\) below \(N\), and every triangulated equation is below \(N + \Delta \), so the three copies of a solution solve the triangulated system and hence the equations. Lemma 9.95 translates between the equations and the decider.

As for Lemma 6.147. The circuit accepts \((i_1, \dots , i_6, o_1, \dots , o_6)\) when the circuit of Theorem 3.83 accepts the last three indices and signs, or when one of five link conditions holds: \(i_4 = i_1 \land o_1 \neq o_4\);   \(i_4 = i_2 + 2T \land o_2 \neq o_4\);   \(i_4 = i_3 + 2^{\ell _a} \land o_3 \neq o_4\);   \(i_4 = i_5 \land o_4 \neq o_5\);   \(i_5 = i_6 \land o_5 \neq o_6\). For fixed indices the signs of the blocks a condition does not constrain range over all values, so the last two conditions say \(w_1 = w_2 = w_3\) and the first three that the windows are read off the common assignment at the offsets \(0\), \(2T\) and \(2^{\ell _a}\). The windows lie inside the two input regions of the tableau, so no padding condition is needed, and item 1 of Theorem 3.83 relates a satisfying assignment to acceptance. The offset of the third window is a power of two, which the algorithm computes from \(\ell _a\) without binary addition; the link conditions cost \(O(r_0)\) gates.

An index decodes into its coordinates by division and remainder, which locates it in the loops. Each kind of equation of the decoupled system has an index in range, a block of sign \(0\) taking the coordinate \(0\), and the table contains it; conversely, every equation the table contains is one of the system.

Lemma 9.100 turns the table into the decoupled system, which is below \(D\) by Lemma 9.96 when there are enough triangulation variables, and Lemma 9.97 relates the system to the game.

The check writes the readable rows, their triangulation and the table with all indices in unary, and loops over the coordinates of the table. The two powers of two are computed capped: \(2^\ell \) at one more than the length of \(b\), which it must equal, and \(2^{\delta }\) at one more than the length of \(O\), which a satisfied length check exceeds, so nothing larger than the input is ever written. The program is that of the canonical decider with the check in place of the constraints’ evaluation, and its running time is the sum of the five calls and of the check on a state whose size is bounded by the calls’ outputs.

Each of the six literal factors has individual degree at most \(d + 1\) and each certificate sum at most \(d + 2\); an assignment check is renamed along an injective map of the variables, which keeps degrees. A nonzero polynomial of individual degree \(e\) in \(m\) variables vanishes on a set of density at most \(m e/q\) (Lemma 3.111).

On the cube the certificate sums vanish, so an assignment check says \(g(1 - g) = 0\). At an index where \(g_O\) is one, the system check says that the equation holds in \(\mathbb {F}\), hence in \(\mathbb {F}_2\), the binary digits of the index being those of its coordinates. For a clause that the circuit accepts, the circuit polynomial is one at the Boolean point holding the clause’s input and the gates’ values (Lemma 6.155), so a literal factor vanishes there, which says that the literal is true.

By Lemmas 9.104 and 9.105 the tables of the windows satisfy the formula, so \(L^*\) accepts strings \(a, b\) whose tape encodings the windows hold. The odd positions of the windows read the strings: the readable answers are the tables of \(g_A\) and \(g_B\), and the string \(O\) that \(L^*\) compared is the table of \(g_O\). The linear tables satisfy the system that table holds, and item 2 of Lemma 9.101 gives the acceptance.

The map \(c \mapsto \sum _i c_i X_i (1 - X_i)\), restricted to the tuples whose image vanishes on the cube, maps onto the polynomials of individual degree at most \(d\) vanishing on the cube, by Lemma 6.161. Compose a linear right inverse of it with a linear projection onto that subspace.

An encoding is \(0\) or \(1\) on the cube and multilinear, so \(g(1 - g)\) vanishes on the cube and has individual degree at most \(2\). At a Boolean point where the circuit polynomial is one, the circuit accepts the clause whose indices and signs the point holds on its input wires (Lemma 6.155), a literal of that clause is true, and its factor vanishes there; so the formula polynomial vanishes on the cube. At an index where \(O\) is one, the equation holds in \(\mathbb {F}_2\), hence in \(\mathbb {F}\). In each case Lemma 9.107 gives the identity.

The encodings are linear, the system polynomial is affine in the linear assignments, and \(g \mapsto g(1 - g)\) is additive in characteristic two; the certificates are values of a linear map.

By item 1 of Lemma 9.101 the output indicator accepts the padded readable answers followed by the table, so by Lemma 9.98 their windows, read off the tables at the odd positions of the tape encodings, satisfy the formula with some witnesses. By item 3 of Lemma 9.101 the linear tables satisfy the system that the table holds. Lemma 9.109 concludes.

The checks on slot values are the checks of the PCP with each evaluation replaced by the value of its slot. A polynomial whose variables lie in the range of an injection is the renaming of one on its domain, which the left inverse of renaming recovers; renaming along an injection keeps the individual degrees.

An equation \(E(z) = \kappa \) between field elements, \(E\) an \(\mathbb {F}_2\)-linear map of the answer bits, holds exactly when the \(t\) coordinate checks of its canonical bits do (Lemma 9.71), and a readable guard rejects exactly when its condition fails (Lemma 9.69). Each check reads the bits of field elements lying inside their answers; the readable checks of the proof check read only readable values, which lie in the readable part.

The readable tables are read off the readable answers, and the readable polynomials off the readable tables. The linear tables are additive in the linear answers and the linear polynomials affine in the linear tables (Lemma 9.110). Alice’s encodings read only the cells of the padded readable answer and of her linear answer below \(2^\ell \), Bob’s only his. An accepted pair makes the verifier’s programs halt, since otherwise its constraint rejects everything; then Lemma 9.111 applies.

The two low-degree questions come from one sample of the seeded test. Equal roles carry equal oracularized answers, so one tuple of polynomials of individual degree at most \(d\) answers both, and the test accepts its honest answers. At one low-degree type the questions agree, and an isolated player’s polynomials are the oracle’s in its slots. A codeword whose block misses the direction of an axis-parallel line does not involve that variable, so its restriction to the line is constant. An oracle’s pair is accepted by the input game, so its PCP satisfies the identities, and the values of the oracle’s point answer are the PCP’s values at the point.

The coarse-graining of \(P\) along Z-bits is diagonal, and a sum \(\sum _k \Pi _k W_k\) over a diagonal projective measurement \(\Pi \) of signed permutations \(W_k\) commuting with it is a signed permutation: on the basis vectors of outcome \(k\) it acts as \(W_k\), which keeps them there. An affine function of X-bits is a constant exclusive or of some of them, whose observable is a product of signed permutations.

A readable bit lies in a readable codeword, a function of the readable input bits, which are Z-bits. Every bit is, the readable input bits fixed, affine in the linear input bits, which are X-bits: the codewords are affine in them, and values, restrictions to lines and canonical bits of field elements are additive. Lemma 9.119 concludes.

The honest strategy is PCC because the oracularization is, its questions of positive weight having oracularized parts of positive weight. It is perfect because every outcome it produces at such a pair is accepted by the oracularized predicate, which Lemma 9.118 turns into acceptance by the typed data. It charges only answers of the types’ lengths, and its bit observables are those of the oracularized measurements along the honest answers, signed permutations diagonal at the readable bits by Lemma 9.120. Lemma 9.76 concludes.

The detyped failure is the average over the pairs of types and the seeds of the failure at the questions an answer-reduced sampler gives them. A role’s nine pairs of types are a ninth of the \(81\), and the registers of a uniform vector carry a uniform sample of the test, with multiplicity one.

The first part is the test’s soundness in the model. The second is Jensen’s inequality for the concave error (Lemma 6.185), with Lemma 9.124.

The first part reads the typed data’s acceptance (Lemma 9.115): two readings that acceptance forces to agree disagree at most as often as the strategy fails there, and Lemma 9.124 sums the failures. The second is Lemma 9.126, the test’s uniform point being read off the registers of a uniform vector. The third chains the second part at the role, the consistency check and the second part at the oracle, through Bob’s point answer of the role and Alice’s point answer of the oracle at the same seed, by the triangle inequality for disagreements across the two players, which costs a factor \(11\).

Two distinct tuples agree at a uniform point with probability at most \(M d / q\), by Schwartz–Zippel (Lemma 3.33), and the registers of a uniform vector carry a uniform point. Lemma 9.127 concludes. Every polynomial of the game lives on the same \(M\) variables, an isolated role’s codewords being the oracle’s in the role’s slots, so no lifting between sets of variables is needed.

Restricted to the axis-parallel line through \(u\) in direction \(i\), \(g\) is a univariate polynomial of degree at most \(d\), whose coefficient on the power of \(X_i\) in that monomial is a nonzero polynomial \(G\) evaluated at \(u\). Where \(G(u) \neq 0\) the restriction is not constant, so it takes the value \(g(u)\) at most \(d\) times; and \(G(u) = 0\) at no more than \(n d q^{n-1}\) points, by Schwartz–Zippel.