@

fix(Verified-zkEVM#141,Verified-zkEVM#171): replace unsound mcaForallDoubleCover axiom with a PROVED refutation; remove vacuous larp

Per the Verified-zkEVM#171 state audit. Two integrity fixes, no new axioms/sorries:
- PROVE mcaForallDoubleCover_not_universal: the global ABF26 T4.21 hypothesis MCAForallDoubleCover
  is NOT universally true (a ZMod 2 counterexample where mcaEvent fires). This replaces the unsound
  `axiom mcaForallDoubleCover_residual` (which asserted it for all codes/radii -> would derive False)
  and its fake re-export theorem mcaForallDoubleCover_holds. Axiom-clean [propext,Classical,Quot].
- Remove 8 vacuous `theorem ..._residual : True := by trivial` larps (0 consumers) that Verified-zkEVM#171/Verified-zkEVM#169
  flagged as placebos named after hard open problems (Verified-zkEVM#14,Verified-zkEVM#114,Verified-zkEVM#116,Verified-zkEVM#112,Verified-zkEVM#113,Verified-zkEVM#29,Verified-zkEVM#13,Verified-zkEVM#62).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@

Author: ArkLib Agent