@

feat(Verified-zkEVM#141,Verified-zkEVM#171): prove a general MCA lower bound + RS-structure necessity (no axioms/sorries)

Novel, axiom-clean [propext, Classical.choice, Quot.sound], sorry-free:
- epsMCA_ge_inv_card_of_mcaEvent: general reusable MCA lower bound -- if any word stack admits a
  bad scalar (mcaEvent fires), then epsMCA >= 1/|F|.
- MCALowerExample.epsMCA_C0_ge_half: the zero linear code over ZMod 2 has epsMCA >= 1/2. Hence the
  Grand-Challenge-1 poly/q upper bound is FALSE for general linear codes -- it genuinely requires
  the Reed-Solomon structure hypothesis. A real necessity/negative result complementing the prize
  upper-bound development.

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

Author: ArkLib Agent