Dependencies

This claim is made under the same standing hypotheses used in the commutativity-of-\(G\) theorem above. The linked SliceBoundednessInput declarations are precisely the two displayed parts of item 3: the averaged \((I-G^y)\otimes Z^y\) residual bound and the domination \(Z^y\ge \mathbb {E}_u A^{u,y}_{g(u)}\).

This claim is made under the same standing hypotheses used in the commutativity-of-\(G\) theorem above, in particular the boundedness item 3. The linked SliceBoundednessInput declarations expose those boundedness hypotheses in Lean; they are not auxiliary assumptions added to the paper statement.

In the nontrivial-regime pasting context of Definition 9.3, the following commutation relations hold:

where

In the nontrivial-regime pasting context of Definition 9.3,

Lemma 9.9 converts 11 into the estimate

where the middle step uses concavity of \(a \mapsto a^{1/(d+1)}\). Equivalently,

For constant \(d\), this is exactly the heuristic completeness comparison for the first construction recorded in ‘references/ldt-paper/ld-pasting.tex‘.

In the nontrivial-regime pasting context of Definition 9.3,

The completed measurements \(\widehat G^x\) satisfy

where

On average over \((u,x) \sim \mathbb {F}_q^{m+1}\),

Let \(H_{\mathrm{meas}}\) be the completion of \(H\) at the fallback outcome. On average over \((u,x) \sim \mathbb {F}_q^{m+1}\),

If \(\lambda _1 \le \lambda _2 \le \cdots \le \lambda _{q^m}\) are the eigenvalues of \(L\), then

If \(k \ge 400md\), then

Let \(M=q^m\). The normalized adjacency matrix of \(C\) is

and the Laplacian is

For \(x \in \mathbb {F}_q\), let \(\operatorname {append}_x(\ell )\) be the line in \(\mathbb {F}_q^{m+1}\) obtained by appending the coordinate \(x\) to every point of a line \(\ell \subseteq \mathbb {F}_q^m\). If \(f \colon \ell \to \mathbb {F}_q\), let \(\operatorname {append}_x(f)\) be the polynomial on \(\operatorname {append}_x(\ell )\) defined by \(\operatorname {append}_x(f)(u,x)=f(u)\).

Let \(\lvert \psi \rangle \in \mathcal H\), let \(A=\{ A_a^x\} \) and \(B=\{ B_a^x\} \) be families of operators on \(\mathcal H\), and let \(\mathcal D\) be a distribution on the question set. We write

when

The average restricted errors are the expectations over \(x \in \mathbb {F}_q\) of the axis-parallel, self-consistency, and restricted diagonal-line failure probabilities of the \(x\)-restricted strategies.

The completed outcome tuples admit the reindexings obtained by separating the first coordinate, moving a third slice to the front, and identifying the one-coordinate split with the original slice question and outcome spaces.

For \(k \ge 1\), let \(\mathsf{Distinct}_k \subseteq \mathbb {F}_q^k\) be the set of tuples \((x_1,\dots ,x_k)\) with pairwise distinct coordinates.

The finite-field trace is the map \(\operatorname {tr}:\mathbb {F}_q\to \mathbb {F}_p\) defined by

For each \(x \in \mathbb {F}_q\), write \(G^x = \sum _g G_g^x\) and define the incomplete outcome \(G_\bot ^x = I-G^x\). The completed measurement \(\widehat G^x\) has outcome set \(\mathcal{P}(m,q,d) \cup \{ \bot \} \) and is given by

A strategy is \((\varepsilon ,\delta ,\gamma )\)-good if it passes the axis-parallel lines test with probability at least \(1-\varepsilon \), the self-consistency test with probability at least \(1-\delta \), and the diagonal lines test with probability at least \(1-\gamma \).

The hypercube graph \(C=(V,E)\) has vertex set \(V=\mathbb {F}_q^m\), and an edge between \(u\) and \(v\) whenever they differ in at most one coordinate. A random edge \((u,v) \sim C\) is sampled by drawing \(u \sim \mathbb {F}_q^m\), \(i \in \{ 1,\dots ,m\} \), and \(x \in \mathbb {F}_q\) uniformly and then setting \(v=\operatorname {rerand}_i(u,x)\).

The Lean context linked here is the nontrivial-regime context used after the reduction explained above. It consists of the data and hypotheses from the pasting theorem at the beginning of this chapter: an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy \((\psi ,A,B,L)\) for the \((m+1,q,d)\) low individual degree test, a family of projective submeasurements \(\{ G^x\} _{x \in \mathbb {F}_q}\) in \(\mathrm{PolySub}(m,q,d)\) satisfying 1–4, an integer \(k \ge 400md\), and the quantities \(\nu \) and \(\sigma \) defined there. It also records the nontrivial-regime assumptions

These extra fields are not assumptions of the unrestricted source theorem; they belong to the restricted proof stage. The unrestricted paper-facing Lean theorem remains MIPStarRE.LDT.Pasting.ldPasting.

Let \(\lvert \psi \rangle \in \mathcal H_{\mathrm A} \otimes \mathcal H_{\mathrm B}\) and let \(0 \le A^u \le I\) be an operator for each \(u \in \mathbb {F}_q^m\). The local variance is

and the global variance is

Fix integers \(m,d \ge 0\) and a prime power \(q\). The \((m,q,d)\) low individual degree test has three equally likely subtests. In the axis-parallel lines test, choose a uniformly random role \(r \in \{ \mathrm A,\mathrm B\} \), a uniformly random point \(u \in \mathbb {F}_q^m\), and a uniformly random coordinate \(i \in \{ 1,\dots ,m\} \). Let \(\ell =\{ u+t e_i : t \in \mathbb {F}_q\} \). Player \(r\) receives \(\ell \) and returns a degree-\(d\) univariate polynomial \(f\colon \ell \to \mathbb {F}_q\); Player \(\overline r\) receives \(u\) and returns a field element \(a \in \mathbb {F}_q\). The verifier accepts when \(f(u)=a\). In the self-consistency test, both provers receive the same uniformly random point \(u \in \mathbb {F}_q^m\) and must return the same field element. In the diagonal lines test, choose a uniformly random role \(r \in \{ \mathrm A,\mathrm B\} \), a uniformly random point \(u \in \mathbb {F}_q^m\), a uniformly random index \(i \in \{ 1,\dots ,m\} \), and a uniformly random direction vector \(v \in \mathbb {F}_q^m\) whose last \(m-i\) coordinates are \(0\). Let \(\ell =\{ u+t v : t \in \mathbb {F}_q\} \). Player \(r\) receives \(\ell \) and returns a degree-\(md\) univariate polynomial \(f\colon \ell \to \mathbb {F}_q\); Player \(\overline r\) receives \(u\) and returns a field element \(a \in \mathbb {F}_q\). The verifier accepts when \(f(u)=a\).

Set

Assume \(q {\gt} 0\), \(k \ge 1\), \(m \ge 1\), \(0 \le \varepsilon \le 1\), and \(d \le q\). Fix an incoming error parameter \(\nu \). Define

The coefficient \(42\) is the Lean cascade scalar; it widens the paper’s printed coefficient \(40\) so that the completion theorem’s extra \(2\zeta _1\) term is absorbed while preserving the final error envelope.

For each \(a\), let

and let \(\lvert v_{a,1} \rangle ,\ldots ,\lvert v_{a,m_a} \rangle \) be an orthonormal basis for the range of \(Q_a\), so that

Let

and let \(\{ \lvert a,i \rangle \} \) be an orthonormal basis of \(\mathbb {C}^m\), indexed by all \(a\) and all \(1 \leq i \leq m_a\). For each \(a\), define

and define

Let \(T = \{ T_a\} \). Then \(T\) is a projective measurement on \(\mathbb {C}^m\).

Let \(A=\{ A_a^x\} _{a \in \mathcal A}\) be a submeasurement. Its completion is the measurement \(\widehat A\) with outcome set \(\widehat{\mathcal A}=\mathcal A \cup \{ \bot \} \) given by \(\widehat A_a^x=A_a^x\) for \(a \in \mathcal A\) and \(\widehat A_\bot ^x = I-\sum _a A_a^x\).

