claimroutine

Enlargement by injections gives equivariant map

Copies over all injections B→KB\to K give a KK-equivariant map CC on V\mathcal V
builds the ambient space and equivariant map
Claim·§3.5 Quotients and enlargement·inside lemLatent alphabet gadget with detecting noise

Statement (paper)

Let ℓ≥b+2\ell\ge b+2, K=F2ℓK=\F_2^\ell, let L\mathcal L be the set of all binary linear injections L:B→KL:B\to K, and let P=∏L∈LV0P=\prod_{L\in\mathcal L}V_0 with C~((xL)L)=∑L∈LLC‾(xL)\widetilde C((x_L)_L)=\sum_{L\in\mathcal L}L\overline C(x_L). Then the map Λ:T=∏LB→K\Lambda:T=\prod_L B\to K, Λ((bL)L)=∑LLbL\Lambda((b_L)_L)=\sum_L Lb_L, is onto, and for V=P/ker⁡Λ\mathcal V=P/\ker\Lambda the map C~\widetilde C descends to a map C:V→KC:\mathcal V\to K, with T/ker⁡ΛT/\ker\Lambda identified with KK, such that C(x+k)=C(x)+kC(x+k)=C(x)+k for all x∈Vx\in\mathcal V and k∈Kk\in K.

In plain English

For ℓ≥b+2\ell\ge b+2, take one copy of V0V_0 for each binary linear injection L:B→KL:B\to K, and let C~\widetilde C sum the images LC‾(xL)L\overline C(x_L). Then Λ:∏LB→K\Lambda:\prod_L B\to K is onto, and on the quotient V=P/ker⁡Λ\mathcal V=P/\ker\Lambda (with T/ker⁡Λ≅KT/\ker\Lambda\cong K) the map C~\widetilde C descends to C:V→KC:\mathcal V\to K satisfying C(x+k)=C(x)+kC(x+k)=C(x)+k.

Why it's here

This builds the ambient space V\mathcal V and the equivariant map CC required by the parent lemma, by combining copies of the base gadget over all embeddings of BB into KK. Surjectivity of Λ\Lambda is what lets KK be identified with T/ker⁡ΛT/\ker\Lambda, and passing to the quotient is what turns the translation action of TT on PP into the translation action of KK on V\mathcal V. The later claims use this CC to transfer the small-change bound and the detection property to the enlarged space.
Classified routine:
A direct linear-algebra verification: surjectivity holds because injections of B into K span K, and the descent of the map to the quotient follows from the equivariance of the base gadget map. It is bookkeeping inside the paper's latent-gadget construction.

Uses

Nothing else in the paper

Used by

claimEnlarged noise preserves small change probabilityclaimHigh-rank families detect with probability 3/16

Sources

PaperOpen
Section
§3.5 Quotients and enlargement
Page
—
Label
—
Line
sections/02-latent.tex:674
Leannot aligned

Phase 2 aligns this node to a Lean declaration.