The Schwartz–Zippel lemma, in the form the low-degree machinery uses

Blueprint lem:schwartz-zippel: two unequal polynomials f, g : 𝔽_q^m → 𝔽_q of total degree at most d agree at a uniformly random point with probability at most d / q.

Mathlib proves the lemma for a single nonzero polynomial and a product of arbitrary finite subsets (MvPolynomial.schwartz_zippel_totalDegree, schwartz_zippel_sum_degreeOf). Everything here is the specialization the paper and the blueprint actually quote:

• the subsets are all of F, so the denominator is q ^ m rather than ∏ #(S i);
• the event is f = g rather than f - g = 0;
• the bound is stated over ℝ, which is where the low-degree machinery's error terms live.

Three forms, because three different consumers want three different shapes:

• prob_agree_le_totalDegree — the blueprint's statement, a probability over ℝ;
• prob_agree_le_individualDegree — the individual-degree variant the blueprint asks for alongside it (m * d / q, since a polynomial of individual degree d in m variables has total degree at most m * d, and this route avoids that lossy step);
• card_agree_le_of_natDegree — the univariate case as a count rather than a probability, which is the form lem:lidt-sync-transfer uses ("two distinct univariate polynomials of degree d agree at no more than d of the q points").

The ℚ≥0-valued intermediate is kept private: it is Mathlib's shape, not ours.

def MIPRE.LowDegree.agree {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (f g : MvPolynomial (Fin m) F) : Finset (Fin m → F)

The points of 𝔽_q^m at which two polynomials agree.

Equations

• MIPRE.LowDegree.agree f g = {x : Fin m → F | (MvPolynomial.eval x) f = (MvPolynomial.eval x) g}

@[simp]

theorem MIPRE.LowDegree.mem_agree {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} {f g : MvPolynomial (Fin m) F} {x : Fin m → F} : x ∈ agree f g ↔ (MvPolynomial.eval x) f = (MvPolynomial.eval x) g

theorem MIPRE.LowDegree.agree_eq_filter {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (f g : MvPolynomial (Fin m) F) : agree f g = {x ∈ Fintype.piFinset fun (x : Fin m) => Finset.univ | (MvPolynomial.eval x) (f - g) = 0}

agree f g is the zero set of f - g, in the shape Mathlib's lemma states.

theorem MIPRE.LowDegree.nnrat_prob_agree_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} {f g : MvPolynomial (Fin m) F} (hfg : f ≠ g) : ↑(agree f g).card / ↑(Fintype.card F) ^ m ≤ ↑(f - g).totalDegree / ↑(Fintype.card F)

The ℚ≥0-valued bound, straight from Mathlib, with the denominators evaluated.

theorem MIPRE.LowDegree.prob_agree_le_totalDegree {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} {f g : MvPolynomial (Fin m) F} (hfg : f ≠ g) {d : ℕ} (hf : f.totalDegree ≤ d) (hg : g.totalDegree ≤ d) : ↑(agree f g).card / ↑(Fintype.card F) ^ m ≤ ↑d / ↑(Fintype.card F)

Schwartz–Zippel (blueprint lem:schwartz-zippel): two unequal polynomials of total degree at most d in m variables over a finite field of size q agree at a uniformly random point of 𝔽_q^m with probability at most d / q.

theorem MIPRE.LowDegree.prob_agree_le_individualDegree {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} {f g : MvPolynomial (Fin m) F} (hfg : f ≠ g) {d : ℕ} (hf : ∀ (i : Fin m), MvPolynomial.degreeOf i f ≤ d) (hg : ∀ (i : Fin m), MvPolynomial.degreeOf i g ≤ d) : ↑(agree f g).card / ↑(Fintype.card F) ^ m ≤ ↑m * ↑d / ↑(Fintype.card F)

The individual-degree variant: if f ≠ g and both have degree at most d in each of the m variables separately, they agree with probability at most m * d / q.

theorem MIPRE.LowDegree.eq_of_majority_agree {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} {f g : MvPolynomial (Fin m) F} {d : ℕ} (hf : ∀ (i : Fin m), MvPolynomial.degreeOf i f ≤ d) (hg : ∀ (i : Fin m), MvPolynomial.degreeOf i g ≤ d) (hsize : 2 * (m * d) ≤ Fintype.card F) (hmajority : Fintype.card F ^ m < 2 * (agree f g).card) : f = g

The majority test used by the classical PCP. If the field has at least 2 * m * d elements, agreement at more than half the points forces polynomial equality. The strict acceptance threshold is essential when the field-size bound is an equality.

theorem MIPRE.LowDegree.eq_of_majority_subset {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} {f g : MvPolynomial (Fin m) F} {d : ℕ} (hf : ∀ (i : Fin m), MvPolynomial.degreeOf i f ≤ d) (hg : ∀ (i : Fin m), MvPolynomial.degreeOf i g ≤ d) (hsize : 2 * (m * d) ≤ Fintype.card F) (S : Finset (Fin m → F)) (hS : ∀ x ∈ S, (MvPolynomial.eval x) f = (MvPolynomial.eval x) g) (hmajority : Fintype.card F ^ m < 2 * S.card) : f = g

A verifier may impose other tests as well: agreement on any accepted set larger than half the field cube already forces the same identity.

theorem MIPRE.LowDegree.card_agree_le_of_natDegree {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {p q : Polynomial F} (hpq : p ≠ q) {d : ℕ} (hp : p.natDegree ≤ d) (hq : q.natDegree ≤ d) : {t : F | Polynomial.eval t p = Polynomial.eval t q}.card ≤ d

The univariate case, as a count: two unequal polynomials of degree at most d over a field agree at no more than d points. This is the form lem:lidt-sync-transfer uses.