For a type \(\tau \in \{ 0,1\} ^k\), let \(\mathsf{Outcomes}_\tau \) be the set of tuples \((g_1,\dots ,g_k)\) such that \(g_i \in \mathcal{P}(m,q,d)\) when \(\tau _i=1\) and \(g_i=\bot \) when \(\tau _i=0\). If \(x_1,\dots ,x_k \in \mathbb {F}_q\), let \(\mathsf{Global}_\tau (x)\) be the subset of \(\mathsf{Outcomes}_\tau \) arising from restrictions of a single polynomial in \(\mathcal{P}(m+1,q,d)\), and let \(\overline{\mathsf{Global}_\tau (x)} = \mathsf{Outcomes}_\tau \setminus \mathsf{Global}_\tau (x)\).

Fix \(k \ge d+1\). For \(x_1,\dots ,x_k \in \mathbb {F}_q\) and outcomes \(g_1,\dots ,g_k \in \mathcal{P}(m,q,d)\cup \{ \bot \} \), define

If \((x_1,\dots ,x_k)\in \mathsf{Distinct}_k\) and \(h \in \mathcal{P}(m+1,q,d)\), define

where the tuple \(h_\tau \) has \(i\)-th entry \(h|_{x_i}\) when \(\tau _i=1\) and \(\bot \) when \(\tau _i=0\). The pasted submeasurement is then

Sample a uniformly random ordered point pair \((u,v)\) and a uniformly random parameter \(t \in \mathbb {F}_q\). Package this data as the diagonal line whose direction is \(v-u\) and whose parametrization visits \(u\) at \(t\) and \(v\) at \(t+1\).

Let \(\mathcal{P}(m,q,d)\) be the set of polynomials \(g \in \mathbb {F}_q[x_1,\dots ,x_m]\) whose degree in each variable is at most \(d\), viewed as functions \(\mathbb {F}_q^m \to \mathbb {F}_q\) via evaluation. (Over finite fields, distinct low-degree polynomials can induce the same function; we identify elements of \(\mathcal{P}(m,q,d)\) with their polynomial representatives, not their functional equivalence classes.)

We write \(\mathrm{PolySub}(m,q,d)\) for the submeasurements indexed by \(\mathcal{P}(m,q,d)\), and \(\mathrm{PolyMeas}(m,q,d)\) for the corresponding measurements.

Let \(A=\{ A_a\} _{a \in \mathcal A}\) be a family of operators and let \(f\colon \mathcal A \to \mathcal B\). The post-processed family \(A_{[f(a)=b]}\) is defined by

The paper defines

We take \(\widehat X\) to be the reduced matrix supplied by the stored datum. For each \(a\), define

A general projective strategy for the \((m,q,d)\) low individual degree test consists of a bipartite state \(\lvert \psi \rangle \in \mathcal H_{\mathrm A} \otimes \mathcal H_{\mathrm B}\) together with point, axis-parallel line, and diagonal-line projective measurements for each prover separately. We write these measurements as \(A^{\mathrm A}, B^{\mathrm A}, L^{\mathrm A}\) on the first prover and \(A^{\mathrm B}, B^{\mathrm B}, L^{\mathrm B}\) on the second.

For \(u \in \mathbb {F}_q^m\), an index \(i \in \{ 1,\dots ,m\} \), and \(x \in \mathbb {F}_q\), let

This is the move obtained by rerandomizing the \(i\)-th coordinate of \(u\) by a uniform additive shift. In Lean, the same edge distribution is represented as the push-forward of the uniform distribution on triples \((u,i,x)\) by the map that replaces the \(i\)-th coordinate by \(x\); since \(x\) is uniform, this is the same distribution as the additive-shift presentation. The corresponding weight-sum identity identifies this push-forward distribution with the explicit edge coefficient used in the matrix proof.

Consider the \((m,q,d)\) low individual degree test. For \(j \in \{ 1,\dots ,m\} \), the \(j\)-restricted diagonal lines test is the diagonal lines test conditioned on \(i=j\). In particular, the \(m\)-restricted diagonal lines test is the diagonal lines test in which the sampled line is a uniformly random line in \(\mathbb {F}_q^m\).

Let \((\psi ,A,B,L)\) be a symmetric strategy for the \((m+1,q,d)\) low individual degree test. For each \(x \in \mathbb {F}_q\), the \(x\)-restricted strategy \((\psi ,A^x,B^x,L^x)\) for the \((m,q,d)\) test is defined by

A role is an element of \(\{ \mathrm A,\mathrm B\} \). For a role \(r \in \{ \mathrm A,\mathrm B\} \), write \(\overline r\) for the other element of \(\{ \mathrm A,\mathrm B\} \).

Let \(\lvert \psi \rangle \in \mathcal H_{\mathrm A} \otimes \mathcal H_{\mathrm B}\). Let \(A=\{ A_a^x\} \) and \(B=\{ B_a^x\} \) be submeasurements with the same answer set, and let \(\mathcal D\) be a distribution on the question set. We write

when

Let \(\lvert \psi \rangle \) be permutation-invariant and let \(A=\{ A_a^x\} \) be a submeasurement. We say that \(A\) is \(\delta \)-strongly self-consistent when

Let \(\mathcal H\) be a Hilbert space and let \(\mathcal A\) be a set of outcomes. A submeasurement on \(\mathcal A\) is a family \(A=\{ A_a\} _{a \in \mathcal A}\) of Hermitian positive semidefinite operators on \(\mathcal H\) such that \(\sum _a A_a \le I\). It is a measurement when \(\sum _a A_a = I\), and it is projective when each \(A_a\) is an idempotent projection. (In the Lean formalization, outcome sets are assumed finite throughout.)

The successor step forms the pasting input by combining the restricted probability estimates with the slice-wise self-improvement data. The Lean construction applies the unrestricted induction-section pasting theorem directly, and the small-error constructor supplies the scalar side conditions \(\gamma \le 1\), \(\zeta \le 1\), and \(d\le q\) internally. Thus the successor proof can call the small-error pasting constructor without carrying \(0{\lt}d\), \(1\le k\), \(\gamma \le 1\), \(\zeta \le 1\), or \(d\le q\) as separate proof inputs. The answer-valued small-error assembly then converts the answer-valued slice data to this pasting interface and applies the checked stage-data theorem.

The paper presents this step by choosing a singular value decomposition

The formalization has two closely related auxiliary declarations. The reduced datum records the downstream consequences of the choice: the matrices \(X\) and \(\widehat X\), the identities \(X^\dagger X=Q\), \(\widehat X\widehat X^\dagger =I\), and \(X^\dagger \widehat X=\sqrt Q\), together with the \(Q_a=X^\dagger T_aX\) restatement. The rectangular-SVD lemmas take explicit matrices \(U,V,\Sigma ,I_{m\times d}\) and derive the two stored \(\widehat X\) identities from the matrix calculation below.

A symmetric projective strategy for the \((m,q,d)\) low individual degree test consists of a permutation-invariant bipartite state \(\lvert \psi \rangle \in \mathcal H \otimes \mathcal H\), a projective point measurement \(A^u=\{ A^u_a\} _{a \in \mathbb {F}_q}\) for each \(u \in \mathbb {F}_q^m\), a projective axis-parallel line measurement \(B^\ell =\{ B^\ell _f\} \) for each axis-parallel line \(\ell \), and a projective diagonal-line measurement \(L^\ell =\{ L^\ell _f\} \) for each line \(\ell \).

For \(1 \le \ell \le k+1\) and a tail type \(\tau _{\ge \ell } \in \{ 0,1\} ^{k-\ell +1}\), define

This records the contribution of all prefixes that can still be completed to total weight at least \(d+1\) once the tail \(\tau _{\ge \ell }\) is fixed.

