claimroutine

Random parametrization is injective and nonproportional

Random matrix entries give an injective, nonproportional map except with small probability
models the random subspace by a random matrix
Claim·§3.2 Generic spaces of characters·inside lemRandom binary subspaces are generic

Statement (paper)

Let xij∈Fx_{ij}\in F be independent and uniform, and let zi(t)=∑j=1rxijtjz_i(t)=\sum_{j=1}^r x_{ij}t_j for t∈F2rt\in\F_2^r. Then the binary linear map t↦(z1(t),z2(t),z3(t))t\mapsto (z_1(t),z_2(t),z_3(t)) from F2r\F_2^r to F3F^3 is non-injective with probability at most (2r−1)q−3(2^r-1)q^{-3}. Conditioned on injectivity, its image is a uniform binary rr-dimensional subspace of F3F^3, and the nonproportionality condition fails with probability Or(q−2)O_r(q^{-2}) apart from the event of noninjectivity.

In plain English

Pick the entries xij∈Fx_{ij}\in F independently and uniformly, and set zi(t)=∑jxijtjz_i(t)=\sum_j x_{ij}t_j. The map t↦(z1(t),z2(t),z3(t))t\mapsto(z_1(t),z_2(t),z_3(t)) from F2r\F_2^r to F3F^3 is non-injective with probability at most (2r−1)q−3(2^r-1)q^{-3}. Given injectivity, its image is a uniform binary rr-dimensional subspace, and the nonproportionality condition fails with probability Or(q−2)O_r(q^{-2}) apart from noninjectivity.

Why it's here

This lets the proof of the lemma replace a uniformly random binary subspace by the image of an explicit random matrix (xij)(x_{ij}) with independent uniform entries, at the cost of a vanishing error. Later claims, such as the specialization step via the polynomial zero bound, can then reason about the independent entries directly.
Classified routine:
Elementary counting/union bound over the 2r−12^r-1 nonzero t∈F2rt\in\F_2^r, each giving a uniform vector in F3F^3, plus the symmetry argument that a uniform random parametrization yields a uniform subspace; a standard reduction step inside the genericity lemma.

Uses

Nothing else in the paper

Used by

claimSpecialization preserves non-membership with high probability

Sources

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

Phase 2 aligns this node to a Lean declaration.