feat(Verified-zkEVM#140): bridge repaired line decoding to grand challenge witnesses

Author: lalalune

ArkLib/Data/CodingTheory/ProximityGap/LineDecodingCoverage.lean

@@ -140,6 +140,18 @@ theorem not_mcaEventBody_of_double_cover (C : Set (ι → A)) (u₀ u₁ : ι 
     False :=
   hpair (pairJointAgreesOn_of_double_cover C S u₀ u₁ v₁ v₂ hv₁ hv₂ hcov)
 
+/-- **Exposed repaired T4.21 hypothesis.** Every stack and every bad scalar carries the
+per-coordinate double cover that the Guruswami--Sudan interpolation route must provide. This is
+the replacement data for the refuted black-box `lineDecodable_imp_epsMCA_le_target`. -/
+def MCAForallDoubleCover (C : Set (ι → A)) (δ : ℝ≥0) : Prop :=
+  ∀ (u : WordStack A (Fin 2) ι) (γ : F), mcaEvent C δ (u 0) (u 1) γ →
+    ∀ S : Finset ι, (S.card : ℝ≥0) ≥ (1 - δ) * Fintype.card ι →
+      (∃ w ∈ C, ∀ i ∈ S, w i = (u 0) i + γ • (u 1) i) →
+      ¬ pairJointAgreesOn C S (u 0) (u 1) →
+      ∃ v₁ ∈ C, ∃ v₂ ∈ C, ∀ i ∈ S, ∃ a a' : F, a ≠ a' ∧
+        v₁ i + a • v₂ i = (u 0) i + a • (u 1) i ∧
+        v₁ i + a' • v₂ i = (u 0) i + a' • (u 1) i
+
 open Classical in
 /-- **Repaired Theorem 4.21, per-stack form.** If for the stack `(u₀, u₁)` every bad scalar's
 witness set is doubly covered by a (scalar-dependent) line-decoder pair in `C`, then no bad
@@ -156,8 +168,7 @@ theorem mcaBadCount_eq_zero_of_double_cover (C : Set (ι → A)) (δ : ℝ≥0)
     mcaBadCount (F := F) C δ u₀ u₁ = 0 := by
   classical
   rw [mcaBadCount, Finset.card_eq_zero, Finset.filter_eq_empty_iff]
-  intro γ _hγ
-  intro hev
+  intro γ _hγ hev
   obtain ⟨S, hsize, hwit, hpair⟩ := hev
   obtain ⟨v₁, hv₁, v₂, hv₂, hcover⟩ := hcov γ ⟨S, hsize, hwit, hpair⟩ S hsize hwit hpair
   exact not_mcaEventBody_of_double_cover C u₀ u₁ S hv₁ hv₂ hpair hcover
@@ -187,6 +198,8 @@ theorem epsMCA_eq_zero_of_forall_double_cover (C : Set (ι → A)) (δ : ℝ≥0
   rw [iSup_congr hzero]
   simp
 
+#print axioms MCAForallDoubleCover
+
 end
 
 end ProximityGap

ArkLib/Data/CodingTheory/ProximityGap/LineDecodingGrandChallenges.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: ArkLib Contributors
+-/
+
+import ArkLib.Data.CodingTheory.ProximityGap.LineDecodingCoverage
+import ArkLib.Data.CodingTheory.ProximityGap.GrandChallengesLattice
+
+/-!
+# Grand Challenge adapters for the repaired line-decoding coverage theorem
+
+`LineDecodingCoverage.lean` proves the corrected coverage-to-vanishing direction for ABF26
+Theorem 4.21. This module exposes the consumer-facing Grand MCA Challenge adapters: the explicit
+double-cover hypothesis gives a lower witness, and hence a faithful lattice-threshold witness,
+without using the refuted black-box `lineDecodable_imp_epsMCA_le_target` surface.
+-/
+
+namespace ProximityGap
+
+open scoped NNReal
+
+set_option linter.unusedDecidableInType false
+
+section LowerWitness
+
+variable {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι]
+variable {F : Type} [Field F] [Fintype F] [DecidableEq F]
+
+/-- **Grand-MCA lower witness from the repaired line-decoding coverage data.** Once the exposed
+double-cover data is available, `epsMCA(C, δ) = 0`, hence any `ε_star` accepts radius `δ` as a
+lower witness. -/
+def GrandChallenges.MCALowerWitness.ofDoubleCover (C : Set (ι → F)) (δ ε_star : ℝ≥0)
+    (hδ_le_one : δ ≤ 1)
+    (hcov : MCAForallDoubleCover (F := F) (A := F) C δ) :
+    GrandChallenges.MCALowerWitness C ε_star :=
+  GrandChallenges.MCALowerWitness.ofLe hδ_le_one <| by
+    rw [epsMCA_eq_zero_of_forall_double_cover C δ hcov]
+    simp
+
+end LowerWitness
+
+namespace GrandChallengesLattice
+
+open GrandChallenges
+
+section LatticeWitness
+
+variable {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι]
+variable {F : Type} [Field F] [Fintype F] [DecidableEq F]
+
+/-- A repaired double-cover target makes the faithful MCA lattice threshold exist. This is the
+line-decoding replacement path that avoids the refuted black-box target entirely. -/
+theorem mcaThresholdExists_ofDoubleCover (C : Set (ι → F)) (δ ε_star : ℝ≥0)
+    (hδ_le_one : δ ≤ 1)
+    (hcov : MCAForallDoubleCover (F := F) (A := F) C δ) :
+    mcaThresholdExists C ε_star :=
+  mcaThresholdExists_of_MCALowerWitness C ε_star
+    (MCALowerWitness.ofDoubleCover C δ ε_star hδ_le_one hcov)
+
+/-- The faithful MCA threshold created from repaired double-cover data satisfies the MCA bound. -/
+theorem mcaThreshold_spec_ofDoubleCover (C : Set (ι → F)) (δ ε_star : ℝ≥0)
+    (hδ_le_one : δ ≤ 1)
+    (hcov : MCAForallDoubleCover (F := F) (A := F) C δ) :
+    let hne := mcaThresholdExists_ofDoubleCover C δ ε_star hδ_le_one hcov
+    mcaSatisfies C ε_star (mcaThreshold C ε_star hne) :=
+  mcaThreshold_spec C ε_star
+    (mcaThresholdExists_ofDoubleCover C δ ε_star hδ_le_one hcov)
+
+end LatticeWitness
+
+end GrandChallengesLattice
+
+#print axioms ProximityGap.GrandChallenges.MCALowerWitness.ofDoubleCover
+#print axioms ProximityGap.GrandChallengesLattice.mcaThresholdExists_ofDoubleCover
+#print axioms ProximityGap.GrandChallengesLattice.mcaThreshold_spec_ofDoubleCover
+
+end ProximityGap