A type is a vector \(\tau \in \{ 0,1\} ^k\). Its weight \(|\tau |\) records how many coordinates lie in \(\mathcal{P}(m,q,d)\) rather than equal \(\bot \).

For every classical strategy, the acceptance probability of the low individual degree test is

where the five terms are the acceptance probabilities of the two axis-parallel role orderings, the self-consistency branch, and the two diagonal role orderings.

Let \(T=\{ T_h\} \) be an optimal solution of the primal SDP, let

and set

Suppose \(M = \{ M^u_o\} \) is a submeasurement with outcomes in some set \(\mathcal O\). For each \(u \in \mathbb {F}_q^m\), let \(S_u\) be a subset of \(\mathcal O \times \mathcal{P}(m,q,d)\). Then

Let \(f,h : \mathrm{AxisLinePolynomial}\, \mathrm{params}\) be two line-polynomial outcomes with distinct underlying polynomials. Then

The native univariate root-counting bound is \(d/q\); the statement deliberately pads this to the paper’s ambient \(md/q\) loss for Lemma 6.1.

The block operators obtained from a bipartite projective strategy are positive semidefinite, and the role-indexed blocks multiply according to the Kronecker delta on roles.

For \(\beta \in \mathbb {F}_q\),

For \(\alpha ,\beta \in \mathbb {F}_q^m\),

Let \(0{\lt}\theta {\lt}1\) and integers \(k,d{\gt}0\) with \(k \ge 2d/\theta \). Define

If \(X\) is Hermitian, \(0 \le X \le I\), and \(\langle \psi \rvert X \otimes I \lvert \psi \rangle \ge 1-\kappa \), then

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m+1,q,d)\) low individual degree test. Let \(\{ G^x\} \in \mathrm{PolySub}(m,q,d)\) be a collection of projective sub-measurements indexed by \(x \in \mathbb {F}_q\) with the following properties:

1. (Consistency with \(A\)) On average over \((u,x) \sim \mathbb {F}_q^{m+1}\),

   \[ A_a^{u,x} \otimes I \simeq _\zeta I \otimes G^x_{[g(u)=a]}. \]

2. (Strong self-consistency) On average over \(x \sim \mathbb {F}_q\),

   \[ G_g^x \otimes I \approx _\zeta I \otimes G_g^x. \]

3. (Boundedness) There exists a positive-semidefinite matrix \(Z^x\) for each \(x \in \mathbb {F}_q\) such that

   \[ \mathbb {E}_x \langle \psi \rvert (I-G^x) \otimes Z^x \lvert \psi \rangle \le \zeta \]

   and for each \(x \in \mathbb {F}_q\) and \(g \in \mathcal{P}(m,q,d)\),

   \[ Z^x \ge \left(\mathbb {E}_u A_{g(u)}^{u,x}\right). \]

Let

Then on average over independent and uniformly random \((u,x),(v,y) \sim \mathbb {F}_q^{m+1}\),

Let \(M=\{ M_o^x\} \) be a projective submeasurement with outcomes in a set \(\mathcal O\). Suppose that

and

on average over independent uniformly random \(x,y \sim \mathbb {F}_q\). Then

For every \(k \ge 2\),

where

1. Head–tail split identities. For every \(k \ge 0\), point tuple \({\boldsymbol {x}}= (x_1,\dots ,x_{k+1})\), and outcome tuple \(\boldsymbol {g}= (g_1,\dots ,g_{k+1})\),

   \[ \widehat G^{x_1}_{g_1}\cdots \widehat G^{x_{k+1}}_{g_{k+1}} = \widehat G^{x_1}_{g_1} \bigl( \widehat G^{x_2}_{g_2}\cdots \widehat G^{x_{k+1}}_{g_{k+1}} \bigr), \]

   and the right half-sandwich analogously rotates the head to the tail.

2. Sum-of-adjoint-products bounds. For every \(r\ge 0\) and \({\boldsymbol {x}}= (x_1,\dots ,x_r) \in \mathbb {F}_q^r\),

   \[ \sum _{g_1,\dots ,g_r} \bigl(\widehat G^{x_1}_{g_1} \cdots \widehat G^{x_r}_{g_r}\bigr)^\dagger \bigl(\widehat G^{x_1}_{g_1} \cdots \widehat G^{x_r}_{g_r}\bigr) \; \le \; I, \]

   and the same bound holds for the reverse-order product family.

3. Generic tensor contraction. If families \(\{ A_a\} _a\) and \(\{ B_b\} _b\) satisfy \(\sum _a A_a^\dagger A_a \le I\) and \(\sum _b B_b^\dagger B_b \le I\), then

   \[ \sum _{a,b} (A_a \otimes B_b)^\dagger (A_a \otimes B_b) \le I. \]

Let \(A=\{ A_a\} \) be a measurement that is \(\zeta \)-strongly self-consistent, and let \(B=\{ B_a\} \) be a submeasurement such that \(A_a \otimes I \approx _\delta B_a \otimes I\). Writing \(B=\sum _a B_a\), one has

The local-variance bound for the point measurements is

Let \(\lvert \psi _{\mathrm{bi}} \rangle \) be a bipartite state on \(\iota \otimes \iota \). If \(x_1,\dots ,x_k\) are sampled independently and uniformly from \(\mathbb {F}_q\), then

where

In the nontrivial-regime pasting context of Definition 9.3,

Let \(G \in \mathrm{PolySub}(m,q,d)\). On the axis-parallel line-test distribution,

Write

where \(\lvert \varphi _\perp \rangle \) is orthogonal to \(\lvert \varphi _0 \rangle \). Then

Let \(G \in \mathrm{PolySub}(m,q,d)\). On the uniform distribution over independent \(u,v \in \mathbb {F}_q^m\),

A symmetric projective strategy \((\psi ,A,B,L)\) is \((\varepsilon ,\delta ,\gamma )\)-good if and only if the following hold on the relevant test distributions:

Let \(H\) be any polynomial-valued submeasurement. Suppose that the pointwise evaluations of \(H\) are consistent with Alice’s point measurement with error \(\nu \), and that \(H\) has the lower mass bound used in Corollary 9.44. Then completing \(H\) at the fallback polynomial preserves point consistency with the enlarged error appearing in the induction statement.

Let \(H\) be any polynomial-valued submeasurement. Suppose that the strategy is good, that \(\gamma ,\zeta \ge 0\), that \(k \ge 1\), and that the restriction of \(H\) to every vertical line is consistent with the vertical-line measurement with error \(\nu _6\). Then the pointwise evaluations of \(H\) are consistent with Alice’s point measurement with error \(\nu \).

The pasted submeasurement satisfies

where

Let

be a two-space projective strategy passing the low individual degree test with error at most \(\varepsilon \). The heterogeneous role-register construction on

produces a symmetric strategy that is \((3\varepsilon ,3\varepsilon ,3\varepsilon )\)-good.

Let \(\psi \) be a normalized bipartite state on \(\mathcal H_{\mathrm A}\otimes \mathcal H_{\mathrm B}\), let \(M^{\mathrm A}\) and \(M^{\mathrm B}\) be projective measurements on the two prover spaces with a common outcome type, and let \(G\) be an arbitrary measurement on the heterogeneous role-register space

After applying the direct-sum role-register symmetrization, the consistency defect between the symmetrized point measurement and \(G\) is the average of the two defects obtained from the occupied principal blocks of \(G\). In particular, each extracted defect is at most twice the symmetrized defect.

In the nontrivial-regime pasting context of Definition 9.3, set

Then, on average over \((u,x) \sim \mathbb {F}_q^{m+1}\),

In the nontrivial-regime pasting context of Definition 9.3, there exists a submeasurement \(H \in \mathrm{PolySub}(m+1,q,d)\) with the following properties.

1. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^{m+1}\),

   \[ A_a^u \otimes I \simeq _\nu I \otimes H_{[h(u)=a]}. \]

2. (Completeness): If \(H = \sum _h H_h\), then

   \[ \langle \psi \rvert H \otimes I \lvert \psi \rangle \ge 1 - \kappa \left(1+\frac{1}{100m}\right) - \nu - e^{-k/(80000m^2)}. \]

