lemmaroutineinferred_dep

Random binary subspaces are generic

Random binary rr-dim subspaces of F3F^3 are generic as d→∞d\to\infty
shows generic subspaces exist for the gadget construction
Lemma·lem:latent-generic·§3.2 Generic spaces of characters

Statement (paper)

For each fixed r≥1r\ge1, a uniformly random binary rr-dimensional subspace of F3F^3 is generic with probability tending to one as d→∞d\to\infty.

In plain English

For each fixed r≥1r\ge1, a uniformly random binary rr-dimensional subspace of F3F^3 is generic (in the sense of Definition 3.5) with probability tending to one as d→∞d\to\infty.

Why it's here

This shows generic subspaces exist for large dd, so the later constructions can fix one. The proof models the random subspace as the image of a random matrix (xij)(x_{ij}), reduces the alignment condition to column-span membership, and then uses a polynomial zero bound with a union bound over finitely many evaluation sets to show both conditions of genericity hold with high probability.
Classified routine:
The proof is a standard probabilistic argument: the subspace is modelled as the image of a random matrix, and the genericity conditions follow from a Schwartz–Zippel-type polynomial zero bound plus a union bound over finitely many evaluation sets.

Uses

defGeneric binary subspaces of F^3

Used by

lemLatent alphabet gadget with detecting noiseclaimBase gadget change probability at most p_*claimConstruction is effective for rational p_*claimFresh isomorphisms make genericity typical

Inside the proof

claimRandom parametrization is injective and nonproportionalclaimAlignment reduces to column-span membershipclaimGeneric non-membership over function fieldclaimSpecialization preserves non-membership with high probability

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    The proof verifies the "nonproportionality condition" and "alignment condition", which are the two parts of the definition of a generic subspace.