Proof of `Quantitative soundness at a fixed evaluation point` (2nd statement)
groundedproofs/Lax253009Proofs/CNAPointSoundness.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
Agreement forces the full Fourier sum to equal one. Split by degree and coefficient size. Avoidance of the decoding set isolates the distinguished label in each large support, making that term at most one third. Therefore one of the two remaining terms is at least one third; use their proved tails.