For any \(1 \le i \le k\),

where

The formalization records the point-to-vertical-line state-dependent-distance estimate with the vertical-line side written as the submeasurement family liftedVerticalLineAnswerFamily. The error term is the same \(8m\varepsilon +4\delta \) as in the complete measurement-valued construction.

Replacing distinct tuples by independent tuples costs the total-variation error \(k^2/q\) from Proposition 9.8. After averaging over \(u\) and \(\mathbf{x}\sim \mathsf{Distinct}_k\), the expected bad mass and the expected pasted interpolation defect are bounded by the one-point sandwich error:

and consequently

where \(\nu _5 = 43km(\varepsilon ^{1/32}+\dots +(d/q)^{1/32})\) (Lemma 9.30). Using \(1/q \le (d/q)^{1/32}\) and \(m\ge 1\), this is further bounded by \(44k^2m(\varepsilon ^{1/32}+\delta ^{1/32}+\gamma ^{1/32}+\zeta ^{1/32}+(d/q)^{1/32})\) as used in Lemma 9.31.

If the tuple of completed slices does not interpolate to the sampled vertical-line value, then some active coordinate witnesses a line-value mismatch. Concretely, for every direction \(u\) and injective tuple \(\mathbf{x}=(x_1,\dots ,x_k)\), let \(\widehat{H}^{\mathbf{x}}\rvert _u\) be the vertical-line restriction of the pasted interpolation family. Then

where \(\operatorname {Defect}_\psi (A,B)\) denotes the bipartite consistency defect \(\max \bigl(0,\, \langle \psi \rvert A_{\mathrm{tot}}\otimes B_{\mathrm{tot}}\lvert \psi \rangle - \sum _a \langle \psi \rvert A_a\otimes B_a\lvert \psi \rangle \bigr)\),

and \(\widehat{H}^{(i)},B^{(i)}\) are the one-point line comparison families (Lemma 9.30) restricted to coordinate \(i\), and \(\operatorname {Bad}(\psi ;u,\mathbf{x})\le 1\).

Define

Then

For every family \(\{ A^u\} \),

Let \(G \in \mathrm{PolySub}(m,q,d)\). On the hypercube edge distribution \((u,v) \sim C\),

Paper origin: references/ldt-paper/orthonormalization.tex lines 534–860 (rank reduction and the \(Q\)-side setup, including 4.28 and 4.29) and 862–1194 (the \(X/\widehat X/P\) algebra: 4.30, 4.33, 4.34, 4.36, 4.37, 4.38, plus the final triangle-inequality calculation producing the \(84\zeta ^{1/4}\) bound). Together these are the late repair stage of the orthogonalization-lemma proof.

Given a normalized bipartite state \(\lvert \psi \rangle \), a measurement \(A = \{ A_a\} \), and the source almost-projective estimate for the left-lifted family \(\{ A_a \otimes I\} \), there exists a locality-preserving projective sub-measurement with error \(84\zeta ^{1/4}\).

More precisely, if \(\lvert \psi \rangle \) is a normalized bipartite state, if \(A = \{ A_a\} \) is a measurement, and if

then there exists a projective sub-measurement \(P = \{ P_a\} \) on the underlying space such that

The locality-preserving form – output \(P_a \otimes I\) rather than an arbitrary lifted family – is recorded in Remark 4.11 and is the form required by the unconditional orthonormalization theorem (4.4).

For every real number \(0 \le \lambda \le 1\),

For a two-space projective strategy passing the low individual degree test with error \(\varepsilon \), the role-register symmetrization is \((3\varepsilon ,3\varepsilon ,3\varepsilon )\)-good. Under the corrected hypothesis \(k\ge 400md\), Theorem 10.14 therefore supplies the Section 6 polynomial measurement used in the final theorem route.

Under the hypotheses of Theorem 10.14 with \(m=1\), there exists a measurement \(G \in \mathrm{PolyMeas}(1,q,d)\) such that, on average over \(u \sim \mathbb {F}_q\),

which is stronger than the bound required by Theorem 10.14 for \(m=1\). Lean also proves the same one-dimensional construction for the answer-valued strategy interface used by the recursive-slice route.

If the target error parameter in Theorem 10.14 is at least \(1\), then the conclusion follows from a distinguished trivial polynomial measurement. Lean also proves the same large-error branch for the answer-valued strategy interface used by the recursive-slice route.

Let \(A = \{ A_a\} \) be a sub-measurement with \(k\) distinct outcomes \(a \in \mathcal A\), and let \(\lvert \mathsf{aux} \rangle \in \mathbb {C}^{k+1}\) be any state. Then there exists a projective sub-measurement \(\widehat{A} = \{ \widehat{A}_a\} \) such that for each outcome \(a\),

Let \(P=\{ P_a\} \) be a sub-measurement and \(Q=\{ Q_b\} \) be a projective sub-measurement. Define \(C_{a,b}=Q_b P_a Q_b\). Then

Given the completed-measurement self-consistency and commutation estimates from Corollary 9.23, the following one-step estimates hold.

1. Self-consistency step. For every \(r\ge 0\),

   \[ \mathbb {E}_{x,y,z}\mathbb {E}_{x_1,\dots ,x_r} \sum _{g} \bigl\| \bigl(\widehat G^{z}_g \otimes I - I \otimes \widehat G^{z}_g\bigr) \lvert \psi \rangle \bigr\| ^2 \; \le \; 2\zeta . \]

2. Commutation step. For every \(r\ge 0\),

   \[ \mathbb {E}_{x,y}\mathbb {E}_{x_1,\dots ,x_r} \sum _{g,h}\sum _{g_1,\dots ,g_r} \bigl\| \bigl( \widehat G^{x}_g \widehat G^{y}_h \otimes \widehat G^{x_r}_{g_r}\cdots \widehat G^{x_1}_{g_1} - \widehat G^{y}_h \widehat G^{x}_g \otimes \widehat G^{x_r}_{g_r}\cdots \widehat G^{x_1}_{g_1} \bigr) \lvert \psi \rangle \bigr\| ^2 \; \le \; \nu _3. \]

3. Two-factor base case. For \(k=2\), the commutation chain reduces to the same tensor-placement convention with the reverse tail product equal to the identity, hence to the pairwise estimate \(\nu _3\).

4. Split equivalences. The half-sandwich families are equivalent, under the head–tail reindexing of Lemma 9.25, to the chain-families used in the move estimates above, with ordered products on the first tensor factor and reverse products on the second tensor factor where these appear in the commutation step.

These are the elementary building blocks assembled by the recursive chain construction in the following lemma.

Let \(\lvert \psi \rangle \) be a state, and let \(A = \{ A_a\} \) and \(B = \{ B_a\} \) be measurements such that

on state \(\lvert \psi \rangle \). Here \(\lvert \psi \rangle \) is not assumed to be permutation-invariant. Then there exists a projective sub-measurement \(P = \{ P_a\} \) such that

This same-space corollary weakens Lemma 4.9 to the public orthonormalization envelope \(100\zeta ^{1/4}\). Thus, if \(A=\{ A_a\} \) and \(B=\{ B_a\} \) are measurements on the same finite-dimensional space satisfying

on a normalized bipartite state \(\lvert \psi \rangle \), then there exists a projective sub-measurement \(P=\{ P_a\} \) such that

This is the corrected Lean theorem proved from the Section 5 projectivization repair construction. The sharper heterogeneous source statement \(84\zeta ^{1/4}\) is now formalized as Lemma 4.9.

If \(x_1,\dots ,x_k\) are sampled independently and uniformly from \(\mathbb {F}_q\), then

where

\(P = \{ P_a\} \) forms a projective sub-measurement.

For each \(a\),

The nontrivial-regime pasting context specializes the consistency of \(H\) with \(A\) and the conversion from the pasted sum to the polynomial in \(G\) to the parameters and error bounds fixed in Definition 9.3.

