Skip to content

Commit ab12d40

Browse files
lalalunelalalune
committed
feat(Verified-zkEVM#141): expose full-code MCA zero event
1 parent 5ce5da4 commit ab12d40

1 file changed

Lines changed: 139 additions & 120 deletions

File tree

‎ArkLib/Data/CodingTheory/ProximityGap/MCALowerBound.lean‎

Lines changed: 139 additions & 120 deletions
Original file line numberDiff line numberDiff line change
@@ -1,120 +1,139 @@
1-
/-
2-
Copyright (c) 2026 ArkLib Contributors. All rights reserved.
3-
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: ArkLib Contributors
5-
-/
6-
import ArkLib.Data.CodingTheory.ProximityGap.Errors
7-
import ArkLib.Data.Probability.Instances
8-
import Mathlib.Data.ZMod.Basic
9-
import Mathlib.FieldTheory.Finite.Basic
10-
11-
/-!
12-
# A general MCA lower bound, and the necessity of the RS-structure hypothesis (proximity)
13-
14-
ABF26 Grand Challenge 1 is an *upper* bound: `ε_mca(RS, δ) ≤ poly(2^m, 1/ρ)/q` for Reed–Solomon
15-
codes at the prize rates. This file proves the complementary *lower* side:
16-
17-
* `mcaEvent_prob_le_epsMCA` — the fundamental primitive: `epsMCA` dominates the bad-scalar
18-
probability of *every* word stack (`epsMCA` is, by definition, the supremum of those).
19-
* `epsMCA_ge_inv_card_of_mcaEvent` — whenever **some** stack admits a bad scalar (`mcaEvent`
20-
fires), `epsMCA ≥ 1/|F|`.
21-
* `MCALowerExample.epsMCA_C0_ge_half` — a concrete witness: the **zero linear code** over `ZMod 2`
22-
has `epsMCA ≥ 1/2`. Hence the Grand-Challenge-1 `poly/q` smallness is **false for general linear
23-
codes** — it genuinely requires the Reed–Solomon structure. This makes precise *why* the prize
24-
hypotheses cannot be dropped, complementing the upper-bound development.
25-
26-
All results are `sorry`-free and axiom-clean (`[propext, Classical.choice, Quot.sound]`).
27-
-/
28-
29-
set_option linter.unusedSectionVars false
30-
31-
open scoped NNReal ENNReal ProbabilityTheory BigOperators
32-
open ProximityGap Code
33-
34-
namespace ProximityGap
35-
36-
variable {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι]
37-
variable {F : Type} [Field F] [Fintype F] [DecidableEq F]
38-
variable {A : Type} [Fintype A] [DecidableEq A] [AddCommGroup A] [Module F A]
39-
40-
open Classical in
41-
/-- **MCA lower-bound primitive.** `epsMCA` dominates the bad-scalar probability of every word
42-
stack, since it is the supremum of those probabilities. -/
43-
theorem mcaEvent_prob_le_epsMCA
44-
(C : Set (ι → A)) (δ : ℝ≥0) (u : WordStack A (Fin 2) ι) :
45-
Pr_{let γ ← $ᵖ F}[mcaEvent C δ (u 0) (u 1) γ] ≤ epsMCA (F := F) (A := A) C δ := by
46-
unfold epsMCA
47-
exact le_iSup (fun u : WordStack A (Fin 2) ι =>
48-
Pr_{let γ ← $ᵖ F}[mcaEvent C δ (u 0) (u 1) γ]) u
49-
50-
open Classical in
51-
/-- **MCA lower bound from a single bad scalar.** If some stack `u` admits a bad scalar `γ₀`
52-
(`mcaEvent` fires), then `epsMCA ≥ 1/|F|`: that scalar contributes `1/|F|` to `u`'s bad-scalar
53-
probability, which `epsMCA` dominates. -/
54-
theorem epsMCA_ge_inv_card_of_mcaEvent
55-
(C : Set (ι → A)) (δ : ℝ≥0) (u : WordStack A (Fin 2) ι) (γ₀ : F)
56-
(hev : mcaEvent C δ (u 0) (u 1) γ₀) :
57-
(1 : ℝ≥0∞) / (Fintype.card F : ℝ≥0∞) ≤ epsMCA (F := F) (A := A) C δ := by
58-
refine le_trans ?_ (mcaEvent_prob_le_epsMCA (F := F) (A := A) C δ u)
59-
rw [prob_uniform_eq_card_filter_div_card]
60-
have hmem : γ₀ ∈ Finset.filter (fun γ => mcaEvent C δ (u 0) (u 1) γ) Finset.univ := by
61-
simp only [Finset.mem_filter, Finset.mem_univ, true_and]; exact hev
62-
have hcard1 : (1 : ℕ) ≤
63-
(Finset.filter (fun γ => mcaEvent C δ (u 0) (u 1) γ) Finset.univ).card :=
64-
Finset.card_pos.mpr ⟨γ₀, hmem⟩
65-
simp only [ENNReal.coe_natCast]
66-
gcongr
67-
exact_mod_cast hcard1
68-
69-
open Classical in
70-
/-- **The full code has zero MCA error.** For `C = univ`, every pair `(u₀, u₁)` is jointly
71-
matchable by codewords (themselves), so `pairJointAgreesOn` always holds and `mcaEvent` never
72-
fires. With `epsMCA_C0_ge_half` this brackets the MCA error across the structural extremes:
73-
`epsMCA univ δ = 0`, while the zero code reaches `≥ 1/2`. -/
74-
theorem epsMCA_univ_eq_zero (δ : ℝ≥0) :
75-
epsMCA (F := F) (A := A) (Set.univ : Set (ι → A)) δ = 0 := by
76-
unfold epsMCA
77-
refine le_antisymm (iSup_le fun u => ?_) (zero_le _)
78-
rw [prob_uniform_eq_card_filter_div_card]
79-
have hfalse : ∀ γ : F, ¬ mcaEvent (Set.univ : Set (ι → A)) δ (u 0) (u 1) γ := by
80-
rintro γ ⟨S, hS, hw, hno⟩
81-
exact hno ⟨u 0, Set.mem_univ _, u 1, Set.mem_univ _, fun i _ => ⟨rfl, rfl⟩⟩
82-
rw [Finset.filter_false_of_mem (fun γ _ => hfalse γ)]
83-
simp
84-
85-
end ProximityGap
86-
87-
namespace ProximityGap.MCALowerExample
88-
89-
instance mcaLowerExample_fact2 : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
90-
91-
open ProximityGap Code
92-
93-
/-- The zero linear code over `ZMod 2` (carrier `{0}`) on one coordinate. -/
94-
abbrev C0 : Set (Fin 1 → ZMod 2) := {(fun _ => 0)}
95-
96-
/-- The witnessing stack `u 0 = 0`, `u 1 = 1`. -/
97-
abbrev u0 : WordStack (ZMod 2) (Fin 2) (Fin 1) := ![(fun _ => 0), (fun _ => 1)]
98-
99-
/-- `mcaEvent` fires for the zero code `C0` at `γ = 0`: the line `0 + 0·1 = 0` equals the codeword
100-
`0` on `S = {0}`, but no codeword equals `u 1 = 1` there, so `¬ pairJointAgreesOn`. -/
101-
theorem mcaEvent_C0 : mcaEvent (F := ZMod 2) C0 0 (u0 0) (u0 1) 0 := by
102-
refine ⟨{0}, ?_, ⟨(fun _ => 0), rfl, ?_⟩, ?_⟩
103-
· simp
104-
· intro i hi; fin_cases i; simp [u0]
105-
· rintro ⟨v₀, hv₀, v₁, hv₁, hag⟩
106-
have hv₁eq : v₁ = (fun _ => 0) := hv₁
107-
have hc := (hag 0 (by simp)).2
108-
rw [hv₁eq] at hc
109-
simp only [u0, Matrix.cons_val_one] at hc
110-
exact absurd hc (by decide)
111-
112-
/-- **The MCA error of the zero linear code is `≥ 1/2`.** Hence the Grand-Challenge-1 `poly/q`
113-
upper bound is FALSE for general linear codes — it genuinely requires the Reed–Solomon structure
114-
hypothesis. -/
115-
theorem epsMCA_C0_ge_half :
116-
(1 : ℝ≥0∞) / 2 ≤ epsMCA (F := ZMod 2) (A := ZMod 2) C0 0 := by
117-
have h := epsMCA_ge_inv_card_of_mcaEvent (F := ZMod 2) (A := ZMod 2) C0 0 u0 0 mcaEvent_C0
118-
simpa using h
119-
120-
end ProximityGap.MCALowerExample
1+
/-
2+
Copyright (c) 2026 ArkLib Contributors. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: ArkLib Contributors
5+
-/
6+
import ArkLib.Data.CodingTheory.ProximityGap.Errors
7+
import ArkLib.Data.Probability.Instances
8+
import Mathlib.Data.ZMod.Basic
9+
import Mathlib.FieldTheory.Finite.Basic
10+
11+
/-!
12+
# A general MCA lower bound, and the necessity of the RS-structure hypothesis (proximity)
13+
14+
ABF26 Grand Challenge 1 is an *upper* bound: `ε_mca(RS, δ) ≤ poly(2^m, 1/ρ)/q` for Reed–Solomon
15+
codes at the prize rates. This file proves the complementary *lower* side:
16+
17+
* `mcaEvent_prob_le_epsMCA` — the fundamental primitive: `epsMCA` dominates the bad-scalar
18+
probability of *every* word stack (`epsMCA` is, by definition, the supremum of those).
19+
* `epsMCA_ge_inv_card_of_mcaEvent` — whenever **some** stack admits a bad scalar (`mcaEvent`
20+
fires), `epsMCA ≥ 1/|F|`.
21+
* `MCALowerExample.epsMCA_C0_ge_half` — a concrete witness: the **zero linear code** over `ZMod 2`
22+
has `epsMCA ≥ 1/2`. Hence the Grand-Challenge-1 `poly/q` smallness is **false for general linear
23+
codes** — it genuinely requires the Reed–Solomon structure. This makes precise *why* the prize
24+
hypotheses cannot be dropped, complementing the upper-bound development.
25+
26+
All results are `sorry`-free and axiom-clean (`[propext, Classical.choice, Quot.sound]`).
27+
-/
28+
29+
set_option linter.unusedSectionVars false
30+
31+
open scoped NNReal ENNReal ProbabilityTheory BigOperators
32+
open ProximityGap Code
33+
34+
namespace ProximityGap
35+
36+
variable {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι]
37+
variable {F : Type} [Field F] [Fintype F] [DecidableEq F]
38+
variable {A : Type} [Fintype A] [DecidableEq A] [AddCommGroup A] [Module F A]
39+
40+
omit [DecidableEq ι] [Fintype F] [DecidableEq F] [Fintype A] [DecidableEq A] in
41+
/-- **No MCA bad scalar exists for the full code.** Since every word is a codeword of
42+
`Set.univ`, the two queried words themselves witness joint agreement on any candidate set. -/
43+
theorem not_mcaEvent_univ
44+
(δ : ℝ≥0) (u₀ u₁ : ι → A) (γ : F) :
45+
¬ mcaEvent (F := F) (A := A) (Set.univ : Set (ι → A)) δ u₀ u₁ γ := by
46+
rintro ⟨S, hS, hw, hno⟩
47+
exact hno ⟨u₀, Set.mem_univ _, u₁, Set.mem_univ _, fun i _ => ⟨rfl, rfl⟩⟩
48+
49+
omit [DecidableEq ι] [DecidableEq F] [Fintype A] [DecidableEq A] in
50+
open Classical in
51+
/-- The bad-scalar probability for any stack against the full code is zero. -/
52+
theorem mcaEvent_prob_univ_eq_zero
53+
(δ : ℝ≥0) (u : WordStack A (Fin 2) ι) :
54+
Pr_{let γ ← $ᵖ F}[
55+
mcaEvent (F := F) (A := A) (Set.univ : Set (ι → A)) δ (u 0) (u 1) γ] = 0 := by
56+
rw [prob_uniform_eq_card_filter_div_card]
57+
rw [Finset.filter_false_of_mem
58+
(fun γ _ => not_mcaEvent_univ (F := F) (A := A) δ (u 0) (u 1) γ)]
59+
simp
60+
61+
open Classical in
62+
/-- **MCA lower-bound primitive.** `epsMCA` dominates the bad-scalar probability of every word
63+
stack, since it is the supremum of those probabilities. -/
64+
theorem mcaEvent_prob_le_epsMCA
65+
(C : Set (ι → A)) (δ : ℝ≥0) (u : WordStack A (Fin 2) ι) :
66+
Pr_{let γ ← $ᵖ F}[mcaEvent C δ (u 0) (u 1) γ] ≤ epsMCA (F := F) (A := A) C δ := by
67+
unfold epsMCA
68+
exact le_iSup (fun u : WordStack A (Fin 2) ι =>
69+
Pr_{let γ ← $ᵖ F}[mcaEvent C δ (u 0) (u 1) γ]) u
70+
71+
open Classical in
72+
/-- **MCA lower bound from a single bad scalar.** If some stack `u` admits a bad scalar `γ₀`
73+
(`mcaEvent` fires), then `epsMCA ≥ 1/|F|`: that scalar contributes `1/|F|` to `u`'s bad-scalar
74+
probability, which `epsMCA` dominates. -/
75+
theorem epsMCA_ge_inv_card_of_mcaEvent
76+
(C : Set (ι → A)) (δ : ℝ≥0) (u : WordStack A (Fin 2) ι) (γ₀ : F)
77+
(hev : mcaEvent C δ (u 0) (u 1) γ₀) :
78+
(1 : ℝ≥0∞) / (Fintype.card F : ℝ≥0∞) ≤ epsMCA (F := F) (A := A) C δ := by
79+
refine le_trans ?_ (mcaEvent_prob_le_epsMCA (F := F) (A := A) C δ u)
80+
rw [prob_uniform_eq_card_filter_div_card]
81+
have hmem : γ₀ ∈ Finset.filter (fun γ => mcaEvent C δ (u 0) (u 1) γ) Finset.univ := by
82+
simp only [Finset.mem_filter, Finset.mem_univ, true_and]; exact hev
83+
have hcard1 : (1 : ℕ) ≤
84+
(Finset.filter (fun γ => mcaEvent C δ (u 0) (u 1) γ) Finset.univ).card :=
85+
Finset.card_pos.mpr ⟨γ₀, hmem⟩
86+
simp only [ENNReal.coe_natCast]
87+
gcongr
88+
exact_mod_cast hcard1
89+
90+
open Classical in
91+
/-- **The full code has zero MCA error.** For `C = univ`, every pair `(u₀, u₁)` is jointly
92+
matchable by codewords (themselves), so `pairJointAgreesOn` always holds and `mcaEvent` never
93+
fires. With `epsMCA_C0_ge_half` this brackets the MCA error across the structural extremes:
94+
`epsMCA univ δ = 0`, while the zero code reaches `≥ 1/2`. -/
95+
theorem epsMCA_univ_eq_zero (δ : ℝ≥0) :
96+
epsMCA (F := F) (A := A) (Set.univ : Set (ι → A)) δ = 0 := by
97+
unfold epsMCA
98+
refine le_antisymm (iSup_le fun u => ?_) (zero_le _)
99+
rw [mcaEvent_prob_univ_eq_zero (F := F) (A := A) δ u]
100+
101+
#print axioms ProximityGap.not_mcaEvent_univ
102+
#print axioms ProximityGap.mcaEvent_prob_univ_eq_zero
103+
104+
end ProximityGap
105+
106+
namespace ProximityGap.MCALowerExample
107+
108+
instance mcaLowerExample_fact2 : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
109+
110+
open ProximityGap Code
111+
112+
/-- The zero linear code over `ZMod 2` (carrier `{0}`) on one coordinate. -/
113+
abbrev C0 : Set (Fin 1 → ZMod 2) := {(fun _ => 0)}
114+
115+
/-- The witnessing stack `u 0 = 0`, `u 1 = 1`. -/
116+
abbrev u0 : WordStack (ZMod 2) (Fin 2) (Fin 1) := ![(fun _ => 0), (fun _ => 1)]
117+
118+
/-- `mcaEvent` fires for the zero code `C0` at `γ = 0`: the line `0 + 0·1 = 0` equals the codeword
119+
`0` on `S = {0}`, but no codeword equals `u 1 = 1` there, so `¬ pairJointAgreesOn`. -/
120+
theorem mcaEvent_C0 : mcaEvent (F := ZMod 2) C0 0 (u0 0) (u0 1) 0 := by
121+
refine ⟨{0}, ?_, ⟨(fun _ => 0), rfl, ?_⟩, ?_⟩
122+
· simp
123+
· intro i hi; fin_cases i; simp [u0]
124+
· rintro ⟨v₀, hv₀, v₁, hv₁, hag⟩
125+
have hv₁eq : v₁ = (fun _ => 0) := hv₁
126+
have hc := (hag 0 (by simp)).2
127+
rw [hv₁eq] at hc
128+
simp only [u0, Matrix.cons_val_one] at hc
129+
exact absurd hc (by decide)
130+
131+
/-- **The MCA error of the zero linear code is `≥ 1/2`.** Hence the Grand-Challenge-1 `poly/q`
132+
upper bound is FALSE for general linear codes — it genuinely requires the Reed–Solomon structure
133+
hypothesis. -/
134+
theorem epsMCA_C0_ge_half :
135+
(1 : ℝ≥0∞) / 2 ≤ epsMCA (F := ZMod 2) (A := ZMod 2) C0 0 := by
136+
have h := epsMCA_ge_inv_card_of_mcaEvent (F := ZMod 2) (A := ZMod 2) C0 0 u0 0 mcaEvent_C0
137+
simpa using h
138+
139+
end ProximityGap.MCALowerExample

0 commit comments

Comments
 (0)