claimroutineinferred_dep

Enlarged noise preserves small change probability

Resampling one copy keeps change probability ps≤p∗p_s\le p_*, with rational noise
gives the small-change property of the lemma
Claim·§3.5 Quotients and enlargement·inside lemLatent alphabet gadget with detecting noise

Statement (paper)

Let μ\mu be the law on V=P/ker⁡Λ\mathcal V=P/\ker\Lambda obtained by choosing a uniform L∈LL\in\mathcal L, updating only the copy of V0V_0 indexed by LL by an independent sample from ν\nu, and passing to the quotient. Then for independent uniform x∈Vx\in\mathcal V and a∼μa\sim\mu we have Pr⁡[C(x+a)≠C(x)]=ps≤p∗\Pr[C(x+a)\ne C(x)]=p_s\le p_*, which is Equation , and μ\mu is a rational probability distribution.

In plain English

Let μ\mu be the noise on V=P/ker⁡Λ\mathcal V=P/\ker\Lambda that picks a uniform injection L∈LL\in\mathcal L, resamples only the LL-indexed copy of V0V_0 from ν\nu, and passes to the quotient. Then Pr⁡[C(x+a)≠C(x)]=ps≤p∗\Pr[C(x+a)\ne C(x)]=p_s\le p_* for independent uniform xx and a∼μa\sim\mu, and μ\mu is rational.

Why it's here

The noise touches only one copy of V0V_0, so the change probability of CC equals the base gadget's change probability psp_s, which the base-gadget claim bounds by p∗p_*. This transfers the small-change bound to the enlarged space built with the equivariant map CC, giving the small-change property of the parent lemma, and μ\mu is rational because it is a finite mixture of rational distributions.
Classified routine:
Direct consequence of the earlier claims: the enlarged noise touches a single copy of V0V_0, so by the equivariant-map construction (claim-lem-latent-2) the change probability reduces to the base gadget's psp_s, which claim-lem-latent-1 bounds by p∗p_*. Rationality holds because μ\mu is a finite uniform mixture of rational distributions.

Uses

claimBase gadget change probability at most p_*claimEnlargement by injections gives equivariant map

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Enlarged noise preserves small change probability" rests on claim-lem-latent-1
  • info
    inferred_dep
    outline: "Enlarged noise preserves small change probability" rests on claim-lem-latent-2