Let \(g, g' : \mathrm{Polynomial}\, \mathrm{params}\) be two distinct full polynomial outcomes with individual degrees at most \(d\). Then

This packages the \(md/q\) loss term used in the mainFormal self-consistency cascade (inductive_step.tex, lines 119–133) and in comMain (commutativity-G.tex).

There exists a set of projection matrices \(\{ Q_a\} \) such that

and

Furthermore,

There exists a set of projective matrices \(\{ R_a\} \) such that

and

For every \(x \in \mathbb {F}_q\), the squared-distance defect of the one-outcome complete part is bounded by that of the original slice submeasurement:

where \(G^x = \sum _g G^x_g\) is the total operator of the slice submeasurement.

For each \(a\),

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m+1,q,d)\) test. For each \(x \in \mathbb {F}_q\), let \((\psi ,A^x,B^x,L^x)\) be the restricted strategy and let \(\varepsilon _x,\delta _x,\gamma _x\) be its three failure probabilities. Then

Let \((\psi ,A^{\mathrm A},B^{\mathrm A},L^{\mathrm A},A^{\mathrm B},B^{\mathrm B},L^{\mathrm B})\) be a projective strategy on two local spaces passing the \((m,q,d)\) low individual degree test with probability at least \(1-\varepsilon \). Adding a role register and placing the two local spaces in the direct sum \(H_{\mathrm A}\oplus H_{\mathrm B}\) yields a symmetric projective strategy that is \((3\varepsilon ,3\varepsilon ,3\varepsilon )\)-good.

If \(g,h \in \mathcal{P}(m,q,d)\) are distinct, then

Let \(g, h:\mathbb {F}_q^m \rightarrow \mathbb {F}_q\) be two distinct polynomials of total degree \(d\). Then

Let

Then the primal is

and the dual is

These semidefinite programs are dual to each other. Moreover there is an optimal pair of solutions \(\{ T_g\} \) to 25 and \(Z\) to 26 such that \(\sum _g T_g = I\) and

In every concrete matrix realization, the uniform family \(T_g=(2|\mathcal{P}(m,q,d)|)^{-1}I\) has total mass \((1/2)I\). The dual operator \(Z=2I\) dominates the identity and satisfies \(Z-A_g\geq I\), hence \(Z\geq A_g\), for every polynomial \(g\). In the canonical block SDP, the corresponding block matrix is feasible, its slack block is \((1/2)I\), and the canonical dual slack for the same dual witness also dominates the block identity. More generally, dual feasibility implies positivity of \(Z\), since the averaged point operators \(A_g\) are positive semidefinite.

From a matrix-level strong-duality witness with complementary slackness of the shape asserted by Lemma 7.8, one obtains a complete measurement \(\{ T_g\} \), a feasible dual operator \(Z\), equality of the primal and dual objectives, and the equations \(T_gZ=T_gA_g\) for all \(g\). Lean isolates the saturated canonical optimal-pair output required from strong duality: a feasible canonical primal matrix, a dual-feasible operator with equal objective value, canonical complementary slackness, and vanishing of the extra canonical slack block. This datum gives the matrix-level slackness-carrying SDP statement, whose witness is already a complete matrix measurement, and is then transported to the abstract Section 9 statement without assuming \(I \le Z\). The displayed measurement witness is read directly from that abstract statement. The canonical saturation datum is now the only matrix-level input used to pass from strong duality to the abstract SDP statement. The paper-facing self-improvement helper consumes the resulting abstract SDP statement.

The uniform primal family \(T_g=(2|\mathcal{P}(m,q,d)|)^{-1}I\) has total mass \((1/2)I\), and the dual operator \(Z=2I\) is positive semidefinite and dominates the identity.

Let \(A=\{ A_a\} \) be a \(\zeta \)-strongly self-consistent submeasurement. Then

Let \(G \in \mathrm{PolyMeas}(m,q,d)\) be a measurement with the following property:

1. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^{m}\),

   \[ A^{u}_a \otimes I \simeq _{\nu } I \otimes G_{[g(u)=a]}. \]

Let

Then there exists \(H \in \mathrm{PolySub}(m,q,d)\) with the following properties:

1. (Completeness): If \(H = \sum _h H_h\), then

   \[ \langle \psi \rvert H \otimes I \lvert \psi \rangle \geq (1-\nu )-\zeta . \]

2. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^m\),

   \[ A^u_a \otimes I \simeq _{\zeta } I \otimes H_{[h(u) = a]}. \]

3. (Strong self-consistency):

   \[ \sum _{h} \langle \psi \rvert H_h \otimes H_h \lvert \psi \rangle \geq \langle \psi \rvert H \otimes I \lvert \psi \rangle - \zeta . \]

4. (Boundedness): There exists a positive-semidefinite matrix \(Z\) such that

   \[ \langle \psi \rvert Z \otimes I \lvert \psi \rangle -\mathbb {E}_{u} \sum _a \langle \psi \rvert A^{u}_{a} \otimes H_{[h(u)=a]} \lvert \psi \rangle \leq \zeta \]

   and for each \(h \in \mathcal{P}(m,q,d)\),

   \[ Z \geq \left(\mathbb {E}_{u} A^{u}_{h(u)}\right). \]

Let \(f : \alpha \to \mathbb {R}\) be a function on a finite index set \(\alpha \) with \(|\alpha | = r\), and let \(L \subseteq \alpha \) with \(|L| = d\) and \(d {\lt} r\). Write \(S = L^\complement \) and assume \(f(s) \leq f(l)\) for every \(s \in S\) and \(l \in L\). Then the pairwise double-counting inequality

holds, and hence also

If in addition \(r \leq (1+2\sqrt{\zeta })\, d\), \(\sum _{x \in \alpha } f(x) \leq 1 + 2\sqrt{\zeta }\), and \(0 \leq \zeta \leq 1/4\), then

After one commutation of a \(G\)-factor through an auxiliary projective family, the two fourth-term contractions are bounded by the same self-consistency and commutation errors used in the switcheroo argument.

For any \(x \in [0, 1]\),

Each \(S_{\tau _{\ge \ell }}\) is Hermitian, positive semidefinite, and bounded by \(I\). Moreover, if \(\tau _{{\gt}\ell }\) is a tail type of length \(k-\ell \), then

Restricting an interpolated polynomial to a vertical line and then postprocessing at a point agrees with evaluating the corresponding slice. The same identities commute with averaging over indexed submeasurements.

The weighted bounds from Lemma 10.3 imply the restricted-probability data used in the successor step.

For each \(a\),

For each \(a\),

For \(u \in \mathbb {F}_q^m\), the last-direction axis-parallel line in \(\mathbb {F}_q^{m+1}\) is

If \((\psi ,A,B,L)\) is a symmetric strategy for the \((m+1,q,d)\) low individual degree test, we write \(B_f^u\) for the operator \(B_f^{\ell _u}\). For a function \(f \colon \ell _u \to \mathbb {F}_q\), we also write \(f(x)\) for \(f(u,x)\).

Let \(\{ A^x_a\} \), \(\{ B^x_a\} \), and \(\{ C^x_{a,b}\} \) be matrices. Suppose that \(A^{x}_a \approx _\delta B^{x}_a\) and that for all \(x\) and \(a\),

Then

Let \(\{ A^x_a\} \), \(\{ B^x_a\} \), and \(\{ C^x_{a,b}\} \) be matrices. Suppose that \(A^x_a \approx _\gamma B^x_a\) and that for all \(x\),

Then

Similarly, suppose that \((A^x_a)^\dagger \approx _\gamma (B^x_a)^\dagger \) and that for all \(x\),

Then

Let \(A=\{ A_a^x\} \) be a submeasurement and \(P=\{ P_a^x\} \) a projective submeasurement such that \(A_a^x \otimes I \approx _\varepsilon P_a^x \otimes I\). Then

Let \(A\) be a \(\delta \)-strongly self-consistent submeasurement and let \(B\) be a submeasurement such that \(A_a^x \otimes I \approx _\varepsilon B_a^x \otimes I\). Then

