Proof of `From FAF acceptance to two-prover success` (1st statement)
groundedproofs/Lax253009Proofs/FAFStrategyExtraction.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
Noncommon questions contribute at most the finite FAF error. Therefore common questions have mass at least acceptance minus that error. Apply the proved rounding theorem to their decoded assignments.