Proof of `Perfect completeness and local decoding of the long-code test` (1st statement)
What this proof establishes
no assumptions
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
If no word produces the initial answer vector, the predicate recognizing that vector composes to the constant false function, contradicting acceptance.