Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Schwartz zippel over finite fields

Statement

Let F be a finite field, m≥1, and f∈F[x1,…,xm] a nonzero formal polynomial of total degree d. For a nonempty subset A⊆F and independent uniform ai∈A, P(f(a1,…,am)=0)≤min⁡(1,d/∣A∣). In particular A=F gives the bound d/∣F∣. A nonzero constant has zero vanishing probability. Nonzero formal polynomials can nonetheless induce the zero function on the whole finite grid when their degree is large.

Facts & Assumptions

Given: The finite field, nonzero formal polynomial and nonempty A above. Uniform independent sampling gives mass ∣A∣−m to each tuple.

[F1]

Total degree is the largest sum of exponents of a nonzero coefficient in the unique finite monomial expansion (Monomials, coefficients, degree in each variable and total degree in F[x1,…,xn]).

[F2]

A nonzero univariate polynomial of degree r over an integral domain has at most r roots (A nonzero polynomial of degree n over an integral domain has at most n distinct roots).

[F3]

In a field every nonzero element has a multiplicative inverse and zero is distinct from one (Field).

[F4]

Successor induction proves a property for all naturals (The principle of mathematical induction).

Proof

1.1F1F2F3given

A field is an integral domain: distributivity gives a0=a(0+0)=a0+a0, so additive cancellation gives a0=0. If ab=0 and a≠0, multiply by a−1 to obtain b=0. Thus F2 applies over F. For m=1 it gives at most d roots in A, and hence probability at most d/∣A∣ and also at most one. If d=0 in any number of variables, F1 makes f a nonzero constant, with no zero evaluations.

2.1step 1.1F1given

To pass from m-1 to m for m>1, suppose the asserted root-count bound holds in m-1 variables for every nonzero polynomial. Put q=∣A∣>0. If d≥q the target minimum is one and the bound is immediate from counting at most all qm tuples. It remains to consider 0<d<q. Collect monomials by the last exponent as f=∑j=0rgjxmj with gr≠0. F1 gives deg⁡gr≤d−r, and 0≤r≤d<q.

3.1step 2.1F1F2

By the m-1 assertion the number B of base tuples in Am−1 on which gr vanishes is at most (d−r)qm−2. For the other qm−1−B tuples, specialization yields a nonzero univariate polynomial of degree exactly r, so F2 bounds its roots by r. A bad base tuple has at most q possible last coordinates, regardless of whether its specialized polynomial is zero. The total zero count is therefore Bq+(qm−1−B)r≤Bq+qm−1r≤(d−r)qm−1+rqm−1=dqm−1. For r=0 the good specializations are nonzero constants and have zero roots, exactly as this count says. Division by qm>0 gives d/q.

4.1step 1.1step 2.1step 3.1F1F3F4∎

Step 1.1 supplies the one-variable base; steps 2.1–3.1 pass the root-count bound to each next number of variables, and F4 gives it for every positive m. The case ∣A∣=1 is covered by the constant case or d≥q, so no hidden division by q-1 occurs. To see why formal nonzero is the right hypothesis, for any finite F the formal product ∏a∈F(X−a) has leading coefficient one and degree ∣F∣, yet vanishes at every element of F. This finite product needs no ordering choice: commuting factors give the same polynomial in any listing. Thus a vanishing polynomial function is compatible with the bound when degree is large.

Depends on

Used by

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources