claimroutineinferred_dep

Specialization preserves non-membership with high probability

Random specialization keeps cc outside the span with probability 1−O(1/q)1-O(1/q)
finishes the alignment failure estimate
Claim·§3.2 Generic spaces of characters·inside lemRandom binary subspaces are generic

Statement (paper)

For each fixed r≥1r\ge1 and each fixed evaluation set EE of size 3r+13r+1, when the entries xij∈Fx_{ij}\in F are uniform and independent, the probability that the specialized column cc lies in the column span of the specialized matrix MM over FF is at most (6r+3)/q(6r+3)/q. Consequently, by a union bound over the finitely many such sets EE (depending only on rr) and conditioning on injectivity, the alignment condition fails with probability tending to zero as d→∞d\to\infty.

In plain English

For fixed rr and a fixed evaluation set EE of size 3r+13r+1, with the entries xij∈Fx_{ij}\in F uniform and independent, the specialized column cc lies in the column span of the specialized matrix MM with probability at most (6r+3)/q(6r+3)/q. A union bound over the finitely many sets EE, together with conditioning on injectivity, shows the alignment condition fails with probability tending to zero as d→∞d\to\infty.

Why it's here

The previous claim shows cc is outside the column span of MM when the xijx_{ij} are indeterminates. Here that fact is transferred to random field values: membership would force a nonzero polynomial in the xijx_{ij} of bounded degree to vanish, and the polynomial zero bound limits this probability to Or(1/q)O_r(1/q). Since EE ranges over finitely many sets depending only on rr, the union bound finishes the failure estimate for alignment, which is the last ingredient of the lemma on generic subspaces.
Classified routine:
Direct specialization of the previous claim via the Schwartz–Zippel (DeMillo–Lipton–Schwartz–Zippel) polynomial zero bound applied to a nonzero minor, followed by a union bound over finitely many evaluation sets.

Uses

claimRandom parametrization is injective and nonproportionalclaimGeneric non-membership over function field

Used by

Nothing in the paper

Sources

PaperOpen
Section
§3.2 Generic spaces of characters
Page
—
Label
—
Line
sections/02-latent.tex:337
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Specialization via polynomial zero bound" rests on claim-lem-latent-generic-1
  • info
    inferred_dep
    outline: "Specialization via polynomial zero bound" rests on claim-lem-latent-generic-3