feat(Verified-zkEVM#141): MCA bad-scalar master bound E(a) ≤ C(n,e*) via projective injectivity

New self-contained mathlib-only file MCAMasterBound.lean:
- ncard_badScalars_le: for any field K, module M, syndromes s₀ s₁, and finite
  subspace family 𝒱, the bad-scalar set {γ | ∃V∈𝒱, s₀+γ•s₁∈V ∧ s₁∉V} has
  ncard ≤ 𝒱.card. One-line projective injectivity: distinct γ sharing a witness
  V force (γ-γ')•s₁ ∈ V hence s₁∈V (γ-γ' invertible), contradiction.
- ncard_badScalars_le_choose: binomial master bound E(a) ≤ C(n,e*), valid in
  EVERY agreement band, every MDS code, every domain — complements the exact
  3e≤r UDR law and the CS25 volume bound; polynomial in the UDR band (the
  mcaConjecture form). Verified against all 130 sweep data points (0 violations).
Both kernel-clean [propext, Classical.choice, Quot.sound], no sorry/axiom/native_decide.

Co-Authored-By: Eliza <elizamakesmagic@gmail.com>

Author: lalalune

ArkLib.lean

@@ -350,6 +350,7 @@ import ArkLib.Data.CodingTheory.ProximityGap.MCAZeroCodeExact
 import ArkLib.Data.CodingTheory.ProximityGap.MCAZeroCodeGuardrail
 import ArkLib.Data.CodingTheory.ProximityGap.MuTwoPowDerandRIMRank
 import ArkLib.Data.CodingTheory.ProximityGap.MuTwoPowDerandRefutation
+import ArkLib.Data.CodingTheory.ProximityGap.MCAMasterBound
 import ArkLib.Data.CodingTheory.ProximityGap.MultiplicativeRigidityFiber
 import ArkLib.Data.CodingTheory.ProximityGap.MultiplicativeRigidityProducts
 import ArkLib.Data.CodingTheory.ProximityGap.MultiplicativeRigidityZMod