claimroutineinferred_dep

Diagonal grid choice avoids all tests

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

Statement (paper)

One can choose the grids, index by index, so that for every fixed nonzero polynomial test over B0B_0 in the selected coordinates, the test does not vanish at the limiting grid. Equivalently, for each fixed ss, the first ss tests T1,…,TsT_1,\ldots,T_s are feasible on a large set of indices, so the chosen prefix length satisfies sn≥ss_n\ge s on a large set, and each TsT_s is nonzero in the limiting grid.

In plain English

Grids can be chosen index by index so that no fixed nonzero polynomial test over B0B_0 in the selected coordinates vanishes at the limiting grid. For each fixed ss, the first ss tests T1,…,TsT_1,\ldots,T_s are feasible on a large set of indices, so the chosen prefix length satisfies sn≥ss_n\ge s there and each TsT_s is nonzero on the limiting grid.

Why it's here

The grid count from the Jensen bound is tnN+j−o(1)t_n^{N+j-o(1)}, while each of the first ss tests kills at most tnN+j−bt_n^{N+j-b} tuples, a power-saving fraction. So for large nn a complete grid avoiding all of T1,…,TsT_1,\ldots,T_s exists, and a diagonal choice over ss handles the whole countable family. This yields the algebraic independence used by the following claims.
Classified routine:
A standard diagonal argument over a countable family of polynomial tests, combining the Jensen grid count (claim-alg-generic-grid-2) with the power-saving vanishing bound (claim-alg-generic-grid-3). Each fixed test removes only a negligible fraction of the complete grids, so the counting goes through.

Uses

claimMany complete grids by JensenclaimPower saving for vanishing tests by induction

Used by

claimCurve coordinates algebraic; transcendence conclusions

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Diagonal grid choice avoids all countable tests" rests on claim-alg-generic-grid-2
  • info
    inferred_dep
    outline: "Diagonal grid choice avoids all countable tests" rests on claim-alg-generic-grid-3