Lax Lean Archive

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

Proof of `The FAF verifier as a finite local-test system` (7th statement)

groundedproofs/Lax253009Proofs/FAFLocalTests.lean · lax-253009

What this proof establishes

thm✓Lax253009.FAFLocalTests (7th statement)

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

Apply finite FAF soundness to the two table families decoded from each global proof, and use the exact acceptance-probability identity.