While this submission is a draft, it cannot be used by other submissions.

Proof of `Finite quantitative soundness of the CNA test with side conditions`

groundedproofs/Lax253009Proofs/CNAQuantitativeSoundness.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.

Read the Lean proof on GitHub

Description

Transpose the random query matrix into independent labels. Project onto the satisfying words, preserving accepted answers and shrinking the decoding set into the original decoding set intersected with those words. Every bad accepting run then supplies a whole fiber of bad evaluation points.