2 The low individual degree test
2.1 The game and its strategies
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\} \).
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\).
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.
Expand the definition of the total acceptance probability as the average of the three subtests. The axis-parallel and diagonal branches each first choose one of the two role orderings uniformly, so their branch acceptance probabilities are the corresponding averages displayed above.
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 \).
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.
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.
The assertions are the block-diagonal matrix calculations for the direct-sum and role-register operators. Positivity follows by writing each positive operator as \(C^*C\) and placing the corresponding square root in the same block decomposition.
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.
The proof is a trace-compression calculation. The \(AB\)-supported component of the symmetrized density pairs with an arbitrary role-register observable only through the principal block indexed by \((\mathrm A,\mathrm{inl})\) on the left and \((\mathrm B,\mathrm{inr})\) on the right, and similarly for the \(BA\) component. Summing over outcomes gives the average-of-two-defects identity, and nonnegativity of consistency defects gives the two factor-two consequences.
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.
The role-register state is the direct-sum version of the symmetrized state in the paper proof. The axis-parallel and diagonal branches are exactly the role averages of the original strategy, and the self-consistency branch is the original point-agreement branch. Since the test chooses among its three branches with equal probability, each branch is bounded by \(3\varepsilon \).
Throughout this work, the term strategy refers to a projective strategy, and the term symmetric strategy refers to a symmetric projective strategy.
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 \).
Using notation which will be introduced in Chapter 3 below, a symmetric strategy is \((\varepsilon ,\delta ,\gamma )\)-good if and only if it satisfies the following three conditions. For \(\ell \) and \(u\) as in the axis-parallel lines test,
And for \(\ell \) and \(u\) as in the diagonal lines test,
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)\).
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\).
2.2 Formal soundness target
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:
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; \]- \[ G_g^{\mathrm A} \otimes I \simeq _\nu I \otimes G_g^{\mathrm B}. \]
The saturated-error branch is already proved. The small-error branch is Proposition 2.16.
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 proof applies the checked two-space role-register construction and then absorbs its explicit errors into \(\nu \) at the nonzero 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 proof is the linked heterogeneous role-register chain, ending in mainFormalConclusion_ofRoleRegisterScalarBoundary. It combines the source-shaped main-induction theorem, the heterogeneous unsymmetrization estimates, the step making measurements projective on both local Hilbert spaces, the completion and line-169 consistency steps, and the final scalar absorption under the nonzero sampling boundary.
The paper states Theorem 2.14 for \(k\ge md\), while the corrected formal route uses the confirmed large-\(k\) condition \(k\ge 400md\) and a nonzero \(k\) boundary for the scalar cascade. The factor \(400\) is now treated as a statement correction, following Theorem 10.14. The other corrected final-theorem boundary is the zero-sampling case allowed when \(d=0\), since \(400md\le k\) then permits \(k=0\). At this excluded boundary the displayed final error itself collapses to \(0\); the formal calculation of this equality is linked in Lean, and the obstruction is documented in [ con26c ] .
The paper statement uses the weaker hypothesis \(k \ge md\), but the proof invokes the Section 6 pasting theorem with side condition \(k \ge 400\, md\). This side condition is not implied by \(k \ge md\). The Lean theorem therefore records the stronger large-\(k\) assumption required by the pasting step, together with the scalar-cascade boundary \(k{\gt}0\), rather than hiding the side-condition gap. The helper mainFormal_trivial_witness remains only for already-saturated branches where \(\nu \ge 1\) makes the three \(\simeq _\nu \) conclusions vacuous; it is not a replacement for the zero-sampling boundary \(k=0\) when \(md=0\). The source-boundary reduction proposition proves the saturated-error branch and delegates the non-vacuous branch to the checked small-error proposition; neither declaration is an extra hypothesis of Theorem 2.14.