claimroutineinferred_dep

Power saving for vanishing tests by induction

Claim·§8.2 A complete grid with generic positions·inside lemGeneric complete grid with independent coordinates

Statement (paper)

Let a nonzero polynomial in the selected coordinates with coefficients in B0B_0 be fixed, and choose representatives of its coefficients. Then on a large set of indices there is some b>0b>0, depending on the polynomial, such that the number of ordered vertex tuples (before requiring edges) at which the polynomial vanishes is at most tnN+j−bt_n^{N+j-b}.

In plain English

For a fixed nonzero polynomial in the selected coordinates over B0B_0, on a large set of indices there is b>0b>0 such that at most tnN+j−bt_n^{N+j-b} ordered tuples of NN vertices in V1V_1 and jj vertices in V2V_2 (ignoring edges) make it vanish.

Why it's here

This extends the one-vertex bound of the previous claim to whole tuples by induction on the coordinates. Each plane-locus vertex has at most tn1−bDt_n^{1-b_D} bad values and each curve-locus vertex has at most DD bad values, so the total number of vanishing tuples is a power below tnN+jt_n^{N+j}. This is the counting input that the diagonal grid choice uses to avoid every polynomial test.
Classified routine:
Follows from the one-vertex vanishing bound (claim-alg-generic-grid-1) by the standard Schwartz–Zippel/Combinatorial-Nullstellensatz-style induction on coordinates, multiplying the per-vertex exceptional counts.

Uses

claimPolynomials vanish rarely on loci

Used by

claimDiagonal grid choice avoids all tests

Sources

PaperOpen
Section
§8.2 A complete grid with generic positions
Page
—
Label
—
Line
sections/07-algebra.tex:244
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Power saving for vanishing tests by induction" rests on claim-alg-generic-grid-1