Schwartz-Zippel Lemma

This file proves the Schwartz-Zippel lemma over finite fields: for a non-zero polynomial φ over ZMod p, a uniformly random point is a root with probability at most deg(φ) / p.

Main theorem

• schwartz_zippel — Pr[φ(x) = 0] ≤ deg(φ) / p for φ ≠ 0

Application

Used in KZGBatch binding proof: if the adversary outputs inconsistent openings, we extract a non-zero polynomial δ with δ(α) = 0. By Schwartz-Zippel, this happens with probability at most deg(δ) / p.

References

• [Schwartz 1980, Zippel 1979 — Probabilistic algorithms for sparse polynomials]
• [Mitzenmacher-Upfal, Probability and Computing, §7.2]

Schwartz-Zippel Lemma

theorem CatCrypt.Prob.schwartz_zippel (p : ℕ) [Fact (Nat.Prime p)] (φ : Polynomial (ZMod p)) (hφ : φ ≠ 0) : Crypto.prTrue (do let x ← Core.SPComp.sample (ZMod p) Core.SPComp.pure (decide (Polynomial.eval x φ = 0))) Core.Heap.empty ≤ ↑φ.natDegree / ↑p

The Schwartz-Zippel lemma: for a non-zero polynomial φ over ZMod p, a uniformly random point is a root with probability at most deg(φ) / p.

Proof outline:

1. Use prTrue_sample_pure_bool to convert probability to fraction
2. Bound the number of roots using Polynomial.card_roots'
3. Divide by p to get the bound

Corollary: Polynomial Identity Testing

theorem CatCrypt.Prob.poly_identity_test (p : ℕ) [Fact (Nat.Prime p)] (φ ψ : Polynomial (ZMod p)) (hne : φ ≠ ψ) : Crypto.prTrue (do let x ← Core.SPComp.sample (ZMod p) Core.SPComp.pure (decide (Polynomial.eval x φ = Polynomial.eval x ψ))) Core.Heap.empty ≤ max ↑φ.natDegree ↑ψ.natDegree / ↑p

Polynomial identity testing (direct corollary of Schwartz-Zippel): for distinct polynomials φ ≠ ψ over ZMod p, a uniformly random point satisfies φ(x) = ψ(x) with probability at most max(deg φ, deg ψ) / p.

Proof: apply schwartz_zippel to the nonzero polynomial φ - ψ, then use natDegree_add_le + natDegree_neg to bound its degree.