Let \(A=\{ A_a\} \) be a measurement that is \(\zeta \)-strongly self-consistent, let \(B=\{ B_a\} \) be a submeasurement such that \(A_a \otimes I \approx _\delta B_a \otimes I\), and let \(C\) be the measurement obtained by adding the missing mass \(I-B\) to one distinguished answer \(a^*\). Then

Let \(A=\{ A_a^x\} \) be a submeasurement and \(B=\{ B_a^x\} \) a measurement such that \(A_a^x \otimes I \simeq _\gamma I \otimes B_a^x\). Then

where \(A^x=\sum _a A_a^x\). In particular,

This is the same statement as Lemma 3.40: for a \(\zeta \)-strongly self-consistent submeasurement \(A\),

Let \(A = \{ A^x_a\} \), \(B = \{ B^x_a\} \), and \(C = \{ C^x_a\} \) be submeasurements such that \(A^x_a \approx _{\delta } B^x_a\). Then

For each \(\alpha \in \mathbb {F}_q^m\), define

Then the following two statements hold.

1. The \(\lvert \varphi _\alpha \rangle \)’s form an orthonormal basis of \(\mathbb {C}^V\).

2. For each \(\alpha \in \mathbb {F}_q^m\), \(\lvert \varphi _\alpha \rangle \) is an eigenvector for \(K\) with eigenvalue \(\frac{1}{M} \cdot \frac{m-|\alpha |}{m}\), where \(|\alpha |\) is the number of nonzero coordinates of \(\alpha \).

Let \(a \in \mathbb {F}_q\). Then

Let \(v \in \mathbb {F}_q^m\). Then

The Laplacian can be written as

If \(x=(x_1,\dots ,x_k)\) is uniformly random in \(\mathbb {F}_q^k\) and \(y=(y_1,\dots ,y_k)\) is uniformly random in \(\mathsf{Distinct}_k\), then

The Lean theorem MIPStarRE.LDT.Test.classicalTestSoundness is a conditional corollary of the quoted Polishchuk–Spielman theorem. It assumes the modeled deterministic low individual degree test pass condition MIPStarRE.LDT.Test.TwoProverClassicalLIDPassCondition and a specialized external hypothesis MIPStarRE.LDT.Test.PolishchukSpielmanClassicalSoundnessStatement at the caller’s chosen slack bound. Under these hypotheses it returns a repository polynomial whose evaluations agree with the point answers up to that slack.

This proposition records the saturated-error reduction for the corrected two-space theorem Theorem 2.14. It proves the saturated-error branch by the trivial consistency bound and reduces the remaining non-vacuous branch to Proposition 2.16. It is not an additional hypothesis of the paper theorem.

This is the non-vacuous branch of the corrected two-space theorem. It proves the conclusions of Theorem 2.14 under \(k\ge 400md\), \(k{\gt}0\), and \(\nu {\lt}1\). It is not a source assumption. Its proof uses the two-space role-register reduction and the scalar absorption available after excluding the zero-sampling boundary.

The printed final theorem starts from a projective strategy on two possibly different local Hilbert spaces. The source proof uses the role-register symmetrization and then unsymmetrizes the polynomial measurement. Lean formalizes this reduction for the general two-space source strategy. The trace-level factor-two unsymmetrization estimate for arbitrary heterogeneous role-register measurements is formalized in Lemma 2.7. The heterogeneous role-register symmetrization may be fed into the source-shaped main-induction theorem under the corrected large-\(k\) hypothesis \(k\ge 400md\), and the resulting role-register consistency estimate can be unsymmetrized into the two point-consistency estimates on the original two-space strategy with the expected factor \(2\).

The remaining steps of the source-boundary passage are also checked. The point-agreement branch is available for the paper-faithful two-space strategy, and the Schwartz–Zippel Step 5 theorem has been generalized from the same-space carrier to a bipartite state on \(H_A\otimes H_B\). The heterogeneous triangle/SDD comparison theorem gives the complete-measurement full-polynomial consistency statement at the end of the paper’s Step 5 calculation. The two heterogeneous orthonormalization applications produce projective submeasurements on the two local Hilbert spaces, and the completion step widens the resulting left- and right-factor state-dependent-distance estimates to the orthonormalize-and-complete error appearing in the paper. The repaired polynomial line-169 consistency relations use the Cauchy–Schwarz loss from the pre-completion orthonormalization estimates, not a new hypothesis. The final point-evaluation triangle postprocesses these relations and the completed \(Q_A,Q_B\) projective consistency estimate by evaluation at a point, combines them by the heterogeneous triangle inequality, and absorbs the explicit pre-absorption errors into the final \(\nu =\texttt{mainFormalError}\) bound under the nonzero scalar-cascade boundary \(0{\lt}k\). This is the small-error branch used in the corrected two-space source theorem, where \(k{\gt}0\) is part of the theorem statement.

The restricted slice strategy is represented in Lean by an answer-valued strategy. The slice self-improvement data are constructed directly: replace only the diagonal part by an inert ordinary covariant measurement and apply the induction-section self-improvement theorem in the form whose hypotheses are the axis-parallel and point self-consistency estimates. Since the Section 9 conclusion is independent of the diagonal-line error parameter, no low-degree support theorem for the answer-valued diagonal outcomes is needed for this step. Such a support theorem would still be necessary for the stronger route which realizes the answer-valued diagonal measurement as an ordinary polynomial-valued covariant measurement, but that realization is not used here.

After the recursive answer-valued slice measurements and the slice-wise self-improvement outputs have been averaged, Lean has a polynomial family which is complete, point-consistent with the actual answer-valued point measurement, strongly self-consistent, and bounded by the witnesses obtained from self-improvement. The boundedness input is presently typed through the point-equivalent ordinary carrier, because the existing boundedness interface for pasting is an ordinary-strategy interface.

The final induction-section pasting invocation is proved by first deriving the answer-valued Section 10 point-commutativity estimate from the answer-valued diagonal-line verifier relation, then invoking the Section 11 scalar chain in the form which assumes this point-commutativity estimate. The proof does not replace the answer-valued strategy by the ordinary carrier for the diagonal-line test; the carrier is used only for the ordinary boundedness interface. This construction is therefore a Lean-only internal construction for the simultaneous successor proof, not a new hypothesis of Theorem 10.14 and not a replacement for Theorem 10.8.

In the small-error successor branch, the proof must apply the induction hypothesis in dimension \(m\) to the restricted strategies indexed by \(x\in \mathbb F_q\), with the same integer \(k\). The successor large-\(k\) hypothesis implies the predecessor large-\(k\) side condition in the corrected formal interface, and the nontrivial small-error branch supplies \(k\ge 1\). This is the genuine recursive use of the theorem; it is not an additional hypothesis on the successor strategy. The answer-valued restriction map for an answer-valued successor strategy is now explicit in Lean; it preserves the full function-valued diagonal answer on the slice, so it does not use the ordinary low-degree realization that is unavailable for arbitrary answer-valued diagonal measurements. The corresponding restricted-probability theorem for answer-valued successor strategies is also checked: the axis-parallel and diagonal slice averages are derived from the ambient answer-valued goodness assumptions, and the diagonal calculation uses the full function-valued answer rather than an ordinary polynomial-valued realization. Lean now also checks the recursive application itself: after these restricted probabilities are constructed, the predecessor answer-valued induction hypothesis gives the main-induction conclusion for every answer-valued restricted slice. The theorem answerMainInduction now supplies this predecessor hypothesis by strong induction on the dimension. Thus the predecessor induction argument is a checked internal construction, not an additional theorem hypothesis.

This is the nontrivial successor branch in the corrected large-\(k\) induction interface. The ordinary successor theorem now reduces to the internal answer-valued induction theorem. That theorem supplies the predecessor induction argument for the restricted slices by a genuine strong induction on the dimension. The answer-valued pasting invocation is recorded in Proposition 10.18, and the answer-valued self-improvement construction is checked by Proposition 10.17. This is a construction internal to the proof, not an assumption of Theorem 10.14. The recursive slice route applies also when \(d=0\); the successor reduction no longer needs a separate degree-zero family construction.

