Proof of `Soundness of the complete nonadaptive long-code test` (1st statement)
groundedproofs/Lax253009Proofs/CNASoundness.lean · lax-253009
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Choose a coefficient threshold that decays slowly enough to keep the decoding set small. Fixed moment and degree cutoffs make the pointwise error decay faster than the requested exponential rate. Finally increase the word width to control small fibers. The decoding set is independent of the side condition.