6 Structure of the proof
This chapter records the main transformations of [ 1 ] at headline level: for each, what it does, what it relies on, and one theorem statement so that the dependency graph reflects the architecture. Working out each section — restating it in the synchronous framework, decomposing it into lemmas, and setting the constants — is a main task of the project. The paper factors several of these transformations through typed verifiers and a detyping step; that machinery is not reproduced here and should be introduced locally where needed.
Following Lin [ 10 ] , every soundness statement below is in value form: a transformation preserves the property “value at most \(1 - \varepsilon \)” up to a quantitative loss, and compression preserves “value at most \(\frac12\)”. No entanglement lower bound is tracked. Remark 5.9 explains why none is needed, Section 4.3 states the abstract lemma (Lin’s compressibility criterion) that turns value-form compression into the halting reduction, and the entanglement clauses of [ 1 ] are recorded for reference in Remark 6.8.
6.1 Conditionally linear functions and samplers
Question distributions must be structured enough that players can sample them on their own in a certifiable way (introspection), yet expressive enough to implement all the verifiers in the pipeline. The right class is that of conditionally linear distributions: linear maps applied in stages, where each stage may depend on the output of the previous ones.
Let \(V = \mathbb {F}_q^s\) and \(\ell \geq 1\). An \(\ell \)-level conditionally linear (CL) function on \(V\) is defined recursively: a \(1\)-level CL function is a linear map \(L : V \to V\); an \(\ell \)-level CL function is given by a direct sum decomposition \(V = V_1 \oplus V_{{\gt}1}\), a linear map \(L_1\) on \(V_1\), and, for each value \(u\) of \(L_1\), an \((\ell -1)\)-level CL function \(L^{u}_{{\gt}1}\) on \(V_{{\gt}1}\); it maps \(z = z_1 + z_{{\gt}1}\) to \(L_1(z_1) + L^{L_1(z_1)}_{{\gt}1}(z_{{\gt}1})\). A CL distribution is the distribution of \((L^\textsc{A}(z), L^\textsc{B}(z))\) for uniformly random \(z \in V\) and CL functions \(L^\textsc{A}, L^\textsc{B}\).
An \(\ell \)-level sampler (Definition 2.25) presents a CL distribution via Turing machines answering structured queries (dimensions, marginals, and evaluations of the linear maps and their canonical complements). This section of the project should fix the query interface once and for all, and prove the closure properties used later: products, concatenation, and reduction of the field size to \(q = 2\) (“downsizing”, using Lemma 3.11).
6.2 Question reduction: introspection
Introspection removes the verifier’s cost of sampling questions: instead of receiving questions for \(\mathsf{V}_{2^n}\), the players sample the questions themselves by measuring shared EPR pairs, and the new verifier uses the Pauli basis test (Theorem 3.8) to force honest sampling. The CL structure of the sampler is what makes commitment to each stage of the sampled question enforceable (the “hiding” directions of the CL decomposition). The result is a verifier whose questions are exponentially smaller, at the price of a fixed number of levels.
There is a polynomial-time Turing machine \(\mathsf{ComputeIntroVerifier}\) that on input \((\mathsf{V}, \lambda , \ell )\) returns a \(5\)-level normal form verifier \(\mathsf{V}^{\textsc{Intro}}= (\mathcal{S}^{\textsc{Intro}}, \mathcal{D}^{\textsc{Intro}})\) with \(\mathsf{TIME}_{\mathcal{S}^{\textsc{Intro}}}(n) = \mathrm{poly}(n, \lambda , \ell )\), \(\mathsf{TIME}_{\mathcal{D}^{\textsc{Intro}}}(n) = \mathrm{poly}(2^{\lambda n}, \ell )\) and \(\left\vert {\mathcal{D}^{\textsc{Intro}}} \right\vert = \mathrm{poly}(\lambda , \ell )\), such that for every \(\lambda \)-bounded \(\ell \)-level verifier \(\mathsf{V}\) there is a function \(\delta (\varepsilon , n) = a\bigl( (\lambda n)^a \varepsilon ^b + (\lambda n)^{-b} \bigr)\) (constants \(a, b\) depending only on \(\ell \)) with, for all \(n\):
(Completeness) If \(\mathsf{V}_{2^n}\) has a value-\(1\) PCC strategy, so does \(\mathsf{V}^{\textsc{Intro}}_n\).
(Soundness) If \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Intro}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^{s}(\mathsf{V}_{2^n}) \geq 1 - \delta (\varepsilon , n)\).
The soundness analysis is a long rigidity argument [ 1 , Section 8 ] . It builds on techniques introduced in [ 3 ] , and it may be adviseable to formalize some of the key lemmas there first. These include the Pauli basis test together with a toolkit of approximate-measurement lemmas (twirling, commutation, sandwiching). For this project, those lemmas should be stated and proved in the tracial/cynchronous setting.
6.3 Oracularization
Oracularization converts a normal form verifier into one where a single player (the “oracle”) receives both original questions and answers both, while the other player receives one of the two questions and must answer consistently. This makes the game’s predicate a pointwise function of one player’s answer — the format required by answer reduction. This is probably the easiest transformation in the paper and could be attempted first to fix the semantics.
There is a polynomial-time Turing machine \(\mathsf{ComputeOracleVerifier}\) mapping a normal form verifier \(\mathsf{V}= (\mathcal{S}, \mathcal{D})\) to a normal form verifier \(\mathsf{V}^{\textsc{Orac}}\) such that, for some \(\delta (\varepsilon ) = \mathrm{poly}(\varepsilon )\) and all \(n\):
(Completeness) If \(\mathsf{V}_n\) has a value-\(1\) PCC strategy then \(\mathsf{V}^{\textsc{Orac}}_n\) has a value-\(1\) symmetric PCC strategy.
(Soundness) If \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Orac}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^{s}(\mathsf{V}_n) \geq 1 - \delta (\varepsilon )\).
(Complexity) The sampler of \(\mathsf{V}^{\textsc{Orac}}\) depends only on \(\mathcal{S}\), with \(\mathsf{TIME}\) within a constant factor and the same number of levels.
6.4 Answer reduction
After introspection the decider still runs in time exponential in \(n\) (it simulates \(\mathcal{D}\) at index \(2^n\)), and the players’ answers are correspondingly long. Answer reduction composes the game with a PCP: by Theorem 3.10 the statement “the original decider would have accepted our answers” is a succinct 3SAT instance; the players commit to a low-degree encoding of a satisfying assignment (their original answers plus the computation tableau) and the new decider spot-checks it, using the low individual degree test to certify the encoding and Lemma 3.12 for the arithmetization. Answers and decider time become polylogarithmic in the original.
There is a polynomial-time Turing machine \(\mathsf{ComputeAnsRedVerifier}\) that on input \((\mathsf{V}, \lambda , \mu , \sigma )\), for \(\mathsf{V}\) an \(\ell \)-level normal form verifier with \(\left\vert {\mathcal{D}} \right\vert \leq \sigma \), \(\mathsf{TIME}_\mathcal{S}(n) \leq (\lambda n)^\mu \) and \(\mathsf{TIME}_\mathcal{D}(n) \leq (2^{\lambda n})^\mu \) for \(n \geq 2\), outputs a \(\max \{ \ell + 2, 5\} \)-level normal form verifier \(\mathsf{V}^{\mathsf{ar}}\) with \(\mathsf{TIME}_{\mathcal{S}^{\mathsf{ar}}}(n), \mathsf{TIME}_{\mathcal{D}^{\mathsf{ar}}}(n) = \mathrm{poly}\bigl( (\lambda n)^\mu , \sigma \bigr)\), whose sampler depends only on \((\mathcal{S}, \lambda , \mu , \sigma )\), and such that for some \(\delta (\varepsilon , n) = \sigma ^a \bigl( (\lambda n)^{\mu a} \varepsilon ^b + (\lambda n)^{-\mu b} \bigr)\) (universal constants \(a, b\)) and all \(n\):
(Completeness) If \(\mathsf{V}_n\) has a value-\(1\) symmetric PCC strategy then \(\mathsf{V}^{\mathsf{ar}}_n\) has a value-\(1\) PCC strategy.
(Soundness) If \(\mathrm{val}^{s}(\mathsf{V}^{\mathsf{ar}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^{s}(\mathsf{V}_n) \geq 1 - \delta (\varepsilon , n)\).
This is the most technically heterogeneous section of the paper ( [ 1 , Section 10 ] ): half classical (tableaux, Tseitin encoding, arithmetization — see Section 3.8) and half quantum (a low-degree “sandwiching” argument recombining the players’ committed polynomials). It may also be the hardest.
6.5 Gap amplification: parallel repetition
Answer reduction leaves a shrunken gap (\(1\) vs. \(1 - 1/\mathrm{poly}(n)\)). Direct parallel repetition (Theorem 5.6, formalized) restores soundness \(\frac12\) with polynomially many repetitions, at polynomial cost in complexity and without anchoring; the anchored, entanglement-form theorem used in [ 1 ] (Theorem 5.22) is not needed (Remark 5.9).
There are universal constants \(b, c, c' {\gt} 0\) and a polynomial-time Turing machine \(\mathsf{ComputeRepeatedVerifier}\) that on input \((\mathsf{V}, \lambda , \tau )\) outputs a normal form verifier \(\mathsf{V}^{\textsc{Rep}}\) whose game \(\mathsf{V}^{\textsc{Rep}}_n\) is the \(k(n)\)-fold direct repetition (Definition 5.1) of \(\mathsf{V}_n\), with \(k(n) = (\lambda n)^{(1 + c')\tau }\), such that if \(\mathsf{V}\) is \(\ell \)-level then \(\mathsf{V}^{\textsc{Rep}}\) is \(\ell \)-level with \(\mathsf{TIME}_{\mathcal{S}^{\textsc{Rep}}}(n) = O(k(n) \mathsf{TIME}_\mathcal{S}(n))\) and \(\mathsf{TIME}_{\mathcal{D}^{\textsc{Rep}}}(n) = O\bigl(k(n) \max (\mathsf{TIME}_\mathcal{D}(n), (\lambda n)^\tau )\bigr)\), the sampler of \(\mathsf{V}^{\textsc{Rep}}\) depends only on \((\mathcal{S}, \lambda , \tau )\), and for all \(n\):
(Completeness) If \(\mathsf{V}_n\) has a value-\(1\) PCC strategy and \(\mathsf{TIME}_\mathcal{D}(n) \leq (\lambda n)^\tau \), then \(\mathsf{V}^{\textsc{Rep}}_n\) has a value-\(1\) PCC strategy.
(Soundness) For all \(\varepsilon {\gt} 0\), if \(\mathrm{val}^{s}(\mathsf{V}_n) \leq 1 - \varepsilon \) and \(\mathsf{TIME}_\mathcal{D}(n) \leq (\lambda n)^\tau \), then \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Rep}}_n) \leq \exp \bigl( -c\, \varepsilon ^{b}\, k(n) / (\lambda n)^{\tau } \bigr)\); in particular \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Rep}}_n) \leq \frac12\) whenever \(\varepsilon \geq (\lambda n)^{-\tau }\), for \(c'\) large enough and \(n \geq 2\).
The game \(\mathsf{V}^{\textsc{Rep}}_n\) is \(\mathsf{V}_n^{k(n)}\): its sampler runs \(k(n)\) independent copies of \(\mathcal{S}\) (a product of conditionally linear functions of the same level) and its decider runs \(\mathcal{D}\) on every coordinate. Completeness: the \(k(n)\)-fold tensor power of a value-\(1\) PCC strategy is a value-\(1\) PCC strategy for the repeated game. Soundness: by the almost-synchronous transport (Theorem 3.3), \(\mathrm{val}^{s}(\mathsf{V}_n) \leq 1 - \varepsilon \) gives \(\mathrm{val}^*(\mathsf{V}_n) \leq 1 - \varepsilon '\) with \(\varepsilon ' = \Omega (\varepsilon ^{a})\) for a universal \(a\); Theorem 5.6 bounds \(\mathrm{val}^*(\mathsf{V}_n^{k(n)})\), where the answer alphabets of \(\mathsf{V}_n\) have size at most \(2^{\mathsf{TIME}_\mathcal{D}(n)}\) so that \(\log (\left\vert {\mathcal{A}} \right\vert \left\vert {\mathcal{B}} \right\vert ) \leq 2 (\lambda n)^\tau \); and \(\mathrm{val}^{s}\leq \mathrm{val}^*\) (Lemma 2.13) concludes, with \(b = 13 a\). The exponent \(b\) and the constants are provisional (Section 1.4).
6.6 The compression theorem
Composing the four transformations — introspection, oracularization, answer reduction, repetition — yields gap-preserving compression: the paper-level form of the compression hypothesis of Lemma 4.11. The soundness clause is the value-form clause that [ 1 ] state first and then strengthen to an entanglement bound (Remark 6.8).
There is a universal constant \(C_0 {\gt} 0\) and a polynomial-time Turing machine \(\mathsf{Compress}\) that on input \((\mathsf{V}, \lambda )\) outputs a \(9\)-level normal form verifier \(\mathsf{V}^{\textsc{Compr}}= (\mathcal{S}^{\textsc{Compr}}, \mathcal{D}^{\textsc{Compr}})\) with \(\mathsf{TIME}_{\mathcal{S}^{\textsc{Compr}}}(n), \mathsf{TIME}_{\mathcal{D}^{\textsc{Compr}}}(n) = \mathrm{poly}(n, \lambda )\), where \(\mathcal{S}^{\textsc{Compr}}\) is independent of \(\mathsf{V}\) and computable from \(\lambda \) in time \(\mathrm{polylog}(\lambda )\). If moreover \(\mathsf{V}\) is a \(\lambda \)-bounded \(9\)-level normal form verifier, then for all \(n \geq C_0\) and \(N = 2^n\):
(Completeness) If \(\mathsf{V}_N\) has a value-\(1\) PCC strategy, then so does \(\mathsf{V}^{\textsc{Compr}}_n\).
(Soundness) If \(\mathrm{val}^{s}(\mathsf{V}_N) \leq \tfrac 12\) then \(\mathrm{val}^{s}(\mathsf{V}^{\textsc{Compr}}_n) \leq \tfrac 12\).
Theorem 6.6 instantiates the hypotheses of Lemma 4.11: take \(A\) to be the set of (descriptions of) normal form verifier games with a value-\(1\) PCC strategy and \(B\) the set of those with \(\mathrm{val}^{s}\leq \frac12\), with the trivially accepting and the trivially rejecting game as the distinguished elements; the complement of \(B\) is semidecided by enumerating synchronous strategies (Lemma 3.13); and a description \((\mathcal{S}, \mathcal{D}, n)\) with \(n\) in binary is precisely a succinct description of the game \(\mathsf{V}_{2^n}\) played by a \(\lambda \)-bounded verifier. Completeness of compression is the preservation of \(A\) and soundness the preservation of \(B\). Making this dictionary precise (in particular the encoding of games by verifier descriptions and the role of \(\lambda \)) is a formalization task of this section. The entanglement form of [ 1 ] (Remark 6.8) instantiates Lemma 4.10 instead, with \(f = \mathrm{Ent}(\cdot , \frac12)\); it is not used by the main theorem.
The paper states the soundness of each transformation with an additional entanglement clause, obtained from the same proofs by tracking the dimension of the extracted strategies: \(\mathrm{Ent}(\mathsf{V}^{\textsc{Intro}}_n, 1 - \varepsilon ) \geq \max \{ \mathrm{Ent}(\mathsf{V}_{2^n}, 1 - \delta (\varepsilon , n)),\ (1 - \delta (\varepsilon , n))\, 2^{2^{\lambda n}}\} \) for introspection; \(\mathrm{Ent}(\mathsf{V}^{\textsc{Orac}}_n, 1 - \varepsilon ) \geq \mathrm{Ent}(\mathsf{V}_n, 1 - \delta (\varepsilon ))\) for oracularization; \(\mathrm{Ent}(\mathsf{V}^{\mathsf{ar}}_n, 1 - \varepsilon ) \geq \mathrm{Ent}(\mathsf{V}_n, 1 - \delta (\varepsilon , n))\) for answer reduction; Theorem 5.22 for anchored repetition; and, composed, \(\mathrm{Ent}(\mathsf{V}^{\textsc{Compr}}_n, \frac12) \geq \frac12 \max \{ \mathrm{Ent}(\mathsf{V}_N, \frac12), 2^{N^\lambda - 1}\} \) for compression. Fed into the variant of Lemma 4.10 tolerating the factor \(\frac12\) (harmless, since the second term grows much faster than the levels of the recursion), with \(f = \mathrm{Ent}(\cdot , \frac12)\), this yields Theorem 6.9 with the stronger conclusion \(\mathrm{Ent}(\mathfrak {G}_\cal {M}, \frac12) = \infty \) for non-halting \(\cal {M}\). The value form adopted here needs none of it; the entanglement clauses remain of interest for the corollaries of Remark 8.5.
6.7 The halting reduction
There is a computable (indeed polynomial-time) map \(\cal {M}\mapsto \mathfrak {G}_{\cal {M}}\) from Turing machines to synchronous game descriptions, with games given by normal form verifiers satisfying the efficiency requirements of Definition 2.29, such that:
if \(\cal {M}\) halts on the empty input then \(\mathrm{val}^{s}(\mathfrak {G}_\cal {M}) = 1\), witnessed by a PCC strategy;
if \(\cal {M}\) does not halt on the empty input then \(\mathrm{val}^{s}(\mathfrak {G}_\cal {M}) \leq \tfrac 12\).
The proof is Lemma 4.11 applied to the instantiation of Remark 6.7; the semidecidability hypothesis of the lemma is Lemma 3.13. The entanglement form of the statement, with the stronger conclusion \(\mathrm{Ent}(\mathfrak {G}_\cal {M}, \frac12) = \infty \) for non-halting \(\cal {M}\), is discussed in Remark 6.8.