claimroutine
Polynomials vanish rarely on loci
Claim·§8.2 A complete grid with generic positions·inside lemGeneric complete grid with independent coordinates
Statement (paper)
On a side whose locus is the plane, for each fixed degree bound there is a such that every nonzero polynomial of degree at most , even with coefficients depending on , vanishes at at most pruned vertices on a large set of indices. On a curve side, a nonzero polynomial of degree in the selected -coordinate has at most zeros among the vertices.
In plain English
On a plane-locus side, for each degree bound there is such that any nonzero polynomial of degree at most , even with -dependent coefficients, vanishes at no more than pruned vertices on a large set of indices. On a curve-locus side, a nonzero polynomial of degree in the selected -coordinate has at most zeros among the vertices.
Why it's here
This supplies the quantitative genericity input for choosing the grid: a nonzero polynomial test can kill only a small fraction of vertices, a power saving on planes and a bounded number on curves. Later claims use it inductively to pick grid vertices whose selected coordinates avoid every given vanishing condition, which gives algebraic independence over . The plane bound comes from the minimality of the locus, while on curves it is simply the degree bound for a one-variable polynomial.
Classified routine:
Follows from the minimality of the plane locus, i.e. vertices not concentrating on curves of bounded degree, plus the fact that a one-variable polynomial of degree D has at most D roots. This is a standard genericity/bookkeeping step inside the generic-grid construction.
Uses
Nothing else in the paper
Used by
Sources
PaperOpen
- Section
- §8.2 A complete grid with generic positions
- Page
- —
- Label
—- Line
sections/07-algebra.tex:216
Leannot aligned
Phase 2 aligns this node to a Lean declaration.