claimroutineinferred_dep

Generic non-membership over function field

Over indeterminates,

c

is not in the column span of

M

generic case before specialization

Claim·§3.2 Generic spaces of characters·inside lemRandom binary subspaces are generic

Statement (paper)

Regard the

x_{ij}

as independent indeterminates and set

L=\F_2(x_{ij})

. Then the vector

c=\bigl(\sqrt{z_1(t)z_2(t)z_3(t)}\bigr)_{t\in E}

does not lie in the

\overline L

-column span of the matrix

M

with

3r

columns and entries

M_{t,(i,j)}=t_jz_i(t)

, where

\overline L

is an algebraic closure of

L

In plain English

Treating the entries

x_{ij}

as independent indeterminates over

\F_2

, with

L=\F_2(x_{ij})

, the vector

c=(\sqrt{z_1(t)z_2(t)z_3(t)})_{t\in E}

is not in the

\overline L

-column span of the

3r

-column matrix

M_{t,(i,j)}=t_jz_i(t)

Why it's here

The previous claim reduced alignment to membership of

c

in the column span of

M

. This claim shows that membership fails in the fully generic setting, where the

x_{ij}

are indeterminates. The next claim specializes the

x_{ij}

to random field elements and uses a polynomial zero bound to show that non-membership persists with high probability.

Classified routine:

A technical step in proving that random binary subspaces are generic: non-membership in a column span over the function field, shown by a degree or independence argument on indeterminates. It is then specialized via the Schwartz–Zippel polynomial zero bound, a standard genericity technique.

Uses

claimAlignment reduces to column-span membership

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:294

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Generic non-membership over function field" rests on claim-lem-latent-generic-2