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. The conditional assembly, its parameter arithmetic and the ambient introspection construction for seven-level inputs are formalized. Supplying answer reduction remains a main task of the project. These soundness analyses use the bipartite framework. The paper factors these transformations through typed verifiers and detypes at specified boundaries (Remark 6.9); the ambient Lean hypotheses also require the runtime adaptation of Remark 6.31.
Following Lin [ 13 ] , 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\)”. The three inner transformations, repetition and compression all carry that property in \(\mathrm{val}^*\), the bipartite tensor-product value: it is the class the compressibility criterion is instantiated with and the form Definition 2.53 requires (Remark 6.204), and no passage between the two values occurs anywhere on the path. The synchronous value is not used, and neither is the almost-synchronous transport of Theorem 3.3; see Remark 2.48 for why that is the better arrangement and Remark 6.8 for the evidence. No entanglement lower bound is tracked. Remark 5.11 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.207.
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}^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\).
Comments.
This is the paper’s definition (linear.tex, def:cl-func); the paraphrase this blueprint carried before started at level \(1\) and let \(V_1 \oplus V_{{\gt}1}\) be any direct sum decomposition, both departures from the paper. Two things about the formalization. Every consumer of the definition — the structure lemma below, the query interface of a sampler, the hiding tests of introspection — works with the decomposition data \((V_1, L_1, L_{{\gt}1,\cdot })\), which the function does not determine; so the Lean object is a presentation, CLFun, an inductive type indexed by the level, with CLFun.eval the function it presents and IsCLFun the paper’s notion (some presentation on \(V\) evaluates to the function). And presentations live on one ambient space \(\mathbb {F}^\iota \) whose register subspaces are sets of coordinates; “a presentation on \(V_T\)” is the predicate CLFun.SupportedOn, under which the paper’s \(V_{{\gt}1}\) is the complement of \(V_1\) inside \(V_T\). The continuations \(L_{{\gt}1,v}\) are indexed by all \(v\) rather than by the range of \(L_1\); the extra ones are never evaluated. The distribution is clDist, in the real-valued format of Definition 2.1.
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 \).
Source.
preliminaries.tex: the orthogonal complement and lem:perp_perp; def:canonical-complement with rk:cancomp; def:cl-canonical; def:Lperp with lem:L_perp_perp. Among the facts ledger node \(1.1.6\) lists as “subfield/trace facts as used”.
Comments.
The paper defines the canonical complement through a canonical Gaussian elimination: reduce the matrix whose rows are a basis of \(S\) to reduced row echelon form and take the standard basis vectors off the pivot columns. The formalization uses instead the equivalent characterization rk:cancomp credits to a referee — the dimension sequence \(u_j\) above — and that choice is what makes the construction usable. It needs no echelon form, and, more importantly, it is manifestly a function of the subspace \(S\): the paper has to argue that the echelon form does not depend on the chosen basis or on the order of its vectors, which is exactly what rk:cancomp spends its length on, whereas here there is nothing to argue. That the two agree is card_pivots: the pivot set has \(\dim S\) elements.
This vocabulary is needed for the lines of the low-degree test, not for CL functions as such: a line \(\ell (u_0, v)\) is presented by the canonical representative \(u_0 = L^{\mathrm{Ln}}_v(u)\) of Definition 3.13, \(L^{\mathrm{Ln}}_v\) being the canonical linear map with kernel \(\mathrm{span}\{ v\} \).
With the notation of Definition 6.2:
(\(\texttt{lem:perp\_ perp}\)) \(\dim S + \dim S^\perp = \dim V\) and \((S^\perp )^\perp = S\), over every field;
(\(\texttt{lem:canonical-complement}\)) \(S\) and its canonical complement are complementary subspaces, and the pivot set has \(\dim S\) elements;
the canonical linear map with kernel \(S\) has kernel exactly \(S\) and range the canonical complement;
(\(\texttt{lem:L\_ perp\_ perp}\)) \(\ker (L^\perp ) = (\ker L)^\perp \).
Item 1 is Mathlib’s, for a nondegenerate reflexive bilinear form, once the dot product is shown to be one. For item 2, let \(0 \neq x \in S\) lie in the canonical complement and let \(j\) be the least index with \(x_j \neq 0\); then \(x\) witnesses \(S \cap \mathrm{span}\{ \hat e_i : i \geq j+1\} {\lt} S \cap \mathrm{span}\{ \hat e_i : i \geq j\} \), so \(j\) is a pivot, so \(x_j = 0\) — a contradiction. The pivot count is an induction on \(j\) along \(u_j + \# \{ \text{pivots} {\lt} j\} = \dim S\), using that \(u_j \leq u_{j+1} + 1\) because the \(j\)-th coordinate is a linear functional on \(S \cap \mathrm{span}\{ \hat e_i : i \geq j\} \) with kernel the next term. Codisjointness then follows by counting dimensions, the complement having \(n - \# J\). Items 3 and 4 are then Mathlib’s projector along a direct sum decomposition.
Let \(L\) be an \(\ell \)-level CL function on \(V\), given with its decomposition data. For \(k \in \{ 1, \ldots , \ell \} \) there are a \(k\)-level CL function \(L_{\leq k} : V \to V\) on \(V\), the \(k\)-th marginal (with \(L_{\le 0} = 0\) and \(L_{{\lt}k} = L_{\le k-1}\)), and, for every prefix \(u \in L_{{\lt}k}(V)\), a register subspace \(V_{k,u}\) of \(V\), the \(k\)-th factor space, and a linear map \(L_{k,u} : V_{k,u} \to V_{k,u}\), the \(k\)-th linear map, such that for all \(x \in V\), writing \(u_i = L_{{\lt}i}(x)\):
\(L_{\leq k}(x) = \sum _{i=1}^{k} L_{i,u_i}\bigl(x^{V_{i,u_i}}\bigr)\), and \(L = L_{\le \ell }\);
the factor spaces \(V_{1,u_1}, \ldots , V_{\ell ,u_\ell }\) are pairwise disjoint register subspaces of \(V\), and \(V = \bigoplus _{i=1}^{\ell } V_{i,u_i}\) when the data are exact, that is, when the last level of every branch leaves no coordinate over.
This is lem:cl-kth of linear.tex, by induction on the level. In Lean the marginal is CLFun.truncate; the factor space and the linear map of a stage are computed both along a run (factorAt, mapAt) and from the prefix alone (factorOfPrefix, mapOfPrefix), and the two agree (factorOfPrefix_eval, mapOfPrefix_eval): that is what makes the paper’s indexing by prefixes well defined, and it is the fact the queries of a sampler rest on. Exactness is CLFun.ExactlyOn. The paper states the lemma as an equivalence, with the data normalized so that the factor spaces always exhaust \(V\); the formalization keeps the paper’s own inductive definition, under which a level-\(0\) remainder is allowed, and records exactness as the separate predicate that samplers are required to satisfy.
Let \(V = U \oplus W\) be a decomposition of \(V\) into complementary register subspaces.
(Levels.) Every \(\ell \)-level CL function is \((\ell +1)\)-level.
(Concatenation.) If \(L\) is a \(k\)-level CL function on \(U\) and \(R_u\) an \(\ell \)-level CL function on \(W\) for each \(u \in L(U)\), then \(x \mapsto L(x^U) + R_{L(x^U)}(x^W)\) is a \((k+\ell )\)-level CL function on \(V\).
(Direct sums.) If \(L\) is a \(k\)-level CL function on \(U\) and \(R\) an \(\ell \)-level CL function on \(W\), then \(x \mapsto L(x^U) + R(x^W)\) is a \(\max (k,\ell )\)-level CL function on \(V\).
Concatenation and direct sums preserve exactness in the sense of Lemma 6.4.
rk:higher-level, lem:cl-concat and lem:cl-func-prod of linear.tex, the last for two summands, which iterates. The Lean constructions are on presentations and carry no hypotheses; that the supports are disjoint enters in the evaluation lemmas identifying the function presented.
Let \(V = \bigoplus _{i=1}^{k} V^{(i)}\) with every \(V^{(i)}\) a copy of \(F^s\), and let \(L^{(i)}\) be an \(\ell \)-level CL function on \(V^{(i)}\) for each \(i\). Then \(x \mapsto (L^{(i)}(x^{(i)}))_i\) is an \(\ell \)-level CL function on \(V\), exact if every \(L^{(i)}\) is, whose marginals, factor spaces and stage maps read off a prefix are those of the \(L^{(i)}\) on the blocks. For two such families \((L^{(i)})\), \((R^{(i)})\), the conditionally linear distribution of the pair of direct sums is the product of the distributions of the pairs \((L^{(i)}, R^{(i)})\).
Item (3) of Lemma 6.5 iterated over the \(k\) summands, done in one induction on the level with the \(k\) presentations side by side: at every stage the register subspace is the union of the blocks’ and the map their direct sum, and the continuations are selected blockwise. The Lean presentation lives on any \(F^\kappa \) with \(\kappa \cong \{ 1, \ldots , k\} \times \{ 1, \ldots , s\} \), so that \(\kappa = \{ 1, \ldots , ks\} \) needs no reindexing. For the distribution: a uniform vector of \(V\) is a \(k\)-tuple of independent uniform vectors of the blocks, and the event that the direct sums take prescribed values is the conjunction of the blockwise events.
Let \(\mathbb {F}\) be a finite field, \(\mathbb {K}\) a subfield, and \(e_1, \ldots , e_t\) a basis of \(\mathbb {F}\) over \(\mathbb {K}\); let \(\kappa : \mathbb {F}^n \to \mathbb {K}^{nt}\) be the \(\mathbb {K}\)-linear bijection reading off the coordinates of each entry in this basis. If \(L\) is an \(\ell \)-level CL function on \(V = \mathbb {F}^n\), then \(L^\kappa = \kappa \circ L \circ \kappa ^{-1}\) is an \(\ell \)-level CL function on \(\mathbb {K}^{nt}\), whose decomposition data are the downsized data of \(L\): for \(j \in \{ 1, \ldots , \ell \} \) and \(u \in L_{{\lt}j}(V)\),
where \(\kappa (V_{j,u})\) is the register subspace of \(\mathbb {K}^{nt}\) on the coordinates \((i, k)\) with \(i\) a coordinate of \(V_{j,u}\). Exactness is preserved, and the CL distribution of \((L^\kappa , R^\kappa )\) is the image under \(\kappa \) of that of \((L, R)\).
lem:cl-downsize and lem:downsize-cl-dist of linear.tex, by induction on the level; the one fact used is that \(\kappa \) commutes with the coordinate projections onto register subspaces (lem:downsize_subspace of preliminaries.tex, in the register case).
Comments.
The paper states the lemma for admissible \(q = 2^t\), \(t\) odd, with the self-dual normal basis of Lemma 3.87; the formalization proves it for any basis of any finite field over any subfield, the coordinates of \(\mathbb {K}^{nt}\) being indexed by pairs \((i, k)\) and identified with \(\{ 1, \ldots , nt\} \) by a reindexing (CLFun.reindex, the transport along any bijection of coordinates, which preserves everything above). The self-dual normal basis matters elsewhere: for the arithmetic of \(\mathbb {F}_{2^t}\) to be computable from \(\mathbb {F}_2\)-data in polynomial time by the samplers and deciders that use it, a matter for the efficient-computability toolkit rather than for this lemma. The paper’s downsized sampler (def:downsize_sampler, lem:downsize_sampler), a Turing machine wrapping a sampler over \(\mathbb {F}_{2^t}\), has no counterpart here: samplers are over \(\mathbb {F}_2\) by definition (Definition 2.44), and a construction native to \(\mathbb {F}_{2^t}\), such as the introspection sampler, is to present the downsized CL functions directly, this lemma supplying their decomposition data.
Every soundness clause of this chapter is stated in \(\mathrm{val}^*\) and none in \(\mathrm{val}^{s}\). The choice follows the source transformation contracts and the direct repetition theorem (Theorem 5.6), all of which already concern \(\mathrm{val}^*\). No scalar transport from a synchronous value bound is needed. In particular, neither the synchronization statement of Theorem 3.3 nor the additional hypotheses discussed in Remark 3.4 enter the composition. The source rigidity analyses can therefore be formalized in their bipartite setting, without the synchronization invariant of Remark 2.48. Lemma 2.14 is used only to read a \(\mathrm{val}^*\) conclusion in \(\mathrm{val}^{s}\) when a synchronous statement is wanted (Theorem 6.214, Theorem 7.1), never in the other direction.
What this costs in turn is that the rigidity and approximate-measurement lemmas the inner analyses consume must be stated bipartitely, as their sources state them, rather than tracially. That is the arrangement of [ 1 ] and of the companion repository’s paper, so it is the arrangement with the least to prove.
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.38) 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.
Introspection is detyped at its exterior boundary. Oracularization stays typed inside answer reduction; the final answer-reduced verifier is then detyped. The exterior levels are \(5\to 7\to 7\) for introspection, answer reduction and repetition. Detyping adds two levels and gives \(\mathrm{failure}_{\mathrm{typed}}\leq 16^{|T|} \mathrm{failure}_{\mathrm{detyped}}\) via a same-state strategy conversion. This is a bound on failure, not a multiplicative comparison of values. The graph must have an edge. The following interfaces retain the effective and timeout hypotheses of the current source [ 34 ] .
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 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.
Given an admissible-field typed sampler \(S\) and a supplied total machine \(R_{\mathrm{field}}(n)=q(n)\), one can construct its coordinate downsizing over \(\mathbb {F}_2\), with dimension \(s(n)\log _2q(n)\) and unchanged levels and types. Runtime is polynomial in \(\mathsf{TIME}_S(n),T_{\mathrm{field}}(n),s(n),\log q(n),|T|\); description size and compilation cost are polynomial in \(|S|,|R_{\mathrm{field}}|,|T|\). The wrapper calls the field routine and dimension query before bounded-prefix parsing. A factor-support bit expands to a whole block of ones or zeros, not to the coordinate representation of a field element. There is no assertion that \(q(n)\) can be recovered from arbitrary sampler code. The introspection and PCP parameter routines separately supply this premise within their budgets; the binary case uses the constant routine. The Lean proof does not use this lemma: its samplers are presented directly over \(\mathbb {F}_2\), in Shoup coordinates (Lemma 6.7), as in Lemmas 6.123 and 6.177 and Definition 6.174.
Put \(t=|T|\). Two independent \(2t\)-bit blocks encode a vertex indicator and its neighbor indicator. A two-level CL graph sampler has a valid-edge event \(E_G\) with \(p=\Pr (E_G)=(2m_G-k_G)/16^t\geq 16^{-t}{\gt}0\). Each ordered adjacent pair has exactly one seed preimage; conditionally on \(E_G\) the types have the specified graph law, with loops counted once. On its support, an invalid edge exposes a zero opposite-neighbor block to at least one player, enabling a trivial local measurement on that branch.
The first CL factor reads the player’s two indicator blocks. The second factor is the whole complementary pair of blocks, with a linear map keeping only the opposite neighbor bit selected by a successful first-block decode. The one-hot indicator makes vertex encodings injective. Thus each ordered edge has exactly one valid seed, out of \(16^{|T|}\) seeds. Reindexing the valid-seed sum by ordered edges proves the conditional law. The sampled question preserves the own block and the selected bit; a failed local validity test has zero opposite block. This proves the semantic sampler and its law. The ambient program is the separate obligation of Lemma 6.20.
For \(\ell \geq 1\), concatenate the two graph levels with the selected type’s \(\ell \) levels on an independent binary seed block. On an unselected branch use the zero CL function. The result has \(\ell +2\) levels and dimension \(4|T|+s(n)\). Conditionally on \(E_G\), the contents are exactly the typed distribution generated by one shared seed; the two question contents need not be independent.
Embed the graph and content presentations into the two summands of the ambient register and concatenate them. The zero fallback consumes the whole content register at its first level and uses empty factors thereafter, so exactness also holds on rejected branches. On an ordered edge each player’s graph output is the fixed view of its own type. Reindexing the valid graph seeds by ordered edges proves the joint conditional law with one common content seed. The positive-level hypothesis covers the three-level typed sampler used by introspection.
Embedding a CL presentation along a coordinate injection preserves its marginal, factor and linear-map queries. In the detyped presentation the first two levels route to the graph sampler. Later levels route to the selected typed presentation using the content prefix. On an unselected branch all marginal and linear outputs are zero; the first content factor is the whole content register and the later factors are empty.
Extend each register-linear map by zero along the coordinate injection and restrict each continuation’s prefix to the original register. Induction on the presentation proves all four query identities. After the two graph levels, the accumulated graph prefix is the original graph part of the query prefix, and its content part is unchanged. These identities give the specified dispatch rules, including the zero fallback. They are the semantic correctness targets for the ambient sampler implementation.
Every fixed finite CL presentation with a full register partition has an actual ambient sampler program, with all marginal, linear and factor query clauses and halting on malformed inputs. In particular the fixed graph presentation has a two-level sampler of dimension \(4|T|\). Its runtime is polynomial in the raw query size, uniformly in the index. A single executable typed sampler can also be specialized to any fixed type, with explicit runtime transfer. These fixed-table bounds may depend on the whole finite presentation; they do not assert polynomial compilation time in a variable graph’s size.
Compile a finite table of all legal queries and use a total fallback elsewhere. For type specialization, a total raw-data adapter inserts the fixed type tag before calling the original program; the original halting theorem applies to every adapted raw query. The program evaluations and cost bounds are checked.
For positive-level partitioned typed CL presentations and a symmetric nonempty graph, every perfect PCC witness for the doubled typed finite game gives a perfect PCC witness for the doubled detyped finite game. The construction keeps the local dimension and tracial state and uses one player-independent measurement rule. This is a construction inside the ambient PCC representation.
Decode the Alice-view pattern, then the disjoint Bob-view pattern, and use a fixed deterministic answer otherwise. On a common seed, either both decoded views identify an actual ordered edge or one side uses the deterministic measurement and the predicate accepts. On an edge the original measurements and predicate are recovered. Positive support transfers commutation and zero failure from the original perfect PCC witness.
An actual ambient typed sampler with \(\ell {\gt}0\) levels and a fixed finite type graph gives an actual ambient sampler with \(\ell +2\) levels and dimension \(4|T|+s(n)\). Its closed program answers the dimension, marginal, linear and factor queries of the detyped presentation, and halts on every malformed query. A polynomial runtime bound transfers from the given typed sampler, with an explicit coefficient and a query degree independent of the index. The constants depend on the fixed graph; uniform polynomial compilation time and description size in a variable graph are not asserted.
Parse the raw query totally. The first two levels use the graph sampler; later levels either return the zero branch or forward one correctly typed query. The graph prefix supplies the selected type. A context-preserving one-call program reattaches the graph result. The proved query identities identify every returned bit string with the constructed CL presentation. The program’s evaluation cost is bounded by a polynomial combining routing, the forwarded call, the returned data size and postprocessing. Bounding that polynomial’s degree supplies the uniform query exponent.
Allow different typed and detyped answer alphabets, with question-dependent coarse-graining maps. If acceptance on every valid edge implies acceptance after those maps, restriction and coarse-graining preserve the state and give failure at most \(16^{|T|}\) times the detyped failure. Thus a decider may reject additional overlong answers. The program-level cutoff must still establish the stated acceptance implication.
Adapt the strategy’s questions and coarse-grain its answer measurements. The acceptance implication bounds conditional failure on each edge. Sum those bounds and apply the already proved detyping conditional-distribution identity.
For \(\ell \geq 1\), the concatenation is implemented with runtime \(\mathrm{poly}(|T|,\mathsf{TIME}_S(n))\), retaining bounded-prefix checks and valid-prefix query semantics. On a zero-tail branch its first factor receives the whole remaining seed block and later factors are zero, so factors still partition the ambient space. Valid factor output gives \(s(n)=O(\mathsf{TIME}_S(n))\). The implementation depends only on \(S,G\). The Lean proof uses the ambient form of this lemma, Lemma 6.18, for a fixed type graph.
Given an actual typed sampler, an all-input terminating typed decider and an executable index routine returning inner and outer answer cuts, construct an ambient detyped verifier. It rejects malformed raw encodings, wrong question lengths and answers beyond the outer cut. Within that cut, a nonedge accepts; a genuine edge additionally enforces the source typed-answer cut and calls the typed decider on the unchanged answers and content questions. On the outer finite answer alphabet its predicate is exactly the finite detyping predicate with the inner rejection included. The inner cut bounds the whole typed answer; an introspection implementation must separately check the original answer component before calling the original decider.
Use actual dimension and cutoff calls followed by a total finite-graph router. Only the canonical Boolean true result accepts. Evaluation determinism gives the exact acceptance equivalence, and the coordinate-numbering identities give the finite predicate equality. These statements prove no runtime bound for the supplied cutoff routine and assume no implicit inequality between the two cuts. Such bounds and the appropriate cut comparison remain explicit requirements when constructing a bounded compiler and transferring completeness.
The actual program-defined detyped verifier has exactly the finite detyping distribution and predicate under the explicit coordinate-numbering equivalence. Every strategy for it restricts to a typed-game strategy on the same state with failure at most \(16^{|T|}\) times its failure. Conversely, a perfect PCC strategy for the typed game gives an actual ambient perfect PCC strategy with the same local dimension. Both sides use the outer answer alphabet and the typed predicate includes rejection beyond the source typed-answer cut; there is no implicit comparison of two different answer alphabets. The Lean restricts a projective strategy in a bipartite model (Definition 8.62), of which a tensor-product strategy is the case of its tensor-product model, to one in the same model.
Transport the common seed and questions along the register equivalence. Finite-sum reindexing proves the distribution identity and exact strategy value preservation. Apply finite-game restriction and completeness, then transport the resulting strategies, including the doubling tags and PCC commutation clauses, to the actual verifier.
An executable index routine producing a unary cost budget gives a total typed decider from arbitrary source code, even if that code does not halt. The wrapper accepts exactly when the source returns the canonical Boolean true within the supplied budget. It preserves the acceptance predicate on inputs whose source evaluation is known to fit. The default construction uses the proved clocked self-interpreter. An explicit wrapper-cost bound combines the actual index-clock cost, interpreter polynomial and routing overhead. This supplies the totality mechanism; instantiating the appropriate growing clock and proving the final compiler’s time, size and answer-format bounds remain separate obligations.
Run the index clock, invoke the clocked universal interpreter on the complete original input, and inspect its success tag and Boolean result. The interpreter halts for every source program. Evaluation determinism identifies its tagged result with precisely an in-budget source evaluation, proving both directions of the acceptance law without a source-termination assumption.
Given the full verifier \((S,D)\) and \(G\), compile the dimension query from \(S\) and identify \(D\)’s timeout counter once at construction time. Let \(B=B_D(n)\) and choose a universal \(c\) with \(K=(cB)^c\geq \mathsf{TIME}_D(n)\). After bounded question checks, accept a non-edge view without scanning its answers. On an edge, inspect at most \(K+1\) symbols of each answer, reject overflow or malformed strings, then simulate the typed decider. An outer timeout \((C(|T|+1)B)^C\) for a sufficiently large universal \(C\) dominates every branch. Its binary coefficients are computed from the original counter; no runtime supremum is computed. All original legal answers have length at most \(K\). A valid edge and a length-\(K+1\) answer force that scan before rejection, ensuring the new game’s runtime-defined alphabet contains all original legal answers. The Lean proof does not use this source-model decider: it uses the executable decider with two answer cuts (Lemma 6.21), made total by the clock of Lemma 6.23.
A perfect PCC typed witness lifts on the same state to a perfect PCC detyped witness. Both players use the same combined rule: on an Alice-view pattern use the original Alice operator, on a Bob-view pattern use the original Bob operator, and otherwise use the identity measurement. The view patterns are disjoint. On valid edges this reproduces the typed strategy; on invalid edges one local measurement is trivial. Projectivity, consistency and the required commutation follow, as does the identical-operator property. This does not assert symmetry of the detyped question distribution.
Fix positive-level typed CL presentations, a symmetric type graph with at least one edge, finite answer alphabets, and a decision predicate. Construct the typed finite game by sampling a uniform ordered edge and a common seed. Construct the detyped finite game using the detyped presentations and the same answer alphabets, accepting outside valid edge views. Any strategy \(S\) for the latter restricts to a strategy \(S'\) for the former on literally the same state and local dimensions, with
The finite detyped game’s distribution equals the CL distribution of the constructed presentations. The two families of fixed player views are disjoint.
Restrict the measurements to the fixed graph view of each typed question. On every ordered edge the decision predicate and conditional failure probability agree. The typed failure is therefore exactly the detyped failure conditioned on valid graph seeds. Nonnegativity lets us bound this subsum by the whole failure sum; there is at least one ordered edge among \(16^{|T|}\) graph seeds. This proves the stated bound and its near-perfect value form. This finite-game result does not yet implement the machine wrapper’s answer cutoff, truncation, or runtime.
Restrict any detyped strategy of success at least \(1-\varepsilon \) to the fixed graph views for typed questions and coarse-grain answers to length \(\mathsf{TIME}_D(n)\). Answer truncation leaves the typed computation unchanged. Conditional detyped acceptance is no larger than acceptance of this legal typed strategy on the same state. Hence its failure is at most \(\varepsilon /p\leq 16^{|T|}\varepsilon \). Taking suprema uses near-optimal strategies and does not assume attainment of the value. In the ambient model nothing is truncated: the executable decider’s typed predicate already includes the source answer cut on the outer alphabet (Lemma 6.21), and the passage to suprema is made by each consumer of the bound.
The restriction to the graph views, with the conditional bound on the same state, is Lemma 6.26 for the finite detyped game. On the executable verifier it is MIPRE.CL.Detyping.DeciderProgram.restrictAmbient_value_ge (Lemma 6.22), which bounds the value of the restricted typed strategy from below by that of the detyped one.
For \(0\leq \varepsilon \leq 16^{-|T|}\), \(\mathrm{Ent}(\mathrm{detype}(V)_n,1-\varepsilon )\geq \mathrm{Ent}(V_n,1-16^{|T|}\varepsilon )\), since the conversion keeps the state and its Schmidt rank. Outside that range use the ordinary value bound; no negative threshold is supplied to \(\mathrm{Ent}\). This clause is separate from the value route. The Lean proof does not use this lemma: the value route needs only the same-state restriction of Lemma 6.22.
The descriptions of \((S,D)\) and the nonempty graph \(G\) suffice to construct the detyped verifier in polynomial description time. It has \(\ell +2\) levels, polynomial sampler and timeout costs, PCC completeness, and same-state soundness loss \(16^{|T|}\). The sampler depends only on \(S,G\). Effective field access for any preceding nonbinary downsizing is the separate hypothesis of Lemma 6.12. The Lean proof has no single detyping compiler. Each transformation builds its own from the pieces of Lemmas 6.18, 6.21 and 6.22, for its own fixed type graph (Lemmas 6.132 and 6.179).
The paper fixes a concrete Turing machine formalism and a timeout-counter normal form \(B(n) = c_0 (c_1 n)^{c_2}\): a machine is wrapped so that it always halts within its bound, and the wrapped description is canonical enough that the parameters can be read back off it. The ambient Lean model instead uses input-size-dependent resource budgets (Section 4.2). This changes the transformation hypotheses; it does not establish the source’s timeout or answer-truncation properties. Remark 6.31 records the required adaptation, and Section 1.3 records the departure.
Three things in those nodes are worth keeping even so, because they are the kind of detail a formalization rediscovers the hard way. The canonical form has to be genuinely injective in the parameters for the timeout bound to be well defined at all, and the audit had to supply an explicit parser to establish it — in the source the parser’s existence was asserted rather than constructed. The overhead polynomial relating a machine’s running time to its bound needs the normalization \(c_1 \geq 2\), without which the claim fails outright at \(c_1 = 1\), \(n = 1\). And the whole scheme rests on the bound dominating \(n\), which holds only because the constants are positive integers. None of the three is deep; all three are the sort of thing that stops a formalization dead.
The model distinction is recorded in Remark 2.51; here are its consequences for the transformations. The source introspection theorem uses an absolute bound \(N^\lambda \) at index \(N\); its simulator rejects after that many steps. Definition 2.49 instead bounds ambient cost on data \(d\) by \(N^\lambda (\left\vert {d} \right\vert +1)^\lambda \). Even on questions and answers of length at most \(N^\lambda \), this supplies a bound of order \(N^{O(\lambda ^2)}\), before simulation overhead, rather than \(N^\lambda \). It also gives no answer-prefix invariance for arbitrary longer strings.
To derive the ambient transformation hypotheses from the source, a normalization construction must restrict the valid input formats, preserve the original answer cut, and prove preservation of values and perfect PCC witnesses. It must provide the absolute simulation budgets and the truncation properties required by the source, including bounded checks on malformed inputs. If this requires a reparameterization \(\lambda ' = p(\lambda )\), its effect on the introspection bound \(\mathrm{poly}(2^{p(\lambda )n},\ell )\) and on the soundness margins must be propagated. Enlarging the answer alphabet to \(N^{\lambda '}\) without rejecting answers beyond the original cut can change the game. A direct proof in the ambient model is another route.
Lemma 6.32 proves the absolute legal-input bound and its universal-simulator overhead. The ambient introspection and answer-reduction contracts now allow the polynomial-exponent bounds \(2^{(\lambda n+1)^C}\) and \(2^{(\lambda n+1)^\mu }\). Answer reduction also retains the input sampler’s degree in its output budget, as in Lemma 6.33. The full compression composition is checked with these revised contracts and still has polynomial output bounds. This is an explicit ambient adaptation; the paper’s source-model theorem statements below retain their original time bounds. The absolute PCP clock, normalization construction and format-preservation clauses remain open. Budget and Verifier.Within record coefficients, degrees, question dimensions and explicit rejection bounds; GapCompression.output_rejects_long constrains the output. None of these supplies normalization for arbitrary \(\lambda \)-bounded inputs. The introspection, oracularization and answer-reduction source displays below use the paper’s absolute-time convention and its bipartite PCC notion. Separate ambient contract definitions carry the Lean tags and statement marks; their inhabitants require the supply targets stated below. In particular, identifying source PCC witnesses with ambient completeness witnesses requires the two directions of Remark 2.8. The comparison is with introspection.tex, oracularization.tex and ld_compiler.tex in the companion paper pinned by [ 34 ] .
For an ambient \(\lambda \)-bounded verifier, \(n\geq 1\), and questions and answers of length at most \((2^n)^\lambda \), the actual original decider halts within \(2^{(\lambda n+1)^5}\) cost. Any fixed universal simulator also halts on those inputs within \(2^{(\lambda n+1)^C}\) for a constant \(C\) depending only on its overhead polynomial. The original answer cut is unchanged. Any fixed polynomial of a polynomial-exponent budget fits another such budget.
The four encoded fields have size at most \(16(2^n)^\lambda +7\). Insert that size into the actual boundedness clause and bound the resulting exponent by \((\lambda n+1)^5\). Bound program and input sizes by the same exponential, and absorb the universal machine’s polynomial overhead. No answer-prefix invariance or malformed-input wrapper is asserted here. This is the absolute legal-input bound of Remark 6.31.
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.
Bound each factor by its corresponding power of \(B\). Compression fixes \(\mu \) before choosing its final bound, so that bound is still polynomial.
The introspective verifier
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.
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;
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;
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.
[\(\bullet \bullet \bullet \) hard]
Given the finite Pauli type graph and its distinguished \(X,Z\) vertices, construct the introspection graph with both hiding chains, the sampling and reading edges, the cross-introspection edge and all loops. It has \(|T_{\mathrm{Pauli}}|+2\ell +6\) vertices, hence \(2\ell +32\) when the Pauli graph has \(26\) vertices. Its type encoding uses binary hiding indices. Retain the supplied three-level Pauli CL family; every auxiliary type has the zero presentation with a full factor partition. The cross-introspection edge asks the two zero-content questions with probability exactly the inverse number of ordered edges. Its conditional failure is at most the edge count times the whole typed game’s failure.
The graph is the symmetric closure of the explicit oriented chains and Pauli edges. Constructor case analysis proves the edge classifications. Summing the uniform common-seed law over the zero auxiliary presentations gives the exact edge probability; nonnegativity bounds its contribution to the total failure. This supplies the graph and CL family. The uniform Pauli sampler and the introspective decision program are supplied by Lemmas 6.123 and 6.125.
Construct the finite predicate on parsed answers, with format and consistency checks, both orientations of the sampling and hiding tests, and the original decision predicate on the cross-introspection edge. The original CL family, original predicate, Pauli predicate and projection of Pauli answers to the original register are explicit parameters. The Pauli predicate is instantiated at the actual Pauli question contents. Accepted sampling answers satisfy every prefix comparison on the whole answer alphabet. Hiding projections use the registers selected by the later answer, as required by the adaptive construction. For every claimed output, the prefix is exactly its projection onto the selected register; at full length, this register is the complete partition. The cross-introspection check retains the original Alice/Bob argument order in either orientation. This is the parsed semantic predicate; byte parsing, global cutoffs and clocked program calls remain separate construction work.
Use a sum of the four answer formats. Dispatch by question constructors and check both orientations. Compute claimed-output prefixes by coordinate restriction, and dual readouts in the selected local register. Unfolding the checks gives the accepted-answer implications; the CL prefix theorem gives the marginal identity without assuming that a claimed answer is in the image.
An actual three-level typed Pauli sampler extends to the complete typed introspection family and then to an actual five-level sampler. Its dimension is \(4(|T_{\mathrm{Pauli}}|+2\ell +6)+s(n)\). Every marginal, linear and factor query agrees with the specified CL family, and malformed queries halt. The typed extension program is independent of \(\ell \). Polynomial runtime transfers with an explicit index-dependent coefficient and an index-independent query degree. Lemma 6.123 supplies the uniform Pauli sampler and its parameter and size bounds for the actual compiler.
Strip the sum tag and forward Pauli queries. Auxiliary queries produce the zero vectors or first-factor indicators of the supplied vector length. Dimension queries call the Pauli sampler. Apply the executable graph detyping compiler and compose its checked cost bound with the extension’s cost bound.
There are Turing machines computing the two halves of \(\mathsf{V}^{\textsc{Intro}}\) separately: one which on input \((\lambda , \ell )\) outputs the sampler \(\mathcal{S}^{\textsc{Intro}}\) in time \(\mathrm{polylog}(\lambda , \ell )\), with \(\mathsf{TIME}_{\mathcal{S}^{\textsc{Intro}}}(n) = \mathrm{poly}(n, \lambda , \ell )\) and \(\mathcal{S}^{\textsc{Intro}}\) a \(3\)-level typed sampler; and one which on input \((\mathsf{V}, \lambda , \ell )\) outputs the decider \(\mathcal{D}^{\textsc{Intro}}\) in standard timeout-counter form, in polynomial time, with \(\left\vert {\mathcal{D}^{\textsc{Intro}}} \right\vert = \mathrm{poly}(\lambda , \ell )\) and timeout bound \(B_{\mathcal{D}^{\textsc{Intro}}}(n) = \mathrm{poly}(2^{\lambda n}, \ell )\). The sampler’s description does not depend on \(\mathsf{V}\) at all. The Lean proof uses the ambient bounds of Lemmas 6.123 and 6.127 instead: polynomial budgets, a clocked decider in place of the timeout-counter form, and bounds for the detyped output rather than for the two typed halves.
The decider has to compute, for a level \(k\) and a prefix \(u\), the orthogonal complement \((L^v_{k+1, u})^\perp \) of the conditionally linear map at that level. The printed procedure computed it by taking a basis of \(\ker (M)\) and forming its canonical complement — and the canonical complement of a basis of \(\ker (M)\) is not a basis of \(\ker (M)^\perp \). Over \(\mathbb {F}_2^2\) the map \(L(x_1, x_2) = (x_1 + x_2, 0)\) is a counterexample, found independently by two checkers. Only the computation was wrong: the test itself is defined abstractly through the complement, so the statement of Lemma 6.38 and its bound are unaffected. It is recorded because a formalization must supply a procedure that is actually correct, and this is the obvious place to get it wrong. The same audit closed a second seam here, an answer-length bound of \(8Q\) that only holds once the honest answer is truncated the way oracularization and answer reduction already truncate theirs.
Completeness: two identities about Pauli measurements
The honest strategy measures EPR pairs in the bases the sampled question prescribes, so the completeness proof is not an approximation argument at all: it is two exact statements about how Pauli operators interact with measurements of a linear map, and then a check that the seven tests of the decider all pass with certainty. Both identities are finite-field linear algebra, and both are plausible early Lean targets.
[\(\bullet \bullet \) medium]
Let \(\mathbb {F}\) be a finite field of characteristic two, with \(\omega =-1\). Let \(L : \mathbb {F}^k \to \mathbb {F}^k\) be linear, let \(W \in \{ X, Z\} \), and for \(a\) in the range of \(L\) pick \(u_a\) with \(L(u_a) = a\). Write \(\sigma ^W_{[L(\cdot ) = a]}\) for the projector onto the event that a \(W\)-basis measurement returns a preimage of \(a\). Then for every \(v \in \ker (L)^\perp \),
and conversely, for every \(a\) in the range of \(L\),
The choice of \(u_a\) off the range of \(L\) is immaterial, since there the projector vanishes.
Each identity is the Fourier expansion of the other over the group \(\ker (L)^\perp \): the character \(v \mapsto \omega ^{\operatorname {tr}(u_a \cdot v)}\) depends only on \(a = L(u_a)\), because two preimages of \(a\) differ by an element of \(\ker (L)\), which the trace pairing annihilates against \(\ker (L)^\perp \).
[\(\bullet \) easy]
Over a finite field of characteristic two, let \(L, R : \mathbb {F}^k \to \mathbb {F}^k\) be linear with \(\ker (R)^\perp \subseteq \ker (L)\). Then the measurements \(\{ \sigma ^Z_{[L(\cdot ) = b]}\} _b\) and \(\{ \sigma ^X_{[R(\cdot ) = d]}\} _d\) commute.
Expand both families by Lemma 6.40. The \(Z\)-side expansion runs over \(v \in \ker (L)^\perp \) and the \(X\)-side over \(w \in \ker (R)^\perp \), and \(\sigma ^Z(v)\) and \(\sigma ^X(w)\) commute exactly when \(\operatorname {tr}(v \cdot w) = 0\). The hypothesis gives \(w \in \ker (L)\) for every such \(w\), and \(v \in \ker (L)^\perp \), so the pairing vanishes term by term.
[\(\bullet \bullet \bullet \) hard]
Over a finite characteristic-two field, reading a linear map of either Weyl eigenbasis outcome is a projective measurement. If \(\ker (R)^\perp \subseteq \ker (L)\), the joint readout with projectors \(\sigma ^Z_{[L(\cdot )=a]}\sigma ^X_{[R(\cdot )=b]}\) is also projective.
The Weyl spectral projectors are self-adjoint idempotents summing to identity, and coarse-graining preserves these properties. By Lemma 6.41, the two coarse-grained families commute. Their products are therefore self-adjoint idempotents; summing over both readouts gives the identity.
If \(\mathsf{V}_{2^n}\) has a value-\(1\) PCC strategy, then \(\mathsf{V}^{\textsc{Intro}}_n\) has one: the players measure their EPR halves in the bases the sampled question prescribes and then play the value-\(1\) strategy of \(\mathsf{V}_{2^n}\) on the question they have obtained. Every test of the decider accepts with certainty, and the resulting strategy is again projective, consistent and commuting. The Lean proof is that of Lemma 6.113, carried to the ambient output verifier: explicit Pauli and auxiliary measurements on a common carrier, rather than the Fourier and commutation argument below.
Lemma 6.40 identifies the honest sampling measurement with a Pauli measurement, which is what the Pauli test checks; Lemma 6.41 gives the commutation the hiding test needs, the hypothesis \(\ker (R)^\perp \subseteq \ker (L)\) being exactly the nesting of consecutive conditionally linear levels. Consistency and projectivity pass through the construction because each player’s measurement is a product of commuting projective measurements.
The soundness toolkit
Soundness needs three groups of lemmas before the induction can start, and they are separated here because they are independent of introspection and reusable: a Pauli twirl, a conversion from sub-measurements to measurements, and a way to condition on part of a question.
[\(\bullet \bullet \bullet \) hard]
Over a finite field of characteristic two, for a subspace \(K\leq \mathbb {F}^k\), twirl by the uniform distribution on \(\tau ^W(K)\), where \(W\in \{ X,Z\} \) and \(W'\) is the other basis. The twirl fixes \(\tau ^{W'}(u)\) if \(u\in K^\perp \) and is zero otherwise. Here the annihilator uses the field-valued dot product. The source proves the general-characteristic statement; this formalization supplies its characteristic-two specialization used by the pipeline.
Conjugation by the opposite Pauli family multiplies an operator by the sign of the trace pairing. Average these signs on \(K\). The character is trivial exactly on \(K^\perp \), by Lemma 6.40; all other character sums vanish.
Over a finite field of characteristic two, for a linear \(L:V\to V\), twirling an operator on \(\mathbb C^V\otimes H\) first by all \(Z\) Paulis and then by \(X(\ker L)\) gives \(\sum _{y\in L(V)}P_y^Z\otimes B^y\), where \(P_y^Z\) projects onto the fibre \(L(v)=y\). If the original operators form a POVM, the blocks form a POVM for each nonempty fibre. Empty fibres impose no condition on \(B^y\). The source proves the general-characteristic statement; the Lean theorem supplies the characteristic-two specialization. It sums over all \(y\in V\), with zero projectors outside the image, and chooses valid POVMs even at empty fibres.
The full \(Z\) twirl removes off-diagonal blocks in the sampled register. The \(X(\ker L)\) twirl averages the remaining diagonal blocks on cosets of \(\ker L\). Define \(B^y\) by this average at a chosen preimage of \(y\) (or at zero when there is none). Translation permutes each coset, so the block depends only on \(y\). Principal compressions and their averages preserve positivity, while linearity sends a normalized family to a normalized family. This constructs the ancillary POVMs directly.
For the fibre projections \(P_y^W\) of \(L\) and every operator \(M\),
The identity remains true after averaging questions and summing measurement outcomes. It introduces no dimension or alphabet factor.
Distinct nonempty fibres give orthogonal characters on \((\ker L)^\perp \). Apply Parseval to the complex-linear action that takes a register operator to its amplified commutator applied to the state. Empty fibre projectors vanish. Summing outcomes and averaging questions preserves the identity. The checked field specialization is characteristic two.
Let \(M_a^x\) be POVMs, \(\psi \) a unit bipartite vector and \(\mu _x\) a conditional unitary distribution. For \(\mathrm T_{\mu _x}(M)=\mathbb E_U UMU^\dagger \), put \(\delta =\mathbb E_x\mathbb E_U\sum _a \| ([M_a^x,U^\dagger ]\otimes I)\psi \| ^2\). Then \(\mathbb E_x\sum _a \| ((\mathrm T_{\mu _x}(M_a^x)-M_a^x)\otimes I)\psi \| ^2\leq \delta \). Jensen and left-unitary invariance of the norm suffice; invariance of the state under \(U\) is not a hypothesis.
Write each conjugation error as \(U[M,U^\dagger ]\). Left multiplication by \(U\) preserves the squared state norm, and convexity bounds the squared norm of the average by the average of the squared norms. Sum over outcomes and average questions. The Lean estimate has constant one and holds for arbitrary operator families and arbitrary state vectors.
Conditionally on \(x\), draw \(U_1,U_2\) independently. Suppose both commutators \([M_a^x,U_i^\dagger ]\) have average outcome-summed squared state norm \(O(\varepsilon )\) and \(\mathbb E\| ((U_2^\dagger \otimes I)-(I\otimes U_2))\psi \| ^2=O(\varepsilon )\). Then \([M_a^x,U_1^\dagger U_2^\dagger ]\) has the same type of bound. Transfer \(U_2\) across the bipartition and back; \(\sum _a(M_a^x)^2\leq I\) controls the summed transfer errors without an outcome-count factor.
Transfer the second unitary to its commuting mirror on Bob’s side, move the first unitary past the measurement, and transfer back. The four-link squared triangle inequality gives coefficients \(4,4,8\) for the two commutator errors and the mirror error. The POVM contraction identity controls the outcome sum. Independent conditional averages preserve these coefficients. With an exact mirror, the composed twirl costs at most four times the sum of the two averaged commutator errors.
[\(\bullet \bullet \) medium]
Let \(A_a^x\) be a PVM, \(B_a^x\geq 0\) with \(\sum _aB_a^x\leq I\), and \(C_a^x\) a POVM satisfying \(C_a^x\geq B_a^x\) pointwise. For a unit bipartite state and an arbitrary question distribution, define
Then \(D_\psi (A,C)\leq 2\delta +4\sqrt\delta \). In particular, if \(D_\psi (A,B)\leq \varepsilon \leq 1\), the conclusion is \(D_\psi (A,C)\leq 6\sqrt\varepsilon \). A coefficient-one square-root bound is not asserted for this literal squared-distance convention.
Using real parts and Cauchy–Schwarz in the outcome-summed state norm, \(\mathbb E_x\langle I-\sum _aB_a^x\rangle \leq 2\sqrt\delta \); here \(\sum _a(B_a^x)^2\leq \sum _aB_a^x\) and \(\sum _a(A_a^x)^2=I\). Since \(0\leq C_a^x-B_a^x\leq I\), \((C_a^x-B_a^x)^2\leq C_a^x-B_a^x\), so \(D_\psi (B,C)\leq 2\sqrt\delta \). The squared triangle bound gives \(D_\psi (A,C)\leq 2D_\psi (A,B)+2D_\psi (B,C)\).
Over a finite characteristic-two field, write the retained register as \(\mathbb {F}^{n_x}\) and the state in each question’s coordinates as \(\mathrm{EPR}_{\mathbb {F}^{n_x}}\otimes \xi _x\), with \(\xi _x\) normalized. Let \(e_0,e_Z,e_X\) be the marginal, fine-\(Z\) commutator and coarse-\(X\) commutator errors of a joint PVM. There are actual normalized POVMs on the complementary Alice space at every retained fibre, whose averaged squared distance from the joint PVM is at most \(2\delta +4\sqrt\delta \), where \(\delta =\mathbb E_x(2e_0+8e_Z+8e_X)\). If the three averaged errors are at most \(0\leq \varepsilon \leq 1\), the bound is \(56\sqrt\varepsilon \). Register dimensions and auxiliary spaces may vary with \(x\). The Lean states it in the register model on \(\mathbb {F}^{n_x}\) (Definition 8.72) of a normalized auxiliary model \(\Xi _x\), of which \(\mathrm{EPR}_{\mathbb {F}^{n_x}}\otimes \xi _x\) is the case of the tensor-product model of \(\xi _x\), with the POVMs in the first player’s algebra of \(\Xi _x\).
Twirl into ancillary POVM blocks, keep the matching fibre using the exact EPR mirror, and complete its submeasurement by summing over the discarded output. Average the pointwise estimates using concavity of the square root. This includes empty fibres. The ambient coordinate transport is proved in Lemma 6.51.
Let \(U_x\subseteq V_x\subseteq V\) be coordinate registers, \(L_x:U_x\to U_x\) linear, and the state be \(\mathrm{EPR}_V\otimes \mathrm{aux}\). Let \(M^x_{y,a}\) be a PVM on Alice’s \(V_x\) register and auxiliary space. Assume its \(y\) marginal is \(O(\varepsilon )\)-close to \(P_y^Z(L_x)\) in the averaged squared state norm, and that its commutators with the fine \(Z\) projectors on \(U_x\) and coarse \(X\) fibre projectors for a map with kernel \((\ker L_x)^\perp \) have total outcome-summed squared norm \(O(\varepsilon )\). For \(0\leq \varepsilon \leq 1\) there are POVMs \(N_a^{x,y}\) on the complementary register outside \(U_x\) in \(V_x\) and Alice auxiliary space with
for a universal \(C\) (once the hypothesis constants are fixed). The sums in the commutator hypotheses include both projector and measurement outcomes. Empty fibres allow any \(N\); their left-hand mass is controlled by consistency, not identically zero.
Split the actual finite coordinate registers by explicit basis equivalences. The ambient EPR state factors exactly, and adjoining or removing the untouched complement preserves every squared state norm. Pull back the local operators, apply Lemma 6.50, and transport its actual POVMs back to the residual register. With each hypothesis bounded by \(\varepsilon \), the conclusion has the explicit constant \(56\). The source’s route: twirl to blocks \(B^z_{y,a}\), retain the matching blocks \(B^y_{y,a}\) using projectivity and EPR consistency, then complete with \(N_a^{x,y}=\sum _z B^y_{z,a}\). Lemma 6.49 accounts for the square-root loss. Transfers across EPR use matrix transpose, in particular \(X(v)^T=X(-v)\); no odd-characteristic identity \(X(v)^T=X(v)\) is presumed.
[\(\bullet \bullet \bullet \) hard]
On a state that factors as a question part times an answer part, a projective measurement of the question part induces a distribution on it, and consistency or commutation statements about the unconditioned measurements transfer to the measurements conditioned on the sampled question. In particular, if \(\sum _{x, y, z} \langle \psi | A^y_{x, z} \otimes B_{x, y, z} |\psi \rangle \geq 1 - \delta \) with \(\{ B_{x,y,z}\} \) projective, then \(I\otimes B_{x, y, z} \approx _\delta A^y_{x, z} \otimes B_{x, y}\).
On a product state, the squared norm of a tensor-product operator factors. The question factor is exactly the probability weight. This gives exact conditioning and commutator identities, also for outcome-dependent tensor decompositions. For conditional consistency, the operators \(A^y_{x,z}\otimes B_{x,y}\) form a positive submeasurement. Expand its distance from \(I\otimes B_{x,y,z}\), use projectivity to identify the cross term with the agreement probability, and bound each diagonal sum by one. The literal summed squared-distance bound is \(2\delta \).
Soundness
[\(\bullet \bullet \bullet \) hard]
There is \(\delta _1(\varepsilon , R) = a\bigl( (\log R)^a \varepsilon ^b + (\log R)^{-b} \bigr)\), with \(a {\gt} 1\) and \(0 {\lt} b {\lt} 1\) depending only on \(\ell \), such that any strategy for \(\mathsf{V}^{\textsc{Intro}}_n\) of value \(1 - \varepsilon \) is within \(\delta _1\) of a projective strategy whose state is \(|\textsc{EPR}_2\rangle ^{\otimes Q} \otimes |\textsc{aux}\rangle \) and whose Pauli-test measurements are the actual Pauli operators \(\sigma ^W_x\) on those \(Q\) qubits, for both players.
Comments.
The formal route keeps the paper’s estimates as distances instead of replacing the strategy: Lemma 6.115 is the application of Theorem 3.38, through Corollaries 3.39 and 3.40, that this proof makes, and Lemma 6.111 accounts for the replacement. The statement above, with its exact state and exact Pauli operators, is not formalized as such.
[\(\bullet \bullet \bullet \) hard]
Construct a CL output-prefix map on every claimed full output; on honest outputs it agrees with the truncated CL evaluation. For any finite game, a subtest of weight \(c{\gt}0\) whose accepted answers force equality of processed outcomes gives averaged squared cross-party distance at most \(2\varepsilon /c\), where the game’s failure is at most \(\varepsilon \). The probability hypothesis is a pushforward bound, so the sampled question map need not be injective. Replacing one side by ideal Pauli readouts of squared error \(\eta \) costs at most \(2\eta +4\varepsilon /c\). All output values, including impossible claims, are controlled. Two such tests with a common opposite-party measurement give a same-side bound \(4\varepsilon /c_1+4\varepsilon /c_2\). A chain of \(k\) squared edge errors bounded by \(\delta \) costs at most \(k^2\delta \), without an outcome-cardinality factor.
Coarse-grain the accepted-answer relations before converting consistency to distance. The opposite-party triangle inequality then gives the same-side estimate. Telescope the operator chain and use Cauchy–Schwarz. These are checked subtest lemmas; their acceptance implications and probability bounds must still be instantiated for the actual introspective decision procedure.
For the concrete parsed introspection game of failure at most \(\varepsilon \), the sampling-prefix and terminal hiding/Read cross-party squared distances are at most \(2|E|\varepsilon \), where \(E\) is the set of ordered type edges. Comparing the terminal hiding and Read measurements on the same side costs at most \(8|E|\varepsilon \). The predicates, question distribution, and Read consistency loop are those of the constructed game; no separate acceptance or selection-weight premise is assumed. Wrong answer constructors have a distinct coarse outcome, so the estimates include the whole answer alphabet. The Pauli subpredicate receives the actual Pauli question contents. The adjacent hiding induction and product-form rigidity remain separate.
Bound each fixed auxiliary edge’s conditional failure using its exact mass \(1/|E|\). The parsed acceptance checks imply the appropriate equality of coarse outcomes, so consistency gives the cross-party bounds. Use the Read consistency loop as the common opposite-party measurement for the same-side comparison. Both hiding orientations are proved directly from the predicate.
For the strategy of Lemma 6.53 and each level \(k \in \{ 1, \ldots , \ell \} \), the player’s reported question agrees with the \(Z\)-measurement of the conditionally linear map at that level up to \(\delta \), and the two players’ reports agree with each other up to \(\delta \). Consequently the reported \(y\) is distributed as the conditionally linear distribution of \(\mathsf{V}_{2^n}\), up to \(\delta \). The Lean proof does not use this lemma as stated: the sampling estimates of Lemmas 6.54 and 6.55 bound cross-party errors on the strategy itself, with no extraction, and feed the induction directly.
[\(\bullet \bullet \bullet \) hard]
For each level \(k\), a player’s answer on the \(\mathtt{Hide}_k\) type is \(\delta \)-close to one computed from the level-\(k\) complement alone, and the chain of these relations across levels \(j \leq k\) is stable: knowing the answer at level \(j\) tells a player nothing about the conditionally sampled part at level \(k\) beyond what it is entitled to. The rigidity form states this as closeness of the hiding measurement to an explicit product of \(Z\)- and \(X\)-measurements on the complements. The Lean proof does not use this lemma as stated: it uses the hiding and reading rigidity of Lemmas 6.76, 6.77 and 6.74.
[\(\bullet \bullet \bullet \) hard]
For each level \(k \in \{ 1, \ldots , \ell + 1\} \) there are ancilla states and projective measurements, acting on the player’s space together with the ancilla, which reproduce the strategy’s behaviour on the first \(k\) levels while acting as the identity on the subspace the first \(k\) levels have already fixed. Running the induction to \(k = \ell + 1\) converts a strategy for \(\mathsf{V}^{\textsc{Intro}}_n\) of value \(1 - \varepsilon \) into a strategy for \(\mathsf{V}_{2^n}\) of value \(1 - \delta (\varepsilon , n)\) on a state of comparable entanglement, which is the soundness and entanglement content of Theorem 6.129. The Lean proof does not use this lemma as stated: its induction is two-sided (Lemma 6.101), followed by the extraction of Lemma 6.102 and the soundness of Lemma 6.104. It tracks the value only, not the entanglement.
For arbitrary finite question maps, computational readout of a shared EPR seed has exactly their common uniform-seed distribution. Tensor each question projector with a projective auxiliary measurement depending on that question. These form a joint PVM, and their accepted mass is exactly the value of the strategy using the auxiliary state and auxiliary measurements in the original game. Discarding the question EPR register incurs no further error or dimension factor. The identity is specialized to the actual CL distribution of a verifier. This assumes the terminal tensor-product measurement form, which the soundness induction below derives from arbitrary high-value introspection play. The Lean states it in the register model (Definition 8.72) of an auxiliary model: the auxiliary measurements form a projective strategy of the auxiliary model (Definition 8.62), and every value model dominating that model has value at least the accepted mass, of which the quantum value is the case of a tensor-product model.
Evaluate the diagonal projectors on the normalized EPR state; the result is the normalized size of the common question fibre. Born probabilities factor over the EPR and auxiliary systems. Rearranging the finite acceptance sum gives the original strategy value. Package the auxiliary PVMs as a legal tensor strategy and compare with the supremum defining quantum value.
Write \(E(a,b,x,\varepsilon )=a(x^a\varepsilon ^b+x^{-b})\). For \(x\geq 1\), \(\varepsilon \geq 0\), \(C,a\geq 0\), \(0{\lt}b\leq 1\) and \(0{\lt}r\leq 1\), there are explicit \(A\geq 1\) and \(0{\lt}B\leq 1\) such that \(C E(a,b,x,\varepsilon )^r\leq E(A,B,x,\varepsilon )\). One can take \(A=\max \{ 1,Ca^r,ar\} \) and \(B=br\). This also absorbs any fixed number of square roots and a fixed rescaling of \(\varepsilon \), including detyping’s factor. For \(0\leq \delta \leq 1\), the state-transfer loss satisfies \(\delta +2\sqrt\delta \leq 3\sqrt\delta \).
Use subadditivity of the \(r\)-power on nonnegative sums and monotonicity of powers with base at least one. Each square root multiplies the exponent by \(1/2\). Absorb the fixed error rescaling into the coefficient before applying the power bound. These are quantitative closure results; they do not replace the soundness induction that must supply the error estimates.
For each fixed exponent \(k\), an actual closed program generates the unary budget \(2^{(\lambda n+1)^k}\). Hardwiring \(\lambda \) adds only its binary encoding size and a fixed overhead; the parameter-to-program compiler is polynomial time. For \(k,\lambda ,n\geq 1\), generation time is polynomial in that budget and is bounded by a uniformly enlarged introspection budget. A total clocked simulator reads the clock at index \(n\) and runs the original program at \(2^n\). For a bounded source verifier and legal original questions and answers, the exponent-five clock preserves acceptance exactly. Its actual compiler has polynomial cost and output size in the source description size and binary parameter length. For a bounded source and positive index, the complete clock generation, reindexing, universal simulation and result check fit a uniformly enlarged introspection budget. This is the original-program simulation component, not the complete introspection predicate or its cutoff parser.
Compose the checked unary arithmetic and exponentiation programs, hardwire the binary parameter using the actual specialization compiler, and bound the cost by a fixed polynomial in the output budget. The reindexing program changes only the source index. Determinism and the legal-query runtime bound show that clocking preserves the source’s accepting result. Compose the actual program constructors for compilation, and absorb the complete execution cost into a fixed polynomial of the generated budget.
For fixed register length \(Q\) and original-answer bound \(R\), actual polynomial time programs parse the paper’s pair and triple answer encodings. They check all register lengths and the separate original-answer cutoff. The encoding uses \(00,01\) for bits and \(10\) for component termination; exact re-encoding rejects extra fields, malformed delimiters and trailing bits. Under \(Q\geq 4\) and \(3R\leq Q\), honest encodings fit strictly below the outer \(8Q\) bound. A guarded source-call program rejects invalid pairs before evaluating the source. On valid pairs, acceptance is exactly source acceptance on the parsed fields, with halting and polynomial runtime transfer for total bounded sources. This component retains the input index and the full register questions. Index-dependent parameter generation and projection to the original question space are supplied by Lemma 6.63. The complete auxiliary-test dispatch remains a separate obligation.
Implement doubling and candidate decoding with list folds, then compare the input against the re-encoded candidates. Injectivity follows from the first delimiter. The checked one-call routing program tests the format and inner cutoffs first, and calls the source only on its accepting route. Determinism gives the acceptance equivalence, and the routing cost theorem bounds the complete execution.
The pair and triple parsers now take binary \(Q,R\) as inputs; requested slices are capped by the actual input length before unary scanning. A closed program computes the canonical bounds from binary \((\lambda ,n)\), queries the source sampler’s dimension at \(2^n\), checks the outer and inner answer cuts and exact zero padding, projects both questions to the source dimension, and runs the source decider at \(2^n\). Both source calls are clocked. The program halts on every raw input even for arbitrary source program texts. For a bounded source and \(n\geq 1\), its acceptance is exactly the guard conjunction with original source acceptance on the projected questions. The actual compiler has polynomial compilation time and description length in both source sizes and binary \(\lambda \). A composed execution bound includes all parameter, query, parsing and simulation costs. Parameter admissibility, absorption of this bound into one universal introspection budget, and the other typed-test branches remain separate obligations.
Compute bounded slices with binary counters and check exact re-encoding. The canonical arithmetic programs generate the actual register and answer bounds. A clocked ordinary sampler query supplies the dimension; boundedness proves that this query fits the exponent-five clock. The guard proves exact source-question lengths and zero-tail membership before the source call. Compose the routing and clocked simulation programs, use determinism for acceptance equivalence, and compose their cost bounds. The AST constructors and specialization compiler establish the binary description bound.
A perfect PCC strategy for the source game gives an actual perfect PCC strategy for the induced four-type Introspect/Sample game, including its loops, sampling edges and cross-introspection edge. Its dimension is the source dimension times the seed alphabet size. Honest Pauli-\(Z\)/Sample and Pauli-\(X\)/first-Hide effects commute and their products vanish whenever the full parsed test rejects. All outcome labels are retained. The extension to all adaptive Read and Hide types is proved in Lemma 6.68. The complete Pauli subgame remains a separate construction.
Tensor the source measurements with diagonal seed-fibre projectors. Disjoint fibres annihilate, so source PCC is needed only for question pairs arising from a common seed. The first hiding PVM is the coarse-graining of the full Pauli-\(X\) measurement that reports the first dual readout and the untouched tail. Check the actual parsed predicate on every constructor.
The first marginal of honest Hide at index \(k\) is exactly the readout of the CL presentation truncated at \(k\). Nonzero Read and Hide effects force their reported vectors to be supported on the active register. The full Pauli-\(X\) measurement factors under the actual local/tail coordinate split, and the stopping Hide measurement has the corresponding dual-linear-X/tail form. Neighboring hiding effects commute; for \(k+1{\lt}\ell \), every answer pair rejected by the actual adjacent-hiding check has zero product. For \(k+1=\ell \), the terminal Hide and Read effects commute and every rejected terminal comparison has zero product. These statements include all outcome labels.
Induct on the CL tree. The common local Z/dual-X PVM annihilates unequal local labels before the tail relation is used. At the first stage, the exact product selects the common dual output and the exact stopping-tail answer. At later stages, nonzero tail effects supply their own support conditions; the actual verifier relations lift through the common local label. Both tail projections in the adjacent comparison use the later reported question. The terminal stage identifies the common prefix and complete dual output.
The actual core, full Read, and Hide measurements extend to PVMs on the common parsed-answer alphabet, acting on one register/source space. Wrong constructors have zero effect. In both orientations of the Introspect/Read edge, every pair of effects commutes and every rejected answer pair has zero product. The same all-constructor guarantees hold in both orientations of every adjacent Hide edge and the terminal Hide/Read edge, with their actual index conditions and parsed verifier predicates.
Embed the proper pair, Read, or Hide labels and extend by zero. For Hide, tensor the adaptive register PVM with the identity on the source register. Summing over all constructors recovers the original PVM normalization. Constructor case analysis reduces the reading edge to its exact refinement identity; all other products vanish. For hiding edges, identify the parsed check exactly with the corresponding CL relation and apply the honest hiding product theorem. Tensoring with the source identity preserves both commutation and rejected-product vanishing.
Recursion on the original CL presentation constructs the honest register PVMs for Read and every Hide level, including adaptive branch-dependent registers. The Read first marginal is exactly the original CL question readout. Attaching the original question-dependent answer measurement gives the full Read PVM, whose Introspect marginal is exact. Its effects commute with Introspect, and every rejection by the actual parsed Introspect/Read test has zero operator product. The hiding edges are proved in Lemma 6.65; assembly with the full Pauli strategy remains an additional obligation.
At a CL node, measure the commuting linear-Z and dual-linear-X outcomes on the selected register, and use the Z outcome to select the continuation on the complement. These factors are disjoint, so their controlled tensor product is a PVM. Nonzero matrix rows force the reported CL question; summing the dual outcome gives its exact computational readout projector. Then tensor the original answer PVM and use its orthogonality.
A perfect PCC source strategy extends to an explicit perfect PCC strategy for the induced game on every auxiliary type: Introspect, Sample, Read and all Hide levels, with the actual uniform ordered-edge law and full parsed answer alphabet. Its dimension is the seed cardinality times the source dimension. The recursive first Hide is exactly the full-register Pauli-\(X\) coarse readout. The concrete parsed \(X\)/first-Hide and \(Z\)/Sample edges commute and have zero rejected products in both orientations. Construction of the honest strategy for all 26 Pauli types is still required for full typed completeness.
Transport the local first-stage Fourier basis through the full-register coordinate equivalence. Assemble the previously constructed measurements on one register/source space. Analyze every edge of the induced auxiliary graph, including loops and the cross-introspection edge. Commuting effects establish PCC; vanishing rejected products establish value one.
The next hiding comparison factors through the preceding fine hiding label: its preceding question prefix, current dual output and remaining tail. The later question prefix is retained as the key. A dummy label handles malformed answers and disagreeing prefixes, so every keyed coarse family is complete. Success in the actual parsed adjacent-Hide test gives conditional squared error at most \(2|E|\varepsilon \). With preceding fine error \(\varepsilon _f\) and prefix-normalizer error \(\eta \), replacement by a commuting ideal prefix costs at most \(6|E|\varepsilon +3\eta +3\varepsilon _f\).
Claimed prefixes nest even outside the image of the CL map. Equal preceding prefixes select the same next register, and the next dual readout and tail depend only on the previously retained tail. The actual accepted-answer relation therefore supplies the guarded equality. Extract its probability from the uniform ordered-edge law and apply conditional consistency and the normalizer replacement of Lemma 6.72.
For any hiding index \(j\) and \(m\leq j\), the actual Hide-\(j\) and Introspect measurements of the reported \(m\)-prefix on Alice’s side have squared distance at most \(8|E|(\ell -j+1)^2\varepsilon \). Every wrong answer constructor contributes to a separate dummy outcome. No honest-image or support assumption is imposed on the strategy’s answers.
Construct the actual path from Hide-\(j\) through the remaining Hide vertices and Read to Introspect. Each accepted edge preserves the reported prefix. Combine its cross-party estimate with the consistency loop at the next vertex to get same-party error \(8|E|\varepsilon \). Telescope the chain with the squared Cauchy–Schwarz inequality.
The same prefix-chain estimate holds on Bob’s side without assuming that the Pauli predicate is symmetric. The actual conditional marginal in the adjacent hiding test is exactly the later answer’s reported-prefix measurement, including the malformed label. If the corresponding Introspect prefix has squared error \(\delta \) from its ideal, then the later Hide normalizer has error at most \(16|E|(\ell -j+1)^2\varepsilon +2\delta \).
Use each forward path edge and the loop at its earlier endpoint to obtain Bob’s estimate via the common Alice measurement. Sum the joint coarse outcomes to identify the actual prefix marginal exactly, then combine the chain and Introspect-prefix distances by the squared triangle inequality.
Let \(M_i,P_i\) be complete projective families on opposite parties and \(Q_y\) a complete projective prefix family commuting with every \(P_i\). For arbitrary keyed maps \(f_y\), define \(T_{y,z}=Q_y\sum _{i:f_y(i)=z}P_i\). This is a PVM. If the fine cross-party squared error is at most \(\varepsilon _f\), the actual marginal \(R_y\) has squared error at most \(\eta \) from \(Q_y\), and the conditional comparison has squared error at most \(\alpha \), then the later measurement has squared error at most \(3\alpha +3\eta +3\varepsilon _f\) from \(T\). There is no alphabet-size factor. Exact mirrors of the primitive prefix and fine families transfer this conclusion to the opposite-party ideal family.
All keyed off-diagonal Born terms are nonnegative because the ideal prefix and fine projectors commute. The diagonal terms recover the original fine overlap after summing the complete prefix family. Convert overlap to squared distance with the prefix attached as a normalizer. Completeness removes Alice’s coarse projectors from the summed normalizer-change error. Apply the three-term squared triangle inequality. Exact mirrors reverse products; commutation restores the order in the ideal family.
The computational readout of the next truncated CL prefix is a complete PVM with zero malformed outcome and commutes with the preceding honest Hide family. Its product with the guarded coarse preceding family is exactly the next honest hiding measurement under the actual test’s retained map. Discarding the redundant key bookkeeping gives exactly the next fine hiding coarse family. Only CL support and the adjacent-level index condition are assumed; the operator identities are proved from the constructed measurements.
The next prefix is a marginal of the next honest Hide PVM, whose effects commute with the preceding Hide effects. Matrix support forces every nonzero effect’s claimed prefix to be fixed by prefix extraction. Expand the ideal conditional product in the next PVM. Rejected products vanish; summing the complete earlier family leaves exactly the indicated next outcome. Finally compose the retained outcome maps.
On an extracted EPR seed register tensored with any normalized auxiliary state, let the actual parsed projective strategy fail with probability at most \(\varepsilon \). Suppose its preceding Alice hiding coarse measurement has cross-party squared error at most \(\varepsilon _f\) from the ideal, and its Bob Introspect prefix has squared error at most \(\delta \) from the ideal prefix. Then the next Bob hiding coarse measurement has cross-party squared error at most
The conclusion concerns the actual complete parsed measurement, including malformed outcomes. No conditional estimate, ideal commutation, mirror or next-level rigidity hypothesis is assumed. Lemma 6.76 below supplies the base, prefix estimates and iteration from the primitive extracted Pauli guarantees. The later product-strategy induction is separate.
Prove transpose invariance of the adaptive honest operators and their exact EPR mirrors, then tensor with the arbitrary auxiliary state. Apply the actual conditional normalizer estimate and the actual prefix-chain bound. Transfer the paired ideal to the other party before coarse-graining cross-party consistency. The retained map on parsed answers and the concrete ideal product identity identify both sides with the next fine hiding families.
Let \(e=|E|\varepsilon \) for the actual parsed game on an EPR seed and arbitrary normalized auxiliary state. Suppose the fixed Pauli-X and Pauli-Z questions have primitive extracted squared errors \(\delta _X\) on Alice and \(\eta _Z\) on Bob. The actual X/first-Hide test gives first-Hide Bob error at most \(4e+2\delta _X\). The Z/Sample and Sample/Introspect tests give every Bob Introspect-prefix error at most \(4\eta _Z+12e\). Projectivity is required where used for coarse-graining; malformed outcomes are included. Constancy of the two Pauli questions is stated explicitly.
Compute the exact Pauli/auxiliary edge masses. Transfer primitive ideal operators across their exact EPR mirrors before coarse-graining. Identify the ideal first hiding family and every ideal prefix as the corresponding coarsened Pauli readouts, then use the actual accepted-answer comparisons.
Under the primitive extracted Pauli guarantees and actual game-success hypothesis above, every hiding level is rigid on both parties. A uniform Bob bound is
and a uniform Alice bound is \(4e+2B\). This completes the hiding-measurement induction without a base-case or prefix-rigidity conclusion among the assumptions. The constant depends on \(\ell \), not on the answer alphabet.
The actual consistency loop transfers Bob rigidity to Alice with cost \(4e+2B_k\). The adjacent step gives \(B_{k+1}\leq 6B_k+(18+48\ell ^2)e+6\delta \). Solve the finite recurrence and substitute the proved base and prefix bounds. No symmetry of the Pauli predicate is needed. Supplying the extracted state and primitive Pauli guarantees from the QLD theorem is a separate interface.
Read’s marginal consisting of a stage’s preceding claimed prefix and its dual answer is rigid at every stage on both parties. Its ideal family is the concrete honest hiding family with its unused X tail summed out. Uniform Alice and Bob squared-error bounds are \((16\ell ^2+8)e+4B\) and \((32\ell ^2+20)e+8B\), respectively.
Every later hiding test preserves this fixed prefix/dual pair, including claimed outputs outside the CL image. Telescope the actual chain to Read at this coarse alphabet, with quadratic path loss. Discard the hiding tail through cross-party projective consistency, then use the Read consistency loop and exact ideal mirror for the other party.
The actual Read joint measurement yields a commutator bound for the full Introspect question/answer and each ideal prefix/dual family. The Sample joint measurement yields the corresponding bound with any finite coarsening of the computational readout, including adaptive prefix and selected-coordinate maps. Both follow from game success and the proved rigidity estimates.
Choose the coarse joint outcome before applying commutation analysis. Its first marginal is tested against Introspect; its second is compared with the proved ideal Read or Sample readout. Removing prefix projectors and constructing the evolving residual strategy remain obligations of the product-form induction.
For a current projective measurement on register \(V\), two actual opposite-party coarse joint PVMs provide the tested \(Z\) and \(X\) marginals. A common sampling marginal provides the remaining linear-readout consistency. If the sum of these six averaged errors is at most \(\varepsilon \) and \(16\varepsilon \leq 1\), the stage constructs actual POVMs on the residual register obtained by removing \(U\) from \(V\), with product-form squared-distance error at most \(224\sqrt{\varepsilon }\). Commutator estimates are conclusions of the coarse tests, rather than hypotheses. The prefix-conditioned identification and iteration across all CL levels remain separate obligations.
Apply commutation analysis to each coarse joint PVM, and combine the two sampling comparisons on the same side. The resulting mixing premises are bounded by \(16\varepsilon \). Apply ambient Pauli mixing on the actual nested registers and simplify \(56\sqrt{16\varepsilon }\).
A family of residual POVMs admits simultaneous projective dilations with one fixed ancilla state for every question and prefix. Prefix projectors are left intact. Compression and Born probabilities are exact, and an original PVM at averaged squared distance \(\delta \) from the product POVM is at averaged squared distance at most \(2\sqrt{\delta }\) from the dilated PVM on the enlarged state. A dependent-family version allows all local register carriers and transported states to vary with the prefix, while retaining the same ancilla alphabet and state. Explicit reassociation preserves the original EPR factor. The Lean states it in a bipartite model: the ancilla is a one-sided extension (Definition 8.75) by the ancilla of a Kraus dilation in a fixed basis state (Lemma 8.77), whose size depends on the POVMs, and so on the question in the dependent-family version, and the reassociation exchanges the two layers of the register model.
Apply simultaneous Naimark dilation only to the residual factor. Compression identifies the mixed quadratic forms, and PVM normalization plus Cauchy–Schwarz bounds the resulting distance. Jensen combines the local bounds. For varying carriers, choose each local dilation and apply the same weighted estimate. Reassembly via the adaptive register permutations remains an obligation of the global induction.
The next visited register and dual readout depend only on the claimed output prefix. In the actual parsed adjacent-Hide game, the earlier player’s coarse answer is therefore conditioned on precisely the later player’s retained prefix. If the later measurement is projective, the conditional squared-distance estimate is at most \(2|E|\varepsilon \). The conditioning marginal is retained as an operator; it is not replaced by an unconditional distance or an assumed ideal hiding measurement.
Prove prefix invariance by recursion on the CL presentation. The four accepted-answer comparisons imply the conditional equality of coarse labels. Use the later joint PVM and its marginal to convert conditional consistency to squared distance, and the actual edge probability \(1/|E|\) to bound failure.
Replacing projective measurements at summed squared state distances \(\delta _A,\delta _B\) changes any test acceptance by at most \(2\sqrt{\delta _A}+2\sqrt{\delta _B}\). Replacing normalized state vectors at squared distance \(\eta \) changes the full game value by at most \(2\sqrt{\eta }\). These bounds have no answer-cardinality factor. The measurement-replacement statements require projectivity, so the mixing output must first undergo a quantitatively controlled common-ancilla dilation.
Apply two Cauchy–Schwarz bounds to the accepted outcomes of the joint PVM. Summing the unchanged party’s outcomes removes it exactly from the distance. For state replacement, the accepted effect is a contraction; expand its quadratic-form difference and average with the normalized question law.
The actual cross-introspection test rejects every non-pair constructor and has probability \(1/|E|\). Terminal product-form measurements therefore construct an original-game strategy on exactly the auxiliary spaces with failure at most \(|E|\varepsilon \). With squared state error \(\eta \) and terminal measurement errors \(\delta _A,\delta _B\), the proved bound is
No separate conditional-acceptance premise is assumed. The Pauli extraction and hiding induction must still produce the state and terminal approximations.
Restrict the acceptance sum to the pair constructors using the parsed predicate, identify their Born law with the original CL distribution, and apply the exact auxiliary-strategy extraction. Combine the actual edge failure bound with the proved state and measurement replacement bounds.
The actual CL continuation acts only on the complement of the visited registers. Its next factor and linear map are computed from the original presentation. The prefix weights are the uniform seed fibre probabilities, agree with the Born law on the EPR register with arbitrary normalized auxiliary state, and sum to one. Full-carrier distances and commutators are exactly the weighted residual errors; impossible prefixes have weight zero.
Split the actual visited coordinates from their complement. Factor the diagonal prefix projector by fibre locality, evaluate its EPR mass, and apply the tensor squared-norm identity. The continuation support follows by recursion on the CL presentation.
The actual prefix projector, adaptive computational readout, and Read dual marginal factor on their concrete selected registers. The Read factorization holds for every claimed prefix, including off-image labels. On canonical selected-coordinate labels its residual operator is precisely the linear dual-X readout required by mixing.
Follow the existing recursive Hide PVM through its coarse marginal. Summing earlier dual answers leaves the Z prefix. Split the X spectral projectors on the actual coordinate partition and identify the recursive dual map with the selected local linear map.
Residual projective measurements assemble into one ambient PVM even though their coordinate spaces depend on the prefix. Prefix branches are orthogonal, so reassembly preserves squared errors exactly and global commutators reduce to the corresponding weighted local commutators. A common ancillary extension commutes with this concrete embedding.
Each branch is supported by its actual honest prefix projector. Distinct projectors multiply to zero; summing the branch normalizers gives identity. The same orthogonality eliminates all cross terms in squared distances and commutators.
Suppose the current residual measurements are projective and their three full-carrier marginal and commutator errors are at most \(\varepsilon \), with \(0\leq \varepsilon \leq 1\). Using the actual prefix law and selected registers, mixing constructs residual POVMs with squared error at most \(56\sqrt{\varepsilon }\). A single fixed ancillary alphabet suffices to produce residual PVMs and one ambient replacement measurement with squared error at most \(2\sqrt{56\sqrt{\varepsilon }}\). Its residual support is exactly the next unvisited register.
Apply the exact conditioning identities to ambient Pauli mixing. Dilate the constructed residual POVMs with one common fixed ancilla, apply the quantitative compression estimate, average square roots by concavity, and use the exact prefix reassembly and register reassociation.
If the selected measurement has the stated current prefix form and the three stage errors are bounded as above, an actual finite-dimensional tensor-product strategy is constructed. The new state retains the original EPR factor, all other measurements are extended by identity, and the selected measurement retains the prefix and newly extracted Z factor. The absolute game-value loss is at most \(2\sqrt{2\sqrt{56\sqrt{\varepsilon }}}\). Arbitrary answer relabelling is allowed. These are single-stage hypotheses, not a completed induction from game success.
Construct the residual Naimark projectors and the ambient joint PVM, replace the selected question, and reassociate the shared EPR-plus-auxiliary state exactly. Pull the acceptance predicate back through answer relabelling before applying value stability; no same-party coarse-distance contraction is used.
Adding the selected coordinate answer preserves the preceding claimed prefix and selects the intended next remaining register. On attainable old prefixes the extended label recovers both components and is injective. For the actual selected linear outcome it is precisely the next sampler prefix. Coarse assembly of the old prefix and current linear Z projector is exactly the next honest prefix projector.
Use locality of claimed-prefix extraction and disjointness of the current factor from visited coordinates. Recover the old prefix and selected coordinates, then identify the actual next sampler value using the sum of its stage maps.
For a current product-form Introspect family, the actual parsed-game Sample and Read tests and the proved rigidity bounds control its prefix-weighted local Z and dual-X commutators, with the same constants as their full-carrier bounds. The current product form is an induction hypothesis; the commutator estimate is derived. Malformed outcomes remain in the common residual answer alphabet.
Embed each selected-coordinate label injectively into the actual option-valued Read alphabet. Keep these nonnegative terms of the global commutator sum and apply the exact factorization and weighted reassembled-commutator identity. For Z, remove only the impossible ideal dummy outcome and use the exact adaptive computational-readout factorization.
The stage marginal error is exactly the squared distance between the advanced coarse residual marginal and the next honest prefix measurement. There is no answer-count loss, and no projectivity or normalized-state hypothesis is needed for this equality.
The extended label is injective on attainable old prefixes, and every other prefix-supported operator vanishes. Thus coarse assembly preserves the squared-error sum exactly. Identify its ideal term with the next-prefix projector assembly.
Adding the deterministically reported current coordinate to each full Introspect answer preserves projectivity and the total commutator errors exactly. The updating decoder overwrites the visited coordinates, reports the advanced prefix, and recovers the old measurement under its old-prefix support invariant. The malformed outcome remains explicit. Replacing all malformed raw Introspect constructors by one fixed malformed constructor preserves the actual parsed-game value and projectivity exactly.
Embed outcomes in the graph of the selected-coordinate function. All off-graph operators are zero. The decoder identities follow from the disjoint visited, current, and remaining coordinates. Every malformed Introspect answer is rejected by the actual predicate’s format check.
The old-prefix and current-Z replacement operators equal the next honest prefix tensored with constructed residual projectors on its actual remaining coordinates and the common enlarged auxiliary space. After any answer decoder, these residuals are PVMs and reassemble to the selected measurement of the returned strategy. Under the old measurement’s refinement identity and the three stage-error bounds, its value loss is at most \(2\sqrt{2\sqrt{56\sqrt{\delta }}}\).
Recover the unique old prefix and current label on attainable branches, transport the residual register by the proved coordinate-set equality, and use zero ambient projectors on all other branches. Coarse-graining the residuals commutes with prefix reassembly. Apply the existing quantitative replacement theorem to this concrete construction.
Write \(e=|E|\varepsilon \), let \(\eta _Z\) be the primitive Bob-Z error and \(\delta _H\) the fixed Alice hiding error, and let \(r\) be the remaining depth. For the current projective prefix product form with its valid-answer support, all three refined stage errors are at most
If this budget is at most one, the actual tests construct the common-ancilla residual projectors. The replacement value loss is at most \(8B_r^{1/8}\). An explicit monotone numerical failure recurrence records this loss.
The Introspect consistency loop transfers Bob’s prefix rigidity to Alice with bound \(8\eta _Z+28e\). Refining the dummy answer adds its old-prefix block to the valid reported marginal. Orthogonality charges the sum of these squared norms to the single dummy outcome, giving marginal error at most \(16\eta _Z+56e\). Combine this with the actual Z and dual-X commutator estimates and apply mixing and dilation. Three square roots give the stated universal coefficient and exponent. The numerical recurrence does not itself construct a sequence of strategies.
Extending by the fixed auxiliary vector and reassociating the register preserves same-party error, cross-party error, and Born probabilities exactly. At every unchanged question the actual replacement has precisely this extension. In particular the primitive Pauli, hiding, and Read errors are unchanged when an Alice Introspect question is replaced.
The deviation vectors are extended by an isometry. Register reassociation preserves their norms, and register ideals remain tensored with the enlarged auxiliary identity. Specialize the actual unchanged-question formula.
Every projective full-answer Introspect measurement has the initial prefix invariant on its original auxiliary space. At each subsequent stage, the actual game tests construct a projective replacement with the next prefix form and valid-answer support. Its failure increases by at most the proved stage loss. Every other question is its original identity extension, and all fixed Alice hiding errors are preserved exactly. The raw selected measurement identity follows from canonicalization and decoder recovery.
At stage zero the visited register is empty; only prefix zero survives. Transport the original measurement to its remaining-register carrier and use a deterministic malformed answer on other branches. At a successor, decode each refined residual before reassembly. Canonicalization preserves game value and is overwritten at the selected question by replacement. Attainable next prefixes satisfy the decoder’s coordinate identity; all other residuals report the malformed answer. Apply the actual stage bounds and the quantitative replacement theorem.
For nonnegative edge multiplier \(m\), set \(C=(512r^2+224)m+128\) and define
Each \(t_n\) is positive. If the initial failure and both fixed primitive errors are at most \(t_N\), the numerical failure after \(n\leq N\) replacements is at most \(t_{N-n}\), and every common stage budget is at most one.
When all three errors are at most \(t\), the budget is at most \(Ct\). The eighth-power threshold and the bound \(8B^{1/8}\) reserve at most \(t_n/2\) for the new loss; the other half bounds the previous failure. Induct on the number of replacements, using the decreasing thresholds.
In the actual parsed-game setup, suppose the starting measurements are projective, the primitive Bob-Z and every fixed Alice hiding error have the stated bounds, and these bounds and the initial failure are at most \(t_\ell \). For every \(n\leq \ell \) there is an actual projective Alice measurement family with the prefix invariant at level \(n\) and failure at most the explicit numerical recurrence. Its auxiliary carrier and product ancilla state are constructed recursively. Bob’s measurement family is retained, all other Alice questions have their exact iterated identity extensions, and the primitive Bob-Z and Alice hiding errors remain unchanged. The Lean states it in the register model (Definition 8.72) of a normalized auxiliary model: each stage adjoins a one-sided ancilla whose size the dilation chooses, so the iteration returns a new normalized auxiliary model in place of the recursive carrier and state, and that model reduces to the original one (Definition 8.80).
Initialize the concrete residual measurement. At each successor apply Lemma 6.96 to the current strategy. The explicit threshold proves its smallness premise, and replacing remaining depth by the full depth bounds the loss by the common recurrence. Exact preservation of the fixed errors supplies the next stage’s primitive inputs.
Suppose the CL presentation covers the whole register exactly. A terminal prefix invariant gives a projective auxiliary measurement \(T_y\) on \(\mathrm{Option}(A)\) for each reported question \(y\). Every valid effect is the question readout at \(y\) tensored with \(T_y(\mathrm{some}(a))\). The malformed effect is the sum over \(y\) of the question readout tensored with \(T_y(\mathrm{none})\); it is not assumed to vanish.
The remaining register is empty at the terminal level, so transport its unique basis vector away. The valid-answer support invariant fixes the reported question on each residual branch. Coarsen only that question component; projectivity and normalization are preserved on the full option alphabet. Reassembling the residual effects gives both formulas.
Exchanging the players in the actual parsed game preserves its value after transposing the Pauli predicate. No symmetry of that predicate is required. The finite Alice construction therefore gives an actual Bob construction, with its prefix invariant, projectivity, untouched questions, and the same failure recurrence. The primitive errors required by the second player are preserved by the first player’s ancillary extension. The Lean exchanges the players by swapping the model, whose register model is the swapped register model along a local isometry with identity homomorphisms (Definition 8.72), so the value and every primitive and hiding error move across with no loss, and the Bob iteration is the Alice iteration in the swapped model, returning a model that reduces to the original one (Definition 8.80).
Swap the ordered type edge and the two seed coordinates. Check the actual directed predicates and transport the register state and state distances. Apply the proved Alice construction to the exchanged game and swap back.
If the initial failure, both primitive Z errors, and the required hiding errors are at most the explicit threshold for \(2\ell \) replacements, there are concrete projective measurement families with Alice’s false-role and Bob’s true-role terminal invariants. The final state uses only fixed local ancillas, and failure is bounded by the single recurrence at \(2\ell \). The Lean’s final state is a model: Alice’s block extends the auxiliary model on her side and Bob’s block the result on his, and the final model reduces to the original one (Definition 8.80).
Run Alice’s false-role block for \(\ell \) steps. The threshold theorem supplies the admissible failure at the midpoint, and the unchanged-question identities supply Bob’s primitive inputs. Run Bob’s true-role block, retaining Alice’s completed measurement. Restarting the numerical recurrence is exactly continuing it, so the two blocks have the stated combined bound.
For a nonempty ordinary answer alphabet, both actual terminal invariants construct an original-game strategy. If the final parsed-game failure is at most \(e\), its value is at least \(1-|E|e\). Each malformed auxiliary outcome is completed to a fixed ordinary answer; its mass need not vanish.
The valid full-option outcome has a unique parsed-answer preimage. Its terminal effect is the actual conditional question readout. Map the malformed auxiliary outcome to a fixed answer; coarse-graining preserves projectivity, and newly accepted Born probabilities are nonnegative. The actual cross-edge mass and the exact common-seed question law give the value bound.
For fixed depth and type graph, the failure after \(N\) replacements is at most a fixed coefficient times the \(3N\)-fold square root of a common input error in the admissible regime. A second explicit coefficient makes the same bound at least one outside that regime. Consequently the combined bound has the paper’s two-term error profile, with positive exponent at most one and constants independent of the register dimension.
Bound each stage loss by a constant times an eighth root and induct over the actual recurrence. Add the reciprocal of the iterated root of the positive threshold to handle the large-error regime. Apply fixed-power absorption to the common input profile.
Suppose the actual parsed-game strategy is projective on an EPR register tensored with a normalized auxiliary state. Assume its failure and only the primitive Alice-X and Bob-Z squared errors are at most \(t\geq 0\). For a source CL presentation covering the whole register exactly, the original game’s quantum value is at least \(1-Ct^{2^{-6\ell }}\), for an explicit coefficient depending only on depth and type-graph size. There is no assumed hiding estimate, future strategy, or smallness condition. If \(t\) has the paper’s two-term profile, the conclusion has that profile with uniform adjusted constants. The Lean’s EPR register tensored with a normalized auxiliary state is the register model (Definition 8.72) of a normalized auxiliary model, and it bounds the value of every value model dominating the POVM strategies of the auxiliary model (Definition 8.78), of which the quantum value is the case of a tensor-product model.
The tested Pauli-Z loop transfers Bob’s primitive estimate to Alice. Full hiding rigidity derives both required hiding families from the actual game and the original two primitive estimates. A fixed coefficient bounds all these inputs simultaneously. Apply the two-block construction and ordinary-answer extraction in the small-error regime. Outside it the same power bound is at least one, and quantum value is nonnegative. Absorb the fixed coefficients and roots into the required profile.
The preceding soundness theorem also applies when the primitive X/Z guarantees hold on a normalized state at squared distance at most \(t\) from the ideal EPR-register state. If those errors and actual game failure are at most \(t\geq 0\), the original-game loss is at most \(20C t^{2^{-(6\ell +1)}}\). The constants again admit the paper’s two-term profile uniformly in the register dimension.
For two PVMs the summed squared difference on a nearby state is bounded by twice its old value plus eight times the squared vector distance. Projective normalization sums over all outcomes before estimating, so there is no answer-cardinality factor. Transfer game failure using value stability. For \(t\leq 1\), all three inputs are at most \(20\sqrt t\); apply the primitive soundness theorem and absorb this extra root. For \(t{\gt}1\) the bound follows from nonnegative quantum value.
Rectangular local isometries transport any projective strategy to an actual projective strategy on the target spaces. Assigning the orthogonal image complement to a fixed outcome normalizes the measurements and preserves every Born probability and the whole game value on the embedded state. The exact operator intertwining also holds after arbitrary answer maps. On a target state at squared distance at most \(\eta \) from the embedded state, image-complement mass is at most \(\eta \). Thus a summed image-measurement error \(\delta \) becomes at most \(2\delta +2\eta \) after completion, on either party and without an outcome-count factor.
The image and its orthogonal complement are orthogonal projections. Complete one outcome, then use the isometry identity to prove compression and intertwining exactly. A complement projection annihilates the embedded state and is a contraction, so its mass on a nearby state is bounded by squared vector distance. Only the chosen outcome receives this complement; the two-term squared triangle inequality gives the error bound.
Any two anticommuting self-adjoint involutions on a nonzero finite carrier extend, with one extra qubit, to the actual Magic Square game. Explicit binary variable measurements and three-bit constraint measurements are projective, preserve the original binary measurements at cells zero and four, and give a value-one PCC strategy for the doubled game. Symmetric input matrices give symmetric grid and constraint matrices.
Construct all nine observables by tensoring the original pair with the single-qubit Pauli pair. Verify the six commuting triples and their parity products. Their joint spectral projectors have zero effect for wrong parity and zero joint effect for inconsistent incidence answers. Evaluate these explicit projectors on the EPR state to prove perfect acceptance and cross-question commutation directly.
All twenty-six actual Pauli question maps have explicit three-stage CL presentations: seed, truncated direction, and the remaining point and scale coordinates. The partition covers \(3m+3\) field coordinates exactly. Both full-Pauli questions evaluate to zero. A supplied binary field basis gives three-stage binary presentations on \((3m+3)t\) bits with the exact Pauli-game question distribution. Canonical encoding is inverse on attained outputs, so arbitrary strategies for the binary game pull back to the actual Pauli game with the same state, dimensions, value, and full-Pauli measurements. This is mathematical sampler content; the uniform program and its runtime are additional obligations.
Construct each register map explicitly and decode its full evaluation into the original sampled question, including canonical line representatives. Use the content-to-coordinate equivalence to identify the uniform laws. Downsize through the given binary basis and number the coordinates. Encode each attained question canonically and pull back measurements along this encoding; the pointwise sample identity proves exact value preservation.
The honest field-register Pauli strategy, with one extra qubit, has explicit PVMs for all twenty-six question types and zero effects for malformed answers. Its full-Pauli measurements are the required register readouts. The actual trace probes are exactly the corresponding Weyl observables, and the verifier phase is their commutation phase. For degree bound at least one, the sampled low-degree, Pauli-point, pair, Magic Square, and distinguished-variable edges have commuting effects and zero product on every rejected answer pair.
Coarse-grain a common Pauli PVM for all same-basis questions. Its multilinear encoding restricts to an affine polynomial on an axis line and degree at most \(m\) on any diagonal; evaluation at the sampled line parameter recovers the point value, even for zero direction. For zero phase use the commuting joint probe PVM, and for nonzero phase use the concrete Magic Square extension. Its distinguished cells preserve the original probes. Coarse-graining preserves commutation and zero rejected products.
For nonzero \(m\), \(m\mid |F|\), and \(d\geq 1\), the actual twenty-six-type Pauli game has a perfect PCC strategy in its doubled presentation, on local dimension twice the cardinality of the field register. All effects, commutation identities, and rejected-product identities are constructed for the actual question distribution and actual verifier predicate.
Positive question mass yields one common content sample and an actual ordered graph edge. A finite graph classification reduces forward edges to the previously checked identities. Reverse edges follow by symmetry of the predicate and commutation; loops use orthogonality of the same PVM. Number the register basis and package the projective families as a synchronous strategy for the doubled game. Zero rejected products give value one under normalized trace, and the tested commutations give PCC.
Suppose an actual projective parsed-game strategy has failure at most \(t\), and supplied local isometries put its state within vector distance \(t\) of the ideal register state. Suppose also that the image measurements have summed squared error at most \(t\) on valid full-register Alice-X and Bob-Z answers. The original game has quantum value at least \(1-C\, \mathrm{root}_{6\ell +2}(t)\), for an explicit coefficient depending only on depth and graph size. The estimate holds for every \(t\geq 0\) and retains all malformed answers and image-complement mass. The local isometries and their estimates are inputs here; Lemma 6.115 supplies them for the actual game from Theorem 3.38. The final loss preserves the paper’s two-term error profile with uniform constants and a positive exponent at most one. The Lean states it for a strategy in any bipartite model, with one local isometry of models (Definition 8.69) into the register model of a normalized auxiliary model (Definition 8.72), and bounds the value of every value model dominating the POVM strategies of the auxiliary model (Definition 8.78), of which the quantum value is the case of a tensor-product model.
A positive submeasurement within squared distance \(\delta \) of a PVM has missing mass at most \(2\sqrt\delta \). Extending it inside the identity therefore changes the error to at most \(2\delta +4\sqrt\delta \). Apply this to the valid raw effects inside the complete coarse images, including their malformed outcome. Complete the local isometry images, preserve the actual embedded game value, and apply finite soundness. For \(t\leq 1\) the common input is at most \(6\sqrt t\); for \(t{\gt}1\) use nonnegative quantum value. No outcome-cardinality factor appears.
One uniform polynomial-time program computes the canonical base point of a line from its field-encoded point and direction, including zero direction. One polynomial in field width plus vector length bounds its runtime, and the program halts on every raw input. The Pauli CL coordinates are numbered explicitly in the order point-X, point-Z, seed, direction, scale-X, scale-Z, with each field coordinate followed by its basis bits.
Scan for the first nonzero direction coordinate, compute the scalar with the checked Shoup inverse and multiplication programs, and subtract that multiple of the direction. Identify this expression with the existing canonical-line representative. Compose the polynomial runtime bounds. The coordinate numbering is a sum and product of explicit finite equivalences; its value equations identify every block and bit.
A perfect PCC source strategy gives a perfect PCC strategy for the actual full parsed introspection game, including all Pauli and auxiliary types. The field-register construction has local dimension \(2|F|^{2^m}D\), where \(D\) is the source dimension. A supplied self-dual binary basis transports the construction to arbitrary binary CL source functions on \(2^m t\) coordinates, with dimension \(2\cdot 2^{2^m t}D\). The binary source functions need not be linear over the larger field.
Put the explicit Pauli PVMs, the auxiliary PVMs, the source strategy and one extra qubit on a common carrier. Check the X/Hide and Z/Sample anchor edges using the exact distinguished Pauli projectors. A positive question pair retains a common content sample; every graph edge then has commuting effects and zero product on rejected answers. Normalized trace gives perfect acceptance. For binary sources, conjugate the quantum register through the self-dual basis before composing the auxiliary measurements.
Any actual projective strategy for the full parsed game restricts to a strategy for the actual QLD game in the same model, hence with the same state. If the original failure is at most \(\varepsilon \), the restricted failure is at most the full ordered-edge count times \(\varepsilon \). Completing malformed outer constructors at a scalar answer leaves every valid full-Pauli answer operator exactly unchanged, for both parties.
Accepted parsed Pauli answers already satisfy the actual Pauli predicate, including on loops. Coarse-grain malformed outer answers to a fixed scalar answer, preserving projectivity and accepted probability. Conditioning on a full-graph edge bounds its shared-seed mean failure; average over the Pauli edges, then pull back along canonical question encoding. A valid full-Pauli answer differs from the scalar completion answer, so its fibre contains only its original raw constructor.
Let \(N\) be the number of ordered edges of the typed graph, so that \(N \geq 1\), let \(\delta _{qld}\) be the error of Theorem 3.38, and let \(\omega \) be a value model. Let \(\mathscr {S}\) be a projective strategy of the binary parsed introspection game in a bipartite model in which the Pauli basis test is sound with \(\omega \) (Definitions 8.62 and 8.82), failing with probability at most \(\varepsilon \), whose two \((\textsc{Pauli}, W)\) measurements have nonzero effects only at full-register Pauli answers. Then the restriction of \(\mathscr {S}\) to the Pauli basis game (Lemma 6.114), its malformed answers completed at a scalar answer, has an extraction in binary coordinates at the error \(T = \delta _{qld}(N\varepsilon , m, d, q)\): an ancilla model, with state \(\psi _{\textsc{aux}}\), whose POVM strategies \(\omega \) dominates, and a local isometry of the strategy’s model into the register model of the ancilla model on \(\mathbb {F}_2^{M \times t}\) (Definition 8.72), which carries the strategy’s state within \(T\) of \(|\textsc{EPR}_2\rangle ^{\otimes Mt} \otimes \psi _{\textsc{aux}}\) and carries the first player’s \(X\) effects and the second player’s \(Z\) effects at the valid full-register answers within \(T\) of the honest qubit readouts, in summed squared state norm. The valid answer at the qubit label \(x\) is the Pauli answer at \(\phi ^{-1}(x)\), for the relabelling \(\phi \) of Corollary 3.40, and it projects back to \(x\). In the tensor-product model of a strategy’s state the test is sound with \(\mathrm{val}^*\) (Lemma 8.83), the ancilla model is, up to isomorphism, the tensor-product model of an auxiliary unit vector, and the local isometry is one between tensor-product models: the familiar form of the extraction, for tensor-product strategies.
Restrict the strategy to the actual Pauli basis game (Lemma 6.114): same model and state, failure at most \(N\varepsilon \), and at a valid answer the same operators. The completion of the malformed answers carries no mass, the strategy having no malformed Pauli outcome, so the restriction’s Pauli measurements are supported on the full-register answers too. Corollary 3.39, at the restriction, gives an extraction in field coordinates at the error \(\delta _{qld}(N\varepsilon , m, d, q)\), with an ancilla model that \(\omega \) dominates, and Corollary 3.40 relabels its register as qubits along the self-dual basis, at the same error. The valid answer at \(x\) projects to \(\phi (\phi ^{-1}(x)) = x\). In Lean the extraction in binary coordinates is a structure (Corollary 3.40), and exists_extraction composes these steps.
Comments.
This is the paper’s use of cor:pauli-binary in the proof of lem:intro-pauli-strat (Lemma 6.53): the conditioning on the Pauli block is the factor \(N\), and the estimates are kept as distances, the form Lemma 6.111 consumes, rather than used to replace the strategy by an exact one. Theorem 3.38 gives all four Pauli estimates, as the paper states them; the extraction keeps the two the consumer uses, Alice’s \(X\) and Bob’s \(Z\). Reading the estimates at the valid answers costs nothing: the decoder of Lemma 6.127 makes the strategy’s Pauli measurements supported on the full-register answers, so the answers read as one register label are that label’s answer alone. Only the binary game is used for soundness; the field-register game of Lemma 6.113 serves completeness. MIPRE/Background/Introspection/RestrictedSoundness.lean and RestrictedProfileSoundness.lean.
Suppose the original game’s CL functions are exact on the whole Pauli register. Let a projective strategy of the binary parsed introspection game, in a bipartite model, fail with probability at most \(\varepsilon \), and let its restriction to the Pauli basis game have an extraction in binary coordinates at an error \(\delta \geq 0\) (Lemma 6.115). Then every value model \(\omega \) dominating the POVM strategies of the extraction’s ancilla model (Definition 8.78) gives the original game value at least \(1 - C\, \mathrm{root}_{6\ell +2}(\max (\varepsilon , \delta ))\), with \(C\) the coefficient of Lemma 6.111 at the \(N\) ordered edges of the typed graph. In the tensor-product model, with \(\omega = \mathrm{val}^*\), this bounds the quantum value of the original game. For \(a \geq 1\) and \(0 {\lt} b \leq 1\), the coefficient \(A = \max \{ 1, C' a^r, ar\} \), where \(r = 2^{-(6\ell +2)}\) and \(C' = C\max (1, N^b)^r\), is at least \(1\) and depends only on \(\ell \), \(a\) and \(b\). It is the coefficient with which Lemma 6.60 turns this loss into the two-term profile \(E(A, br, x, \varepsilon )\) of that lemma when \(\delta \leq E(a, b, x, N\varepsilon )\) and \(x \geq 1\), which is how Lemma 6.126 absorbs the error of Theorem 3.38.
Lemma 6.111, applied to the strategy with the local isometry and the ancilla model of the extraction, at the common error \(\max (\varepsilon , \delta )\). The Pauli question’s sampler is constant, the valid answer at a register label projects back to that label, and at a valid answer the restriction’s operators are the strategy’s (Lemma 6.114), so the extraction’s estimates are the hypotheses of that lemma. The coefficient is a maximum of terms at least one.
Comments.
The exactness hypothesis is the consumer’s and covers all \(M t = M \log q\) coordinates of the register, whereas the paper’s original questions have length \(s(N) \leq Q\). Reaching an arbitrary original game therefore still needs the padding of the source register to \(Q\) coordinates to be composed with this lemma; that step is not part of it.
For \(m=2^j\) and a field of size \(2^k\) with \(j\leq k\), a uniform program computes the direction selector from canonical field bits; every index has exactly \(2^{k-j}\) seeds. Uniform axis and diagonal programs compute the selected coordinate erasure, truncated direction, and canonical line point, and halt polynomially on all raw inputs. Replacing the old arbitrary field enumeration by this selector gives explicit three-level field and binary CL families. A proved seed permutation identifies their decoded question distribution exactly with the existing QLD game.
Number field elements by their canonical bit value and select the high \(j\) bits. Splitting the bit index into quotient and remainder gives the equal fibre sizes. Compose this program with coordinate masks and the canonical-line routine. Relabel only the seed in the uniform content space to compare with the old field enumeration; all decoded question fields then agree literally. Transport the uniform distribution through that permutation.
For explicit unary field and selector widths and point dimension, uniform polynomial-time programs compute all three Pauli marginals, linear maps and factor indicators in the numbered binary register. For positive odd field degree and selector width at most field degree, these are the exact downsized CL queries in the effective self-dual basis. Linear and factor correctness hold for arbitrary prefixes. A total router handles the four query kinds and the fixed twenty-six type labels.
Construct the self-dual basis effectively and convert field rows in both directions. Pack the point, seed, direction and scalar registers in the proved coordinate order. Execute the appropriate stage maps and compose successive stages for marginals; factor indicators use the fixed register partition. The type decoder tabulates only the fixed finite type set. Canonical index-dependent parameter selection and the all-index sampler packaging are supplied by Lemma 6.123.
The full padded-register Read relation has an exact executable check, including the original answer cutoff. For a bounded source verifier and the explicit depth, dimension and answer-length hypotheses, a clocked source marginal call implements the padded Sample relation. Independently, a uniform polynomial-time elimination program computes the exact canonical quotient representative of a supplied binary row span.
Parse canonical answer encodings while retaining unrestricted full-register dual labels. Restrict only the source sampling call to the original coordinates; exact zero extension proves its padded-game semantics. Use the source boundedness estimate to discharge the clock. For canonical reduction, identify the leading coordinates of the computed pivot basis with the canonical pivot set, and characterize the remainder by its coset and canonical complement. The dual-map specialization and the executable Hide checks are composed in Lemma 6.125.
For a compatible seed permutation, explicit-selector and legacy Pauli outputs are related by an actual binary question equivalence. The decoded legacy questions agree under this equivalence.
Conjugate the seed permutation through the binary basis and change only the line question seeds. Prove that this output map intertwines the two presentations with the common seed permutation, and that decoding agrees. The full strategy transport, including mixed edges and PCC completeness, is supplied by Lemma 6.126.
For \(s\leq 2^m t\), explicitly embed an arbitrary \(s\)-bit source register into the Pauli qubit register. Padding preserves perfect PCC play and source dimension. Every projective strategy for the padded source game, in any bipartite model, restricts to one of the original source game in the same model with exactly the same value; so the padded game’s value is at most the original’s in every value model approached by the projective strategies of the models it dominates, \(\mathrm{val}^*\) and \(\omega ^{\mathrm{co}}\) among them. For positive depth and exact original partitions, unused coordinates can be consumed by a zero component of the first factor without changing depth or evaluation. The resulting full typed game has a perfect PCC strategy of dimension \(2^{2^m t+1}D\).
Number the Boolean cube and basis-bit coordinates explicitly. Pull source questions along the embedding and retain the original measurement rule. Positive padded question mass has a common source seed, proving PCC and perfect acceptance. Split a uniform padded seed into its original and unused coordinates to prove exact value preservation for arbitrary strategies. A direct sum with a zero map on the complement consumes every unused coordinate while preserving the CL evaluation. Apply the full binary completeness construction.
The exact full-register padding preserves evaluation but changes factor and dual data. Its honest Read and Hide dual labels can carry unused coordinates. The new executable Read check implements this full-register variant, and the Sample program implements the padded sampling relation. The executable Hide checks use a row-space membership relation on the full register. A question-local quotient decoder converts accepted dual labels to the semantic local dual readouts, without identifying the two coordinate orders. Honest semantic labels satisfy the relaxed relation unchanged. Prefix guards and attained Introspect outputs supply the support needed by the clocked source calls. This bridge is proved in Lemma 6.125; it does not require the full-register dual labels to lie in the original source subspace.
The effective odd-degree field, self-dual basis and explicit dyadic selector give an index-dependent Pauli typed sampler. Extending and detyping it gives a five-level sampler whose program is computed uniformly from binary \(\lambda \). For every input and index its dimension and runtime coefficient are bounded by \((\lambda n+1)^C\), at a fixed input-size degree \(C\). When \(\lambda n=0\), the final sampler has dimension zero.
Compute unary field and register parameters within the polynomial sampler budget, then compose the checked uniform Pauli query router with the typed and graph routers. At positive indices, absorb their fixed polynomial costs into one exponent. Separate constant-time branches at zero parameter or zero index supply the exact all-index bound.
A uniform polynomial-time program checks the actual QLD predicate on binary questions and answers, preserving all twenty-six question types. Canonical answer encoding and decoding agree on accepted payloads. The total decoder always produces a legal answer constructor for its Pauli question, and the executable full-Pauli projection agrees with the semantic qubit register.
Parse the exact answer shape for each type, convert between effective field rows and the self-dual question basis, and compose the checked line, table, probe and phase programs. Prove each finite branch before combining the type dispatch. Full-table outcomes use the same explicit cube numbering as the register projection.
The actual binary decision kernel implements all auxiliary branches using one source-simulation clock and the supplied canonical parameters. Accepted raw answers decode into a finite quotient game: original answers retain their finite length bound and Pauli answers retain the actual QLD alphabet. Conversely, accepted finite answers with the honest prefix, source-output and Pauli-format support conditions have accepted canonical encodings.
Use row-space membership to express the hiding relation independently of the local coordinate enumeration. Decode dual labels blockwise; prefix agreement makes the selected transforms agree in every tested block. Clocked source queries implement the guards and source decision call. Canonical format inversions and bounded source-answer decoding then give the raw soundness and honest encoding implications in both orientations.
Explicit seed relabelling intertwines the full typed question law and predicate, including mixed edges. Quotient dual decoding and finite-register reindexing preserve the required Pauli support. The actual QLD soundness theorem therefore supplies the extraction witness used by introspection, with its field-size tails absorbed at the canonical parameters. Honest completeness retains PCC, exact dimension and the executable guards’ support.
Transport the shared seed and each question’s answer map explicitly. Relabel quotient coordinates before selecting local dual representatives. The distinguished full Pauli measurements remain fixed throughout, so decoder-enforced support passes to the actual QLD restriction. Apply QLD extraction, binary basis transport and the proved finite-game induction, then absorb the canonical field and register error terms.
The compiled five-level verifier satisfies the ambient resource contract on every program input and index, including the output-description and answer-cutoff bounds. At positive indices its actual acceptance is the canonical raw kernel. Finite graph detyping transfers raw perfect PCC completeness outward and transfers high output value inward with the fixed graph loss. Total finite answer decoding then increases value and enforces the full Pauli support required by QLD soundness. The value identities hold in every value model (Definition 8.34); the restriction to the cutoff, the detyping transport and the decoding hold for projective strategies in any bipartite model (Definition 8.62).
Prepare the shared clock and canonical resources once, clamp source descriptions, and route every source call through the same bounded simulation interface. Combine the all-index sampler, decider and cutoff estimates into one budget exponent. Restrict to the enforced finite answer cutoff, apply the graph-detyping transport, and merge each question’s answer fibers under the finite decoder. Its range gives the Pauli support directly.
The pinned manuscript already runs the \(Z\) commutation analysis on the coarse operators. The earlier blueprint statement that this rewrite remained undone was stale. The checked product-form stage derives commutators from coarse joint measurements, now instantiated by the actual Sample and Read tests. Full hiding rigidity, its normalizer replacement, Read rigidity, and the common-ancilla dilation theorem are proved. The actual adaptive prefix law, Z and dual-X factorizations, weighted conditioning, minimal residual support, projective reassembly, next-prefix label assembly, and a concrete single-stage strategy replacement are now checked. Answer refinement and updating, next-prefix residual reassembly, the actual three-error budget, and exact preservation of the unchanged measurements’ errors are also proved. Initialization, decoded valid-answer support, the raw selected-measurement identity, an explicit small-error threshold, and finite iteration on both players are now constructed and composed. Terminal extraction completes malformed outcomes without additional loss. The complete finite-game soundness theorem derives hiding and the second Z estimate from just the primitive Alice-X/Bob-Z guarantees; it handles approximate extracted states, all error sizes, and the paper’s power profile. The actual QLD extraction adapter, full question and answer transports, uniform verifier construction, all-index budgets and raw finite-game connection are now proved in Lemmas 6.126 and 6.127. Their top-level assembly supplies the ambient seven-level input contract in Lemma 6.132. This does not claim the separate generic-depth, source-runtime theorem below.
The theorem
In the source model, a Turing machine \(\mathsf{ComputeIntroVerifier}\) runs in time \(\mathrm{poly}(\left\vert {\mathsf{V}} \right\vert ,\log \lambda ,\ell )\), polynomial in its input length for each fixed \(\ell \). On input \((\mathsf{V}, \lambda , \ell )\) it 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 )\), with its decider in standard timeout-counter form, such that for every \(\ell \)-level verifier \(\mathsf{V}\) satisfying the source absolute \(\lambda \)-bound 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}^*(\mathsf{V}^{\textsc{Intro}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^*(\mathsf{V}_{2^n}) \geq 1 - \delta (\varepsilon , n)\).
The Lean proof does not use this source-model theorem. It uses the ambient contract, Definition 6.130, supplied for \(7\)-level inputs by Lemma 6.132. General depth, the timeout-counter form and the entanglement clause are not formalized.
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 \).
The ambient soundness contract requires \(n\geq 1\). For nonzero \(a,b\), Lean’s real power convention makes \(\delta (\varepsilon ,0)=0\); retaining soundness at zero would force an unintended exact conclusion at original index \(1\). The paper’s overview starts with \(n\geq 1\), although its later theorem display quantifies over all naturals. Moreover \(2\leq 2^n\) holds exactly when \(n\geq 1\), matching the bounded-input domain. The compression consumer already has \(n\geq 2\) and supplies this hypothesis.
Evaluate the two zero-base powers using their nonzero exponents. The index equivalence follows from monotonicity of \(2^n\) and its value at zero.
The ambient contract MIPRE.Introspection 7 is inhabited. The fixed instance MIPRE.Introspection.seven supplies the introspection input to the compression pipeline. It has one common all-index resource exponent and the required soundness profile, and handles the exceptional zero cases. Its scope is the ambient contract at \(\ell =7\); Theorem 6.129 separately states the source-model result for arbitrary fixed depth. The compiler is defined explicitly, its constants chosen once, and its soundness field is the \(\mathrm{val}^*\) instance of a soundness theorem that holds in every value model in which the Pauli basis test is sound (Theorem 8.84).
Choose one even canonical parameter constant that absorbs the QLD field-size tails, and use the proved clocked universal machine. Combine the sampler, decider, cutoff and description estimates into one resource exponent. Encode the supported honest finite strategy to obtain ambient perfect PCC completeness, using the zero-index branch separately. For positive-index soundness, restrict to the enforced answer cutoff, detype, decode finite answers and apply actual QLD extraction followed by the source-game bound. Absorb the fixed detyping loss into the profile constants. These constructions fill every field of the ambient contract; their axiom audit contains only propext, Classical.choice and Quot.sound. For the cost model and the PCC representation they work in, see Remarks 6.31 and 2.8.
The checked soundness analysis follows the rigidity argument of [ 1 , Section 8 ] and techniques introduced in [ 6 ] : the Pauli basis test and the twirling, commutation and sandwiching toolkit. These lemmas use the bipartite setting, as in the sources; the pipeline carries \(\mathrm{val}^*\) throughout (Remark 6.8).
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.
The source theorem supplies a polynomial-time Turing machine \(\mathsf{ComputeOracleVerifier}\) mapping an \(\ell \)-level normal form verifier \(\mathsf{V}= (\mathcal{S}, \mathcal{D})\), whose decider is in standard timeout-counter form, to a typed verifier \(\mathsf{V}^{\textsc{Orac}}\) such that, for some \(\delta (\varepsilon ) = O(\sqrt{\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\) PCC strategy, in which moreover both players measure with the same family of operators.
(Soundness) If \(\mathrm{val}^*(\mathsf{V}^{\textsc{Orac}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^*(\mathsf{V}_n) \geq 1 - \delta (\varepsilon )\).
(Complexity) The sampler of \(\mathsf{V}^{\textsc{Orac}}\) depends only on \(\mathcal{S}\), with \(\mathsf{TIME}_{\mathcal{S}^{\mathrm{ora}}}(n) = \mathrm{poly}(\mathsf{TIME}_\mathcal{S}(n))\) and \(\ell \) typed levels. The decider has time \(\mathrm{poly}(\mathsf{TIME}_\mathcal{S}(n),B_\mathcal{D}(n))\).
The oracularized decider’s preamble performs a type check, a question-length check, and a bounded parse of each answer component against the decider’s timeout bound \(B_\mathcal{D}(n)\); answers failing the parse are grouped into one distinguished outcome, so the oracle families are projective measurements and not sub-measurements.
The typed oracularized verifier is the pair of Lemma 6.141 and Lemma 6.142, and it inhabits the specification of Definition 6.144, with the running times of Lemma 6.143. Completeness and soundness of its typed game are the transfers of Lemma 6.140, read through the decider’s acceptance law, with \(\delta (\varepsilon ) = 24\sqrt{\varepsilon }\). Through the detyping compiler of Lemma 6.29, the verifier with \(\ell + 3\) levels has the same completeness and soundness with \(\delta (\varepsilon ) = 1536\sqrt{\varepsilon }\): the factor \(16^3\) of the three types, under the square root, times \(24\).
Formalized form.
The ambient model has no timeout-counter form. The formalization replaces it with an index routine that supplies, at each index \(n\), a parse cut \(B(n)\) and a simulation budget \(K(n)\); the decider runs its core under the clocked universal machine for \(K(n)\) steps, which makes it total, as the detyping compiler requires. Soundness holds at every budget. Completeness holds once \(K(n)\) covers the running time of the core, which is polynomial in the running times of \(\mathsf{V}\) at \(n\) (Lemma 6.143): this is the hypothesis that the timeout bound supplies in the source. The typed sampler has the levels of the input sampler, at least one.
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.
Source.
oracularization.tex, sec:orac-def and fig:oracle-decider, with the samplers, deciders and typed question strings stripped away: all oracularization uses of a sampler is the pair of maps \(L^\textsc{A}, L^\textsc{B}\) on the seed space.
Comments.
The oracularized game is synchronous with no extra hypothesis, which is what makes the PCC vocabulary of Definition 2.7 available on it: equal questions carry equal roles, and the third check then rejects unequal answers.
Two of the four repairs of Remark 6.146 are about the verifier and are not addressed here, and it is worth being explicit rather than appearing to have discharged them. Grouping the decider’s failed bounded parses into one distinguished outcome (repair 3) has no content at a finite game-level answer alphabet, where there is no parse to fail; what survives of it is the shape check, which rejects an answer whose shape does not match its role. The truncation of answers to \(B_\mathcal{D}(n)\) symbols (repair 4) is a statement about a decider and does not appear at this level at all. Repair 2, that the completeness witness has identical measurement operators rather than a symmetric state, and repair 1, the single square root in the soundness loss, belong to the two clauses, which are separate obligations.
Let \(S = (L^\textsc{A}, L^\textsc{B}, D)\) be a seeded game and let \(T\) be a PCC synchronous strategy for the doubled game of \(S\), whose questions are \((\mathsf{false}, x)\) for Alice and \((\mathsf{true}, y)\) for Bob. Define a synchronous strategy \(\Sigma ^\textsc{Orac}(T)\) for the oracularization of \(S\), on the same Hilbert space, by
and \(N^{(v,\, x)}_u = 0\) when the shape of \(u\) does not match the role \(v\). Then \(\Sigma ^\textsc{Orac}(T)\) is a synchronous strategy, it is PCC, and if \(T\) has value \(1\) then so does \(\Sigma ^\textsc{Orac}(T)\). Both players measure with this one family of operators (Remark 6.216).
That the oracle’s operators are projections is where PCC is used: the seed \(z\) always lands on a question pair of positive weight, so \(M^{(\mathsf{false}, L^\textsc{A}(z))}_a\) and \(M^{(\mathsf{true}, L^\textsc{B}(z))}_b\) commute, and a product of two commuting projections is a projection. Their sum over \((a,b)\) is the product of the two sums, hence the identity. The family is PCC because the four operators \(M^{(\mathsf{false}, L^\textsc{A}(z))}_a, M^{(\mathsf{true}, L^\textsc{B}(z))}_b\) at one seed commute pairwise — two at one question because distinct outcomes of a projective measurement are orthogonal, one of each by the hypothesis — so every product of them commutes with every other.
For value \(1\) it suffices, by Lemma 2.12 read in the converse direction, that every rejected outcome pair at a question pair of positive weight has probability zero, and in fact each of the decider’s checks that can fail makes one of the two operators, or their product, vanish. A shape mismatch gives the zero operator by definition. A pair the input predicate rejects gives the zero operator as well: its probability is zero by Lemma 2.12, and the normalized trace on matrices is faithful, so a self-adjoint idempotent of vanishing trace is \(0\). Check 2(a) is orthogonality of distinct outcomes at a repeated question, which is available because two questions of positive weight with equal roles are equal. Check 2(b) is orthogonality again, after the oracle’s other factor has been commuted out of the way.
Let \(S\) be a seeded game with nonempty seed space and nonempty answer alphabet, let \(0 \leq \varepsilon \leq 1\), and let \(N\) be a synchronous strategy for the oracularization of \(S\) with value at least \(1 - \varepsilon \). Let \(\Sigma (N)\) be the strategy for the doubled game of \(S\) in which Alice measures \(\{ N^{(\textsc{A},\, x)}_a\} \) and Bob measures \(\{ N^{(\textsc{B},\, y)}_b\} \), each relabelled so that the oracle-shaped answers are grouped into one fixed answer. Then \(\Sigma (N)\) has value at least \(1 - 24\sqrt{\varepsilon }\).
Fix a seed \(z\) and write \(O_{(a,b)}\) for the oracle’s measurement at \((\textsc{O}, z)\) relabelled onto answer pairs, and \(C_a\), \(D_b\) for Alice’s and Bob’s at \((\textsc{A}, L^\textsc{A}(z))\) and \((\textsc{B}, L^\textsc{B}(z))\); the relabellings group the shape failures into one distinguished outcome, so all three are measurements and not sub-measurements. Each of the nine ordered role pairs carries a ninth of the question weight, so at any one of them a set of outcome pairs the decider rejects carries mass at most \(9\varepsilon \) on average over the seed. Applying this at \((\textsc{O}, \textsc{O})\), \((\textsc{O}, \textsc{A})\) and \((\textsc{O}, \textsc{B})\) gives, on average over \(z\),
By Lemma 2.39, \(\sum _{(a,b)} \left\| {C_aD_b - O_{(a,b)}} \right\| _{hs}^2 \leq 3(\alpha + \beta )\) at each seed, so on average at most \(54\varepsilon \). By Lemma 2.40 applied at each seed with \(\mathrm{acc}\) the accepted pairs, the value of \(\Sigma (N)\) at that seed is at least \(1 - \gamma \) minus twice the square root of that closeness; averaging and using Cauchy–Schwarz once more to take the average inside the square root gives \(\mathrm{val}^*\geq 1 - 9\varepsilon - 2\sqrt{54\varepsilon } \geq 1 - 24\sqrt{\varepsilon }\), the last step because \(\varepsilon \leq \sqrt\varepsilon \) for \(\varepsilon \leq 1\) and \(2\sqrt{54} {\lt} 15\).
Let \(S\) be a seeded game with nonempty seed space and nonempty answer alphabet, let \(0 \leq \varepsilon \leq 1\), and let \(N\) be a tensor-product strategy for the oracularization of \(S\) with value at least \(1 - \varepsilon \). Let \(\Sigma (N)\) be the strategy for the game of \(S\), on the same state, in which Alice measures the first player’s \(\{ N^{(\textsc{A},\, x)}_a\} \) and Bob the second player’s \(\{ N^{(\textsc{B},\, y)}_b\} \), each relabelled so that the oracle-shaped answers are grouped into one fixed answer. Then \(\Sigma (N)\) has value at least \(1 - 24\sqrt{\varepsilon }\). Consequently, for every \(\varepsilon {\gt} 0\), if \(\mathrm{val}^*\) of the oracularization of \(S\) exceeds \(1 - \varepsilon \), then \(\mathrm{val}^*\) of the game of \(S\) is at least \(1 - 24\sqrt{\varepsilon }\).
A tensor-product strategy is projective, so no dilation is needed, and its measurements are projective measurements in the two factors of its tensor-product model (Definition 8.49). The first statement is Lemma 8.57 in that model: \(\Sigma (N)\) is the strategy whose measurements are the extracted families, on the same state, and its value is their model value. The argument there is the matrix one, written once for a bipartite model: the chain of three cross-party deviations behind projective front factors, each bounded by one role pair’s conditional failure, the oracle’s joint marginal carrying its acceptance, the single square root of the measurement form of Lemma 2.40, and the average over the seed of the four role pairs used, which gives \(\mathrm{val}^*\geq 1 - 9\varepsilon - 2\sqrt{54\varepsilon } \geq 1 - 24\sqrt\varepsilon \). The paper’s chain eq:oracle-1 to eq:oracle-3 is not needed: the oracle’s measurement enters only through its joint marginal, so there is no marginalization step inside a pair-indexed family, and the second player’s two isolated measurements are multiplied in one order only, so there is no commutation step. For the second statement, when \(\varepsilon \leq 1\) a strategy of value above \(1 - \varepsilon \) exists and the first applies; when \(\varepsilon {\gt} 1\) the bound is negative.
Lemmas 6.135 and 6.136 are the two clauses of Theorem 6.133 with the samplers, deciders and typed question strings stripped away, and they settle the two repairs that are about the strategies: repair 2, the identical measurement operators, is structural, because a synchronous strategy is one family played by both players; and repair 1, the single square root, is where the constant \(24\) comes from. What they do not do is inhabit Definition 6.144: the complexity clause, the bounded parse and its grouping (repair 3), the truncation to \(B_\mathcal{D}(n)\) (repair 4) and the level accounting of Remark 6.145 are all statements about a verifier and none of them appears at this level. The soundness constant here is \(24\) rather than an unspecified \(c\); the ambient contract asks only for some fixed \(c{\gt}0\), so the game-level lemma is stronger than the contract needs on that point and silent on every other.
Lemma 6.136 is stated for synchronous strategies, and a verifier-level statement cannot use that form: \(\mathrm{val}^*\) is a supremum over tensor-product strategies, and so is the strategy transport of detyping, while the bridge from synchronous to general values (Theorem 3.3) is off the critical path. The paper’s own soundness theorem is bipartite. Lemma 6.137 is that form, with the same constant.
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\).
In the setting of Definition 6.139:
(Soundness) for every \(\varepsilon {\gt} 0\) and every answer cut \(T\), if the quantum value of the typed oracularized game exceeds \(1 - \varepsilon \), then \(\mathrm{val}^*(\mathsf{V}_n) \geq 1 - 24\sqrt\varepsilon \) with answers of length at most \(B\);
(Completeness) if \(\mathsf{V}_n\) has a value-\(1\) PCC strategy with answers of length at most \(B\), then for every \(T \geq 8B + 3\) the doubled typed oracularized game has a value-\(1\) PCC synchronous strategy.
The same holds for any typed predicate whose acceptance implies the oracularized predicate after a reading of the answers, for soundness, and for any typed predicate that accepts an encoding of every answer pair the oracularized predicate accepts, for completeness.
The typed game samples a uniform ordered pair of types and one common uniform seed, and the identity gives the oracle the seed itself, so its question distribution is exactly that of the oracularization. For soundness, a tensor-product strategy of the typed game, played through the parse on the same state, is a strategy of the oracularization that loses nothing, because the typed predicate accepts only what the oracularized one accepts after parsing; then Lemma 6.137 applies. For completeness, the strategy of Lemma 6.135, whose two players use identical operators, is doubled and its outcomes pushed forward along the honest encoding: the serialization for an oracle’s pair, the string itself for an isolated player’s answer. Summing a projective measurement over the fibres of a map keeps it projective and keeps commutation, and the pushed-forward strategy wins whenever the original does, because an accepted answer has the shape its type asks for and parses back from its encoding. The serialization of two strings of length at most \(B\) has length at most \(8B + 3\). In the ambient model the input witness already answers with strings of length at most \(B\); in the source model that is what the truncation of Lemma 6.173 provides.
For every sampler \(\mathcal{S}\) with at least one level there is a typed sampler over \(\mathcal{T}^\textsc{Orac}\), with the levels of \(\mathcal{S}\), whose typed CL functions are those of Definition 6.139: the identity for \(\textsc{O}\), and the CL functions \(L^\textsc{A}\), \(L^\textsc{B}\) of \(\mathcal{S}\) for \(\textsc{A}\), \(\textsc{B}\), the same for both players. It depends on \(\mathcal{S}\) alone, and its program is computed from the program of \(\mathcal{S}\) in polynomial time. There are constants \(c, m, e\) such that, whenever \(\mathcal{S}\) runs within \(B(\left\vert {d} \right\vert + 1)^k\) on inputs \((n, d)\) and \(B\), \(\left\vert {\mathcal{S}} \right\vert \) and \(n\) are at most \(W\), the typed sampler runs within \(c(W + 1)^m(\left\vert {d} \right\vert + 1)^{e(k + 1)}\) on inputs \((n, d)\).
The program is a fixed core run on the program of \(\mathcal{S}\) through the s-m-n construction of Lemma 4.8, as the repeated sampler is. The core answers a typed query with at most one call to \(\mathcal{S}\), through the universal machine of Lemma 4.7. The dimension query is forwarded unchanged. A query at an isolated type is forwarded as the query of the corresponding original player. A query at the type \(\textsc{O}\) is answered from the query itself, with no call: the identity’s marginals are the seed, its first stage map is the identity and its later ones are zero, its first factor space is everything and its later ones are empty. The zero vectors are written over the supplied vector rather than over the dimension, so the core never allocates by a dimension it has not been given. A forwarded query is at most twice the typed query plus a constant, and since \(\left\vert {d} \right\vert + 1 \geq 2\) the resulting constant factor is absorbed into the degree, so no term exponential in \(k\) enters the coefficient.
Let \(\mathsf{V}\) be a normal form verifier whose sampler has \(\ell + 1\) levels, and let an index routine supply at each index \(n\) a parse cut \(B(n)\) and a simulation budget \(K(n)\). There is a typed decider over \(\mathcal{T}^\textsc{Orac}\) that halts on every input, whatever the programs of \(\mathsf{V}\) do, whose program is computed from those of \(\mathsf{V}\) and the routine in polynomial time, and which accepts \((n, t, x, u, y, a, b)\) exactly when a fixed core accepts it within \(K(n)\) steps. For \(x, y\) of length \(s(n)\) the core accepts exactly the answers that the bit-string predicate of Definition 6.139 accepts at the cut \(B(n)\): both answers parse by role against \(B(n)\), the checks of fig:oracle-decider hold, and for each oracle the decider of \(\mathsf{V}\) accepts \((n, L^\textsc{A}z, L^\textsc{B}z, a_1, a_2)\). Consequently, for the typed predicate the detyping compiler reads off this decider, at an inner cut of at least \(8B(n) + 3\): if its typed game has value above \(1 - \varepsilon \) then \(\mathrm{val}^*(\mathsf{V}_n) \geq 1 - 24\sqrt{\varepsilon }\) at the cut \(B(n)\), whatever the budget; and a value-\(1\) PCC strategy of \(\mathsf{V}_n\) at the cut \(B(n)\) gives one of the doubled typed game, when the core’s accepting runs on answers within the inner cut take at most \(K(n)\) steps.
The decider is a fixed shell run on the three programs through the s-m-n construction of Lemma 4.8. The shell asks the index routine for \((K(n), B(n))\) and runs the core under the clocked universal machine of Lemma 4.7 for \(K(n)\) steps. This replaces the paper’s timeout-counter form, which the ambient model does not have, and it makes the decider total, which the detyping compiler of Lemma 6.29 requires. The core parses each answer by role and runs the checks that need no call. For each oracle it runs the game check: two marginal queries to the sampler and one call to the decider of \(\mathsf{V}\), all through the universal machine. The decider of \(\mathsf{V}\) need not halt on the inputs it rejects, so both directions of the core’s acceptance law go through inversion lemmas of the programs rather than through determinism. The two value statements are those of Lemma 6.140, read through the acceptance law.
In the setting of Lemma 6.142, let the sampler and the decider of \(\mathsf{V}\) run within \(T_S(\left\vert {d} \right\vert + 1)^k\) and \(T_D(\left\vert {d} \right\vert + 1)^k\) on inputs \((n, d)\), with \(T_S, T_D \leq W\). There are constants depending only on \(\ell \) such that:
the core runs on every well-formed input \(c\) within \(c_0(W + 1)^m(\left\vert {c} \right\vert + 1)^{e(k + 1)}\);
hence, if the budget \(K(n)\) is at least that bound at the largest core input whose answers lie within the inner cut, the completeness statement of Lemma 6.142 holds with no further hypothesis;
the decider runs on every input \((n, d)\) within \(c_1(W + 1)^{m_1}(\left\vert {d} \right\vert + 1)^{e_1}\) whenever \(K(n)\), \(B(n)\), the index routine’s running time at \(n\), the description lengths of the three programs and \(n\) are at most \(W\), and the degree \(e_1\) does not depend on \(k\).
The core’s cost is the sum of the costs of its stages, each bounded through the cost lemmas of the routing combinators and the overhead of the universal machine. The answers of the sampler of \(\mathsf{V}\) to the marginal queries are sized by its correctness clause, as vectors of length \(s(n)\), and not by its running time; otherwise the time of the decider of \(\mathsf{V}\), of degree \(k\) in its input, would compound to degree \(k^2\). Affine size bounds are absorbed into powers of \(\left\vert {c} \right\vert + 1 \geq 2\), so that no constant depends on \(k\). The decider’s own cost is that of the index routine and of the clocked universal machine on the budget and the input, so the running time of \(\mathsf{V}\) enters only through the budget.
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\).
An earlier version of MIPRE.Oracularization was untyped and level-preserving, with value transfers as fields. It was satisfied by a transformation that does not oracularize at all: keep the input sampler, and let the output decider reject any answer longer than the parse bound and otherwise run the input decider. At the parse bound its game is \(\mathsf{V}_n\) itself, so completeness is the identity and soundness holds with \(c = 1\). No field saw the oracle form of the output — that one player’s answer alone decides the game check, and the other player’s answer must equal one of its components — and that form is the only property of oracularization that answer reduction uses: the probabilistically checkable proof replaces exactly that game check (Lemma 6.179), and the decoding step returns to exactly that form (Lemma 6.189).
The specification of Definition 6.144 sees the oracle form in both halves: the sampler is fixed to the oracle’s, and the decider’s acceptance implies the oracularized predicate. It is inhabited by the construction, and the value transfers are theorems about every inhabitant, both for the typed game and for the verifier with \(\ell + 3\) levels that the detyping compiler produces. In the source, oracularization is internal to the proof of Theorem 6.192, whose analysis uses the typed verifier and detypes only the final answer-reduced verifier. The checked composition MIPRE.GapCompression.ofPipeline does not consume MIPRE.Oracularization, and the detyped verifier is not a stage of compression.
Node \(1.3.5\) was added late — round 12 of the campaign found that oracularization.tex was covered by no ledger node at all, although both of its theorems are consumed by answer reduction — and it carries four repairs that the statement above has been written to respect.
The soundness constant \(\delta _\textsc{Orac}\) carries one square root: the step from a \(1 - O(\varepsilon )\) measurement-closeness to a \(1 - O(\sqrt{\varepsilon })\) statement about the value is an application of [ 6 , Fact 4.31 ] , not an identity. An earlier revision of this blueprint wrote \(\delta (\varepsilon ) = \mathrm{poly}(\varepsilon )\), which is not merely imprecise but false as stated: \(\sqrt{\varepsilon }\) is not a polynomial in \(\varepsilon \).
The completeness witness’s extra property is identical measurement operators, not symmetry of the state. The campaign found the claim that the constructed strategy is symmetric “by construction” unjustified — the hypothesis supplies a value-\(1\) PCC strategy whose state is reused unchanged, and no lemma in the paper symmetrizes such a strategy while preserving projectivity, consistency and value \(1\). SPCC was withdrawn from the completeness clause in consequence. The ambient interface starts from a different strategy representation; transferring this source witness requires Remark 2.8.
The oracle families are genuine projective measurements. Outcomes failing the decider’s bounded parse are grouped into a distinguished outcome; leaving that implicit made them sub-measurements, which the later sandwiching argument may not use.
The truncation of answers to \(B_\mathcal{D}(n)\) symbols is justified by a corollary of the timeout-counter form, not by the assertion that a timeout-form decider inspects at most \(B_\mathcal{D}(n)\) symbols. Nothing forces \(B_\mathcal{D}(n)\) to exceed the time bound \(T\) against which the PCP decodes, so the truncation is load-bearing and a formalization must carry it explicitly.
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.83 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.111 for the arithmetization. Answers and decider time become polylogarithmic in the original.
There is a polynomial-time algorithm that, on the inputs of Theorem 3.83 under the same hypotheses, outputs a circuit with two inputs of length \(\ell _0 = \lceil \log 2T \rceil \), three of length \(r_0 = O(\log T + \log \sigma )\) and five single-bit inputs, with at most \(s_0 = \mathrm{poly}(\log T, \log n, Q, \sigma )\) gates, which describes the decider \(\mathcal{D}\) on \((n, x, y)\) at time \(T\) in the sense of Definition 3.82: the variables of the decoupled 5SAT formula fall into five blocks, the first two being the players’ answer strings, and every clause touches each block once. The parameters \(\ell _0, r_0, s_0\) are computable in time polynomial in the bit lengths of \(n, T, Q, \sigma \). (The padded description, with the outer variable count a power of two, is the padding step of the PCP, Remark 6.169.)
Run the describer of Theorem 3.83 to get a circuit \(C_3\) on \(3 r_0 + 3\) inputs, \(r_0\) being that theorem’s index width, and set \(\ell _0 = \lceil \log 2T \rceil \). Since \(2^{r_0} \geq 4T\) and \(2^{\ell _0} {\lt} 4T\) we have \(\ell _0 \leq r_0\), so an \(\ell _0\)-bit index compared with an \(r_0\)-bit one is zero-padded and \(i_2 + 2T {\lt} 4T \leq 2^{r_0}\) does not overflow. The output circuit accepts \((i_1, \ldots , i_5, o_1, \ldots , o_5)\) when any of nine conditions holds: the first is \(C_3(i_3, i_4, i_5, o_3, o_4, o_5) = 1\), and the other eight are \(i_1 {\lt} 2T \land i_1 = i_3 \land o_1 \neq o_3\); \(i_2 {\lt} 2T \land i_3 = i_2 + 2T \land o_2 \neq o_3\); \(i_1 \geq 2T\) with \(i_1\) even and \(o_1 = 1\), or \(i_1\) odd and \(o_1 = 0\); the same two for \(i_2, o_2\); \(i_3 = i_4 \land o_3 \neq o_4\); and \(i_4 = i_5 \land o_4 \neq o_5\).
For a fixed triple of indices the signs of the blocks a condition does not constrain range over all of \(\{ 0,1\} ^3\), so a decoupled clause is satisfied exactly when the literals of the blocks it does constrain are. The last two conditions therefore say \(w_1 = w_2 = w_3\), the first two that the common assignment agrees with \(a\) below \(2T\) and with \(b\) on \([2T, 4T)\), and the middle four that \(a\) and \(b\) carry the blank padding above \(2T\). So a satisfying five-tuple is exactly a satisfying assignment of \(\varphi _{3}\) extending the answer blocks, and item 1 of Theorem 3.83 finishes it. Sizes and running times are those of \(C_3\) plus \(O(r_0)\) gates for the eight conditions.
An earlier sketch here described decoupling as a generic syntactic transformation — split a clause that touches a block twice by adding a fresh variable and an equality clause — which is not the construction the source gives and does not produce the promised index lengths: \(\ell _0\) is pinned to \(\lceil \log 2T \rceil \) by the answer blocks, and a generic splitting fixes neither that nor \(r_0\). The proof above is the source’s.
The parities of the four padding conditions are a repair of the verification campaign, and the one place where a careless transcription breaks completeness rather than soundness. Blocks are \(0\)-indexed and the blank encodes as \(10\), so the honest padding begins at the even index \(2T\) and puts \(1\) at even indices and \(0\) at odd ones; the pre-repair text had it the other way round, which the honest assignment violates. The formalization’s tape encoding agrees with the repaired parity, so nothing had to be adapted — but nothing was taken on trust either.
[\(\checkmark \) (mostly) in Mathlib]
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\).
Source.
The paper states this in preliminaries.tex, Section sec:ld-encoding, alongside Lemma 3.111; it is recorded here, with its consumer, because Theorem 6.164 is the only place the blueprint uses it.
Comments.
The identification of \(\{ 0,1\} ^m\) with \(\{ 1, \ldots , M\} \) is any fixed bijection — the paper says “lexicographic”; the formalization uses the repository’s existing little-endian bitsVal convention, so that the encoding of an answer block agrees with the tape indexing of Theorem 3.83. The choice is invisible to the statements below, the same bijection appearing in the encoding and in the decoding.
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\).
[\(\bullet \bullet \bullet \) hard]
Embed the five blocks of a decoupled formula into larger blocks. Add every clause whose first or second literal is beyond its original answer block and has the blank-tape sign: positive at even indices, negative at odd indices. The enlarged formula is satisfied exactly when the restrictions satisfy the original formula and both complete answer tails equal the blank tape. Thus a circuit implementing this clause set still describes the same decider, provided the original answer block has length at least \(2T\).
Restriction proves the original clauses. To isolate an answer-tail bit, choose the signs in the other four blocks so that their literals are false. Conversely, each added clause contains a true blank-tail literal. Extend the three auxiliary assignments arbitrarily, and use that every accepted answer has length at most \(T\), so its tape is blank beyond \(2T\). This is the semantic part of the paper’s prop:exciting-padding-prop; the circuit algorithm and its cost remain separate obligations.
Binary equality, array lookup by a binary index, and formula renaming have ambient polynomial-time programs. The least power of two above a unary number can be produced in unary in polynomial time. Binary normalization, predecessor, and addition or subtraction of a unary offset are polynomial-time as well.
Scan the supplied array instead of expanding its index. Rename the formula’s postorder input nodes. For power-of-two rounding, double a unary accumulator once per binary digit, capping every intermediate state by twice the input length plus one. Normalize binary numbers by a fold of the binary constructor; the existing borrow machine gives predecessor, including a separate zero case. The offset loops have explicit bounds on every intermediate encoding.
There are effectively computed parameters \(m(T,\sigma )\) and \(s(n,T,Q,\sigma )\), with \(m\) a power of two, \(m=O(\log T+\log \sigma )\), \(2^m\geq 2T\), \(s\geq m\), and \(5m+5+s\) a power of two polynomially bounded in \(\log n+\log T+Q+\sigma \). On a valid specification and a unary budget of length \(s\), an ambient polynomial-time program constructs a well-formed circuit with five \(m\)-bit blocks, five signs, and exactly \(s\) gates, describing exactly the same accepting answer prefixes. The parameter program is polynomial-time in the binary parameter lengths.
Implement the padded clause predicate by a renamed formula and comparisons with the original block bounds. Round the common width up to a power of two. From the circuit program’s proved output bound \(s_1\), set \(m'=2^{\lceil \log _2(6m+5+s_1)\rceil }\) and \(s=m'-5m-5\). Append copying OR gates to reach exactly \(s\) gates; this preserves the last-gate output convention and fan-out two. The unary budget prevents an invalid short input from demanding exponentially many output gates. In the PCP verifier the formatted view will supply this budget; connecting that caller remains part of Theorem 6.164.
The padded dimensions extend to ambient polynomial-time classical PCP parameters \((k,m,s)\) with \(k\) odd, \(q=2^k\geq 82m'\), and both \(m\mid q\) and \(m'\mid q\). The field is moreover eventually larger than every fixed power of \(8(Q+1)m'\): for every \(e\), once \(Q\geq 2^e\), \(q\geq (8(Q+1)m')^e\), while \(k\) stays polylogarithmic in \(Qm'\).
Choose \(k=2(s_0^2+\mathrm{size}(m'))+7\) with \(s_0=\mathrm{size}(Q)+\mathrm{size}(m')+3\). Then \(q\geq 128(2^{\mathrm{size}(m')})^2\geq 82m'\). Both dimensions are powers of two at most \(q\), hence divide it. Since \(8(Q+1)m'{\lt}2^{s_0}\), for \(s_0\geq e\) we get \((8(Q+1)m')^e{\lt}2^{s_0e}\leq 2^{s_0^2}\leq q\), and \(Q\geq 2^e\) gives \(s_0{\gt}e\); this is the field size answer reduction’s low-degree test needs (FieldLarge), whose exponent this construction need not know. Compute the degree in unary from the binary lengths of \(Q\) and \(m'\) and combine it with the already verified \((m,s)\) program.
Over a field of characteristic two, every well-formed circuit with \(n\) inputs and \(s\) gates has a Boolean-valued arithmetization on exactly \(n+s\) coordinates, of individual degree at most five, hence at most six. An input is accepted exactly when it extends to a Boolean assignment at which this polynomial is one.
The current circuit interface bounds gate fan-out, but permits repeated reads of one external input. Route the first read through the external variable and each later read through its preceding input gate. These copy links use each variable at most once and preserve all Boolean gate values. In characteristic two, \(1+w_g+\mathrm{rhs}_g\) indicates gate consistency. Multiply these factors and the output literal. A variable contributes at most one degree from its own factor, two from ordinary fan-out, one from a copy link, and one from the output literal. Restrict to the exact input and gate coordinates by setting all other variables to zero; this preserves degree and evaluation. The polynomial-time field evaluator for this expression is supplied by Lemma 6.156.
There is an ambient polynomial-time evaluator for the routed circuit polynomial on binary coefficient vectors, uniform in the supplied monic binary modulus. Over a characteristic-two field containing a root of that modulus, correctly sized inputs evaluate to the circuit polynomial at the corresponding field point, including its restriction to the exact finite set of input and gate coordinates.
Dispatch the five gate constructors, scan preceding input copies, and use the verified coefficient-vector addition and modular multiplication programs. Multiply the consistency factors and output coordinate directly. The scan stores only the supplied coordinates and preceding gate/value pairs; the accumulator width never grows, even on malformed inputs. Its ambient cost therefore has a global polynomial bound. Induction over the gate prefix identifies its accumulator with the product of the polynomial factors. The Shoup field uses the same quotient carrier and canonical coefficient representation after recording its exact degree. This proves circuit evaluation; assembling the PCP verifier and its prescribed runtime bound remains part of Theorem 6.164.
For a well-formed circuit with \(5m+5\) inputs and exactly \(m'\) input and gate variables, the typed algebraic PCP is complete and majority-sound for the actual five-block formula. If the circuit describes a decider, completeness uses its accepted answer prefixes, and soundness recovers accepted prefixes and both entire decoded answer tapes.
Identify little-endian indices with Boolean cube points by an explicit bijection. The circuit’s input order is exactly the five PCP blocks followed by their signs, with inverse encodings preserving every literal. Transport the finite circuit polynomial to the advertised PCP dimension. Its Boolean witnesses correspond to precisely the circuit’s clauses. Apply the honest-proof construction and majority decoding, then the describer’s exact accepting-tape relation. These are typed algebraic tests; the raw verifier program is a separate obligation.
Valid formatted PCP inputs for the constructed parameters have encoded size polynomial in \(L=\log n+\log T+Q+\sigma \). Consequently every ambient polynomial-time program on these inputs has runtime polynomial in \(L\).
A list of \(r\) field blocks of width \(k\) has encoded size at most \((4k+2)r+1\). The two view lists therefore have total size at most \((4k+2)(2m'+6)+3\). The padded outer dimension is polynomial in \(L\), and \(k=2\mathrm{size}(m')+7\leq 2m'+7\). Add the valid specification’s size bound and compose the resulting polynomial with the program’s ambient time bound.
A uniform ambient program checks specification validity and all view dimensions, constructs the padded circuit within the view’s unary output budget, and performs both polynomial tests. On a represented low-degree proof it accepts exactly when the typed algebraic tests hold. Invalid specifications and malformed views are rejected. Its runtime on valid formatted inputs is polynomial in \(\log n+\log T+Q+\sigma \).
Use binary comparisons for the parameters and list scans for the shape checks. Evaluate the circuit and both field identities using coefficient-vector arithmetic. Fixed-width evaluation at the Shoup quotient’s root is injective, so raw bit equality is field equality. The clause coordinates and answer blocks agree with the typed proof view. Apply Lemma 6.158 to the assembled program.
A Boolean formula has a polynomial arithmetization over any nontrivial commutative ring, agreeing with its Boolean value on Boolean inputs. The degree in each variable is at most the number of occurrences of that variable, including identifications made by the assignment of formula inputs to polynomial variables.
Replace conjunction by multiplication, negation by subtraction from one, and disjunction of \(f,g\) by \(1-(1-f)(1-g)\). Induction on the formula proves both claims. The circuit application must bound external input occurrences as well as gate fan-out; the current circuit well-formedness predicate only bounds the latter.
Let \(f\) be a polynomial over a field, of individual degree at most \(d\), vanishing on \(\{ 0,1\} ^m\). There are polynomials \(c_i\), each of individual degree at most \(d\), such that the polynomial identity \(f=\sum _i c_i X_i(1-X_i)\) holds. Division in a single coordinate can be performed without increasing the degree in any coordinate, leaving degree at most one in the selected coordinate.
Repeatedly replace the part divisible by \(X_i^2\) with the corresponding multiple of \(X_i\). This decreases the degree in coordinate \(i\) while preserving all other coordinate bounds. Eliminate each coordinate in turn. The remaining multilinear polynomial vanishes on the Boolean cube and is therefore zero. The general Nullstellensatz total-degree bound alone does not give the individual-degree bounds required here.
Write \(p=\varphi \prod _{i=1}^5(g_i-X_{s_i})\) and \(z_c=\sum _j c_jX_j(1-X_j)\). The algebraic verifier tests \(c_0=p\) and \(c_0=z_c\) at its sampled point. If \(p\) vanishes on the Boolean cube and has individual degree at most \(d\), certificates of individual degree at most \(d\) pass both tests everywhere. Conversely, if \(\varphi \) has individual degree at most six, all \(g_i,c_j,c_0\) have individual degree at most \(d\), and \(|\mathbb {F}|\geq 2m(6+5\max \{ d,1\} )\), acceptance on more than half of \(\mathbb {F}^m\) forces both polynomial identities. On each Boolean point with \(\varphi =1\), one of the five answer evaluations equals its sign.
Completeness uses Lemma 6.161. For soundness, the two tested polynomials have individual degree at most \(6+5\max \{ d,1\} \) and \(d+2\), respectively. Schwartz–Zippel forces equality from strict majority agreement. Evaluation on the Boolean cube annihilates every zero-certificate term, so the product of the five literal factors is zero on a described clause. This is the algebraic component only: padding, answer-block embeddings, decoded answer strings and the ambient verifier program remain separate obligations.
Embed each of the five answer polynomials in its own coordinate block of the \(m'\)-variate point, with distinct sign coordinates outside those blocks. This preserves individual degree, and for multilinear answers the product of the five literal factors is multilinear. Consequently a degree-six Boolean clause-description polynomial and a satisfying five-tuple of Boolean assignments give a degree-seven PCP proof passing both algebraic tests at every point. Conversely, for \(q\geq 82m'\), strict majority acceptance of a degree-seven proof implies that the Boolean decoding satisfies every described Boolean clause. These are statements about the existing PCP proof type and its typed evaluations.
Injectivity of each coordinate embedding preserves degrees; the images of different blocks, and their sign coordinates, are disjoint. A coordinate therefore contributes degree at most one to the literal product. Encode the five assignments multilinearly and apply the zero-basis decomposition to the degree-seven constraint. For soundness, transport the degree bounds to the ambient point and use Lemma 6.162. Any answer evaluation equal to its Boolean sign survives the decoding map.
Scope.
Lemma 6.157 supplies the clause-description polynomial and its relation to the input decider. Lemma 6.159 supplies the raw verifier and its runtime.
There is a verifier \(\mathsf{M}^{\mathsf{ar}}\) which, given a valid decider specification \((\mathcal{D}, n, T, Q, \sigma , x, y)\) — validity requiring \(\left\vert {\mathcal{D}} \right\vert \leq \sigma \), \(\max \{ Q, 2\lceil \log n \rceil \} \leq T\) and \(\left\vert {x} \right\vert , \left\vert {y} \right\vert \leq Q\), as exact inequalities — together with a PCP view \((z, \Xi )\), rejects any invalid specification or misformatted view, runs in time \(\mathrm{poly}(\log T, \log n, Q, \sigma )\) and satisfies:
(Completeness) if \(\left\vert {a} \right\vert ,\left\vert {b} \right\vert \leq T\) and \(\mathcal{D}\) accepts \((n, x, y, a, b)\) within \(T\) steps, then the low-degree proof with \(g_1, g_2\) the low-degree encodings (Definition 6.149) of the padded answers is accepted with probability \(1\) over uniform \(z\);
(Soundness) any low-degree proof accepted with probability greater than \(\frac12\) has \(\mathrm{Coded}(g_1), \mathrm{Coded}(g_2)\) equal to the padded encodings of two strings whose prefixes, of length at most \(T\), \(\mathcal{D}\) accepts within \(T\) steps.
Here the parameters are \((q, m, d, m', s) = \mathrm{pcpparams}(n, T, Q, \sigma )\) with \(q = 2^k\) for an odd \(k\), \(d = 7\), \(m' = 5m + 5 + s\) and \(2T \leq 2^m\), computable in time polynomial in the bit lengths of \((n, T, Q, \sigma )\); and both variable counts \(m\) and \(m'\) of the arithmetization must be powers of two dividing \(q\) (Remark 6.169).
The verifier checks the arithmetized formula and a certificate that its constraint polynomial vanishes on the Boolean cube. Soundness against the low-degree proofs in the statement follows from Lemma 3.111. The PCP theorem itself does not run a quantum low-degree test or consume Pauli-test soundness; those belong to its later composition with a nonlocal game. Four obligations are separate in the source and stay separate here: the proof format and query structure, completeness, the zero-testing argument with its error bounds, and the complexity bound the composition consumes.
The Lean field family is indexed by odd extension degrees, as required by the parameter choice. Requiring a field of cardinality \(2^k\) for every natural \(k\) would include \(k=0\) and make the contract uninhabitable. The constructed verifier uses the canonical polynomial-basis representation and uniform field programs from the proved binary irreducible-polynomial constructor (Lemma 3.103). Its exact axiom guard contains only Lean’s standard axioms. Effective self-dual normal coordinates are supplied by Lemma 3.87; integrating those coordinates into the downsizing consumers remains a separate obligation.
The theorem has four obligations, and they are separate in the source because they fail separately.
[\(\bullet \bullet \) medium]
The proof \(\Pi \) that \(\mathsf{M}^{\mathsf{ar}}\) reads is well defined: it consists of the low-degree encodings \(g_1, g_2\) of the two padded answer prefixes, together with the auxiliary polynomials the zero-test needs, in the stated input formats; and \(\mathsf{M}^{\mathsf{ar}}\)’s queries and decision rule are determined by them.
A proof is five \(m\)-variate and \(m'+1\) \(m'\)-variate polynomials of individual degree at most \(d\) (PcpProof); the verifier reads, at a point \(z\), the five answer polynomials on their blocks and the constraint polynomials (PcpProof.ev), as \(k\)-bit blocks (PcpProof.rawView), and an honest view is well formatted (viewFormat_rawView).
[\(\bullet \bullet \) medium]
If \(\left\vert {a} \right\vert ,\left\vert {b} \right\vert \leq T\) and the decider accepts \((n, x, y, a, b)\) within \(T\) steps, then the honestly generated proof \(\Pi \) — the low-degree encodings of the actual answers, with the auxiliary polynomials computed from them — makes \(\mathsf{M}^{\mathsf{ar}}\) accept with certainty.
Combine the padded describer’s accepting witness, the degree-seven zero certificate, and the equivalence of raw and typed tests.
[\(\bullet \bullet \bullet \) hard]
If \(\mathsf{M}^{\mathsf{ar}}\) accepts with probability greater than \(\tfrac 12\) on views of a fixed proof whose answer and certificate polynomials all have individual degree at most seven, then the decider accepts the answers the first two polynomials decode to. The entire decoded answer vectors equal the padded tape encodings of the accepted prefixes.
Zero-testing of the constraint polynomial against a zero basis, with Lemma 3.111 bounding the probability that a nonzero polynomial vanishes on a random point. The stated error bounds are what the composition consumes, so a formalization should carry them rather than an asymptotic form.
[\(\bullet \bullet \) medium]
\(\mathsf{M}^{\mathsf{ar}}\) runs in time \(\mathrm{poly}(\log T, \log n, Q, \sigma )\), with circuit-size and randomness bounds of the same form. These are the bounds the composition of Remark 6.195 consumes; in particular the randomness bound is what makes the answer-reduced sampler conditionally linear.
The verifier is a polynomial-time program, and its encoded input on a formatted view is polynomial in \(\log n+\log T+Q+\sigma \) (pcpInput_size_polynomial), whence its running time (verifyPcp_time_le). The circuit has \(m'\) coordinates, polynomial in the same quantity (outerDim_polynomial), and the randomness, a point of \(\mathbb F_q^{m'}\), is \(km'\) bits, polynomial by the parameter bound (exists_paramsBound_classical).
The hypothesis is not cosmetic and was a confirmed defect in the source. The \(m\)-variate low-degree test needs \(m \mid q\), and \(q\) is a power of two, so \(m\) must be one as well. The padded description guarantees this only for the outer variable count \(m' = 5m + 5 + s\); the inner \(m\), inherited from the succinct-SAT reduction, carries no such guarantee, which leaves the conditionally linear functions of the axis-parallel and diagonal lines ill defined and the applications of low-degree soundness with an unverified hypothesis. The repair is to round \(m\) up to a power of two in the padding step, which costs nothing asymptotically. A formalization must state it as a hypothesis, as Theorem 6.164 does.
[\(\bullet \bullet \bullet \) hard]
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.
Three steps, of which only the middle one is about sandwiches.
From evaluations to outcomes. Fix \(i\) and write \(\eta \) for the probability that the \(i\)th coordinate of \(A\) and \(G^{i,x}\) return different functions. The Born probabilities do not depend on \(y\), and two different functions are separated at \(y\) with probability at least \(1-\varepsilon \), so the evaluated disagreement is at least \((1-\varepsilon )\eta \); since \(\eta \leq 1\) this gives \(\eta \leq \delta +\varepsilon \) with no case split. Both measurements are projective, so their squared distance across the parties is exactly \(2\eta \).
One layer at a time. Split the outcome as \((o, g)\) with \(g\) the last coordinate. Alice’s element is the palindrome \(A_g A_o A_g\) of her two marginals, and three replacements move it to Bob’s \(G_g C_o G_g\): the right \(A_g\), then \(A_o\), then the left \(A_g\). Each multiplies a known deviation by a family \(F\) with \(\sum F^\dagger F\leq I\) — the joint projections, the product of the contraction \(A_g\) with the projective \(G_g\), and \(G_g C_o\) with \(\sum _o C_o^2\leq I\) — so each costs exactly the deviation it multiplies (the paper’s fact:add-a-proj). The three costs are added as square roots, by Minkowski’s inequality in \(\ell ^2\) over the index and the outcomes: each layer adds twice the square root of its coordinate’s squared distance, and by induction on \(k\) the square root of the outcome-level squared distance between \(A\) and \(C\) is at most \(2\sum _i (2(\delta +\varepsilon ))^{1/2}\). The cruder \((a+b+c)^2\leq 3(a^2+b^2+c^2)\) would lose a factor \(3\) at every layer, exponential in \(k\).
Back to agreement, then evaluation. Against a projective measurement, \(1-\sum _g\langle \psi |A_g\otimes C_g|\psi \rangle \) is a sum of cross terms against the deviations and is at most the square root of the squared distance, whatever \(C\) is; Jensen moves the average over \(x\) inside the root. Evaluating both sides at \(y\) merges outcomes, and since every Born probability involved is nonnegative, merging can only add agreement.
Comments.
Both relations are the paper’s consistency relation of games.tex — a disagreement probability — and not the squared distance that \(\simeq _\delta \) denotes here; this entry previously stated the hypothesis and the conclusion as squared distances with an unspecified constant, which is equivalent up to the factor of 1 but is not how the source states it or how its consumer, Lemma 6.187, uses it. The source defers the proof to NW19’s Fact 4.34, whose import was audited [ 34 ] ; the formalization re-derives it, and the constant \(2\sqrt{2}\) it produces is the universal constant the source leaves implicit. Two generalizations cost nothing and are kept: \(y\) may be drawn from any distribution independent of \(x\), with the collision bound stated against it; and the families are arbitrary finite sets with evaluation maps, so the consumer’s alphabets extended by zero projectors are covered without comment. The collision bound is a hypothesis: for polynomial families it is Lemma 3.111, applied by the consumer.
For a source decider in standard timeout-counter form (Remark 6.30) with \(B=B_D(n)\), simultaneously replacing its two answers by their length-\(B\) prefixes preserves the result: accept, reject, or timeout. The counter depends only on \(n\) and the underlying machine is simulated for at most \(B\) steps, so none of the changed cells can be read. This is not the false assertion \(\mathsf{TIME}_D(n)\leq B\); wrapper runtime may be polynomial in \(B\). The Lean proof does not use this lemma: ambient deciders have no timeout counter, and answers beyond the cut are rejected by the decider itself (Lemma 6.21).
The typed oracle verifier is compiled in time polynomial in the input description. Its sampler preserves \(\ell \) levels, depends only on the input sampler, and runs in \(\mathrm{poly}(\mathsf{TIME}_S(n))\). Its decider runs in \(\mathrm{poly}(\mathsf{TIME}_S(n),B_D(n))\), including the bounded format checks. This is the typed construction used inside answer reduction. In the ambient model the decider’s running time is polynomial in the budget of its index routine, and a budget polynomial in the running times of the input verifier covers the core (Lemma 6.143).
The sampler is that of Lemma 6.141: its program is a polynomial-time function of the input sampler’s (MIPRE.OracleSampler.samplerProgFun), within the time bound oracleSampler_timeBound. The decider is that of Lemma 6.142, whose program is a polynomial-time function of the input programs (MIPRE.OracleDecider.deciderProgFun), and its running time is Lemma 6.143.
Coarse-grain a perfect input PCC witness by length-\(B_D(n)\) prefix truncation. Orthogonal projector sums preserve completeness and projectivity; commutation and consistency are preserved by the common deterministic map. The preceding truncation lemma preserves value one on the same state. These measurements supply the honest isolated-player and joint-oracle measurements with legal answer lengths and the same combined operator rule for both players. The Lean proof does not use this lemma: an honest witness already answers within the cut, so no truncation is needed (Lemma 6.180).
The following answer-reduction obligations use the parameter routine and input hypotheses of Theorem 6.192. In measurement relations, “consistent” means close in the cross-party squared distance of Definition 2.28; bounds on game failure are stated separately. Put \(\theta =16^{|T^{\mathrm{ar}}|}\varepsilon _{\mathrm{out}}\), \(E=\delta _{\mathrm{CL}}(\theta ,q,m',d,m'+6)\) and \(\rho =m'd/q\). The common upper bound \(\kappa \) below absorbs both the individual and simultaneous errors; it is not a renaming of the source’s individual \(\delta _1\) or simultaneous \(\delta _2\).
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.
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:
equal types have equal answers;
the oracle’s \(\mathrm{Point}_6\) answer agrees with an isolated player \(v\)’s \(\mathrm{Point}_v\) answer in component \(v\);
an isolated player \(v\)’s input codeword passes the \(m\)-variable test on copy \(v\);
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;
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 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.
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|\).
The program first runs a routine computing the PCP parameters at the index: \(\lambda \) and \(n\) in unary (\(\lambda \) replaced by \(0\) at the index \(0\)), \(Q\) by a power loop, \(\mu \) in unary and \(T=2^{(Q+5)(\mu +1)}\), the parameters by the PCP decider’s parameter program, and the copies’ offsets, lengths, selector widths and seeds in unary; every loop is as long as one of \(\lambda \), \(n\), \(\mu \), \(Q\), \(k\), \(m\), \(s\), and the bit length of \(T\) is the product of one quantity below \(W\) and one below \(\mu +1\). A query at a type is then split: the bits of the PCP part are answered outright, and the others make up a query to the typed oracularized sampler, answered through the universal machine, below its own level; beyond it the marginal is asked at its last level and a linear map or factor query has a zero oracle half. A PCP query is answered by the copy its type names, on the three runs of \(k\)-bit blocks: the seed on the seed run, the selected direction on the direction run and the line’s base point on the point run, computed by the introspection sampler’s Shoup programs. Each of the three kinds of answer is the Shoup bits of the presentation’s, run by run. The forwarded query is at most linearly larger than the typed query, so the oracularized sampler’s time on it, which is polynomial in \(W\) times the query’s size to the power \(e(\mu +1)\), raises only constants to the power \(\mu +1\); the rest is polynomial-time work on data of dominated size. Bounds of the shape \((c(W+1)^m X^e)^{\mu +1}\) are closed under sums, products, fixed polynomials and such calls, which is the whole accounting.
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.
The decider runs the sampler’s parameter routine, computes \(Q\) and \(T\), asks the input sampler for both players’ full marginals at the oracle halves of the two questions through the universal machine, and runs the PCP verifier on each question’s game-check view. It then parses each answer into \(k\)-bit blocks and decides on blocks. Of the low-degree test’s decision only a point question against a line question of the same copy is ever checked, and there it is the line-versus-point check of the introspection programs on the line the question describes: the seed’s high bits select the axis or mask the diagonal direction, and the line’s base point is the sampler’s third-stage representative. The five steps are organised by what the type pair asks for: at most one comparison of two answer blocks, one low-degree subtest and one game check, chosen by a finite table of the types. Every stage halts on every input, since the parses are total, the input sampler halts on every input and the PCP verifier runs on the encoding of a genuine input; so no clock is needed, and acceptance is the predicate by determinism. Its time is dominated as the sampler’s is: each marginal query is the oracle half of a question with a constant-size header, and everything else is polynomial-time work on the context.
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\).
The output is the typed verifier of Lemmas 6.177 and 6.178 through the detyping compiler, at a cutoff routine that runs the parameter routine and writes both cuts \(32(k+1)(m'+7)^2\). Its programs place the input programs in fixed contexts, which is polynomial time. Take \(W=(\lambda n+1)^\mu +\sigma +\lambda +n\): it is above \(Q\), \(\lambda \), \(\sigma \), \(n\), both input programs’ sizes and the input sampler’s dimension, so the typed sampler’s and decider’s bounds apply. The detyped sampler’s coefficient is the router’s cost polynomial at the index, with the typed sampler’s coefficient raised to the router’s degree; the detyped decider runs the typed sampler on the dimension query, the cutoff routine, and at most one call to the typed decider on a typed input with questions of the typed sampler’s dimension, whose oracle halves are the input sampler’s questions, and answers within the cut. The dimension and the cut are polynomial in \(W\) and the PCP’s parameters. Every bound has the shape \((c(W+1)^m)^{\mu +1}(|d|+1)^{e(\mu +1)}\), and the sum of the constants and the largest exponents give \(P\) and \(d\).
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).
Each player measures the oracularized game’s honest strategy (Lemma 6.135) at the oracularized question its seed’s oracle half determines, and post-processes the outcome classically: an oracle answering the pair \((a,b)\) at seed \(x\) holds a PCP proof of \((x,a,b)\) from Theorem 6.164, whose first two answer polynomials are the low-degree encodings of \(a\) and \(b\); an isolated player \(v\) answering \(a\) holds the low-degree encoding of \(a\) at copy \(v\) and zero elsewhere; each answers every low-degree question honestly, with the values at a point and the restrictions to a line. A measurement read through a question map and a question-dependent answer map stays projective, PCC when pairs of positive weight are read as pairs of positive weight, and of value \(1\) when the old strategy’s operators for rejected pairs multiply to zero there and every accepted old pair is read as an accepted new one. Two typed questions of positive weight are read off one seed: their oracle halves are an oracularized pair of positive weight, whose checks (equal roles give equal answers, an oracle’s component matches the isolated player’s, the oracle’s pair is accepted) are exactly the consistency the five steps of the answer-reduced predicate need, and their PCP halves are questions of one PCP vector, where the seeded test (Definition 3.13) accepts honest answers of polynomials of individual degree at most \(7\), the base points the presentation outputs being already canonical. The oracle’s check passes at every point because the input decider accepts within the PCP’s time bound \(T=2^{(Q+5)(\mu +1)}\), \(Q=(\lambda n+1)^\mu \): it runs within \(2^Q(\left\vert {d} \right\vert +1)^\mu \) on every input, and the answers are already cut at \(2^Q\), so the timeout of Lemma 6.173 is here a consequence of determinism rather than a truncation. The PCP’s validity needs \(2\lceil \log n\rceil \leq T\), which is where \(\lambda ,\mu \geq 1\) enters. Honest answers are at most \(32(k+1)(m'+7)^2\) bits long, the answer cut, where the detyped decider’s predicate is the typed game’s; detyping completeness (Lemma 6.25) gives the output’s strategy.
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.
Detyping soundness (Lemma 6.27) restricts the strategy to the typed game with the typed decider’s predicate, which is the typed answer-reduced predicate at the answer cut, on the same state.
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).
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 typed game samples a uniform ordered pair of the \(54\) types and a uniform seed, so the failure conditioned on one type pair is at most \(54^2\theta =2916\theta \) (sum_edges_le). Restricted to one copy’s type pairs at a fixed oracle half, the strategy is a strategy for that copy’s seeded low-degree game, whose failure is at most the conditioned typed failure, averaged over the seed (sum_copyFail_le, sum_copyFail6_le); an equality subtest between two players’ answers gives their disagreement (sum_dis_edge_le).
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.
The two input-codeword tests are type pairs of the typed game: an isolated player’s point of copy \(i\) against the oracle’s \(\mathrm{Point}_6\), in both orders of the players. Each fails at most the conditioned typed failure, which bounds the disagreement of the two evaluations averaged over the seed.
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).
For each seed and copy, the seeded low-degree test’s soundness extracts the measurements (exists_ext1, ext1_spec), with error \(\delta _{\mathrm{sim}}\) at the copy’s failure; in the Lean the restricted strategy is a projective strategy in the model, and the soundness is the model’s (Definition 8.65); \(\varepsilon \mapsto \varepsilon ^{b'}\) is concave, so the errors average over the seed to \(\delta _{\mathrm{sim}}\) at the average failure (sum_deltaSim_le, sum_deltaSim1_le).
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.
The simultaneous test at \((q,m',d,m'+6)\) extracts \(J\) per seed (exists_ext6, ext6_spec), in the model as for the single copies, and averaged as for them (sum_deltaSim6_le). The relations chain by the triangle inequality for disagreement: one player’s evaluated \(J\) against the other’s point of the sixth copy, that point against the other’s point of copy \(i\), and that against the other’s evaluated \(G_i\) (sum_dis_JAe_GBe_le, sum_dis_GAe_JBe_le).
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 )\).
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.
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)\).
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.
With \(\theta \leq 16^{54}\varepsilon \), the combined error is at most \(39204\cdot 16^{54}Z^{3A}\varepsilon ^{b'}+(Q+1)^{-2}+22Z^{3A}2^{-b'Q}\), \(Z=8(Q+1)m'\), \(A=\lceil a'\rceil \), over the large field. The parameters bound \(Z\) by a polynomial in \(Q\sigma \), and \(N^\mu \leq Q\leq N^{2\mu }\) for \(N=\lambda n\geq 2\), so \(24\sqrt{7\, \mathrm{err}}\) is at most \(\sigma ^a(N^{\mu a}\varepsilon ^{b'/2}+N^{-\mu b'/2})\) for a constant \(a\) depending only on the parameter polynomial, past a threshold on \(Q\geq n+1\).
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.
The output sampler is the detyping compiler’s sampler of the typed sampler, which is built from the input sampler and \((\lambda ,\mu ,\sigma )\) only; its program is a polynomial-time function of the input sampler’s program and \((\lambda ,\mu ,\sigma )\).
In the source model there is a polynomial-time Turing machine \(\mathsf{ComputeAnsRedVerifier}\) that on input \((\mathsf{V}, \lambda , \ell , \mu , \sigma )\), for \(\mathsf{V}\) an \(\ell \)-level normal form verifier whose decider is in standard timeout-counter form, 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}}\) whose decider is in standard timeout-counter form with \(B_{\mathcal{D}^{\mathsf{ar}}}(n)=\mathrm{poly}(\sigma ,(\lambda n)^\mu )\), 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 , \ell , \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 a universal constant \(C_{\mathrm{ar}}\), for all \(n \geq C_{\mathrm{ar}}\):
(Completeness) If \(\mathsf{V}_n\) has a value-\(1\) PCC strategy then \(\mathsf{V}^{\mathsf{ar}}_n\) has a value-\(1\) PCC strategy.
(Soundness) If \(\mathrm{val}^*(\mathsf{V}^{\mathsf{ar}}_n) {\gt} 1 - \varepsilon \) then \(\mathrm{val}^*(\mathsf{V}_n) \geq 1 - \delta (\varepsilon , n)\).
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.
Audit against the source (2026-09-23).
Oracularization’s first ambient contract was vacuous: a wrapper that keeps the input verifier satisfied every field (Remark 6.145). This one does not admit that witness, because its complexity clause does the work: an input whose decider runs in time \(2^{(\lambda n+1)^\mu }\) at degree \(\mu \), with answers of that length, must give an output within a polynomial in \((\lambda n+1)^\mu +\sigma +\lambda +n\) that rejects longer answers. A constant decider fails too: always accepting breaks soundness once \((\lambda n)^{-\mu b}\) is small, and always rejecting breaks completeness. Against the source’s thm:ar (ld_compiler.tex) the contract is a weakening at every point where it differs:
it drops the hypothesis that the input decider is in timeout-counter form, and assumes the time bound only semantically, through Verifier.Within, at the index in question; a construction clocks the input decider itself, as the typed oracularized decider does (Lemma 6.142);
its decider bound \(2^{(\lambda n+1)^\mu }\) exceeds the source’s \((2^{\lambda n})^\mu \), but its logarithm is still polynomial in \((\lambda n+1)^\mu \), which is all the PCP needs;
it allows \(b = 1\) and requires \(a \geq 1\), both choices of the prover;
it omits the Entanglement clause, which compression does not use;
\(\delta \) vanishes at \(\sigma = 0\), but no input satisfies \(\left\vert {\mathcal{D}} \right\vert \leq 0\), program encodings having positive size (MIPRE.Cost.esize_pos).
So the contract is neither trivially satisfiable nor, as far as this comparison shows, stronger than the source. The comparison does not replace the proof, which is the only check of the time bounds against the construction.
The ambient contract MIPRE.AnswerReduction 5 is inhabited.
By the answer-reduced verifier over the classical PCP decider. The three hypotheses the construction and its analysis ask of the decider hold for it: its field is the Shoup field, by definition; its parameters are polynomial in \((\log n,\log T,Q,\sigma )\), the padded dimension being so and the field degree polylogarithmic in \(Qm'\); and its field is eventually larger than every fixed power of \(8(Q+1)m'\) (Lemma 6.154). The complexity clause and the answer cut below the output bound are Lemma 6.179, completeness is Lemma 6.180 at the cut and hence at the bound, and soundness is Lemma 6.190 at the bound. Runtime and answer-cut normalization (Remark 6.31), the PCC bridge (Remark 2.8) and the typed oracle interface (Remark 6.145) are absorbed by the construction: the input’s time bound is used semantically, the output rejects answers beyond its cut, and the typed oracularized game is the one Lemma 6.189 plays.
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.
The decomposition above records the current repaired source [ 34 ] : common-field downsizing precedes the direct sum; conditioned test success includes equality and formats; the simultaneous measurement is projective on complete tuples; and decoding preserves the original timeout answer cutoff. These are open formalization obligations, not unresolved source claims. The source additionally tracks an entanglement factor \(1/2\) from doubling Schmidt rank during typed symmetrization. The value-only ambient contract does not include that clause. None of the new obligations is marked as proved merely because the source ledger validates it.
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 end to end) restores soundness \(\frac12\) with polynomially many repetitions, at polynomial cost in complexity and without anchoring; the anchored, entanglement-form theorem used in [ 1 ] ( [ 10 ] ) is not needed (Remark 5.11).
There are a universal constant \(c {\gt} 0\) and a polynomial-time Turing machine \(\mathsf{ComputeRepeatedVerifier}\) that on input \((\mathsf{V}, \ell , \lambda , \tau , \beta )\), for \(\mathsf{V}\) an \(\ell \)-level normal form verifier, outputs an \(\ell \)-level 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 answers of length at most \(B(n) = 2^{\beta (|\lambda | + |n|)}\), with \(|\cdot |\) the bit length — up to the encoding of answer tuples as strings, the decider parsing a self-delimiting \(k(n)\)-tuple, each coordinate against \(B(n)\), and rejecting malformed answers — with \(k(n) = 2^{\tau (|\lambda | + |n|)}\), \(\mathsf{TIME}_{\mathcal{S}^{\textsc{Rep}}}(n) = \mathrm{poly}\bigl(k(n), \mathsf{TIME}_\mathcal{S}(n)\bigr)\) and \(\mathsf{TIME}_{\mathcal{D}^{\textsc{Rep}}}(n) = \mathrm{poly}\bigl(k(n), B(n), \mathsf{TIME}_\mathcal{D}(n), \left\vert {\mathsf{V}} \right\vert \bigr)\), the sampler of \(\mathsf{V}^{\textsc{Rep}}\) depending only on \((\mathcal{S}, \lambda , \ell , \tau )\), and for all \(n\):
(Completeness) If \(\mathsf{V}_n\) has a value-\(1\) PCC strategy, then \(\mathsf{V}^{\textsc{Rep}}_n\) has a value-\(1\) PCC strategy.
(Soundness) For all \(0 {\lt} \varepsilon \leq 1\), if \(\mathrm{val}^*(\mathsf{V}_n) \leq 1 - \varepsilon \) then
\begin{equation*} \mathrm{val}^*(\mathsf{V}^{\textsc{Rep}}_n) \; \leq \; \exp \Bigl( - \frac{c\, \varepsilon ^{13}\, k(n)}{B(n) + 1} \Bigr)\; . \end{equation*}
The game \(\mathsf{V}^{\textsc{Rep}}_n\) is \(\mathsf{V}_n^{k(n)}\) at the truncated alphabet: 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 is a direct application of Theorem 5.6: the hypothesis is already a \(\mathrm{val}^*\) bound, so nothing has to be transported first. That theorem bounds \(\mathrm{val}^*(\mathsf{V}_n^{k(n)})\) by \(\exp \bigl( -c\, k(n)\, \varepsilon ^{13} / (\varepsilon + \log (\left\vert {\mathcal{A}} \right\vert \left\vert {\mathcal{B}} \right\vert )) \bigr)\), and the answer alphabets are the strings of length at most \(B(n)\), so \(\log (\left\vert {\mathcal{A}} \right\vert \left\vert {\mathcal{B}} \right\vert ) \leq 2(B(n) + 1)\) and the denominator is at most \(3(B(n) + 1)\), the factor absorbed into \(c\). The exponent \(13\) is the one of Theorem 5.6 itself, with no further loss: carrying the hypothesis in \(\mathrm{val}^*\) rather than \(\mathrm{val}^{s}\) removes both the transport’s polynomial loss and the factor \(\kappa ^{13}\) that its diagonal-weight hypothesis used to contribute. The conclusion is in \(\mathrm{val}^*\), as is the hypothesis: that is the form Definition 2.53 asks of the final game, and it is available at every step because nothing in the chain ever leaves \(\mathrm{val}^*\) (Remark 6.8). In [ 1 ] the answer length is the timeout bound \(B_\mathcal{D}(n)\) read off the decider and \(\tau \) is chosen against it; the ambient model has no timeout-counter form, so the parse length is the explicit parameter \(\beta \), and the choice of \(\tau \) against it is Lemma 6.202. The counts are powers of two rather than the paper’s \((\lambda n)^\tau \) because a program of the ambient model writes \(2^{\tau (|\lambda | + |n|)}\) down by a walk over the bits of \(\lambda \) and \(n\), where \((\lambda n)^\tau \) would need multiplication; \((\lambda n + 1)^\tau \leq 2^{\tau (|\lambda | + |n|)} \leq (\lambda n + 1)^{6\tau }\) for \(\lambda , n \geq 1\), so nothing downstream can tell the difference.
Lean statement.
The theorem is the structure MIPRE.Repetition, parametrized by \(\ell \): the repeated sampler as a function of the input sampler and \((\lambda , \tau )\) with its program computable in polynomial time, the repeated decider’s program as a polynomial-time function of the input programs and \((\lambda , \tau , \beta )\), the packaging as an \(\ell \)-level normal form verifier, the complexity clause in the vocabulary of budgets (Verifier.Within) at a degree affine in the input’s — the repeated decider runs the input decider through the universal machine, whose overhead is polynomial — and the two value clauses at the answer bounds stated, with \(\lambda n + 1\) in place of \(\lambda n\) so that every quantity is meaningful at every index. An earlier statement of this theorem coupled the answer length to a hypothesis \(\mathsf{TIME}_\mathcal{D}(n) \leq (\lambda n)^\tau \) and took \(k(n) = (\lambda n)^{(1 + c')\tau }\) for a constant \(c'\) depending on a parameter \(\kappa \) left over from the transport through \(\mathrm{val}^{s}\); writing the consumer showed that the repetition count and the answer length have to be independent parameters, and the constant \(c'\) is now the choice of \(\tau \) in Lemma 6.202. It is inhabited by MIPRE.repetition (MIPRE/Background/Repetition/Verifier.lean): the repeated sampler runs \(k(n)\) copies of \(\mathcal{S}\) through the universal machine, its CL functions the direct sums of the input’s (MIPRE.Repeat.repSampler); the repeated decider sanitizes its input, parses the two answers as self-delimiting tuples and runs \(\mathcal{D}\) on every coordinate (MIPRE.Repeat.repDecider); both are the s-m-n construction on a fixed core, so their programs are polynomial-time functions of the inputs. The game of the output at index \(n\) is the direct repetition of \(\mathsf{V}_n\) up to a relabeling of the questions into blocks and the embedding of encoded answer tuples (valStar_repVerifier, by quantumValue_extendAnswers); completeness is the tensor power carried across that relabeling, soundness is Theorem 5.6 on the repeated game, and the complexity clause is the explicit running-time accounting of the two programs (repSampler_timeBound, repDecider_timeBound), each dominated by \(c (W + 1)^m (|d| + 1)^{e (k + 1)}\) for constants produced by the accounting itself, \(W\) the argument of the polynomial.
6.6 The compression theorem
The three exterior stages are introspection, full answer reduction (with its typed oracle step), and repetition. Their ambient contracts yield gap-preserving compression, 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.207).
Assume \(I : \texttt{MIPRE.Introspection 7}\) and \(A : \texttt{MIPRE.AnswerReduction 5}\), the contracts of Definitions 6.130 and 6.193. Using the supplied repetition construction of Theorem 6.196, there is a universal constant \(C_0 {\gt} 0\) and a polynomial-time procedure \(\mathsf{Compress}\) that on input \((\mathsf{V}, \lambda )\) outputs a \(7\)-level normal form verifier \(\mathsf{V}^{\textsc{Compr}}= (\mathcal{S}^{\textsc{Compr}}, \mathcal{D}^{\textsc{Compr}})\) with runtime coefficients bounded by \(\mathrm{poly}(n,\lambda )\) at a fixed input-size degree, 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 \(7\)-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}^*(\mathsf{V}_N) \leq \tfrac 12\) then \(\mathrm{val}^*(\mathsf{V}^{\textsc{Compr}}_n) \leq \tfrac 12\): the class “\(\mathrm{val}^*\leq \tfrac 12\)” is preserved, in the same value at both ends.
Let \(\mathsf{ComputeIntroVerifier}\) and \(\mathsf{ComputeAnsRedVerifier}\) denote the procedures provided by \(I\) and \(A\), respectively. These are assumed ambient procedures in this proof. \(\mathsf{Compress}(\mathsf{V}, \lambda )\) is \(\mathsf{ComputeIntroVerifier}(\mathsf{V}, \lambda , 7)\), then \(\mathsf{ComputeAnsRedVerifier}(\cdot , \lambda , \mu , \sigma (\lambda ))\), then \(\mathsf{ComputeRepeatedVerifier}(\cdot , 7, \lambda , \tau , \beta )\), with \(\mu \) from Lemma 6.201, \(\sigma (\lambda )\) a polynomial in \(\lambda \) dominating \(C_{\mathrm{intro}} (\lambda + 1)^{C_{\mathrm{intro}}}\), \(\beta \) an exponent with \(\mathrm{poly}\bigl((\lambda n + 1)^\mu + \sigma (\lambda )\bigr) \leq (\lambda n + 1)^\beta \), and \(\tau \) from Lemma 6.202; \(C_0\) dominates \(2\), \(C_{\mathrm{ar}}\), the introspection and answer-reduction margin thresholds, the threshold for the lower bound on \(\varepsilon _2\), and \(\tau \), as recorded in Pipeline/Compress.lean. The complexity clauses chain the three complexity clauses through the budgets: every bound is a monotone polynomial expression in \(n\), \(\lambda \), \(\sigma (\lambda )\) and the sizes of the programs along the chain, hence at most a polynomial in \(n + \lambda \). The value clauses are Remark 6.203. In Lean this is MIPRE.GapCompression.ofPipeline: an Introspection 7, an AnswerReduction 5 and a Repetition 7 give a GapCompression. \(\sigma (\lambda )\) is computed by iterating the program of \(\lambda (n)\) of Lemma 6.210, there being no polynomial-time arithmetic in the toolkit for the paper’s \(\lceil C_{\mathrm{intro}} \lambda ^{C_{\mathrm{intro}}} \rceil \), which only has to be dominated; it also dominates the size of the introspective sampler, which the complexity clause of Definition 6.193 bounds by \(\sigma \). Oracularization is not a stage: it is the first step of the proof of Theorem 6.192.
The assumed ambient introspection contract outputs a \(5\)-level verifier, and the answer-reduction contract takes \(\ell \) to \(\max \{ \ell +2,5\} \), here \(7\); these match the exterior levels of the source constructions. Then direct repetition preserves it (Theorem 6.196); so \(\mathsf{Compress}\) outputs a \(7\)-level verifier on every input, and \(7\) is consequently the level at which the recursion closes. A verifier of fewer levels is presented at that level by padding its decomposition with trivial factors, which an \(\ell \)-level conditionally linear function (Definition 6.1) admits. In [ 1 ] the count is \(9\), anchored repetition adding two levels (Remark 5.11).
The output contract.
The conditional theorem constructs a MIPRE.GapCompression: a record of the constant \(C_0\); the compressed sampler \(\lambda \mapsto \mathcal{S}^{\textsc{Compr}}_\lambda \), a valid \(7\)-level sampler for every \(\lambda \), with a polynomial-time program computing its description from the binary representation of \(\lambda \) (Lemma 6.200); the polynomial-time map \(\mathsf{Compress}\) from pairs of programs and \(\lambda \) to the program of the compressed decider; the packaging of every output, well-formed input or not, as a \(7\)-level normal form verifier with that sampler and that decider; the bound \(\mathrm{poly}(n, \lambda )\) on the running times of the output at index \(n\), at the degree deg in the size of the input that Definition 2.45 carries, the same bound on the dimension of the compressed sampler (in the paper a consequence of its running time) and on the length of the answers the compressed decider can accept (output_rejects_long: the paper’s repeated decider accepts only after fully parsing the answers, so an answer longer than its time bound forces a timeout, the property the amended proof of Lemma 6.211 relies on; in the ambient model, where running times scale with the input, it is a demand on the construction, an explicit length check); and the completeness and soundness clauses for \(\lambda \)-bounded \(7\)-level inputs at \(n \geq C_0\). The checked pipeline constructs an instance from the stated transformation hypotheses; it does not inhabit introspection or answer reduction, nor discharge their source-model adaptations. The halting reduction consumes an instance (Remark 6.204). Two readings are fixed there. \(\mathsf{V}_N\) is taken with answers of length at most \(N^\lambda \), the explicitly chosen input answer cut (also the ambient runtime coefficient), and \(\mathsf{V}^{\textsc{Compr}}_n\) with answers of length at most the stated running-time bound — beyond which its decider rejects, so that its value is the same with any larger alphabet (Verifier.valStar_eq_of_rejects) — since the exact running times of Definition 2.46 are not functions of the verifier in the formalization. And “a value-\(1\) PCC strategy” is a PCC synchronous strategy of value \(1\) for the game on the doubled question set (Verifier.HasPerfectPCC, on Verifier.doubledGame: Alice’s questions tagged \(0\), Bob’s tagged \(1\), every other pair of weight zero and rejected), which is a synchronous game for every verifier, so nothing is presupposed of the decider. An earlier reading took \(\mathsf{V}^{\textsc{Compr}}_n\) itself as the synchronous game, which asks its decider to reject unequal answers to equal questions — a property of the decider that the paper never states, synchronous there being a property of strategies, and one the paper’s completeness clause does not supply. The doubled game is the precise ambient completeness interface. The source’s identical operators and support commutation do not by themselves put its state in the ambient normalized tracial representation. Applying source completeness requires the ambient-to-source direction of Remark 2.8 for its input and the source-to-ambient direction for its output; those are supply obligations, not definitional identifications.
The type MIPRE.GapCompression is inhabited.
Comments.
MIPRE/Background/Pipeline.lean. It is the first time the assembly is instantiated with the actual stage instances rather than hypotheses, so it is a check from the supply side that ofPipeline composes with them as they are. An inhabitant of MIPRE.AnswerReduction 5 closes the sorry of HaltingGameValue.halting_reduces_to_gameValue in one line.
The three exterior stages are chained through a parameter budget: each stage’s soundness clause is applied contrapositively, and each application needs a strict margin between the loss it suffers and the gap it is handed. Those margins are arithmetic facts about the imported constants, isolated here as Lemma 6.201 and Lemma 6.202. The provenance notes name the corresponding nodes of the companion repository’s ledger (vidick/mipre-proof); see planning/ledger-informed-plan.md.
For all inputs \((\mathsf{V}, \lambda )\) — \(\lambda \)-bounded or not, well-formed or not — the sampler \(\mathcal{S}^{\textsc{Compr}}\) of \(\mathsf{Compress}(\mathsf{V}, \lambda )\) depends only on \(\lambda \), and there is a Turing machine \(\mathtt{ComputeSampler}\) that outputs its description from \(\lambda \) in time \(\mathrm{polylog}(\lambda )\).
Chain the verifier-independence of the sampler through the three stages: introspection’s sampler depends only on \((\lambda , \ell )\), answer reduction’s only on its input sampler and the parameters, and repetition’s only on its input sampler and \((\lambda , \ell , \tau )\). \(\mathtt{ComputeSampler}\) is then realized by running \(\mathsf{Compress}\) on the trivial verifier. It is this lemma that makes the recursion of Section 6.7 possible at all: a fixed point has to quote its own sampler, so the sampler must not depend on what is being compressed. In Lean the lemma is built into the statement of Theorem 6.197: the fields sampler and samplerProg of MIPRE.GapCompression are the map \(\lambda \mapsto \mathcal{S}^{\textsc{Compr}}_\lambda \) and its polynomial-time description, and output_sampler says that every output carries it. The chaining is MIPRE.Pipeline.sampler, the composite of the three sampler maps, with samplerProg_eq its polynomial-time description and output_sampler the claim for every input.
[\(\bullet \bullet \) medium]
Given the ambient contracts of Definitions 6.130 and 6.193, write \((a_1,b_1)\) and \((a_2,b_2)\) for their respective soundness constants, with \(a_1,a_2\geq 1\), and \(x = \lambda n\). Put \(\varepsilon _1 = \bigl( 8 a_1 x^{a_1} \bigr)^{-1/b_1}\).
\(\delta _1(\varepsilon _1, n) {\lt} \frac12\) for all \(x \geq (4 a_1)^{1/b_1}\).
For every \(K\) and \(C\) there are a universal \(\mu \geq C\) and a threshold \(N\) such that, for all \(x \geq N\) and all \(1 \leq \sigma \leq x^K\),
\begin{equation*} \sigma ^{a_2} x^{-b_2 \mu } \; {\lt}\; \frac{\varepsilon _1}{2}\; ; \end{equation*}and then, with \(\varepsilon _2 = \bigl( \varepsilon _1 / (3 \sigma ^{a_2} x^{\mu a_2}) \bigr)^{1/b_2}\), \(\delta _2(\varepsilon _2, n) {\lt} \varepsilon _1\).
The first term of \(\delta _1(\varepsilon _1, n)\) is exactly \(\frac18\) and the second is at most \(\frac14\) once \(x^{b_1} \geq 4 a_1\). For the second item take \(\mu \) with \(\mu b_2 \geq K a_2 + a_1 / b_1 + 1\): then \(\sigma ^{a_2} x^{-b_2 \mu } \leq x^{-a_1/b_1 - 1}\), which is below \(\varepsilon _1 / 2 = (8 a_1)^{-1/b_1} x^{-a_1/b_1} / 2\) as soon as \(x {\gt} 2 (8 a_1)^{1/b_1}\); and the first term of \(\delta _2(\varepsilon _2, n)\) is exactly \(\varepsilon _1 / 3\). The paper fixes \(\sigma = \lceil C_{\mathrm{intro}} \lambda ^{C_{\mathrm{intro}}} \rceil \) and \(\mu = \lceil \max \{ C_{\mathrm{intro}}, (9 a_1 + 2 a_2 C_{\mathrm{intro}}) / (b_1 b_2) \} \rceil \) and has the bound for all \(n \geq 2\); the formalization takes \(\sigma \) any polynomial in \(\lambda \) dominating \(C_{\mathrm{intro}} (\lambda + 1)^{C_{\mathrm{intro}}}\) and the size of the introspective sampler, hence \(\sigma \leq x^K\) for a universal \(K\), and a threshold on \(n\) that \(C_0\) absorbs.
[\(\bullet \) easy]
With \(\varepsilon _2\) as in Lemma 6.201, \(1 / \varepsilon _2 \leq x^P\) for a universal \(P\) and all \(x\) past a threshold. Consequently, for every \(c {\gt} 0\) and every \(\beta \) there is a universal integer \(\tau \) such that, with \(z = \lambda n + 1\), for every \(k \geq z^\tau \) and every \(0 \leq B \leq z^\beta \), the repetition bound \(\exp \bigl( -c\, \varepsilon ^{13} k / (B + 1) \bigr)\) of Theorem 6.196 is at most \(\frac12\) for all \(n \geq \tau \), all integers \(\lambda \geq 1\) and all \(\varepsilon \geq z^{-P}\); the counts \(k(n) \geq z^\tau \) and \(B(n) \leq z^{6\beta }\) of that theorem qualify.
\(1 / \varepsilon _2 = \bigl( 3 \sigma ^{a_2} x^{\mu a_2} (8 a_1)^{1/b_1} x^{a_1/b_1} \bigr)^{1/b_2}\), and each factor is a power of \(x\) once \(x \geq \max \{ 3, 8 a_1\} \) and \(\sigma \leq x^K\). Then \(c\, \varepsilon ^{13} z^\tau / (z^\beta + 1) \geq \frac{c}{2} z^{\tau - 13 P - \beta } \geq \frac{c}{2} z \geq \log 2\) for \(\tau \geq 13 P + \beta + 1 + 2/c\) and \(z \geq \tau \). Purely arithmetic, and computationally testable — the companion repository tests it.
[\(\bullet \) easy]
The soundness clause of Theorem 6.197 is obtained by applying each transformation’s soundness clause contrapositively, with a margin at every step. From \(\mathrm{val}^*(\mathsf{V}_N) \leq \frac12\) and \(\delta _1(\varepsilon _1, n) {\lt} \frac12\): were \(\mathrm{val}^*(\mathsf{V}^{(1)}_n) {\gt} 1 - \varepsilon _1\), the assumed ambient introspection contract would give \(\mathrm{val}^*(\mathsf{V}_N) \geq 1 - \delta _1 {\gt} \frac12\), so \(\mathrm{val}^*(\mathsf{V}^{(1)}_n) \leq 1 - \varepsilon _1\). The same step through the assumed ambient answer-reduction contract, using \(\delta _2(\varepsilon _2, n) {\lt} \varepsilon _1\) (Lemma 6.201), gives \(\mathrm{val}^*(\mathsf{V}^{(2)}_n) \leq 1 - \varepsilon _2\); and Theorem 6.196 with Lemma 6.202 brings that below \(\frac12\). Oracularization is internal to the proposed source proof of answer reduction; it is not a separate premise of this conditional value chain.
Every step of that chain is an implication between \(\mathrm{val}^*\) bounds, which is worth recording because the route of [ 1 ] cannot take it. There the repetition step’s soundness hypothesis is an entanglement bound, and \(\mathrm{Ent}(\mathfrak {G}, 1 - \varepsilon ) = \infty \) needs \(\mathrm{val}^*(\mathfrak {G}) {\lt} 1 - \varepsilon \) strictly — a non-strict \(\leq \) leaves the value possibly attained and the entanglement requirement finite. So the paper runs the whole chain in \(\mathrm{Ent}\), starting it at the threshold \(1 - \delta _1\) rather than at \(\frac12\); the value-form route would force it to apply repetition at \(\varepsilon _2/2\) instead of \(\varepsilon _2\), at a cost of \(2^{17}\) in the exponent of its repetition parameter. Direct repetition (Theorem 5.6) takes a value hypothesis and so needs no strictness and pays no such factor: this is the second place, after Remark 5.11, where the value-form pipeline is cheaper than the entanglement-form one rather than merely equivalent to it. It is also why no entanglement lower bound has to be tracked anywhere in this chapter.
Theorem 6.197 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}^*\leq \frac12\), with the trivially accepting and the trivially rejecting game as the distinguished elements; the complement of \(B\) is semidecided by enumerating tensor-product strategies, the \(\mathrm{val}^*\) half of Lemma 3.112; and a description \((\mathcal{S}, \mathcal{D}, n)\) with \(n\) in binary is a succinct description of the game \(\mathsf{V}_{2^n}\) played by a \(\lambda \)-bounded verifier. Completeness of compression is the preservation of \(A\); preservation of \(B\) is the soundness clause of Theorem 6.197 verbatim, hypothesis and conclusion being in the same value. Taking \(B\) in \(\mathrm{val}^*\) throughout is what keeps Theorem 3.3 out of the pipeline altogether: the source transformations and direct repetition already use that value (Remark 6.8). It is also the form in which the semidecision procedure is available, the rounding argument for the \(\mathrm{val}^{s}\) half not being the same one. Making this dictionary precise is a formalization task of this section. The four obligations recorded here from the referee report (R1) — the universe of the criterion’s strings, compression from a succinct input, preservation on inputs that are not \(\lambda \)-bounded descriptions, and the choice of \(\lambda \) along the recursion — are settled as follows, against the per-level form of the lemma (compressibility_criterion_levels, Lemma 4.11), whose classes \(A_n, B_n\) are indexed by the level of the recursion.
Strings are descriptions, never games. If they were games, \(\textsc{Compr}\) could not be polynomial-time, a game of \(\mathsf{V}_{2^n}\) having \(2^{\mathrm{poly}(n, \lambda )}\) questions. A string is a pair \((\lambda , \mathcal{D})\) of a parameter and a decider program, read as the verifier \((\mathcal{S}^{\textsc{Compr}}_\lambda , \mathcal{D})\) with the compressed sampler of Lemma 6.200, the length check of Definition 2.46 being enforced by a wrapper around \(\mathcal{D}\); so every string names a normal form verifier, and the interpretation sits outside every time bound. In Lean the decider component is the datum the string carries, run by the universal machine (Verifier.ofSamplerDeciderD): a datum that is not the encoding of any program still names a verifier, whatever the interpreter does with it, and on the encoding of a program the reading is the program’s own run (Decider.wrap_accepts_prog). Decoding the datum to a program with a fallback, the earlier reading, would have obliged the compressor’s decider of item 2 to reimplement the decoder — a tree-grammar check — in the ambient model, to reproduce a fallback nobody wanted. \(A_n\) is the set of strings whose verifier is \(n\)-bounded and whose \(n\)-th game has a value-\(1\) PCC strategy and whose decider rejects every answer longer than the answer bound at index \(n\); \(B_n\) the set of those that are \(n\)-bounded, reject long answers, and have \(\mathrm{val}^*\leq \frac12\) at index \(n\) (Verifier.InClassA, InClassB, the rejection clause being Verifier.RejectsLong; disjoint, since a perfect PCC strategy gives \(\mathrm{val}^*= 1\)). The rejection clause is Step 6 of the paper’s decider \(F\) — an explicit length check before \(\mathcal{D}^{\textsc{Compr}}\) is run, which the amended proof of Lemma 6.211 spends to identify the answer alphabets of \(\mathsf{V}^{\mathsf{halt}}_n\) and \(\mathsf{V}^{\textsc{Compr}}_n\) — made a condition on membership: the soundness direction of the compressor’s obligation raises the answer bound from the one a class is read with to the one Theorem 6.197 takes its hypothesis at, and only a decider that rejects beyond the former keeps the value fixed under that (Verifier.valStar_eq_of_rejects; enlarging the bound can otherwise only raise the value). Only the length check has to go into the wrapper: the answer-length bound is a condition on membership in these classes, not on well-formedness, synchronicity is asked of no decider at all (the value-\(1\) PCC strategy lives on the doubled game), and the paper’s timeout counter is not needed either — a decider that fails to halt simply fails to be \(n\)-bounded, and its string then lies in neither class. Tying the bound \(\lambda = n\) to the level is what replaces the choice of \(\lambda \) along the recursion (Lemma 6.210): the levels \(r(e) = 2^{K + 1 + \left\vert {e} \right\vert }\) at which the recursion runs are exponential in \(\left\vert {e} \right\vert \), above every polynomial in \(\left\vert {e} \right\vert \) that the paper’s \(\lambda \) has to dominate.
Compression from a succinct input. The compressor cannot read the string it is handed: its time is polynomial in the length of \((\hat x, n)\), hence polylogarithmic in \(n\), and a single bit query to \(\hat x\) costs up to \(n\). On \((\hat x, n)\) it therefore outputs the string \((\lambda (n), \mathcal{D}_{\hat x})\), where \(\lambda (n) = \mathrm{poly}(n)\) is a fixed formula and \(\mathcal{D}_{\hat x}\) is the decider that, at its own index \(N\), reads \(x = (\lambda ', \mathcal{D}')\) from \(\hat x\) by bit queries (at most \(2n + O(1)\) of them, rejecting otherwise), forms the verifier \(\mathsf{V}'\) of \(x\) frozen at index \(2n + 1\) (Verifier.freeze: a program that replaces the index in its input by the frozen one, so that its sampler and decider answer at every index as \(\mathsf{V}'\) does at index \(2n + 1\), and its game at index \(2^n\) is the game of \(x\) at level \(2n + 1\) — freeze_valStar, freeze_hasPerfectPCC, with \(\lambda \)-boundedness transferred by freeze_isBounded; the answer-length bound is immaterial above the length the decider rejects, Verifier.valStar_eq_of_rejects, hasPerfectPCC_of_le) — runs \(\mathsf{Compress}(\mathsf{V}', \lambda (n))\), and finally the compressed decider at index \(N\). The freezing reconciles the recursion’s levels \(n \to 2n + 1\) with the compression theorem’s \(n \leftarrow 2^n\), at the cost of a logarithmic factor in \(\lambda (n)\). Theorem 6.197 at index \(n \geq C_0\) then transfers the class of \(x\) at level \(2n + 1\) to the class of the output at level \(n\), and the output is \(n\)-bounded for \(n\) above a universal threshold: its size is \(\left\vert {\hat x} \right\vert + O(\log n) \leq n\) by the slack \(2\left\vert {\hat x} \right\vert \leq n\) of the lemma, and its time at index \(N\) is \(\mathrm{poly}(N, n) \leq N^n\). In Lean that transfer is done once, against a specification of the output written before its construction — MIPRE.Halting.CompressorSpec: the parameter \(\lambda (n)\) the output carries, the agreement of its decider at every index with the compressed decider of the frozen verifier, its \(n\)-boundedness, the growth of \(\lambda (n)\) that freeze_isBounded consumes, and the answer-budget comparison of exists_ansBound_le — and CompressorSpec.toObligations is the class transfer, in both directions, from those fields alone. What the construction owes is exactly the fields of that structure. The program half is done: MIPRE.Halting.haltProg is the decider of the output — it reads \(x\) from its succinct description by bit queries (Cost.Prog.readProg), rebuilds the description of the wrapped decider of \(x\) and freezes it at \(2n + 1\) in the ambient model, runs \(\mathsf{Compress}\), and runs the result on its own input through the universal machine (prepProg, prepProg_runs) —, the output string comprStr is \(\lambda (n)\) together with that decider with \((c, n, \lambda (n))\) hardcoded, and comprStr_accepts is the field accepts_compr verbatim, from the forward runs and the inversion haltProg_accepts_iff. The accounting is done too, with \(\lambda (n) = 2^{2 \log n}\) (Lemma 6.210: isBounded_comprStr, lamOf_ge, ansBound_le_lamOf), the compressor is a polynomial-time function (comprPoly), and exists_obligations inhabits the structure: obligation (d) is discharged.
Junk inputs. Nothing is demanded of the compressor off strings in \(A_{2n+1} \cup B_{2n+1}\), every string names a verifier, and \(\lambda \)-boundedness is decided nowhere. What the lemma does demand is that the complement of \(B_n\) be semidecidable: “not \(n\)-bounded” is witnessed by an index and an input on which a time bound fails — a search, so \(\Sigma _1\), and this is Lemma 6.205 —, “accepts some answer longer than the bound” is witnessed by the tuple and a run, a search again (Verifier.rePred_not_rejectsLong), and “\(\mathrm{val}^*{\gt} \frac12\) at index \(n\)” is the \(\mathrm{val}^*\) half of Lemma 3.112 applied to the tabulated game, which is computable from an \(n\)-bounded verifier. No disjunct decides \(n\)-boundedness, which is \(\Pi _1\); the point of taking the disjunction is that it does not have to (Verifier.not_inClassB_iff), and Lemma 6.206 is the three merged. Two things about the search for a violated bound. The budget it tests against is a cost and not a number of machine steps, and a step is not a unit of cost, so Machine.runForD below does not decide it and Lemma 4.14 is what does. And the index at which a bound fails ranges over all of \(\mathbb {N}\), while the bound reads its input with the index encoded in binary; carrying the index as a datum, read back by Data.natOf, is what makes the encoding primitive recursive in the search witness and so keeps the enumeration from needing the primitive recursiveness of \(n \mapsto \mathrm{encode}(n)\), which the development did not have when that enumeration was written — it is now MIPRE.Cost.Data.primrec_encode_nat, written for the tabulation of item 3 and load-bearing under it. The clause “computable from an \(n\)-bounded verifier” is load-bearing and not a convenience: acceptance by a decider is \(\Sigma _1\), so a tabulation correct at every string would decide the halting problem — take two strings whose deciders differ only in how long they run before accepting. Boundedness is what makes acceptance decidable, by supplying a budget within which the decider must halt, and one budgeted run then settles it (Verifier.accepts_iff_runForD, on Machine.runForD: iterate the evaluation machine’s step function \(3k\) times and read off the result if the configuration reached is final, which is enough because a derivation of cost \(t\) is a run of at most \(3t\) steps and final configurations are fixed). Every Lean statement about the tabulation’s acceptance carries that hypothesis for this reason — the two sampler runs are budgeted otherwise and carry none, as the paragraph after this enumerate records — and it does one more thing than supply the budget: the time clauses of \(\lambda \)-boundedness are guarded by \(2 \leq n\), so at \(n = 0, 1\) no budget exists at all, and what excludes those two indices is the size clause — every program encodes to a non-empty datum, so \(2 \leq \left\vert {\mathcal{D}} \right\vert \leq \left\vert {\mathsf{V}} \right\vert \leq \lambda \) (Verifier.IsBounded.two_le, on Cost.Prog.two_le_esize). Each statement carried a second hypothesis until the doubling, and why it did is worth naming: a game description denotes a synchronous game by construction — Definition 2.43 rejects unequal answers to equal questions — whereas \(\mathsf{V}_n\) does no such thing, so no description can match a verifier that is not synchronous at \(n\), and \(B_n\) does not ask that it be. What is tabulated is therefore not the game of \(\mathsf{V}_n\) but its doubled one (MIPRE.Game.doubled, Verifier.doubledGame): the questions are \(\{ 0,1\} \times \mathcal{X}\), Alice is asked a question tagged \(0\) and Bob one tagged \(1\), and every other pair — the diagonal included — carries no weight and is rejected outright. Two things follow, and both are what make the repair cheap. The diagonal carries no weight, so the description’s veto is implied by the distribution rather than imposed on the verifier, and the doubled game is synchronous whatever \(\mathsf{V}_n\) is; and since the decision predicate rejects off the tag block as well, a description matches the doubled game totally, at every question pair and not merely on the support, so quantumValue_eq_of_equiv and SyncStrategy.isPCC_relabel apply unchanged and no support-restricted version of either is needed. Neither value moves: \(\mathrm{val}^*\) is unchanged because a strategy for the doubled game restricts to Alice’s \(0\)-tagged and Bob’s \(1\)-tagged measurements while one for the original ignores the tag (quantumValue_doubled), and a value-\(1\) PCC strategy doubles to one (SyncStrategy.double, isPCC_double), the doubled support mapping into the original so that no commutation obligation is added. The match (MIPRE.Halting.tab_match) is therefore asked of every \(n\)-bounded verifier, synchronous or not, which is what Lemma 6.206 needs and what \(B_n\) was never going to supply; and the separate soundness clause that used to stand beside it — that the description does not overshoot, forcing the diagonal tuples to reject being a lowering of the value — is deleted, the soundness branch of Theorem 6.214 taking the equality of values instead. The tabulation itself is read with the answer alphabet enumerated by Verifier.answerEquiv and the doubled question alphabet by Verifier.tagEquiv, a tag bit prepended to the point’s bit string, and a description matching the doubled game along those indexings has the value of \(\mathsf{V}_n\) (quantumValue_toGame_eq_valStar_doubled), which is what carries the verdict of a procedure that runs on game descriptions back to the verifier. The same transport in \(\mathrm{val}^{s}\) is Verifier.syncValue_syncGame_eq_one_doubled, which is what item 1 of Theorem 6.214 needs; see the end of this remark.
The choice of \(\lambda \). Absorbed into item 1.
Of this dictionary the per-level lemma, the Lean statement of Theorem 6.197 as a hypothesis (MIPRE.GapCompression) and the value bookkeeping are in Lean: the quantum value is invariant under relabelings of the alphabets (quantumValue_eq_of_equiv, the tool for the tabulation) and under always-rejected extra answers (quantumValue_extendAnswers, by zero extension one way and merging of outcomes the other). The synchronous value transports the same way (syncValue_eq_of_equiv, from SyncStrategy.relabel, which preserves both the value and the commutation condition — value_relabel, isPCC_relabel), so a value-\(1\) PCC strategy of \(\mathsf{V}_n\) reaches the tabulation (Verifier.exists_perfectPCC_syncGame); and the two vocabularies for the synchronous value are identified, MIPRE.syncValue of a description read in the foundations being HaltingGameValue.gameValue of the same description (GameData.gameValue_eq_syncValue, by repackaging strategies in both directions, toSyncStrategy and ofSyncStrategy). For the games of a verifier the deciders’ acceptance at an index determines \(\mathrm{val}^*\) and the perfect PCC strategies (Verifier.valStar_congr, hasPerfectPCC_congr), which survive answer padding and give \(\mathrm{val}^*= 1\) (valStar_eq_one_of_hasPerfectPCC). The frozen verifier of item 2 is in Lean with its value, PCC and \(\lambda \)-boundedness transfer (Verifier.freeze), and so is the ambient toolkit its decider is built from: a description travels as a bit string through the postorder serialization Data.toBitsPost, read back by the stack machine Data.parse (postorder rather than preorder because a stack machine is a loop of the ambient model, while a recursive-descent reader is not), with the reading and writing programs Prog.parseProg, Prog.serProg; every string names a parameter through the normalization Data.natOf, so no validity condition on strings is needed; and the format checks and budgets are the bounded walks Prog.bitWalkProg, eqBitsProg and the arithmetic incProg, toUnaryProg, mulProg, polyProg, each with a cost bound of the shape \(T \cdot (\left\vert {\text{input}} \right\vert + 1)\) that Definition 2.45 asks for. Costs compose through Cost.PolyBounded, which also gives the threshold above which a polynomial bound falls under \(2^n\). The dictionary itself is now in Lean: MIPRE.Halting.descLam and descDecD read a string as a parameter and a decider, Vof is the verifier it denotes, and classA, classB are \(A_n, B_n\), with answers cut at the length beyond which a compressed decider with that parameter rejects. What remains is collected as the fields of MIPRE.Halting.Obligations, the structure Theorem 6.214 is proved from (planning/formalization-plan.md, H4; planning/h4-assembly.md): the two distinguished strings, the semidecider, and the compressor. The tabulation was a fourth group of fields and is one no longer — it is proved below, and halting_reduction uses those theorems directly. The reading of a string as a verifier is in Lean too: Decider.wrap is the wrapper — it computes \(s(N)\) by running the sampler through the universal machine, compares it with the lengths of the two questions, and runs the string’s own decider through the universal machine if both agree — and Verifier.ofSamplerDecider is the normal form verifier a pair denotes, with ofSamplerDecider_accepts saying that it accepts exactly when the questions have the sampler’s dimension and the string’s decider accepts. The two distinguished strings of the criterion are covered at the level of verifiers by hasPerfectPCC_of_accepts_diagonal (a decider that is synchronous at \(n\) and accepts one fixed answer on every question pair has a value-\(1\) PCC strategy: the paper’s trivial strategy) and valStar_eq_zero_of_rejects_all, and both are now realized by strings: MIPRE.Halting.yYes and yNo are the descriptions \((0, \mathcal{D})\) whose deciders are the program nil, which returns nil and so accepts nothing, and a six-node program returning encode true exactly on the empty answer from both players. Their \(\lambda \)-boundedness is Verifier.ofSamplerDecider_isBounded, and behind it the wrapper’s time accounting (Halting/WrapperCost.lean), proved on arbitrary data throughout since Definition 2.45 quantifies over every input at the index and no stage may assume it is handed a question pair: the length program on any datum, one length check comparing Data.spine with \(s(n)\), the head whose cost depends on the index alone, and the three outcomes of the whole. That is also the first inhabitant of \(\lambda \)-boundedness anywhere in the development — every earlier proof of it was conditional on another time bound — so Definition 2.49, twice repaired, is now known to be satisfiable. The computation of the tabulation — running the sampler on every point of \(\mathbb {F}_2^{s(n)}\) to count the question weights, and the decider under its budget to fill in the acceptance table — is in Lean too, and with it the whole of that obligation: MIPRE.Halting.tab is the \(n\)-th game of the verifier a string denotes, tab_computable its computability in the string and the level, tab_match the match of item 3 above — against the doubled game of \(\mathsf{V}_n\), with \(n\)-boundedness its only hypothesis — tab_value the equality of values read off it, and gameValue_tab_eq_one the completeness branch in the vocabulary of HaltingGameValue. Three features of the construction are worth recording, because that is where the work went. A computability proof may not mention a verifier: a verifier is a structure carrying proofs while Primrec quantifies over data, so the tabulation is written twice — Halting.tabOf takes seven arguments that are plain data and no verifier (the two encoded programs, the sampler’s dimension at the level, the answer cut, the budget the two sampler runs are given and its exponent, and the level), with dimOf, margOf and accOf running the two programs under the budgets CL.Sampler.queryUnder and Decider.acceptBudget, each defaulting when its budget is missed; tab is tabOf fed what the string supplies; and dimOf_eq, margOf_eq, accOf_iff are the bridge back, saying that those runs deliver the verifier’s own sampler and decider, so that the default is never taken. Which budget the sampler runs are given is not a detail: they used to read it off \(n\)-boundedness, and they now take it as a parameter and are fed the one Theorem 6.197 supplies at every parameter and every index (Halting.sampler_timeBound, from GapCompression.sampler_time), so that dimOf_eq and margOf_eq carry no hypothesis at all. They have to: a computable presentation (Lemma 6.205) asks for the sampler’s dimension at every string and level, \(n = 0\) and \(n = 1\) included, which the budget \(n^n(\left\vert {q} \right\vert + 1)^n\) of \(n\)-boundedness cannot reach — the time clauses being guarded by \(2 \leq n\), as item 3 says. So the family Vof is computably presented outright (Halting.computablyPresented_Vof), and the hypothesis Lemma 6.205 leaves to its user is discharged once. accOf cannot follow and provably must not: the decider of the verifier a string denotes is the string’s own, wrapped, and nothing bounds it unconditionally, so accOf_iff — and with it tab_match and tab_value — keeps \(n\)-boundedness, for the reason item 3 gives. The programs have to be got into data: the compressed sampler’s program is delivered by a polynomial-time function of \(\lambda \), which is not a Mathlib-computable function of its argument in any direct sense, and what carries it is that the tabulation runs that function on an encoded input (Cost.PolyTimeFun.computable_encode_comp); the decider is the wrapper around the string’s own, that being what \(\lambda \)-boundedness bounds, so the wrapper’s syntax tree is rebuilt in Data (Cost.Prog.ProgD.dWrapCore, the encoding of wrapCore by rfl) around the string’s own decider, which enters as the datum it is. (An earlier reading decoded the datum to a program with a fallback on nil, and the tabulation had to decide program-hood to make the same fallback; the reading changed when the compressor’s decider of obligation O4 turned out to need that decoder in the ambient model, see item 1.) The two clauses are separate arguments: the \(\mu \) clause is a count, Verifier.weightList placing one unit of weight at the index pair on which the two marginals of a point of \(\mathbb {F}_2^{s(n)}\) land, so that its question weight is the number of points landing on a given pair and its total weight is \(2^{s(n)}\), which is exactly the quotient the sampler’s distribution is (questionWeight_weightList, totalWeight_weightList); the \(D\) clause is the acceptance table read back (acc_mem_iff) along the relabelings eXof and eAof, which carry Verifier.tagEquiv and answerEquiv across the arithmetic of the two sizes. Both clauses are where the doubling is actually performed, and each takes one indexing that prepends a tag bit: Verifier.accListW is the acceptance table indexed by two given indexings of the questions rather than by bitsToIdx twice, with the old accList recovered as the case of two equal ones by rfl, so that nothing downstream of that name changed. Prepending the tag rather than appending it is what keeps the bounds and injectivity of bitsToIdx applicable verbatim at length \(s(n) + 1\); and the weight list still enumerates \(\mathbb {F}_2^{s(n)}\) once, so the total weight is still \(2^{s(n)}\) — enumerating the strings of length \(s(n) + 1\) instead would compile and silently halve every probability. The entanglement form of [ 1 ] (Remark 6.207) instantiates Lemma 4.10 instead, with \(f = \mathrm{Ent}(\cdot , \frac12)\); it is not used by the main theorem.
Call a family \(a \mapsto \mathsf{V}^a\) of normal form verifiers computably presented when the program of its sampler, the program of its decider, and the dimension \(s^a(n)\) of its sampler’s ambient space are computable in \(a\) (and, for the dimension, in \(n\)). For such a family the set of pairs \((a, \lambda )\) with \(\mathsf{V}^a\) not \(\lambda \)-bounded (Definition 2.49) is recursively enumerable.
Every clause of Definition 2.49 is universally quantified — over indices \(m \geq 2\), and, inside the two time bounds, over the inputs of the sampler and of the decider at \(m\) — and the remaining clause \(\left\vert {\mathsf{V}} \right\vert \leq \lambda \) is a comparison of two computable numbers. So the negation is an unbounded search for a pair (index, input), and each test is decidable: the dimension clause because the dimension is computable by hypothesis, the two time bounds by Lemma 4.14. The index is carried as a datum and read back by Data.natOf, which is a surjection onto \(\mathbb {N}\) inverting the encoding on canonical binary data, so nothing is lost and the encoding the time bounds prepend to their input is primitive recursive in the witness.
Comments.
The hypothesis is not an artefact of the proof: \(\lambda \)-boundedness of a family of verifiers cannot be enumerably refuted unless the family can be run, and the three data named are exactly what running it takes. They are also what the tabulation of item 3 needs before anything else — the question weights come from running the sampler over \(\mathbb {F}_2^{s(n)}\) — so the hypothesis is discharged once, for the family Vof, and serves both.
[\(\bullet \bullet \) medium]
Let the family Vof of verifiers named by strings be computably presented (Lemma 6.205) and let \(x, n \mapsto \mathfrak {G}_{x,n}\) be a computable family of game descriptions with \(\mathrm{val}^*(\mathfrak {G}_{x, n}) = \mathrm{val}^*(\mathsf{V}^x_n)\) whenever \(\mathsf{V}^x\) is \(n\)-bounded. Then there is a closed program of the cost model halting on \(\mathrm{encode}(x, n)\) exactly when \(x \notin B_n\): obligation O3 of Remark 6.204.
\(x \notin B_n\) is “\(\mathsf{V}^x\) is not \(n\)-bounded, or its decider accepts some answer longer than the answer bound at index \(n\), or \(\mathrm{val}^*(\mathsf{V}^x_n) {\gt} \frac12\)” (Verifier.not_inClassB_iff). Under the hypothesis on the family the last disjunct may be read on \(\mathfrak {G}_{x,n}\) instead, in both directions: if \(\mathsf{V}^x\) is \(n\)-bounded the two values are equal, and if it is not then the first disjunct holds anyway. The first disjunct is recursively enumerable by Lemma 6.205; the second by the same pattern with a simpler witness — the tuple and a step budget, tested by one budgeted run of the decider (Verifier.rePred_not_rejectsLong); the third by the \(\mathrm{val}^*\) half of Lemma 3.112 along the computable family. A union of recursively enumerable sets is recursively enumerable, by dovetailing. Lemma 4.15 turns the result into a program on the encodings of pairs.
Comments.
The hypothesis is an equality of values under \(n\)-boundedness alone, and for a while that was more than the tabulation delivered: a game description denotes a synchronous game by construction, so the match was asked only of a verifier synchronous at \(n\) (item 3 of Remark 6.204), while membership in \(B_n\) does not carry synchronicity, and the semidecider was therefore not obtainable from the tabulation together with a disjunction, as the plan had it. Three ways to close the gap were on the record, none of them this lemma’s to choose, and the choice has since been made: it is the first. The game is tabulated on a doubled question set \(\{ 0,1\} \times \mathcal{X}\) — Alice on the first copy, Bob on the second — so that the distribution avoids the diagonal and the forced rejections there are never asked about (MIPRE.Game.doubled and Verifier.doubledGame, with MIPRE.Halting.tab_match now matching the doubled game; item 3 there has the construction). MIPRE.Halting.tab_value is then this lemma’s second hypothesis exactly, \(n\)-boundedness being its only condition.
The other two were rejected for what they would have cost elsewhere, which is why the choice was not this lemma’s to make. Making the wrapper of item 1 reject unequal answers to equal questions would change what a string denotes, and the denotation is what accOf_iff, the classes \(A_n, B_n\) and the compression hypothesis of Theorem 6.197 are all stated about; all three would be reopened, and the wrapper is deliberately the length check and nothing else (item 1). Adding synchronicity at \(n\) to \(B_n\) would leave the tabulation alone but move the cost into the preservation clause of the compressor, which would then have to produce a verifier synchronous at \(n\) as well as a bounded one — and that clause is the one obligation of Remark 6.204 still open. The doubling costs nothing outside the tabulation, and it is not the only hypothesis this lemma has lost: the family Vof is computably presented outright (MIPRE.Halting.computablyPresented_Vof, off the re-budgeted sampler runs of Remark 6.204), so MIPRE.Halting.exists_sem takes no hypotheses at all; Obligations (Halting/Reduction.lean) sits below it in the import order and halting_reduction applies it directly, so O3 is a theorem and not a field. The rejection clause of the classes arrived later than the doubling and cost this lemma one more disjunct, enumerated by the same search; what it buys is the soundness direction of the compressor’s obligation (Remark 6.204, item 1).
[\(\bullet \bullet \) medium]
The paper states the soundness of each transformation with an additional entanglement clause, obtained from the same proofs by tracking the Schmidt rank 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 \frac12 \mathrm{Ent}(\mathsf{V}_n, 1 - \delta (\varepsilon , n))\) for answer reduction, the factor \(\frac12\) being the Schmidt-rank doubling of the symmetrization step; the anchored repetition theorem of [ 10 ] ; 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.214 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.145.
One proviso on the measure: the clauses above are transcribed from [ 1 ] , where the quantity is the least Schmidt rank of a bipartite tensor-product strategy, whereas \(\mathrm{Ent}\) of Definition 2.13 is the least dimension of a synchronous one. Identifying these measures would require a separate strategy and dimension comparison; no such comparison follows merely from the synchronization statement of Theorem 3.3. These clauses are recorded in the paper’s measure and are not consumed by the value-form Lean pipeline.
6.7 The halting reduction
The ingredients, with provenance to the companion repository’s ledger nodes.
There is a Turing machine \(F\) and a decider \(\mathcal{D}^{\mathsf{halt}}= F\) carrying its own description, with a timeout bound \(B_{\mathcal{D}^{\mathsf{halt}}}(n)\), such that \(\mathcal{D}^{\mathsf{halt}}\) is total within its timeout and \(\mathsf{V}^{\mathsf{halt}}= (\mathtt{ComputeSampler}(\lambda ), \mathcal{D}^{\mathsf{halt}})\) is a normal form verifier. The self-reference is by direct construction rather than by the recursion theorem, the input-length check precedes the \(n\)-step simulation of \(\cal {M}\), and the halting-freeze convention makes the decider total.
By construction: the decider is the program MIPRE.Halting.haltProg, closed (haltProg_wellScoped), and the verifier the compressor’s output denotes is a normal form verifier because every string denotes one (Vof_comprStr, Verifier.ofSamplerDecider). Totality on succinct descriptions is haltProg_runs with haltProg_runs_inv; the time bound that replaces the timeout counter is Lemma 6.210.
Comments.
The Lean decider is \(F\) with the self-reference removed, along the route of Remark 6.204: MIPRE.Halting.haltProg takes \((c, n, \lambda )\) in front of its input, reads the string \(x\) that \((c, n)\) succinctly describes by bit queries through the universal machine (Cost.Prog.readProg), rebuilds in the ambient model the description of the verifier \(x\) denotes — the wrapped decider, wrapBuildProg, then both programs frozen at index \(2n + 1\), freezeBuildProg —, runs \(\mathsf{Compress}\) on it at \(\lambda \), and runs the compressed decider on its own input (prepProg, prepProg_runs). The compressor’s output is the string comprStr: \(\lambda \) and this decider with \((c, n, \lambda )\) hardcoded, a normal form verifier by construction since every string denotes one. The paper’s Step 2, the \(n\)-step simulation of \(\cal {M}\), is the compressibility criterion’s business (Lemma 4.11) and does not appear, and there is no timeout counter: the decider is total on succinct descriptions because every stage halts (haltProg_runs, haltProg_runs_inv), and its running time is the accounting of Lemma 6.210, which is what is still open.
The paper’s route.
The self-referential decider of the source, with the recursion theorem, is MIPRE.Halting.dec (Halting/Paper/Decider.lean): for a machine \(\cal {M}\) and a parameter \(\lambda \), the efficient Kleene fixed point (Lemma 4.9, Cost.kleeneFix) of the polynomial-time map \(\texttt{F}: d' \mapsto \mathtt{hardcode}\ \texttt{body}\ (\cal {M}, (\lambda , d'))\), so that on \((n, x, y, a, b)\) it runs body on its own description and the input. body is the program of a polynomial-time function prep returning the program to run and its input — the constant-true program if \(\cal {M}\) halts on the empty input within \(\log n\) steps of the clocked universal machine, the constant-false one if the search program of the second branch (see Lemma 6.211) halts within \(\log n\) steps on the description of \(\mathcal{D}^{\mathsf{halt}}\)’s own verifier, and otherwise the compressed decider \(\mathsf{Compress}((\mathtt{ComputeSampler}(\lambda ), \mathtt{wrap}\ \mathcal{D}^{\mathsf{halt}}), \lambda )\) on the input — followed by one call of the universal machine (body_runs_iff, dec_runs_iff). The verifier is \(\mathsf{V}^{\mathsf{halt}}= \texttt{Vhalt}\ \cal {M}\ \lambda = \mathtt{ofSamplerDecider}\ (\mathtt{ComputeSampler}(\lambda ))\ \mathcal{D}^{\mathsf{halt}}\), the wrapper of Definition 2.46 around \(\mathcal{D}^{\mathsf{halt}}\). The budget \(\log n\) in place of the source’s \(n\) is the criterion’s reading and costs nothing: the levels of the recursion are \(n, 2^n, \ldots \), along which \(\log \) grows without bound. There is no timeout counter here either: totality within a bound is the accounting of Lemma 6.210.
[\(\bullet \bullet \) medium]
For all integers \(C, C' \geq 1\), all \(\lambda \geq 4 \max \{ (4C)^{8C},\ C \log C' \} \) and all \(n \geq 2\),
Bound each factor of the left-hand side by a power of \(n\) — \(C' \leq 2^{\log C' + 1}\), \(\lambda \leq 2^{\log \lambda + 1}\), \(C \leq 2^{C}\), and \(2 \leq n\) — so that the claim reduces to the linear inequality \(4C + C \log C' + C \log \lambda \leq \lambda \). Two of its three terms are a quarter of \(\lambda \) by hypothesis outright. The third, \(C \log \lambda \leq \lambda /4\), is the only one with content, and it is \(\lambda {\lt} 2^{\lambda / 4C}\): writing \(q = \lambda / 4C\), the hypothesis \(\lambda \geq 4(4C)^{8C}\) gives \(q \geq 8C + 4\), and there \(4C(q+1) {\lt} q^2 \leq 2^q\), the second inequality holding from \(q = 4\) on.
Comments.
In Lean \(\log \) is \(\mathtt{Nat.log\ 2}\), which makes the threshold no larger, and the hypothesis \(C' \geq 1\) is dropped: \(C' {\lt} 2^{\log _2 C' + 1}\) holds at \(C' = 0\) as well, so the Lean statement is the stronger one. What consumes this in the halting reduction is the boundedness of a compressed verifier: its running times are \(\mathrm{poly}(n, \lambda )\) (GapCompression.decider_time, sampler_time) while Definition 2.49 asks for \(n^\lambda \), and this is the inequality that turns the first into the second once \(\lambda \) is past a threshold depending on the degree alone — which is what keeps \(\lambda \) polynomial in the description length rather than exponential in it.
[\(\bullet \) easy]
There is a \(\lambda \), computable from the description of \(\cal {M}\) in polynomial time and of size \(\mathrm{poly}(\left\vert {\cal {M}} \right\vert )\), such that \(\mathsf{V}^{\mathsf{halt}}\) is \(\lambda \)-bounded and \(\mathsf{TIME}_{\mathcal{D}^{\mathsf{halt}}}(n), \mathsf{TIME}_{\mathcal{S}^{\mathsf{halt}}}(n) = \mathrm{poly}(n, \left\vert {\cal {M}} \right\vert )\).
MIPRE.Halting.isBounded_comprStr: the sampler clauses from the compression theorem’s own bounds at \(\lambda (n)\), the size clause from the criterion’s slack \(2\left\vert {c} \right\vert \leq n\) and PolyBounded.absorb_log, the decider clause from the explicit wrapper cost Prog.wrapCore_cost’ around innerBound and PolyBounded.absorb; the parameter is computed in binary by comprPoly.
Comments.
In the Lean route of Remark 6.204 the parameter is a function of the level, \(\lambda (n) = 2^{2 \log n}\) (MIPRE.Halting.lamOf, at least \((n+1)^2\) and written in binary by the compressor in time \(O(\log n)\)), and the boundedness claim is the field CompressorSpec.isBounded_compr: the verifier the output denotes is \(n\)-bounded, uniformly in the description \((c, n)\), for every \(n\) past a threshold depending on \(\mathsf{Compress}\) and the universal machine alone (isBounded_comprStr, Halting/CompressorCost.lean). Its three clauses are the sampler’s (GapCompression.sampler_dim, sampler_time at \(\lambda (n)\)), the size’s (the compressed sampler’s program is \(\mathrm{poly}(\log n)\) and the wrapper carries \(c\), which the slack \(2\left\vert {c} \right\vert \leq n\) of Lemma 4.11 leaves room for), and the decider’s: the wrapper’s cost with explicit constants (Prog.wrapCoreCost, Halting/WrapperCost.lean) around the preparation, the universal machine and the compressed decider’s own time (GapCompression.decider_time). Each is absorbed into \(m^n \cdot (\left\vert {d} \right\vert +1)^n\) by PolyBounded.absorb (Halting/Absorb.lean): a polynomially bounded function of the largest of the index, the level and the input size is below \(m^n \cdot y^n\) once \(n\) is past a threshold set by the polynomial, which is Lemma 6.209 in a coarser form. The growth conditions that freezing at \(2n + 1\) needs are lamOf_ge and ansBound_le_lamOf, and exists_compressorSpec assembles the specification from a polynomial-time program computing the output string, which comprPoly (Halting/CompressorProgram.lean) is. There is no timeout counter and no \(\mathsf{TIME}_{\mathcal{D}^{\mathsf{halt}}}\) to compute: totality within a bound is the accounting itself.
The paper’s route.
For the verifier \(\texttt{Vhalt}\ \cal {M}\ \lambda \) of Lemma 6.208 the parameter is a function of the machine, as in the source: MIPRE.Halting.exists_lamBound (Halting/Paper/Cost.lean) gives a threshold \(\Lambda _0\), depending on the compressor, the universal machines and the search program alone, such that for every \(\cal {M}\) and every \(\lambda \geq \Lambda _0 + 4\left\vert {\cal {M}} \right\vert \) the verifier is \(\lambda \)-bounded and the compressor’s bound \(\mathrm{poly}(n, \lambda )\) is below \(n^\lambda \) at every level \(n \geq 2\). So \(\lambda (\cal {M}) = \Lambda _0 + 4\left\vert {\cal {M}} \right\vert \) is affine in \(\left\vert {\cal {M}} \right\vert \); the factor \(4\) is the size of \(\mathcal{D}^{\mathsf{halt}}\), which carries its own description twice (esize_dec: \(2(\left\vert {\cal {M}} \right\vert + \left\vert {\lambda } \right\vert )\) plus a constant), absorbed by PolyBounded.absorb_log. The running time of \(\mathcal{D}^{\mathsf{halt}}\) on \((n, d)\) is the source’s \(\mathrm{poly}(n, \left\vert {\cal {M}} \right\vert )\) in the fine form \(Q(n + \left\vert {\cal {M}} \right\vert + \lambda ) \cdot (\left\vert {d} \right\vert + 1)^k\) for a polynomial \(Q\) and a degree \(k\) depending on the same data (dec_cost, decCostPoly, dec_cost_spec), assembled along the fixed point’s time transfer (Cost.kleeneFix_runs_of), the run of prep and the universal machine’s overhead on the compressed decider; the wrapped decider’s is Prog.wrapCoreCost around it (Vhalt_decider_cost, wrapCoreCost_le_WZ), which the class verifier of Definition 2.52 consumes at the fixed level of Theorem 6.214. The parameter is computed from \(\cal {M}\) in polynomial time by MIPRE.Halting.lamF (the size of \(\cal {M}\) in unary, four copies, plus the constant, read in binary), which the class verifier of Theorem 6.214 runs on \(\cal {M}_z\) (lamz).
[\(\bullet \bullet \) medium]
For every \(n\):
if \(\cal {M}\) halts within \(n\) steps then \(\mathrm{val}^*(\mathsf{V}^{\mathsf{halt}}_n) = 1\), witnessed by a value-\(1\) PCC strategy;
if \(\cal {M}\) does not halt within \(n\) steps then \(\mathsf{V}^{\mathsf{halt}}_n\) and \(\mathsf{V}^{\textsc{Compr}}_n\) are the same game up to an identification of the answer alphabets; in particular \(\mathrm{val}^*(\mathsf{V}^{\mathsf{halt}}_n) = \mathrm{val}^*(\mathsf{V}^{\textsc{Compr}}_n)\), and \(\mathsf{V}^{\mathsf{halt}}_n\) has a value-\(1\) PCC strategy if and only if \(\mathsf{V}^{\textsc{Compr}}_n\) does.
Item 1 is the fixed-answer strategy: when \(\cal {M}\) halts within \(n\) steps, \(\mathcal{D}^{\mathsf{halt}}\) accepts every answer pair on every question pair in the support, so any strategy has value \(1\) and the constant-\(0\) strategy is PCC. For item 2, \(\mathcal{D}^{\mathsf{halt}}\) at index \(n\) performs the same question-length check as \(\mathcal{D}^{\textsc{Compr}}\) and then runs \(\mathcal{D}^{\textsc{Compr}}(n, x, y, a, b)\) verbatim, with \(\mathtt{TIMEOUT}\) rejecting in both, so the two deciders accept on exactly the same inputs; and the two verifiers share the sampler \(\mathcal{S}^{\mathsf{halt}}= \mathtt{ComputeSampler}(\lambda )\) (Lemma 6.200), so a strategy for either is a strategy for the other with the same winning probability. The timeout counter of \(\mathcal{D}^{\mathsf{halt}}\) does not interfere: its bound is chosen in Lemma 6.210 so that the computations above finish first.
Comments.
Item 2 is, in the Lean route, the acceptance agreement MIPRE.Halting.comprStr_accepts: the decider of the verifier the compressor’s output denotes accepts, at every index, exactly what the compressed decider of the described verifier frozen at \(2n + 1\) accepts, with the same sampler (Vof_comprStr); the transfer of values and of value-\(1\) PCC strategies along it, in both directions, is CompressorSpec.toObligations. Item 1 does not appear at this point of the route: the halting case is the criterion’s, through the distinguished string yYes of Lemma 4.11, and the \(n\)-step simulation of \(\cal {M}\) is the criterion’s recursion, not the decider’s.
Along the paper’s route (Lemma 6.208, Halting/Paper/) both items are the decider’s: MIPRE.Halting.accepts_iff (Halting/Paper/Decider.lean) says that \(\mathcal{D}^{\mathsf{halt}}\) at index \(n\) accepts \((x, y, a, b)\) exactly when the questions have the sampler’s dimension and then: everything, if \(\cal {M}\) halts within \(\log n\) steps; nothing, if the search program halts within \(\log n\) steps on the description of \(\mathsf{V}^{\mathsf{halt}}\); and otherwise exactly what the compressed decider of \(\mathsf{V}^{\mathsf{halt}}\) itself accepts. Item 1 is the first clause with the diagonal strategy (A_of_branch1); item 2 is the third clause, the transfer of values and of value-\(1\) PCC strategies along it being A_step and B_step (Halting/Paper/Induction.lean) with the answer alphabets identified through rejectsLong_of_not_branch1, the compressed decider accepting no answer longer than its bound. The second clause is Lin’s search branch, which the criterion route has too (decFunV of Halting/Compression.lean): the value form of the compression theorem has no base case for soundness, and the search — the semidecider of “\(\mathrm{val}^*{\gt} \frac12\) at the fixed level \(C\) of the verifier this string describes”, exists_semL on the tabulation tabL — supplies it (B_of_branch2: value \(0\) once it fires).
Item 2 is deliberately not “\(\mathrm{val}^*(\mathsf{V}^{\mathsf{halt}}_n) \leq \frac12\)”. That per-level bound is false: if \(\cal {M}\) halts for the first time at step \(T\), then for every \(n {\lt} T\) it does not halt within \(n\) steps, yet \(\mathrm{val}^*(\mathsf{V}^{\mathsf{halt}}_n) = 1\) — item 1 gives value \(1\) at every level \(\geq T\), and item 2 together with the completeness clause of Theorem 6.197 carries it downward from level \(2^n\) to level \(n\), which is exactly how the completeness half of Theorem 6.214 is proved. The absolute bound needs \(\cal {M}\) never to halt, and is then the conclusion of the recursion in Theorem 6.214, not an ingredient of it. Recorded here because an earlier revision of this chapter did state item 2 as the bound, and because the ledger node ‘1.6.3’ states it that way too; the formalization should follow the paper.
Let \(\lambda \mapsto \mathcal{S}^\lambda \) be samplers of a level \(\ell \) whose programs are computed from \(\lambda \) in polynomial time and which run within, and have dimensions at most, a polynomial in \(n + \lambda \) at index \(n\). Let \(R : z \mapsto \cal {M}_z\) be computable in polynomial time, \(\lambda (z) = \Lambda _0 + 4\left\vert {\cal {M}_z} \right\vert \), and \(n_0\) an index. There is a program which, on \((z, r)\) with \(r\) at least as long as the dimension \(s\) of \(\mathcal{S}^{\lambda (z)}\) at \(n_0\), halts within a polynomial in \(\left\vert {z} \right\vert + \left\vert {r} \right\vert \) with the two marginals of \(\mathcal{S}^{\lambda (z)}\) at \(n_0\) at the first \(s\) bits of \(r\). For a polynomial-time verifier with this sampler and a polynomial above these bounds, the distribution of its game on \(z\) is, on the questions of \(\mathcal{S}^{\lambda (z)}\) embedded as bit strings, the distribution of \(\mathcal{S}^{\lambda (z)}\) at \(n_0\), and it has no weight elsewhere.
The program computes \(\cal {M}_z\), \(\lambda (z)\) and the program of \(\mathcal{S}^{\lambda (z)}\), asks it its dimension \(s\) through the universal machine, converts \(s\) to unary, takes the first \(s\) bits of the seed and asks the two marginals there; each stage runs within a polynomial in the total input length. At level \(0\) the marginal queries are not specified, but the questions are empty, the CL function of level \(0\) being exactly on the empty set only, and there the program outputs the empty pair. Of the \(2^B\) seeds, those producing a question pair are the extensions of the points of \(\mathbb {F}_2^s\) producing it, each in \(2^{B - s}\) ways, so the uniform seed pushes forward to the distribution of \(\mathcal{S}^{\lambda (z)}\).
[\(\bullet \bullet \bullet \) hard]
Assume an ambient MIPRE.GapCompression. There is a computable map \(\cal {M}\mapsto \mathfrak {G}_{\cal {M}}\) from Turing machines to explicit synchronous game descriptions (Definition 2.43), such that:
if \(\cal {M}\) halts on the empty input then \(\mathfrak {G}_\cal {M}\) has a value-\(1\) PCC strategy, so \(\mathrm{val}^{s}(\mathfrak {G}_\cal {M}) = \mathrm{val}^*(\mathfrak {G}_\cal {M}) = 1\);
if \(\cal {M}\) does not halt on the empty input then \(\mathrm{val}^*(\mathfrak {G}_\cal {M}) \leq \tfrac 12\), and hence also \(\mathrm{val}^{s}(\mathfrak {G}_\cal {M}) \leq \tfrac 12\) (Lemma 2.14).
Moreover the reduction is polynomial-time: for every polynomial-time map \(z \mapsto \cal {M}_z\) from strings to machines there is a polynomial-time verifier in the sense of Definition 2.52, efficient on every input, whose game on \(z\) has a value-\(1\) PCC strategy if \(\cal {M}_z\) halts on the empty input and quantum value at most \(\tfrac 12\) if it does not.
MIPRE.Halting.halting_reduction_of in \(\mathrm{val}^*\) and halting_reduces_to_gameValue_of in \(\mathrm{val}^{s}\), from Theorem 6.197 as a GapCompression: Lemma 4.11 at the classes of Remark 6.204, whose four obligations are the theorems named below, the last through exists_obligations. This proves computability of the explicit tabulation. It does not assert polynomial-time enumeration of that table.
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}\).
The tabulation of Theorem 6.214 gives both values at once (halting_reduction_both_of): at a halting machine the tabulated game has a value-\(1\) PCC strategy, and at a non-halting one its quantum value is at most \(\tfrac 12\). A separating function composed with the map would decide halting, against Theorem 3.79. An r.e. language reduces to the halting problem by a computable map, which composes with the quantum-value reduction; the converse inclusion is Lemma 7.5. These are the conditional forms of the results of Chapter 7, which Corollary 6.199 instantiates.
The efficient source presentation.
The polynomial-time reduction in the source recursive.tex, thm:halting [ 34 ] , returns sampler and decider program descriptions for a game at a fixed index; those programs run in time polynomial in \(\left\vert {\cal {M}} \right\vert \). This is the source efficiency claim. Enumerating their finite question distribution and accepted answer tuples yields the computable explicit description used here, but the number of entries can exceed a polynomial in the program size. The efficient verifier presentation and the explicit table are different codomains; the second is the criterion route’s, the first is now formalized too (MIPRE.Halting.classV, below).
The paper’s route, at a fixed level.
The source’s statement is now formalized for the verifier itself: MIPRE.Halting.halting_paper (Halting/Paper/Main.lean) says that for every machine \(\cal {M}\) and every \(\lambda \geq \Lambda _0 + 4\left\vert {\cal {M}} \right\vert \) (Lemma 6.210), the verifier \(\texttt{Vpaper}\ \cal {M}\ \lambda = \texttt{Vhalt}\ \cal {M}\ \lambda \) of Lemma 6.208 with the search program semL, at the fixed level \(C = \max (C_0, 2)\) and with answers of length at most the compressor’s bound \(\mathrm{poly}(C, \lambda )\), has a value-\(1\) PCC strategy if \(\cal {M}\) halts on the empty input and value at most \(\frac12\) if it does not (halting_paper_valStar in \(\mathrm{val}^*\)). The proof is the downward induction of the source along the levels \(C, 2^C, 2^{2^C}, \ldots \) (Halting/Paper/Induction.lean): a halting machine puts every level past its halting time in the class of value-\(1\) PCC verifiers (item 1 of Lemma 6.211), and the completeness clause of Theorem 6.197 carries the class down one level at a time (A_step), the search branch never firing since it would put the start level below \(\frac12\); for a non-halting machine, a value above \(\frac12\) at level \(C\) makes the search halt at some step, every level whose \(\log \) exceeds it has value \(0\), and the soundness clause carries \(\leq \frac12\) down to \(C\) (B_step), a contradiction. This is the criterion’s argument at a fixed level with the succinct description replaced by the hardcoded one. The game is the source’s \(\mathsf{V}^{\mathsf{halt}}\) at index \(C\): its sampler is \(\mathtt{ComputeSampler}(\lambda (\cal {M}))\) and its decider runs within the polynomial bound of Lemma 6.210, which is what makes the reduction polynomial-time once read off a uniform program, the class-level statement of Definition 2.52.
The class verifier.
That program is MIPRE.Halting.classV (Halting/Paper/ClassVerifier.lean, ClassMain.lean), a PolyVerifier for a polynomial-time map \(R : z \mapsto \cal {M}_z\). Its sampler sampProg is that of Lemma 6.213 for the compressed samplers at the level \(C\): on \((z, r)\) it computes \(\cal {M}_z\), \(\lambda (z) = \Lambda _0 + 4\left\vert {\cal {M}_z} \right\vert \) and the compressed sampler’s program \(\mathtt{ComputeSampler}(\lambda (z))\), asks it its dimension \(s(C)\) through the universal machine, and returns its two marginals at the first \(s(C)\) bits of the seed (sampProg_runs); so the uniform seed of length \(B \geq s(C)\) pushes forward to the compressed sampler’s distribution. Its decider decProg, on \((z, x, y, a, b)\), computes the description of \(\mathcal{D}^{\mathsf{halt}}\) (decBuild, the fixed tree around \(\cal {M}_z\) and \(\lambda (z)\)) and its wrapper, rejects if \(a\) or \(b\) exceeds the cutoff \(2^{K + \deg \cdot \left\vert {\lambda (z)} \right\vert }\) — a power of two, computable from \(\left\vert {\lambda (z)} \right\vert \) in unary and above the compressor’s answer bound for \(K\) chosen from \(G\) — and otherwise runs the wrapper on \((C, x, y, a, b)\) through the universal machine (decProg_accepts). Both run within an explicit polynomially bounded cost in their total input length (sampProg_runs, decProg_runs), so the verifier is efficient (classV_efficient), and its game has the value of \(\mathsf{V}^{\mathsf{halt}}\) at level \(C\) with the answers cut at the cutoff (classV_value: the game is the restriction of \(\mathsf{V}^{\mathsf{halt}}\)’s to the questions of length \(s(C)\), quantumValue_restrictQuestions, with the answers extended by always-rejected ones, quantumValue_extendAnswers), which is \(1\) or at most \(\frac12\) by the previous paragraph (classV_values). This is the polynomial-time clause of the theorem, and \(\mathrm{RE}\subseteq \mathrm{MIP}^*\) for the class of Definition 2.52 in Theorem 7.6.
The proof is Lemma 4.11 applied to the instantiation of Remark 6.204; the semidecidability hypothesis of the lemma is the \(\mathrm{val}^*\) half of Lemma 3.112. The obligations of that instantiation are inherited here, and all four listed in Remark 6.204 are formalized: the tabulation (MIPRE.Halting.tab, with tab_match, tab_value and gameValue_tab_eq_one), the semidecider on top of it (MIPRE.Halting.exists_sem, Lemma 6.206, which takes no hypotheses), the two distinguished strings MIPRE.Halting.yYes_mem and yNo_mem, and the compressor (Lemmas 6.208, 6.210 and 6.211: MIPRE.Halting.comprPoly, its specification exists_compressorSpec, and exists_obligations). The synchronization invariant that an earlier revision also required of the games produced inside \(\mathsf{Compress}\) is no longer among them (Remark 6.8).
In Lean the assembly is MIPRE.Halting.halting_reduction (Halting/Reduction.lean), which takes three hypotheses: a MIPRE.GapCompression (which is Theorem 6.197), a universal machine, and an inhabitant of MIPRE.Halting.Obligations, whose content is exactly the compressor — compr, compr_spec, and the threshold above which its guarantee holds. The other three obligations of Remark 6.204 are theorems that the proof applies directly, and the fourth is now a theorem too: MIPRE.Halting.exists_obligations (Halting/CompressorProgram.lean) inhabits the structure, so MIPRE.Halting.halting_reduction_of takes only a GapCompression and a universal machine — of which Cost.exists_efficient_universal provides one — and is free of sorry. So the reduction is machine-checked from an inhabitant of the compression contract alone; supplying that inhabitant is Theorem 6.198. The #print axioms check shows no further unproved assumption. That assembly concludes in \(\mathrm{val}^*\) only, and item 1 claims more: the witness is a PCC strategy, so \(\mathrm{val}^{s}= \mathrm{val}^*= 1\). The two steps that carry it there are now in Lean, neither of them part of the instantiation. First, a synchronous strategy transports along a relabeling of the alphabets (MIPRE.syncValue_eq_of_equiv, from SyncStrategy.relabel, which preserves the value and the commutation condition), so a value-\(1\) PCC strategy of \(\mathsf{V}_n\) — a strategy of its doubled game, which is what HasPerfectPCC is — gives one for a description tabulating that doubled game: Verifier.exists_perfectPCC_syncGame_doubled, hence Verifier.syncValue_syncGame_eq_one_doubled. Second, MIPRE.syncValue and HaltingGameValue.gameValue — parallel developments with parallel notions of synchronous strategy — are the same number on the same description (HaltingGameValue.GameData.gameValue_eq_syncValue), so the conclusion is available in the vocabulary of halting_reduces_to_gameValue (Section 7): Verifier.gameValue_toGame_eq_one_doubled, which on the tabulation is MIPRE.Halting.gameValue_tab_eq_one. Soundness needs neither step, only \(\mathrm{val}^{s}\leq \mathrm{val}^*\) (Lemma 2.14), which is Verifier.gameValue_toGame_le_of_valStar_le_doubled in the same vocabulary. The soundness bridge against \(\mathsf{V}_n\) itself is still there and still true; the three un-doubled completeness bridges went with the restatement of HasPerfectPCC on the doubled game (Theorem 6.197, “two readings”), a strategy of the doubled game having no reason to agree with itself across the two tags on the diagonal, which carries no weight. Both steps consume the tabulation’s agreement with \(\mathsf{V}_n\) in the form of the two alphabet equivalences and the matching of \(\mu \) and \(D\) along them, not merely the equality of \(\mathrm{val}^*\) they imply — from that equality alone the synchronous half cannot be recovered, \(\mathrm{val}^{s}\leq \mathrm{val}^*\) pointing the wrong way. That is why MIPRE.Halting.tab_match delivers the matching data and not only the equality of values, with tab_value reading that equality off it; the tabulation builds the equivalences anyway, out of answerEquiv and questionEquiv, so the stronger statement cost nothing.
The conditional ambient halting construction yields a witness in SyncStrategy, represented by a single projective measurement family and normalized trace probabilities. Within that representation the common family is part of the definition (Definition 2.4). The source instead tracks identical operators on a bipartite state through its transformations. These are distinct representations: identical operators alone do not supply either direction of Remark 2.8. The checked downstream halting and tabulation proofs start with the ambient interface and therefore do not discharge that source-to-ambient obligation. The entanglement form, with the stronger conclusion \(\mathrm{Ent}(\mathfrak {G}_\cal {M}, \frac12) = \infty \) for non-halting \(\cal {M}\), is discussed in Remark 6.207.