claimroutine

Base gadget change probability at most p_*

Base gadget has change probability ps≤p∗p_s\le p_*, with threshold r∗=b+2r_*=b+2
small-change bound for the enlarged gadget
Claim·§3.5 Quotients and enlargement·inside lemLatent alphabet gadget with detecting noise

Statement (paper)

For the quotient (V0,B,C‾,ν)(V_0,B,\overline C,\nu) constructed above, the change probability satisfies ps≤(1−θ)s≤exp⁡(−θs)≤exp⁡(θ−Hr0/8)≤p∗p_s\le(1-\theta)^s\le\exp(-\theta s)\le\exp(\theta-H_{r_0}/8)\le p_*. Moreover, all choices made so far (namely r0r_0, ε0\eps_0, dd, b=3db=3d, θ\theta, ss) depend only on p∗p_*, and we set r∗=b+2r_*=b+2.

In plain English

For the quotient gadget (V0,B,C‾,ν)(V_0,B,\overline C,\nu), the change probability satisfies ps≤(1−θ)s≤exp⁡(−θs)≤exp⁡(θ−Hr0/8)≤p∗p_s\le(1-\theta)^s\le\exp(-\theta s)\le\exp(\theta-H_{r_0}/8)\le p_*. All parameters chosen so far (r0r_0, ε0\eps_0, dd, b=3db=3d, θ\theta, ss) depend only on p∗p_*, and we set r∗=b+2r_*=b+2.

Why it's here

The noise formula for the latent coloring gives ps≤(1−θ)sp_s\le(1-\theta)^s, and the choice of ss then pushes this below p∗p_*. Because every parameter depends only on p∗p_*, the threshold r∗=b+2r_*=b+2 is fixed before ℓ\ell is chosen, as the lemma requires. The enlarged-noise claim that uses this can therefore start from a base gadget with small change probability and a fixed threshold.
Classified routine:
Direct parameter bookkeeping: it combines the latent-coloring noise formula (lem-latent-noise) with the choice of s, using the elementary bound (1-θ)^s ≤ e^{-θs}, and records that every parameter depends only on p_*.

Uses

lemRandom binary subspaces are genericlemLatent coloring change probability formula

Used by

claimEnlarged noise preserves small change probability

Sources

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

Phase 2 aligns this node to a Lean declaration.