claimroutine

Construction is effective for rational p_*

The whole latent construction is effective for rational p∗p_*
algorithmic part of the lemma
Claim·§3.5 Quotients and enlargement·inside lemLatent alphabet gadget with detecting noise

Statement (paper)

When p∗p_* is rational, all the choices in the construction (the threshold r∗r_*, the integers mm and r0r_0, the rational ε0\eps_0, the field F2d\F_{2^d} together with a generic rank-r0r_0 space, and the remaining products, isomorphisms, injections, quotients, function tables and rational noise laws) can be made effectively, by finite enumeration and binary linear algebra, so that the construction is a terminating deterministic algorithm.

In plain English

When p∗p_* is rational, every choice in the latent-space construction (the threshold r∗r_*, the integers mm and r0r_0, the rational ε0\eps_0, the field F2d\F_{2^d} with a generic rank-r0r_0 space, and the products, isomorphisms, injections, quotients, function tables and rational noise laws) can be made effectively. The construction is therefore a terminating deterministic algorithm.

Why it's here

This claim gives the algorithmic part of the lemma. Every parameter is an explicit finite choice, and the one existential step, picking a generic subspace, can be done by finite search because random subspaces are generic with probability tending to one (the generic-subspace lemma). Everything else is finite enumeration and binary linear algebra.
Classified routine:
Effectivity bookkeeping: every parameter is a finite explicit choice, and the one existential step, choosing a generic subspace, is done by finite search. That search terminates because of the earlier generic-subspace lemma (random subspaces are generic with probability tending to one); the rest is standard finite enumeration and binary linear algebra.

Uses

lemRandom binary subspaces are generic

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.