Proof of `Repeated squaring of fortified projection tests`
groundedproofs/Lax253009Proofs/FortifiedSquaring.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
Fix the first random test and partition its successful answers by their common projection. Each part is a rectangle in the second questions. Apply fortification on each part and average; first-copy success is at most the original soundness by fixing the second random test.