1 Overview

This blueprint records the formalization plan for the low individual degree test paper of Ji, Natarajan, Vidick, Wright, and Yuen [ JNV\(^{+}\)20 ] . The paper is available as arXiv:2009.12982.

Theorem 1.1 Raz–Safra

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

\[ \mathbb {P}_{u \sim \mathbb {F}_q^m}[g(u)=a] \ge 1-\varepsilon -\operatorname{poly}(m)\cdot \operatorname{poly}(d/q). \]

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

Remark 1.2

The paper theorem is an external classical soundness input and is not used by the current low individual degree test formalization route.

Proof ▶

See Raz–Safra [RS97].

Theorem 1.3 Polishchuk–Spielman

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

\[ \mathbb {P}_{u \sim \mathbb {F}_q^m}[g(u)=a] \ge 1-\operatorname{poly}(m)\cdot \bigl(\operatorname{poly}(\varepsilon )+\operatorname{poly}(d/q)\bigr). \]

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

Remark 1.4

The paper theorem is an external classical soundness input. The nearby Lean corollary below records the specialized conditional interface currently present in the repository; it is not used to mark this source theorem as formalized.

Proof ▶

See Polishchuk–Spielman [PS94].

Proposition 1.5 Conditional Polishchuk–Spielman corollary

✓

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.

Proof ▶

The Lean proof applies the specialized external Polishchuk–Spielman hypothesis to the modeled low individual degree test pass condition.

Remark 1.6 A degree-\((d+1)\) strategy that passes with probability \(1-\frac{1}{m}\)

Fix the polynomial \(h(x_1, \ldots , x_m) = x_1^{d+1}\). Consider the following classical strategy for the degree-\(d\) low individual degree test. On a point query \(u \in \mathbb {F}_q^m\), Prover \(\mathrm{A}\) answers \(a = h(u)\). On an axis-parallel line query \(\ell = \{ u + x e_i : x \in \mathbb {F}_q\} \), Prover \(\mathrm{B}\) returns the restriction \(h\vert _{\ell }\) when \(i \neq 1\), since \(h\) is then constant along \(\ell \), and returns the zero polynomial when \(i = 1\).

The verifier certainly accepts whenever \(i \neq 1\), which happens with probability \(1 - \frac{1}{m}\). Thus the strategy passes the degree-\(d\) test with probability at least \(1-\varepsilon \) for \(\varepsilon = \frac{1}{m}\). However, Prover \(\mathrm{A}\) is answering according to a polynomial whose individual degree in the first variable is \(d+1\). By Schwartz–Zippel, any polynomial \(g\) of individual degree at most \(d\) agrees with \(h\) on at most a \(\frac{d+1}{q}\) fraction of all inputs, so

\[ \mathbb {P}_{u \sim \mathbb {F}_q^m}[g(u)=a] \le 1 - m\varepsilon + \frac{d+1}{q}. \]

This shows that the \(m\)-dependent slack in Theorems 1.3 and 1.7 is unavoidable up to polynomial factors.

Theorem 1.7 Main theorem, informal

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))\).

Proof ▶

This is the informal form of Theorem 2.14.