The paper theorem 4.4 is proved in Lean with the \(100\zeta ^{1/4}\) constant. The declaration checked here is the completion-route theorem with the weaker bound \(120\zeta ^{1/4}\), recorded in orthonormalizationCompletionRouteError. See [ con26a ] .

Let \(\lvert \psi \rangle \) be a normalized permutation-invariant state, and let \(A=\{ A_a\} _{a\in \mathcal A}\) be a sub-measurement which is bipartite strongly self-consistent with error \(\zeta \). Then there exists a projective sub-measurement \(P=\{ P_a\} _{a\in \mathcal A}\) such that

This is the self-consistency specialization of Proposition 4.13. Let \(\lvert \psi \rangle \) be a normalized bipartite state, let \(A=\{ A_a\} \) be a measurement, and let \(0\leq \zeta \). If \(A\) is bipartite strongly self-consistent with error \(\zeta \), then there exists a projective sub-measurement \(P=\{ P_a\} \) such that

This is the same-space measurement corollary recorded in Remark 4.11. Let \(\lvert \psi \rangle \) be a normalized bipartite state, let \(A=\{ A_a\} \) and \(B=\{ B_a\} \) be measurements on the same finite-dimensional space, and let \(0 \leq \zeta \). Assume the bipartite consistency estimate

Then there exists a projective sub-measurement \(P=\{ P_a\} \) such that

If \(A\) is \(\delta \)-strongly self-consistent, then \(A_a^x \otimes I \simeq _\delta I \otimes A_a^x\). If \(A\) is a measurement, the converse also holds.

Let \(A=\{ A_a\} _{a \in \mathcal A}\) be a family of operators and let \(f\colon \mathcal A \to \mathcal B\). Then

Consequently, if \(\{ A_a\} \) is a submeasurement, respectively a measurement, then \(\{ A_{[f(a)=b]}\} \) is again a submeasurement, respectively a measurement.

Let \(A\) be a \(\delta \)-strongly self-consistent submeasurement and let \(P\) be a projective submeasurement such that \(P_a^x \otimes I \approx _\varepsilon A_a^x \otimes I\). Then for every function \(f\),

If \(A=\{ A_a^x\} \) and \(B=\{ B_a^x\} \) are measurements such that \(A_a^x \otimes I \simeq _\delta I \otimes B_a^x\), and \(f\) is a map on the answer set, then

If \(A=\{ A_a^x\} \) and \(B=\{ B_a^x\} \) are measurements, then

If \(A\) and \(B\) are measurements and \(A_a^x \otimes I \simeq _\delta I \otimes B_a^x\), then

If both measurements are projective, the converse also holds: if \(A_a^x \otimes I \approx _{2\delta } I \otimes B_a^x\) then \(A_a^x \otimes I \simeq _\delta I \otimes B_a^x\).

Suppose \(A_a^x \otimes I \simeq _\varepsilon I \otimes B_a^x\), \(C_a^x \otimes I \simeq _\delta I \otimes B_a^x\), and \(C_a^x \otimes I \simeq _\gamma I \otimes D_a^x\), where all four families are measurements. Then

Suppose \(A=\{ A_a^x\} \) is a projective submeasurement satisfying

Then for every operator \(B\) with \(0 \le B \le I\),

Suppose \((A_i)_a^x \approx _{\delta _i} (A_{i+1})_a^x\) for \(i=1,\dots ,k\). Then

For vectors \(\lvert \psi _1 \rangle ,\dots ,\lvert \psi _k \rangle \),

Let \(A=\{ A_a^x\} \) and \(B=\{ B_a^x\} \) be measurements and let \(C=\{ C_a^x\} \) be a submeasurement. If \(A_a^x \otimes I \simeq _\delta I \otimes C_a^x\) and \(A_a^x \otimes I \approx _\varepsilon B_a^x \otimes I\), then

If \(A\) is \(\delta \)-strongly self-consistent, then

If \(A\) is projective, the converse also holds.

If \(A\) is \(\delta \)-strongly self-consistent and \(f\) is a function on its answer set, then

Suppose Provers \(\mathrm{A}\) and \(\mathrm{B}\) pass the low individual degree test with probability \(1-\varepsilon \). Then there exists a polynomial \(g \colon \mathbb {F}_q^m \to \mathbb {F}_q\) with individual degree \(d\) such that

Here \(a\) denotes the prover’s point answer.

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m+1,q,d)\) low individual degree test. Let \(\{ G^x\} _{x \in \mathbb {F}_q}\) denote a set of projective sub-measurements in \(\mathrm{PolySub}(m,q,d)\) with the following properties:

1. (Consistency with \(A\)) On average over \((u,x) \sim \mathbb {F}_q^{m+1}\),

   \[ A_a^{u,x} \otimes I \simeq _\zeta I \otimes G^x_{[g(u)=a]}. \]

2. (Strong self-consistency) On average over \(x \sim \mathbb {F}_q\),

   \[ G_g^x \otimes I \approx _\zeta I \otimes G_g^x. \]

3. (Boundedness) There exists a positive-semidefinite matrix \(Z^x\) for each \(x \in \mathbb {F}_q\) such that

   \[ \mathbb {E}_x \langle \psi \rvert (I-G^x) \otimes Z^x \lvert \psi \rangle \le \zeta \]

   and for each \(x \in \mathbb {F}_q\) and \(g \in \mathcal{P}(m,q,d)\),

   \[ Z^x \ge \left(\mathbb {E}_u A_{g(u)}^{u,x}\right). \]

Let

Then on average over independent and uniformly random \((u,x),(v,y) \sim \mathbb {F}_q^{m+1}\),

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m,q,d)\) low individual degree test. On average over independent and uniformly random \(u,v \sim \mathbb {F}_q^m\),

Assume the standing hypotheses and

Let \(\sigma ,\zeta _1,\zeta _2,\zeta _3\) be the cascade quantities defined above. Then

and the concrete quantity

also satisfies

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m+1,q,d)\) low individual degree test. Let \(\{ G^x\} _{x \in \mathbb {F}_q}\) be projective submeasurements in \(\mathrm{PolySub}(m,q,d)\) with the following properties:

1. (Completeness): If \(G = \mathbb {E}_x \sum _g G_g^x\), then

   \[ \langle \psi \rvert G \otimes I \lvert \psi \rangle \ge 1-\kappa . \]

2. (Consistency with \(A\)): On average over \((u,x) \sim \mathbb {F}_q^{m+1}\),

   \[ A_a^{u,x} \otimes I \simeq _\zeta I \otimes G^x_{[g(u)=a]}. \]

3. (Strong self-consistency): On average over \(x \sim \mathbb {F}_q\),

   \[ G_g^x \otimes I \approx _\zeta I \otimes G_g^x. \]

4. (Boundedness): There exists a positive-semidefinite matrix \(Z^x\) for each \(x \in \mathbb {F}_q\) such that

   \[ \mathbb {E}_x \langle \psi \rvert (I-G^x)\otimes Z^x \lvert \psi \rangle \le \zeta \]

   and for each \(x \in \mathbb {F}_q\) and \(g \in \mathcal{P}(m,q,d)\),

   \[ Z^x \ge \mathbb {E}_u A^{u,x}_{g(u)}. \]

Let \(k \ge 400md\) be an integer, and set

Then there exists a pasted measurement \(H \in \mathrm{PolyMeas}(m+1,q,d)\) with the following property.

1. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^{m+1}\),

   \[ A_a^u \otimes I \simeq _\sigma I \otimes H_{[h(u)=a]}. \]

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m+1,q,d)\) low individual degree test. Let \(\{ G^x\} _{x \in \mathbb {F}_q}\) be projective submeasurements in \(\mathrm{PolySub}(m,q,d)\) with the following properties:

