feat(Verified-zkEVM#121/Verified-zkEVM#141): prove the GS-exposed prize is vacuous without faithfulness (anti-vacuity guard) (Verified-zkEVM#192)

New genuine result (not previously in tree): epsMCAgs C δ (fun _ => ∅) = 0, hence the bare 'exists L, epsMCAgs C δ L ≤ B' holds for ANY bound B (via the empty list family). This formally proves WHY the FaithfulGSFamily hypothesis used throughout GrandChallenge141PrizeMath.lean is mathematically indispensable: dropping it makes the GS-exposed Grand-Challenge-1 prize statement vacuous. mcaEventGSrow's witness must lie in L, so L=∅ kills every bad event. A structural anti-vacuity guard (Verified-zkEVM#121), not a closure of the open prize.

VERIFICATION: proved sorry-free and axiom-clean [propext, Classical.choice, Quot.sound] via 'lake env lean' on content-identical theorems while the dependency oleans were consistent. A full-library re-verify is currently impossible because concurrent activity invalidated the Mathlib cache and the shared checkout is mid-rebuild (lean exiting code 143 / SIGTERM on Mathlib.Logic.Basic) — an infrastructure state, not a defect in this proof.

Co-authored-by: ArkLib Agent <agent@arklib.local>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: 3 people