1. (Completeness): If \(G=\mathbb {E}_x \sum _g G_g^x\), then

   \[ \langle \psi \rvert G \otimes I \lvert \psi \rangle \ge 1-\kappa . \]

2. (Consistency with \(A\)): On average over \((u,x) \sim \mathbb {F}_q^{m+1}\),

   \[ A_a^{u,x} \otimes I \simeq _\zeta I \otimes G_{[g(u)=a]}^x. \]

3. (Strong self-consistency): On average over \(x \sim \mathbb {F}_q\),

   \[ G_g^x \otimes I \approx _\zeta I \otimes G_g^x. \]

4. (Boundedness): There are positive semidefinite operators \(Z^x\) such that

   \[ \mathbb {E}_x \langle \psi \rvert (I-G^x) \otimes Z^x \lvert \psi \rangle \le \zeta \]

   and for each \(x \in \mathbb {F}_q\) and \(g \in \mathcal{P}(m,q,d)\),

   \[ Z^x \ge \mathbb {E}_u A_{g(u)}^{u,x}. \]

Let \(k \ge 400md\) and set

and

Then there exists a measurement \(H \in \mathrm{PolyMeas}(m+1,q,d)\) with the following property:

1. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^{m+1}\),

   \[ A_a^u \otimes I \simeq _\sigma I \otimes H_{[h(u)=a]}. \]

Let \((\psi , A^{\mathrm A}, B^{\mathrm A}, L^{\mathrm A}, A^{\mathrm B}, B^{\mathrm B}, L^{\mathrm B})\) be a projective strategy that passes the \((m,q,d)\) low individual degree test with probability at least \(1-\varepsilon \). Let \(k{\gt}0\) be an integer with \(k \ge 400md\), and set

Then there exist projective measurements \(G^{\mathrm A}, G^{\mathrm B} \in \mathrm{PolyMeas}(m,q,d)\) with the following properties:

1. on average over \(u \sim \mathbb {F}_q^m\),

   \[ A_a^{\mathrm A,u} \otimes I \simeq _\nu I \otimes G^{\mathrm B}_{[g(u)=a]}, \qquad I \otimes A_a^{\mathrm B,u} \simeq _\nu G^{\mathrm A}_{[g(u)=a]} \otimes I; \]
2. \[ G_g^{\mathrm A} \otimes I \simeq _\nu I \otimes G_g^{\mathrm B}. \]

If \(0 \le \varepsilon \), then

and \(E \ge 0\).

This is the corrected numerical form of the theorem; the paper-gap note [ con26b ] records the replacement of the printed bound \(k \ge md\) by \(k \ge 400md\). Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m,q,d)\) low individual degree test. Let \(k \ge 400md\) and set

and

Then there exists a measurement \(G \in \mathrm{PolyMeas}(m,q,d)\) such that, on average over \(u \sim \mathbb {F}_q^m\),

If \(d {\gt} 0\) and a two-prover projective strategy passes the \((m,q,d)\) low individual degree test with probability \(1-\varepsilon \), then there are global polynomial measurements whose evaluations agree with the point answers except with error \(\operatorname{poly}(m)(\operatorname{poly}(\varepsilon )+\operatorname{poly}(d/q))\).

Let \(\lvert \psi \rangle \) be a state in \(\mathcal H_{\mathrm A} \otimes \mathcal H_{\mathrm B}\). Let \(A = \{ A^x_a\} \) be a sub-measurement acting on \(\mathcal H_{\mathrm A}\) and \(B=\{ B^y_b\} \) be a sub-measurement acting on \(\mathcal H_{\mathrm B}\). Then there exist Hilbert spaces \(\mathcal H_{\mathrm A_{\mathsf{aux}}}\) and \(\mathcal H_{\mathrm B_{\mathsf{aux}}}\), a state \(\lvert \mathsf{aux} \rangle \in \mathcal H_{\mathrm A_{\mathsf{aux}}} \otimes \mathcal H_{\mathrm B_{\mathsf{aux}}}\), and projective sub-measurements \(\widehat{A} = \{ \widehat{A}^x_a\} \) and \(\widehat{B}=\{ \widehat{B}^y_b\} \) acting on \(\mathcal H_{\mathrm A} \otimes \mathcal H_{\mathrm A_{\mathsf{aux}}}\) and \(\mathcal H_{\mathrm B} \otimes \mathcal H_{\mathrm B_{\mathsf{aux}}}\), respectively, such that, if \(\lvert \widehat{\psi } \rangle = \lvert \psi \rangle \otimes \lvert \mathsf{aux} \rangle \), then for all \(x,y,a,b\),

In addition, \(\lvert \mathsf{aux} \rangle \) is a product state. The word “measurement” in the source statement is read here in the projective-submeasurement sense used by Lemma 4.7: for a general sub-measurement, the residual mass is carried by the additional \(\bot \) outcome in the auxiliary construction, so the original outcomes need not sum to the identity.

Let \(\lvert \psi \rangle \) be a permutation-invariant state, and let \(A = \{ A_a\} \) be a sub-measurement with strong self-consistency

Then there exists a projective sub-measurement \(P = \{ P_a\} \) such that

Suppose Provers \(\mathrm{A}\) and \(\mathrm{B}\) pass the \(k=2\) surface-versus-point low-degree test with probability \(1-\varepsilon \). Then there exists a degree-\(d\) polynomial \(g \colon \mathbb {F}_q^m \to \mathbb {F}_q\) such that

Here \(a\) denotes the prover’s point answer.

Let \(G \in \mathrm{PolyMeas}(m,q,d)\) be a measurement with the following properties:

1. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^{m}\),

   \[ A^{u}_a \otimes I \simeq _{\nu } I \otimes G_{[g(u)=a]}. \]

Let

Then there exists a projective submeasurement \(H \in \mathrm{PolySub}(m,q,d)\) with the following properties:

1. (Completeness): If \(H = \sum _h H_h\), then

   \[ \langle \psi \rvert H \otimes I \lvert \psi \rangle \geq (1-\nu )-\zeta . \]

2. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^m\),

   \[ A^u_a \otimes I \simeq _{\zeta } I \otimes H_{[h(u) = a]}. \]

3. (Strong self-consistency):

   \[ H_h \otimes I \approx _{\zeta } I \otimes H_h. \]

4. (Boundedness): There exists a positive-semidefinite matrix \(Z\) such that

   \[ \langle \psi \rvert Z \otimes (I - H) \lvert \psi \rangle \leq \zeta \]

   and for each \(h \in \mathcal{P}(m,q,d)\),

   \[ Z \geq \left(\mathbb {E}_{u} A^{u}_{h(u)}\right). \]

Let \((\psi ,A,B,L)\) be an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m,q,d)\) low individual degree test. Let \(G \in \mathrm{PolyMeas}(m,q,d)\) be a measurement with the following property:

1. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^m\),

   \[ A_a^u \otimes I \simeq _\nu I \otimes G_{[g(u)=a]}. \]

Let

Then there exists a projective submeasurement \(H \in \mathrm{PolySub}(m,q,d)\) with the following properties:

1. (Completeness): If \(H=\sum _h H_h\), then

   \[ \langle \psi \rvert H \otimes I \lvert \psi \rangle \ge (1-\nu )-\zeta . \]

2. (Consistency with \(A\)): On average over \(u \sim \mathbb {F}_q^m\),

   \[ A_a^u \otimes I \simeq _\zeta I \otimes H_{[h(u)=a]}. \]

3. (Strong self-consistency):

   \[ H_h \otimes I \approx _\zeta I \otimes H_h. \]

4. (Boundedness): There exists a positive semidefinite operator \(Z\) such that

   \[ \langle \psi \rvert Z \otimes (I-H) \lvert \psi \rangle \le \zeta \]

   and for each \(h \in \mathcal{P}(m,q,d)\),

   \[ Z \ge \mathbb {E}_u A_{h(u)}^u. \]

Under the standing hypotheses, if

then

Under the standing hypotheses, assume

Define

Then