From 58da71004fd978e5adea0d8ef82660fb0c06499f Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Tue, 17 Mar 2026 22:50:25 +0000
Subject: [PATCH 01/14] initial progress

---
 ArkLib/Data/CodingTheory/Basic.lean           |  89 +++++++++++-
 .../ProximityGap/ProximityGenerators.lean     | 134 ++++++++++++++++++
 2 files changed, 222 insertions(+), 1 deletion(-)
 create mode 100644 ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean

diff --git a/ArkLib/Data/CodingTheory/Basic.lean b/ArkLib/Data/CodingTheory/Basic.lean
index 244023024..6042c0346 100644
--- a/ArkLib/Data/CodingTheory/Basic.lean
+++ b/ArkLib/Data/CodingTheory/Basic.lean
@@ -1787,6 +1787,14 @@ lemma wt_eq_zero_iff [Zero F] {v : ι → F} :
   by_cases IsEmpty ι <;>
   aesop (add simp [wt, Finset.filter_eq_empty_iff])
 
+def restrictedWord (c : ι → F) (T : Finset ι) : T → F := fun i : T => c i
+
+/-- Let `C` be a code of length `ι`. For every subset `T ⊆ ι`, we define the restricted code `C|T`
+as the set of words `w` of length `T`, obtained by restricting `ι` to `T`. -/
+def restrictedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
+  {w | ∃ c ∈ C, w = restrictedWord c T}
+
+
 end
 
 end
@@ -1943,7 +1951,6 @@ variable {F : Type*} {A : Type*} [AddCommMonoid A]
          {ι : Type*} [Fintype ι]
          {κ : Type*} [Fintype κ]
 
-
 /-- Module code defined by left multiplication by its generator matrix.
   For a matrix G : Matrix κ ι F (over field F) and module A over F, this generates
   the F-submodule of (ι → A) spanned by the rows of G acting on (κ → A).
@@ -2033,6 +2040,86 @@ scoped syntax &"ρ" term : term
 scoped macro_rules
   | `(ρ $t:term) => `(LinearCode.rate $t)
 
+
+-- open Classical in
+-- lemma gen_matrix_exists [Semiring F] [Nonempty ι] (LC : LinearCode ι F) : ∃ (G : Matrix κ ι F),
+--   LC = fromRowGenMat G := by
+--   unfold fromRowGenMat
+--   simp only [range_vecMulLinear]
+--   have : LC.FG := by
+--     unfold LinearCode at LC
+--     have h₁ : LC ≤ ⊤ := by
+--       simp only [le_top]
+--     have {a b : LinearCode ι F} : a ≤ b → b.FG → a.FG := by
+--       unfold LinearCode at a b
+--       intros h h'
+--       rw [Submodule.fg_def] at h'
+--       rcases h' with ⟨s, hs, hspanB⟩
+--       refine Submodule.spanRank_finite_iff_fg.mp ?_
+--       sorry
+--     apply this h₁
+--     rw [@Submodule.fg_def]
+--     use (Finset.image (fun (i j : ι) ↦ if i = j then 1 else 0) Fintype.elems).toSet
+--     have {s : Finset (ι → F)} : s.toSet.Finite := by
+--       simp
+--     apply And.intro this
+--     simp only [Finset.coe_image]
+--     apply Submodule.eq_top_iff'.mpr
+--     intros x
+--     apply (mem_span_image_iff_exists_fun F).mpr
+--     use (fun y ↦ x y)
+--     ext y
+--     rw [sum_apply]
+--     rw [Finset.sum_eq_single]
+--     swap
+--     exact ⟨y, by simp only [SetLike.mem_coe]; exact complete y⟩
+--     · simp
+--     · intros b _ h
+--       simp
+--       intros h'
+--       aesop
+--     · simp
+
+
+--   have : ∃ S : Set (ι → F), LC = Submodule.span F S  := by
+--     use LC
+--     simp
+
+--   have blah := @Submodule.instNonemptySubtypeSetEqSpan LC
+
+--   sorry
+
+
+lemma linCode_FG [Field F] (LC : LinearCode ι F) : LC.FG := by
+  exact Submodule.FG.of_finite
+
+
+open Classical in
+lemma gen_matrix_exists' [Field F] [Fintype F] [Nonempty ι] (LC : LinearCode ι F) : ∃ (G : Matrix κ ι F),
+  LC = fromRowGenMat G := by
+  unfold fromRowGenMat
+  simp only [range_vecMulLinear]
+  have LC_FG : LC.FG := linCode_FG LC
+  have LC_genSet : ∃ S : Set (ι → F), LC = Submodule.span F S  := by
+    use LC
+    simp
+  rcases LC_genSet with ⟨S, S_spans_LC⟩
+  have S_Finite : S.Finite := Set.toFinite S
+  rw [S_spans_LC]
+
+  sorry
+
+
+/-- A linear code is maximum distance separable (MDS) if  its parameters meet the Singleton bound.
+-/
+def IsMDSCode [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=
+  Code.dist LC.carrier = length LC - dim LC + 1
+
+/-- A linear code of length `ι` and dimension `dim` is MDS if and only if any `dim` rows of its
+generator matrix are linearly independent. -/
+lemma MDS_iff_dim_lin_ind_rows_in_GenMatrix [CommRing F] [DecidableEq F] (LC : LinearCode ι F) :
+  IsMDSCode LC ↔ sorry := by sorry
+
 end
 
 section
diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
new file mode 100644
index 000000000..ea6ead0ce
--- /dev/null
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Katerina Hristova
+-/
+
+-- import ArkLib.Data.CodingTheory.Basic
+-- import ArkLib.Data.CodingTheory.GuruswamiSudan
+-- import ArkLib.Data.CodingTheory.Prelims
+-- import ArkLib.Data.CodingTheory.ReedSolomon
+-- import ArkLib.Data.CodingTheory.InterleavedCode
+-- import ArkLib.Data.Polynomial.Bivariate
+-- import ArkLib.Data.Polynomial.RationalFunctions
+-- import ArkLib.Data.Probability.Notation
+-- import Mathlib.Algebra.Field.Basic
+-- import Mathlib.Algebra.Lie.OfAssociative
+-- import Mathlib.Algebra.Module.Submodule.Defs
+-- import Mathlib.Algebra.Polynomial.Basic
+-- import Mathlib.Data.Finset.BooleanAlgebra
+-- import Mathlib.Data.Real.Basic
+-- import Mathlib.Data.Real.Sqrt
+-- import Mathlib.Data.Set.Defs
+-- import Mathlib.FieldTheory.RatFunc.AsPolynomial
+-- import Mathlib.FieldTheory.Separable
+-- import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
+-- import Mathlib.Probability.Distributions.Uniform
+-- import Mathlib.RingTheory.Henselian
+-- import Mathlib.RingTheory.PowerSeries.Basic
+-- import Mathlib.RingTheory.PowerSeries.Substitution
+-- import Mathlib.LinearAlgebra.Matrix.Vec
+-- import Mathlib.Data.Matrix.Mul
+-- import Mathlib.Order.SetNotation
+
+import Mathlib.Probability.Distributions.Uniform
+import Mathlib.Algebra.MvPolynomial.Basic
+import Mathlib.LinearAlgebra.LinearIndependent.Defs
+import ArkLib.Data.CodingTheory.Basic
+import ArkLib.Data.Probability.Notation
+import Mathlib.Algebra.Module.Defs
+import Mathlib.Topology.UnitInterval
+import Mathlib
+
+/-!
+# Proximity Generators fundamental definitions
+
+Define the fundamental definitions for proximity gap properties of generic codes and
+module codes over (scalar) rings.
+
+## Main Definitions
+
+### Proximity Gap Definitions
+- `proximityMeasure`: Counts vectors close to linear combinations with code `C`
+
+
+## References
+
+- [BCIKS20] Eli Ben-Sasson, Dan Carmon, Yuval Ishai, Swastik Kopparty, and Shubhangi Saraf.
+  Proximity gaps for Reed–Solomon codes. In 2020 IEEE 61st Annual Symposium on Foundations of
+  Computer Science (FOCS), 2020. Full paper: https://eprint.iacr.org/2020/654, version 20210703:203025.
+
+
+-/
+
+namespace Generator
+
+open NNReal Finset Function ENNReal
+open scoped ProbabilityTheory
+open scoped BigOperators
+
+section
+
+variable {ι : Type} [Fintype ι] [DecidableEq ι]
+         {F : Type} [Field F] [Fintype F] [DecidableEq F]
+         {ℓ : Type} [Fintype ℓ]
+
+def Generator (S ℓ F : Type) : Type := S → (ℓ → F)
+
+-- noncomputable instance {S : Set (ι → F)} : Fintype S := Fintype.ofFinite ↑S
+
+-- noncomputable def probs {S : Set (ℓ → F)} [Nonempty S] (G : Generator S) : Set ENNReal :=
+--   {y | ∃ v : ℓ → F, v ≠ 0 ∧ y = Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]}
+
+def IsZeroEvadingGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_ze : ℝ≥0∞) : Prop :=
+  ε_ze ∈ Set.Icc 0 1 ∧
+  (SupSet.sSup {y | ∃ v : ℓ → F, v ≠ 0 ∧ y = Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]}) ≤ ε_ze
+
+def IsPolynomialGen {s : ℕ} {S : Fin s → Set F} (G : Generator (∀ i, S i) ℓ F) : Prop :=
+  ∃ P : ℓ → MvPolynomial (Fin s) F, LinearIndependent F P ∧
+  ∀ x : (∀ i, S i), G x = MvPolynomial.eval (fun i ↦ x i) ∘ P
+
+def M_G {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Matrix S ℓ F :=
+  Matrix.of G
+
+def IsMDSGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Prop :=
+ LinearCode.IsMDSCode (LinearCode.fromRowGenMat (M_G G))
+
+-- def denseSet
+
+-- Code.restrictedCode
+
+open unitInterval
+
+/-- A subset of `ι` is dense if `|T| ≥ |ι| * (1 − γ)`, for some γ -/
+def IsDenseSet (T : Finset ι) (γ : ℝ) : Prop := Finset.card T ≥ (Fintype.card ι) * (1 - γ)
+
+def Matrix (U : ℓ → ι → F) : Matrix ℓ ι F := Matrix.of U
+
+def Condition {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (U : ℓ → ι → F)
+  (T : Finset ι) (γ : ℝ) (x : S) (LC : LinearCode ι F) : Prop :=
+  let v := Matrix.vecMul (G x) (Matrix.of U)
+  Finset.card T ≥ (Fintype.card ι) * (1 - γ) ∧
+  Code.restrictedWord v T ∈ Code.restrictedCode LC T
+
+
+
+def IsMCAGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_mca : ℝ≥0 → ℝ≥0)
+(hε_mca : Set.Icc 0 1 → Set.Icc 0 1) : Prop := sorry
+
+
+
+
+-- def zeroEvading' {S : Set (ℓ → F)} [Nonempty S] (G : Generator S) (ε_ze : ℝ≥0∞) : Prop :=
+--   ε_ze ∈ Set.Icc 0 1 ∧
+--   (SupSet.sSup
+--     (
+--       Set.image
+--         (fun (v : ℓ → F) ↦ (Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]))
+--         {v | v ≠ 0}
+--     )
+--   ) ≤ ε_ze
+
+end
+
+end Generator

From 4bf4ff7d4481e4307b0a14d1a70f9b25ed9e7233 Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Tue, 17 Mar 2026 23:31:30 +0000
Subject: [PATCH 02/14] draft of MCA gen

---
 .../ProximityGap/ProximityGenerators.lean     | 22 +++++++------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
index ea6ead0ce..1f7e9b6a2 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
@@ -66,6 +66,7 @@ namespace Generator
 open NNReal Finset Function ENNReal
 open scoped ProbabilityTheory
 open scoped BigOperators
+open unitInterval
 
 section
 
@@ -94,29 +95,22 @@ def M_G {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Matrix S 
 def IsMDSGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Prop :=
  LinearCode.IsMDSCode (LinearCode.fromRowGenMat (M_G G))
 
--- def denseSet
-
--- Code.restrictedCode
-
-open unitInterval
 
 /-- A subset of `ι` is dense if `|T| ≥ |ι| * (1 − γ)`, for some γ -/
 def IsDenseSet (T : Finset ι) (γ : ℝ) : Prop := Finset.card T ≥ (Fintype.card ι) * (1 - γ)
 
-def Matrix (U : ℓ → ι → F) : Matrix ℓ ι F := Matrix.of U
 
 def Condition {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (U : ℓ → ι → F)
-  (T : Finset ι) (γ : ℝ) (x : S) (LC : LinearCode ι F) : Prop :=
+  (T : Finset ι) (γ : ℝ) (LC : LinearCode ι F) (x : S) : Prop :=
   let v := Matrix.vecMul (G x) (Matrix.of U)
   Finset.card T ≥ (Fintype.card ι) * (1 - γ) ∧
-  Code.restrictedWord v T ∈ Code.restrictedCode LC T
-
-
-
-def IsMCAGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_mca : ℝ≥0 → ℝ≥0)
-(hε_mca : Set.Icc 0 1 → Set.Icc 0 1) : Prop := sorry
-
+  Code.restrictedWord v T ∈ Code.restrictedCode LC T ∧
+  ∃ j : ℓ, Code.restrictedWord (U j) T ∉ Code.restrictedCode LC T
 
+def IsMCAGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F)
+  (ε_mca : Set.Icc 0 1 → Set.Icc 0 1) (U : ℓ → ι → F) (T : Finset ι) (LC : LinearCode ι F) : Prop :=
+  ∀ γ ∈ Set.Icc 0 1,
+  Pr_{let x ←$ᵖ S}[(Condition G U T γ LC x) ] ≤ Real.toEReal (ε_mca γ)
 
 
 -- def zeroEvading' {S : Set (ℓ → F)} [Nonempty S] (G : Generator S) (ε_ze : ℝ≥0∞) : Prop :=

From a3a501915fab500147ed111e9cf9b6db9fc7d180 Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Tue, 17 Mar 2026 23:32:03 +0000
Subject: [PATCH 03/14] change restricted code

---
 ArkLib/Data/CodingTheory/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/Basic.lean b/ArkLib/Data/CodingTheory/Basic.lean
index 6042c0346..d240f7b6d 100644
--- a/ArkLib/Data/CodingTheory/Basic.lean
+++ b/ArkLib/Data/CodingTheory/Basic.lean
@@ -1787,14 +1787,13 @@ lemma wt_eq_zero_iff [Zero F] {v : ι → F} :
   by_cases IsEmpty ι <;>
   aesop (add simp [wt, Finset.filter_eq_empty_iff])
 
-def restrictedWord (c : ι → F) (T : Finset ι) : T → F := fun i : T => c i
+def restrictedWord (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c
 
 /-- Let `C` be a code of length `ι`. For every subset `T ⊆ ι`, we define the restricted code `C|T`
 as the set of words `w` of length `T`, obtained by restricting `ι` to `T`. -/
 def restrictedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
   {w | ∃ c ∈ C, w = restrictedWord c T}
 
-
 end
 
 end

From 493788acb73befe6cfbd97e795d08aca3ef18d75 Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Thu, 19 Mar 2026 13:48:49 +0000
Subject: [PATCH 04/14] update dependencies

---
 ArkLib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/ArkLib.lean b/ArkLib.lean
index 563eda1be..49e444e5f 100644
--- a/ArkLib.lean
+++ b/ArkLib.lean
@@ -49,6 +49,7 @@ import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.ReedSolomonGap
 import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.WeightedAgreement
 import ArkLib.Data.CodingTheory.ProximityGap.Basic
 import ArkLib.Data.CodingTheory.ProximityGap.DG25
+import ArkLib.Data.CodingTheory.ProximityGap.ProximityGenerators
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.EllipticCurve.BN254
 import ArkLib.Data.Fin.Basic

From 5e8c610e2cbb1c2a47144dd9df716667f0afad21 Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Thu, 26 Mar 2026 14:12:46 +0000
Subject: [PATCH 05/14] RS codes are MDS

---
 ArkLib/Data/CodingTheory/ReedSolomon.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/ArkLib/Data/CodingTheory/ReedSolomon.lean b/ArkLib/Data/CodingTheory/ReedSolomon.lean
index f6eeb0f28..b00b2a97d 100644
--- a/ArkLib/Data/CodingTheory/ReedSolomon.lean
+++ b/ArkLib/Data/CodingTheory/ReedSolomon.lean
@@ -23,6 +23,7 @@ import Mathlib.Data.NNReal.Basic -- for instFloorSemiring of ℝ≥0
 
 * [Arnon, G., Chiesa, A., Fenzi, G., and Yogev, E., *WHIR: Reed–Solomon Proximity Testing
     with Super-Fast Verification*][ACFY24]
+* [Guruswami, V., Rudra, A., Sudan M., *Essential Coding Theory*, online copy][GRS25]
 -/
 
 namespace ReedSolomon
@@ -435,6 +436,13 @@ theorem minDist' {ι : Type*} [Fintype ι] [DecidableEq ι] {F : Type*} [Field F
       simp
     omega
 
+/-- Reed-Solomon codes are maximum distance separable (MDS). -/
+lemma isMDS_code {ι : Type*} [Fintype ι] [DecidableEq ι] {F : Type*} [Field F] [DecidableEq F]
+  {α : ι ↪ F} [NeZero n] (h : n ≤ Fintype.card ι) : LinearCode.IsMDS ((ReedSolomon.code α n)) := by
+  unfold IsMDS
+  rw [length_eq_domain_card', dim_eq_deg_of_le' h, Code.dist_eq_minDist]
+  exact minDist' h
+
 /-- Generalized distance equality for RS code with arbitrary finite index type `ι`. -/
 theorem dist_eq' {ι : Type*} [Fintype ι] [DecidableEq ι] {F : Type*} {n : ℕ} {α : ι ↪ F}
     [Field F] [DecidableEq F] [NeZero n] (h : n ≤ Fintype.card ι) :

From bf7f6c9210cb4973eb2faa2b8b4fea42f2c5a2a8 Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Thu, 26 Mar 2026 14:21:28 +0000
Subject: [PATCH 06/14] more coding theory results

---
 ArkLib/Data/CodingTheory/Basic.lean | 152 ++++++++++++----------------
 1 file changed, 64 insertions(+), 88 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/Basic.lean b/ArkLib/Data/CodingTheory/Basic.lean
index d240f7b6d..69a579eca 100644
--- a/ArkLib/Data/CodingTheory/Basic.lean
+++ b/ArkLib/Data/CodingTheory/Basic.lean
@@ -89,6 +89,12 @@ import CompPoly.Data.Nat.Bitwise
   We define the block length, rate, and distance of `C`. We prove simple properties of linear codes
   such as the singleton bound.
 
+## References
+
+* [Guruswami, V., Rudra, A., Sudan M., *Essential Coding Theory*, online copy][GRS25]
+* [Bordage, S., Chiesa, A., Guan, Z., Manzur, I., *All Polynomial Generators Preserve Distance
+with Mutual Correlated Agreement*][BSGM25]
+
 ## TODOs
 - Implement `ENNRat (ℚ≥0∞)`, for usage in `relDistFromCode` and `relDistFromCode'`,
   as counterpart of `ENat (ℕ∞)` in `distFromCode` and `distFromCode'`.
@@ -1787,12 +1793,21 @@ lemma wt_eq_zero_iff [Zero F] {v : ι → F} :
   by_cases IsEmpty ι <;>
   aesop (add simp [wt, Finset.filter_eq_empty_iff])
 
-def restrictedWord (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c
+/-- Let `c` be a word of length `ι`. For every finite `ι`-subset `T` , we define the projection of a
+word `c` to `T` as the word obtained by restricting the indexing set of `c` to `T`.
+We denote this by `c|[T]`.
+Definition 3.6 [BSGM25]. -/
+def projectedWord [Fintype ι] (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c
+
+notation:60 c "|[" T "]" => projectedWord c T
 
-/-- Let `C` be a code of length `ι`. For every subset `T ⊆ ι`, we define the restricted code `C|T`
-as the set of words `w` of length `T`, obtained by restricting `ι` to `T`. -/
-def restrictedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
-  {w | ∃ c ∈ C, w = restrictedWord c T}
+/-- Let `C` be a code of length `ι`. For every finite `ι`-subset `T`, we define the projected code
+`C|[T]` as the set of projected codewords `c|[T]`, for `c ∈ C`.
+Definition 3.6 [BSGM25]. -/
+def projectedCode [Fintype ι] (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
+  {w | ∃ c ∈ C, w = c|[T]}
+
+notation:60 C "|[" T "]" => projectedCode C T
 
 end
 
@@ -1940,8 +1955,6 @@ abbrev LinearCode.{u, v} (ι : Type u) [Fintype ι] (F : Type v) [Semiring F] :
 lemma LinearCode_is_ModuleCode.{u, v} {ι : Type u} [Fintype ι] {F : Type v} [Semiring F]
     : LinearCode ι F = ModuleCode ι F F := by rfl
 
--- TODO: MDS code
-
 namespace LinearCode
 
 section
@@ -1951,16 +1964,15 @@ variable {F : Type*} {A : Type*} [AddCommMonoid A]
          {κ : Type*} [Fintype κ]
 
 /-- Module code defined by left multiplication by its generator matrix.
-  For a matrix G : Matrix κ ι F (over field F) and module A over F, this generates
-  the F-submodule of (ι → A) spanned by the rows of G acting on (κ → A).
-  The matrix acts on vectors v : κ → A by: (G • v)(i) = ∑ k, G k i • v k
-  where G k i : F is the scalar and v k : A is the module element.
+For a matrix G : Matrix κ ι F (over field F) and module A over F, this generates
+the F-submodule of (ι → A) spanned by the rows of G acting on (κ → A).
+The matrix acts on vectors v : κ → A by: (G • v)(i) = ∑ k, G k i • v k
+where G k i : F is the scalar and v k : A is the module element.
 -/
 noncomputable def fromRowGenMat [Semiring F] (G : Matrix κ ι F) : LinearCode ι F :=
   LinearMap.range G.vecMulLinear
 
-/-- Linear code defined by right multiplication by a generator matrix.
--/
+/-- Linear code defined by right multiplication by a generator matrix. -/
 noncomputable def fromColGenMat [CommRing F] (G : Matrix ι κ F) : LinearCode ι F :=
   LinearMap.range G.mulVecLin
 
@@ -2039,85 +2051,49 @@ scoped syntax &"ρ" term : term
 scoped macro_rules
   | `(ρ $t:term) => `(LinearCode.rate $t)
 
+/-- Every linear code over a field `F` is a finitely generated `F`-module. -/
+lemma linear_code_is_FG [Field F] (LC : LinearCode ι F) : LC.FG := Submodule.FG.of_finite
 
--- open Classical in
--- lemma gen_matrix_exists [Semiring F] [Nonempty ι] (LC : LinearCode ι F) : ∃ (G : Matrix κ ι F),
---   LC = fromRowGenMat G := by
---   unfold fromRowGenMat
---   simp only [range_vecMulLinear]
---   have : LC.FG := by
---     unfold LinearCode at LC
---     have h₁ : LC ≤ ⊤ := by
---       simp only [le_top]
---     have {a b : LinearCode ι F} : a ≤ b → b.FG → a.FG := by
---       unfold LinearCode at a b
---       intros h h'
---       rw [Submodule.fg_def] at h'
---       rcases h' with ⟨s, hs, hspanB⟩
---       refine Submodule.spanRank_finite_iff_fg.mp ?_
---       sorry
---     apply this h₁
---     rw [@Submodule.fg_def]
---     use (Finset.image (fun (i j : ι) ↦ if i = j then 1 else 0) Fintype.elems).toSet
---     have {s : Finset (ι → F)} : s.toSet.Finite := by
---       simp
---     apply And.intro this
---     simp only [Finset.coe_image]
---     apply Submodule.eq_top_iff'.mpr
---     intros x
---     apply (mem_span_image_iff_exists_fun F).mpr
---     use (fun y ↦ x y)
---     ext y
---     rw [sum_apply]
---     rw [Finset.sum_eq_single]
---     swap
---     exact ⟨y, by simp only [SetLike.mem_coe]; exact complete y⟩
---     · simp
---     · intros b _ h
---       simp
---       intros h'
---       aesop
---     · simp
-
-
---   have : ∃ S : Set (ι → F), LC = Submodule.span F S  := by
---     use LC
---     simp
-
---   have blah := @Submodule.instNonemptySubtypeSetEqSpan LC
-
---   sorry
-
-
-lemma linCode_FG [Field F] (LC : LinearCode ι F) : LC.FG := by
-  exact Submodule.FG.of_finite
-
-
-open Classical in
-lemma gen_matrix_exists' [Field F] [Fintype F] [Nonempty ι] (LC : LinearCode ι F) : ∃ (G : Matrix κ ι F),
-  LC = fromRowGenMat G := by
+/-- Given a linear code of length `ι` and dimension `dim` over a field `F`, there exists a
+`dim x ι` matrix over `F` which generates the code. -/
+lemma gen_matrix_exists [Field F] (LC : LinearCode ι F) :
+    ∃ (G : Matrix (Fin (dim LC)) ι F), LC = fromRowGenMat G := by
   unfold fromRowGenMat
-  simp only [range_vecMulLinear]
-  have LC_FG : LC.FG := linCode_FG LC
-  have LC_genSet : ∃ S : Set (ι → F), LC = Submodule.span F S  := by
-    use LC
-    simp
-  rcases LC_genSet with ⟨S, S_spans_LC⟩
-  have S_Finite : S.Finite := Set.toFinite S
-  rw [S_spans_LC]
-
-  sorry
-
-
-/-- A linear code is maximum distance separable (MDS) if  its parameters meet the Singleton bound.
--/
-def IsMDSCode [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=
+  have LC_basis := Module.finBasis F LC
+  let G : Matrix (Fin (Module.finrank F ↥LC)) ι F :=
+    fun i => LC_basis i
+  use G
+  simp only [range_vecMulLinear, G, Matrix.row]
+  ext x
+  rw [Submodule.mem_span_range_iff_exists_fun]
+  constructor
+  · intros h
+    use LC_basis.equivFun ⟨x, h⟩
+    have x_to_lin_comb : (⟨x, h⟩ : LC).1 = ∑ i, LC_basis.equivFun ⟨x, h⟩ i • (LC_basis i).1 := by
+      rw (occs := .pos [1]) [←Module.Basis.sum_equivFun LC_basis ⟨x, h⟩, @Submodule.coe_sum]
+      congr
+    simp only [Module.Basis.equivFun_apply] at x_to_lin_comb ⊢
+    exact x_to_lin_comb.symm
+  · rintro ⟨x, h⟩
+    rw [←h]
+    apply Submodule.sum_smul_mem LC x
+    intros c _
+    exact Submodule.coe_mem (LC_basis c)
+
+/-- Given a linear code of length `ι` and dimension `dim` over a field `F`, we define its `dim x ι`
+generator matrix as a matrix whose rows are an `F`-basis of the code. -/
+noncomputable def genMatrixFromCode [Field F] (LC : LinearCode ι F) : Matrix (Fin (dim LC)) ι F :=
+  fun i => Module.finBasis F LC i
+
+/-- A linear code is maximum distance separable (MDS) if its parameters meet the singleton bound. -/
+def IsMDS [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=
   Code.dist LC.carrier = length LC - dim LC + 1
 
-/-- A linear code of length `ι` and dimension `dim` is MDS if and only if any `dim` rows of its
-generator matrix are linearly independent. -/
-lemma MDS_iff_dim_lin_ind_rows_in_GenMatrix [CommRing F] [DecidableEq F] (LC : LinearCode ι F) :
-  IsMDSCode LC ↔ sorry := by sorry
+/-- A linear code `LC` of length `ι` and dimension `dim` over a field `F` is MDS if any `dim` columns
+of the generator matrix whose rows are an `F`-basis of `LC` are linearly independent. [GRS25] -/
+lemma colRank_genMatrix_eq_dim_of_MDS [Field F] [DecidableEq F] (LC : LinearCode ι F) :
+    Matrix.colRank (genMatrixFromCode LC) = dim LC := by
+  sorry
 
 end
 

From 768c2c164d7a833e255b9d20658477aecee913ec Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Thu, 26 Mar 2026 14:24:20 +0000
Subject: [PATCH 07/14] WIP

---
 .../CodingTheory/ProximityGap/ProximityGenerators.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
index 1f7e9b6a2..817099c48 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
@@ -58,7 +58,9 @@ module codes over (scalar) rings.
   Proximity gaps for Reed–Solomon codes. In 2020 IEEE 61st Annual Symposium on Foundations of
   Computer Science (FOCS), 2020. Full paper: https://eprint.iacr.org/2020/654, version 20210703:203025.
 
-
+* [Guruswami, V., Rudra, A., Sudan M., *Essential Coding Theory*, online copy][GRS25]
+* [Bordage, S., Chiesa, A., Guan, Z., Manzur, I., *All Polynomial Generators Preserve Distance
+with Mutual Correlated Agreement*][BSGM25]
 -/
 
 namespace Generator
@@ -93,7 +95,7 @@ def M_G {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Matrix S 
   Matrix.of G
 
 def IsMDSGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Prop :=
- LinearCode.IsMDSCode (LinearCode.fromRowGenMat (M_G G))
+ IsMDS (LinearCode.fromRowGenMat (M_G G))
 
 
 /-- A subset of `ι` is dense if `|T| ≥ |ι| * (1 − γ)`, for some γ -/
@@ -104,8 +106,8 @@ def Condition {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (U : 
   (T : Finset ι) (γ : ℝ) (LC : LinearCode ι F) (x : S) : Prop :=
   let v := Matrix.vecMul (G x) (Matrix.of U)
   Finset.card T ≥ (Fintype.card ι) * (1 - γ) ∧
-  Code.restrictedWord v T ∈ Code.restrictedCode LC T ∧
-  ∃ j : ℓ, Code.restrictedWord (U j) T ∉ Code.restrictedCode LC T
+  Code.projectedWord v T ∈ Code.projectedCode LC T ∧
+  ∃ j : ℓ, Code.projectedWord (U j) T ∉ Code.projectedCode LC T
 
 def IsMCAGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F)
   (ε_mca : Set.Icc 0 1 → Set.Icc 0 1) (U : ℓ → ι → F) (T : Finset ι) (LC : LinearCode ι F) : Prop :=

From cf14a184158f5a096af2ad8f5e3c5a45972541ac Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Thu, 26 Mar 2026 16:52:07 +0000
Subject: [PATCH 08/14] cleanup

---
 .../ProximityGap/ProximityGenerators.lean     | 120 +++++++-----------
 1 file changed, 45 insertions(+), 75 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
index 817099c48..eb4c70207 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
@@ -4,71 +4,44 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Katerina Hristova
 -/
 
--- import ArkLib.Data.CodingTheory.Basic
--- import ArkLib.Data.CodingTheory.GuruswamiSudan
--- import ArkLib.Data.CodingTheory.Prelims
--- import ArkLib.Data.CodingTheory.ReedSolomon
--- import ArkLib.Data.CodingTheory.InterleavedCode
--- import ArkLib.Data.Polynomial.Bivariate
--- import ArkLib.Data.Polynomial.RationalFunctions
--- import ArkLib.Data.Probability.Notation
--- import Mathlib.Algebra.Field.Basic
--- import Mathlib.Algebra.Lie.OfAssociative
--- import Mathlib.Algebra.Module.Submodule.Defs
--- import Mathlib.Algebra.Polynomial.Basic
--- import Mathlib.Data.Finset.BooleanAlgebra
--- import Mathlib.Data.Real.Basic
--- import Mathlib.Data.Real.Sqrt
--- import Mathlib.Data.Set.Defs
--- import Mathlib.FieldTheory.RatFunc.AsPolynomial
--- import Mathlib.FieldTheory.Separable
--- import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
--- import Mathlib.Probability.Distributions.Uniform
--- import Mathlib.RingTheory.Henselian
--- import Mathlib.RingTheory.PowerSeries.Basic
--- import Mathlib.RingTheory.PowerSeries.Substitution
--- import Mathlib.LinearAlgebra.Matrix.Vec
--- import Mathlib.Data.Matrix.Mul
--- import Mathlib.Order.SetNotation
-
-import Mathlib.Probability.Distributions.Uniform
-import Mathlib.Algebra.MvPolynomial.Basic
-import Mathlib.LinearAlgebra.LinearIndependent.Defs
 import ArkLib.Data.CodingTheory.Basic
 import ArkLib.Data.Probability.Notation
 import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.MvPolynomial.Basic
+import Mathlib.LinearAlgebra.LinearIndependent.Defs
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.Probability.Distributions.Uniform
 import Mathlib.Topology.UnitInterval
-import Mathlib
+
+
 
 /-!
 # Proximity Generators fundamental definitions
 
-Define the fundamental definitions for proximity gap properties of generic codes and
-module codes over (scalar) rings.
+Define the fundamental definitions for generators functions.
 
 ## Main Definitions
 
-### Proximity Gap Definitions
-- `proximityMeasure`: Counts vectors close to linear combinations with code `C`
-
+- `generator`: a generator `G` over a field `F` with output size `ℓ` is a function that maps a seed
+`x` in a set `S` to a coefficient vector in `F^ℓ`
+- `zero-evading generators`: a generator is zero-evading with a zero-evading error `ε_ze` if the
+probability of obtaining a zero output from a non-zero vector is bounded above by `ε_ze`
+- `polynomial generator`: the output is defined by `ℓ` linearly independent multivariate polynomials
+- `MDS generator`: A generator is MDS if the matrix whose rows are the outputs of the generator
+function is a generator matrix for an MDS code
+- `MCA generator`
 
 ## References
 
-- [BCIKS20] Eli Ben-Sasson, Dan Carmon, Yuval Ishai, Swastik Kopparty, and Shubhangi Saraf.
-  Proximity gaps for Reed–Solomon codes. In 2020 IEEE 61st Annual Symposium on Foundations of
-  Computer Science (FOCS), 2020. Full paper: https://eprint.iacr.org/2020/654, version 20210703:203025.
-
 * [Guruswami, V., Rudra, A., Sudan M., *Essential Coding Theory*, online copy][GRS25]
 * [Bordage, S., Chiesa, A., Guan, Z., Manzur, I., *All Polynomial Generators Preserve Distance
-with Mutual Correlated Agreement*][BSGM25]
+with Mutual Correlated Agreement*][BSGM25]. Full paper : https://eprint.iacr.org/2025/2051}
 -/
 
-namespace Generator
+namespace CoreDefinitions
 
-open NNReal Finset Function ENNReal
+open NNReal ENNReal
 open scoped ProbabilityTheory
-open scoped BigOperators
-open unitInterval
 
 section
 
@@ -76,32 +49,39 @@ variable {ι : Type} [Fintype ι] [DecidableEq ι]
          {F : Type} [Field F] [Fintype F] [DecidableEq F]
          {ℓ : Type} [Fintype ℓ]
 
+/-- The type of generators, where a generator `G` over a field `F` with output size `ℓ` is a function
+that maps a seed `x` in a set `S` to a coefficient vector in `F^ℓ`.
+Definition 3.10 [BSGM25]. -/
 def Generator (S ℓ F : Type) : Type := S → (ℓ → F)
 
--- noncomputable instance {S : Set (ι → F)} : Fintype S := Fintype.ofFinite ↑S
-
--- noncomputable def probs {S : Set (ℓ → F)} [Nonempty S] (G : Generator S) : Set ENNReal :=
---   {y | ∃ v : ℓ → F, v ≠ 0 ∧ y = Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]}
-
-def IsZeroEvadingGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_ze : ℝ≥0∞) : Prop :=
-  ε_ze ∈ Set.Icc 0 1 ∧
-  (SupSet.sSup {y | ∃ v : ℓ → F, v ≠ 0 ∧ y = Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]}) ≤ ε_ze
-
-def IsPolynomialGen {s : ℕ} {S : Fin s → Set F} (G : Generator (∀ i, S i) ℓ F) : Prop :=
+/-- A generator `G` is zero-evading with a zero-evading error `ε_ze` if the probability of obtaining
+a zero output from a non-zero vector is bounded above by `ε_ze`.
+Definition 3.11 [BSGM25]. -/
+def IsZeroEvadingGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_ze : ℝ≥0∞) :
+    Prop :=
+    ε_ze ∈ Set.Icc 0 1 ∧
+    (SupSet.sSup {y | ∃ v : ℓ → F, v ≠ 0 ∧ y = Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]}) ≤ ε_ze
+
+/-- Let the set `S` be a product of `ℓ` subsets of `F`. A polynomial generator is a generator if
+there exist `ℓ` linearly independent multivariate polynomials, such that the output is an evaluation
+of the seed at each of these polynomials.
+Definition 3.19 [BSGM25]. -/
+def IsPolynomialGenerator {s : ℕ} {S : Fin s → Set F} (G : Generator (∀ i, S i) ℓ F) : Prop :=
   ∃ P : ℓ → MvPolynomial (Fin s) F, LinearIndependent F P ∧
   ∀ x : (∀ i, S i), G x = MvPolynomial.eval (fun i ↦ x i) ∘ P
 
+/-- A matrix whose rows are the outputs of the generator function.
+Defined inside Definition 3.5 [BSGM25]. -/
 def M_G {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Matrix S ℓ F :=
   Matrix.of G
 
-def IsMDSGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Prop :=
- IsMDS (LinearCode.fromRowGenMat (M_G G))
-
-
-/-- A subset of `ι` is dense if `|T| ≥ |ι| * (1 − γ)`, for some γ -/
-def IsDenseSet (T : Finset ι) (γ : ℝ) : Prop := Finset.card T ≥ (Fintype.card ι) * (1 - γ)
-
+/-- A generator `G` is MDS if the matrix `M_G` whose rows are the outputs of the generator
+function is a generator matrix for an MDS code.
+Definition 3.5 [BSGM25]. -/
+def IsMDSGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Prop :=
+ LinearCode.IsMDS (LinearCode.fromRowGenMat (M_G G))
 
+/-- The condition for MCA generator. -/
 def Condition {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (U : ℓ → ι → F)
   (T : Finset ι) (γ : ℝ) (LC : LinearCode ι F) (x : S) : Prop :=
   let v := Matrix.vecMul (G x) (Matrix.of U)
@@ -109,22 +89,12 @@ def Condition {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (U : 
   Code.projectedWord v T ∈ Code.projectedCode LC T ∧
   ∃ j : ℓ, Code.projectedWord (U j) T ∉ Code.projectedCode LC T
 
-def IsMCAGen {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F)
+/-- Definition 3.14 [BSGM25]. -/
+def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F)
   (ε_mca : Set.Icc 0 1 → Set.Icc 0 1) (U : ℓ → ι → F) (T : Finset ι) (LC : LinearCode ι F) : Prop :=
   ∀ γ ∈ Set.Icc 0 1,
   Pr_{let x ←$ᵖ S}[(Condition G U T γ LC x) ] ≤ Real.toEReal (ε_mca γ)
 
-
--- def zeroEvading' {S : Set (ℓ → F)} [Nonempty S] (G : Generator S) (ε_ze : ℝ≥0∞) : Prop :=
---   ε_ze ∈ Set.Icc 0 1 ∧
---   (SupSet.sSup
---     (
---       Set.image
---         (fun (v : ℓ → F) ↦ (Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]))
---         {v | v ≠ 0}
---     )
---   ) ≤ ε_ze
-
 end
 
-end Generator
+end CoreDefinitions

From bd2af9df5367175b9a278691ff243d63a3d9df9e Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Thu, 26 Mar 2026 21:16:21 +0000
Subject: [PATCH 09/14] remove extra lemma until proved

---
 ArkLib/Data/CodingTheory/Basic.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/Basic.lean b/ArkLib/Data/CodingTheory/Basic.lean
index 69a579eca..c3b300064 100644
--- a/ArkLib/Data/CodingTheory/Basic.lean
+++ b/ArkLib/Data/CodingTheory/Basic.lean
@@ -2089,12 +2089,6 @@ noncomputable def genMatrixFromCode [Field F] (LC : LinearCode ι F) : Matrix (F
 def IsMDS [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=
   Code.dist LC.carrier = length LC - dim LC + 1
 
-/-- A linear code `LC` of length `ι` and dimension `dim` over a field `F` is MDS if any `dim` columns
-of the generator matrix whose rows are an `F`-basis of `LC` are linearly independent. [GRS25] -/
-lemma colRank_genMatrix_eq_dim_of_MDS [Field F] [DecidableEq F] (LC : LinearCode ι F) :
-    Matrix.colRank (genMatrixFromCode LC) = dim LC := by
-  sorry
-
 end
 
 section

From 81adf532dcbf654b818a1aa758fb6a4de4edf265 Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Thu, 26 Mar 2026 21:16:50 +0000
Subject: [PATCH 10/14] minor corrections

---
 .../ProximityGap/ProximityGenerators.lean     | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
index eb4c70207..044924169 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
@@ -14,7 +14,6 @@ import Mathlib.Probability.Distributions.Uniform
 import Mathlib.Topology.UnitInterval
 
 
-
 /-!
 # Proximity Generators fundamental definitions
 
@@ -38,13 +37,13 @@ function is a generator matrix for an MDS code
 with Mutual Correlated Agreement*][BSGM25]. Full paper : https://eprint.iacr.org/2025/2051}
 -/
 
+section
+
 namespace CoreDefinitions
 
 open NNReal ENNReal
 open scoped ProbabilityTheory
 
-section
-
 variable {ι : Type} [Fintype ι] [DecidableEq ι]
          {F : Type} [Field F] [Fintype F] [DecidableEq F]
          {ℓ : Type} [Fintype ℓ]
@@ -68,7 +67,7 @@ of the seed at each of these polynomials.
 Definition 3.19 [BSGM25]. -/
 def IsPolynomialGenerator {s : ℕ} {S : Fin s → Set F} (G : Generator (∀ i, S i) ℓ F) : Prop :=
   ∃ P : ℓ → MvPolynomial (Fin s) F, LinearIndependent F P ∧
-  ∀ x : (∀ i, S i), G x = MvPolynomial.eval (fun i ↦ x i) ∘ P
+  ∀ x : (∀ i, S i), G x = MvPolynomial.eval (fun i ↦ (x i : F)) ∘ P
 
 /-- A matrix whose rows are the outputs of the generator function.
 Defined inside Definition 3.5 [BSGM25]. -/
@@ -85,16 +84,16 @@ def IsMDSGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) :
 def Condition {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (U : ℓ → ι → F)
   (T : Finset ι) (γ : ℝ) (LC : LinearCode ι F) (x : S) : Prop :=
   let v := Matrix.vecMul (G x) (Matrix.of U)
-  Finset.card T ≥ (Fintype.card ι) * (1 - γ) ∧
+  (T.card : ℝ) ≥ (Fintype.card ι) * (1 - γ) ∧
   Code.projectedWord v T ∈ Code.projectedCode LC T ∧
   ∃ j : ℓ, Code.projectedWord (U j) T ∉ Code.projectedCode LC T
 
 /-- Definition 3.14 [BSGM25]. -/
 def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F)
-  (ε_mca : Set.Icc 0 1 → Set.Icc 0 1) (U : ℓ → ι → F) (T : Finset ι) (LC : LinearCode ι F) : Prop :=
-  ∀ γ ∈ Set.Icc 0 1,
-  Pr_{let x ←$ᵖ S}[(Condition G U T γ LC x) ] ≤ Real.toEReal (ε_mca γ)
-
-end
+  (ε_mca : ℝ → ℝ) (U : ℓ → ι → F) (T : Finset ι) (LC : LinearCode ι F) : Prop :=
+  ε_mca  ∈ Set.Icc 0 1 ∧
+  ∀ γ ∈ Set.Icc 0 1, Pr_{let x ←$ᵖ S}[(Condition G U T γ LC x) ] ≤ ENNReal.ofReal (ε_mca γ)
 
 end CoreDefinitions
+
+end

From 6696a7d5cfe8c9d03f77489d6232a1342a82579a Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Tue, 31 Mar 2026 14:36:05 +0300
Subject: [PATCH 11/14] more edits

---
 ArkLib/Data/CodingTheory/Basic.lean           | 14 +++++-
 .../ProximityGap/ProximityGenerators.lean     | 45 ++++++++++---------
 2 files changed, 37 insertions(+), 22 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/Basic.lean b/ArkLib/Data/CodingTheory/Basic.lean
index c3b300064..e68f102d9 100644
--- a/ArkLib/Data/CodingTheory/Basic.lean
+++ b/ArkLib/Data/CodingTheory/Basic.lean
@@ -2055,7 +2055,8 @@ scoped macro_rules
 lemma linear_code_is_FG [Field F] (LC : LinearCode ι F) : LC.FG := Submodule.FG.of_finite
 
 /-- Given a linear code of length `ι` and dimension `dim` over a field `F`, there exists a
-`dim x ι` matrix over `F` which generates the code. -/
+`dim x ι` matrix over `F` which generates the code.
+Theorem 2.2.7 [GRS25]. -/
 lemma gen_matrix_exists [Field F] (LC : LinearCode ι F) :
     ∃ (G : Matrix (Fin (dim LC)) ι F), LC = fromRowGenMat G := by
   unfold fromRowGenMat
@@ -2085,10 +2086,21 @@ generator matrix as a matrix whose rows are an `F`-basis of the code. -/
 noncomputable def genMatrixFromCode [Field F] (LC : LinearCode ι F) : Matrix (Fin (dim LC)) ι F :=
   fun i => Module.finBasis F LC i
 
+/-- Given a linear code of length `ι` and dimension `dim` over a field `F`, we define its `dim x ι`
+generator matrix as a matrix whose columns are an `F`-basis of the code. -/
+noncomputable def genMatrixFromCode' [Field F] (LC : LinearCode ι F) : Matrix ι (Fin (dim LC)) F :=
+  (genMatrixFromCode LC).transpose
+
 /-- A linear code is maximum distance separable (MDS) if its parameters meet the singleton bound. -/
 def IsMDS [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=
   Code.dist LC.carrier = length LC - dim LC + 1
 
+/-- A linear code `LC` of length `ι` and dimension `dim` over a field `F` is MDS if any `dim` columns
+of the generator matrix whose rows are an `F`-basis of `LC` are linearly independent. [GRS25] -/
+lemma colRank_genMatrix_eq_dim_of_MDS [Field F] [DecidableEq F] (LC : LinearCode ι F) :
+    Matrix.colRank (genMatrixFromCode LC) = dim LC := by
+  sorry
+
 end
 
 section
diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
index 044924169..268c16d2e 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
@@ -41,25 +41,25 @@ section
 
 namespace CoreDefinitions
 
-open NNReal ENNReal
+open NNReal ENNReal unitInterval
 open scoped ProbabilityTheory
 
-variable {ι : Type} [Fintype ι] [DecidableEq ι]
-         {F : Type} [Field F] [Fintype F] [DecidableEq F]
+variable {ι : Type} [Fintype ι]
+         {F : Type} [Field F] [Fintype F]
          {ℓ : Type} [Fintype ℓ]
 
-/-- The type of generators, where a generator `G` over a field `F` with output size `ℓ` is a function
-that maps a seed `x` in a set `S` to a coefficient vector in `F^ℓ`.
+/-- The type of generators, where a generator `G` over a field `F` with output size `ℓ` is a
+function that maps a seed `x` in a set `S` to a coefficient vector in `F^ℓ`.
 Definition 3.10 [BSGM25]. -/
 def Generator (S ℓ F : Type) : Type := S → (ℓ → F)
 
 /-- A generator `G` is zero-evading with a zero-evading error `ε_ze` if the probability of obtaining
 a zero output from a non-zero vector is bounded above by `ε_ze`.
 Definition 3.11 [BSGM25]. -/
-def IsZeroEvadingGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_ze : ℝ≥0∞) :
-    Prop :=
-    ε_ze ∈ Set.Icc 0 1 ∧
-    (SupSet.sSup {y | ∃ v : ℓ → F, v ≠ 0 ∧ y = Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]}) ≤ ε_ze
+def IsZeroEvadingGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_ze : I) :
+  Prop :=
+  (sSup {y | ∃ v : ℓ → F, v ≠ 0 ∧ y = Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]})
+    ≤ ENNReal.ofReal ε_ze
 
 /-- Let the set `S` be a product of `ℓ` subsets of `F`. A polynomial generator is a generator if
 there exist `ℓ` linearly independent multivariate polynomials, such that the output is an evaluation
@@ -70,29 +70,32 @@ def IsPolynomialGenerator {s : ℕ} {S : Fin s → Set F} (G : Generator (∀ i,
   ∀ x : (∀ i, S i), G x = MvPolynomial.eval (fun i ↦ (x i : F)) ∘ P
 
 /-- A matrix whose rows are the outputs of the generator function.
-Defined inside Definition 3.5 [BSGM25]. -/
+Defined inside Definition 3.12 [BSGM25]. -/
 def M_G {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Matrix S ℓ F :=
   Matrix.of G
 
+noncomputable example {S : Type} [Nonempty S] [Fintype S] [DecidableEq F] (G : Generator S ℓ F) :
+  LinearCode S F := LinearCode.fromColGenMat (M_G G)
+
 /-- A generator `G` is MDS if the matrix `M_G` whose rows are the outputs of the generator
 function is a generator matrix for an MDS code.
-Definition 3.5 [BSGM25]. -/
-def IsMDSGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Prop :=
- LinearCode.IsMDS (LinearCode.fromRowGenMat (M_G G))
+Definition 3.12 [BSGM25]. -/
+def IsMDSGenerator {S : Type} [Nonempty S] [Fintype S] [DecidableEq F] (G : Generator S ℓ F) :
+  Prop := LinearCode.IsMDS (LinearCode.fromColGenMat (M_G G))
 
 /-- The condition for MCA generator. -/
-def Condition {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (U : ℓ → ι → F)
-  (T : Finset ι) (γ : ℝ) (LC : LinearCode ι F) (x : S) : Prop :=
-  let v := Matrix.vecMul (G x) (Matrix.of U)
-  (T.card : ℝ) ≥ (Fintype.card ι) * (1 - γ) ∧
+def Condition {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (LC : LinearCode ι F)
+  (x : S) (U : ℓ → (ι → F)) (γ : I) : Prop :=
+  let v := Matrix.vecMul (G x) (U)
+  ∃ (T : Finset ι), (T.card : ℝ) ≥ (Fintype.card ι) * (1 - γ) ∧
   Code.projectedWord v T ∈ Code.projectedCode LC T ∧
   ∃ j : ℓ, Code.projectedWord (U j) T ∉ Code.projectedCode LC T
 
 /-- Definition 3.14 [BSGM25]. -/
-def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F)
-  (ε_mca : ℝ → ℝ) (U : ℓ → ι → F) (T : Finset ι) (LC : LinearCode ι F) : Prop :=
-  ε_mca  ∈ Set.Icc 0 1 ∧
-  ∀ γ ∈ Set.Icc 0 1, Pr_{let x ←$ᵖ S}[(Condition G U T γ LC x) ] ≤ ENNReal.ofReal (ε_mca γ)
+def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_mca : I → I)
+  (LC : LinearCode ι F) : Prop :=
+  ∀ U : ℓ → (ι → F), ∀ γ : I,
+    Pr_{let x ←$ᵖ S}[(Condition G LC x U γ)] ≤ ENNReal.ofReal (ε_mca γ)
 
 end CoreDefinitions
 

From c8ce0c8291e0f8feebb247fe50ca5927611f4a4b Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Fri, 3 Apr 2026 00:42:54 +0300
Subject: [PATCH 12/14] MDS matrices

---
 ArkLib/Data/CodingTheory/Prelims.lean | 33 +++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/Prelims.lean b/ArkLib/Data/CodingTheory/Prelims.lean
index f00a3a3ca..398b80b19 100644
--- a/ArkLib/Data/CodingTheory/Prelims.lean
+++ b/ArkLib/Data/CodingTheory/Prelims.lean
@@ -7,6 +7,8 @@ Authors: Katerina Hristova, František Silváši, Julian Sutherland, Chung Thai
 import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.LinearAlgebra.Matrix.Rank
 import Mathlib.LinearAlgebra.AffineSpace.Pointwise
+import Mathlib.LinearAlgebra.AffineSpace.Combination
+import Mathlib.RingTheory.Henselian
 
 section TensorCombination
 variable {F : Type*} [CommRing F] [Fintype F] [DecidableEq F]
@@ -35,7 +37,7 @@ noncomputable section
 variable {F : Type*}
          {ι : Type*} [Fintype ι]
          {ι' : Type*} [Fintype ι']
-         {m n : ℕ}
+         {m n k : ℕ}
 
 namespace Matrix
 
@@ -63,6 +65,12 @@ def colSpan : Submodule F (ι → F) :=
 def colRank : ℕ :=
   Module.finrank F (colSpan U)
 
+/-- A `k × n` matrix is MDS (Maximum Distance Separable) if every square `k × k` submatrix
+obtained by selecting `k` columns has nonzero determinant. Equivalently, every set of `k` columns
+is linearly independent. -/
+def IsMDS [CommRing F] (G : Matrix (Fin k) (Fin n) F) : Prop :=
+  ∀ σ : Fin k ↪ Fin n, (G.submatrix id σ).det ≠ 0
+
 
 end
 
@@ -81,7 +89,7 @@ variable [CommRing F] [Nontrivial F]
 
 /-- An m×n matrix has full rank if the submatrix consisting of rows 1 through n has rank n. -/
 lemma rank_eq_if_subUpFull_eq (h : n ≤ m) :
-   (subUpFull U (Fin.castLE h)).rank = n  → U.rank = n  := by
+   (subUpFull U (Fin.castLE h)).rank = n → U.rank = n := by
    intro h_sub_mat_rank
    apply le_antisymm
    ·  exact Matrix.rank_le_width U
@@ -167,6 +175,27 @@ lemma rank_eq_min_row_col_rank : U.rank = min (rowRank U) (colRank U) := by
   rw [rowRank_eq_colRank, rank_eq_colRank]
   simp_all only [min_self]
 
+/-- An MDS matrix has rank equal to its number of rows. The proof selects the first `k` columns
+to form a nonsingular square submatrix `H`, deduces `rank H = k`, and then shows `rank G ≥ k`
+via the factorisation `H = G * Pᵀ`. The upper bound `rank G ≤ k` is `rank_le_card_height`. -/
+lemma rank_eq_of_IsMDS [Field F] {G : Matrix (Fin k) (Fin n) F}
+    (hMDS : G.IsMDS) (hkn : k ≤ n) : G.rank = k := by
+  set H : Matrix (Fin k) (Fin k) F := G.subLeftFull (Fin.castLE hkn)
+  rw [full_row_rank_via_rank_subLeftFull hkn]
+  rw [@rank_eq_iff_det_ne_zero]
+  have : ∀ σ : Fin k ↪ Fin n, (G.submatrix id σ).det ≠ 0 := hMDS
+  have hh : G.subLeftFull (Fin.castLE hkn) = (G.submatrix id (Fin.castLEEmb hkn)) := rfl
+  rw [hh]
+  apply this
+
+
+/-- **Column rank of an MDS matrix**: for an MDS matrix `G : Matrix (Fin k) (Fin n) F`
+with `k ≤ n`, the column rank equals `k` (the number of rows / code dimension). -/
+theorem colRank_genMatrix_eq_dim_of_MDS [Field F] {G : Matrix (Fin k) (Fin n) F}
+    (hMDS : G.IsMDS) (hkn : k ≤ n) : colRank G = k := by
+  rw [←rank_eq_colRank]
+  exact rank_eq_of_IsMDS hMDS hkn
+
 end
 
 end Matrix

From 535ee6c1cbe6fd3b9534f8b786653e8b1cec1a9d Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Fri, 3 Apr 2026 00:44:19 +0300
Subject: [PATCH 13/14] more progress on MDS lemmas

---
 ArkLib/Data/CodingTheory/Basic.lean | 65 +++++++++++++++++++++++++----
 1 file changed, 56 insertions(+), 9 deletions(-)

diff --git a/ArkLib/Data/CodingTheory/Basic.lean b/ArkLib/Data/CodingTheory/Basic.lean
index e68f102d9..85bda6107 100644
--- a/ArkLib/Data/CodingTheory/Basic.lean
+++ b/ArkLib/Data/CodingTheory/Basic.lean
@@ -16,6 +16,7 @@ import Mathlib.Topology.MetricSpace.Infsep
 import Mathlib.Data.Real.ENatENNReal
 import CompPoly.Data.Nat.Bitwise
 
+
 /-!
   # Basics of Coding Theory
 
@@ -2081,25 +2082,71 @@ lemma gen_matrix_exists [Field F] (LC : LinearCode ι F) :
     intros c _
     exact Submodule.coe_mem (LC_basis c)
 
-/-- Given a linear code of length `ι` and dimension `dim` over a field `F`, we define its `dim x ι`
-generator matrix as a matrix whose rows are an `F`-basis of the code. -/
-noncomputable def genMatrixFromCode [Field F] (LC : LinearCode ι F) : Matrix (Fin (dim LC)) ι F :=
+def IsGenMatrix [Field F] (LC : LinearCode ι F) (G : Matrix (Fin (dim LC)) ι F) : Prop :=
+  LC = fromRowGenMat G
+
+noncomputable def matrix_from_basis [Field F] (LC : LinearCode ι F) : Matrix (Fin (dim LC)) ι F :=
   fun i => Module.finBasis F LC i
 
+/-- A linear code is the `F`-submodule spanned by the rows of its generator matrix. -/
+lemma eq_span_rows [Field F] (LC : LinearCode ι F) :
+    LC = Submodule.span F (Set.range LC.matrix_from_basis) := by
+  unfold matrix_from_basis
+  ext x
+  rw [Submodule.mem_span_range_iff_exists_fun]
+  constructor
+  · intros h
+    use (Module.finBasis F LC).equivFun ⟨x, h⟩
+    have x_to_lin_comb : (⟨x, h⟩ : LC).1 =
+      ∑ i, (Module.finBasis F LC).equivFun ⟨x, h⟩ i • ((Module.finBasis F LC) i).1 := by
+      rw (occs := .pos [1]) [←Module.Basis.sum_equivFun (Module.finBasis F LC) ⟨x, h⟩, @Submodule.coe_sum]
+      congr
+    simp only [Module.Basis.equivFun_apply] at x_to_lin_comb ⊢
+    exact x_to_lin_comb.symm
+  · rintro ⟨x, h⟩
+    rw [←h]
+    apply Submodule.sum_smul_mem LC x
+    intros c _
+    exact Submodule.coe_mem ((Module.finBasis F LC) c)
+
+/-- A linear code is the code obtained by left multiplication by the generator matrix constructed
+from the basis of the code. -/
+lemma genMatrixFromCode [Field F] (LC : LinearCode ι F) :
+    LC = fromRowGenMat (matrix_from_basis LC) := by
+  unfold fromRowGenMat
+  simp only [range_vecMulLinear, Matrix.row]
+  exact eq_span_rows LC
+
+/-- The rank of the generator matrix equals the dimension of the linear code. -/
+lemma rank_genMatrix_eq_dim [Field F] (LC : LinearCode ι F) :
+    dim LC = Matrix.rank (matrix_from_basis LC) := by
+  unfold dim
+  have h := Matrix.rank_eq_finrank_span_row (LC.matrix_from_basis)
+  symm
+  rw [h]
+  have := congrArg (fun K : Submodule F (ι → F) => Module.finrank F ↥K) (eq_span_rows LC)
+  exact this.symm
+
+
 /-- Given a linear code of length `ι` and dimension `dim` over a field `F`, we define its `dim x ι`
 generator matrix as a matrix whose columns are an `F`-basis of the code. -/
-noncomputable def genMatrixFromCode' [Field F] (LC : LinearCode ι F) : Matrix ι (Fin (dim LC)) F :=
-  (genMatrixFromCode LC).transpose
+noncomputable def genMatrixFromCode_via_cols [Field F] (LC : LinearCode ι F) : Matrix ι (Fin (dim LC)) F :=
+  (matrix_from_basis LC).transpose
 
 /-- A linear code is maximum distance separable (MDS) if its parameters meet the singleton bound. -/
 def IsMDS [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=
   Code.dist LC.carrier = length LC - dim LC + 1
 
+open Matrix
 /-- A linear code `LC` of length `ι` and dimension `dim` over a field `F` is MDS if any `dim` columns
-of the generator matrix whose rows are an `F`-basis of `LC` are linearly independent. [GRS25] -/
-lemma colRank_genMatrix_eq_dim_of_MDS [Field F] [DecidableEq F] (LC : LinearCode ι F) :
-    Matrix.colRank (genMatrixFromCode LC) = dim LC := by
-  sorry
+of the generator matrix whose rows are an `F`-basis of `LC` are linearly independent. [GRS25]
+Equivalently, a linear code is MDS if and only if its generator matrix is MDS. -/
+lemma colRank_genMatrix_eq_dim_of_MDS {k n : ℕ} [Field F] [DecidableEq F]
+  (LC : LinearCode (Fin n) F) : LC.IsMDS ↔ Matrix.IsMDS (matrix_from_basis LC):= by
+  rw [genMatrixFromCode LC]
+  constructor
+  · sorry
+  · sorry
 
 end
 

From e8c405268f9f25d3b0b3ea722a74b006fa58786c Mon Sep 17 00:00:00 2001
From: Katerina Hristova <katherina.hristova@gmail.com>
Date: Tue, 7 Apr 2026 17:32:20 +0300
Subject: [PATCH 14/14] initial progress on rmk 3.21

---
 .../ProximityGap/ProximityGenerators.lean     | 130 +++++++++++++++++-
 1 file changed, 129 insertions(+), 1 deletion(-)

diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
index 268c16d2e..953f8cf7c 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
@@ -12,6 +12,7 @@ import Mathlib.LinearAlgebra.LinearIndependent.Defs
 import Mathlib.Order.CompletePartialOrder
 import Mathlib.Probability.Distributions.Uniform
 import Mathlib.Topology.UnitInterval
+import Mathlib
 
 
 /-!
@@ -65,7 +66,7 @@ def IsZeroEvadingGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S
 there exist `ℓ` linearly independent multivariate polynomials, such that the output is an evaluation
 of the seed at each of these polynomials.
 Definition 3.19 [BSGM25]. -/
-def IsPolynomialGenerator {s : ℕ} {S : Fin s → Set F} (G : Generator (∀ i, S i) ℓ F) : Prop :=
+def IsPolynomialGenerator {s : ℕ} (S : Fin s → Set F) (G : Generator (∀ i, S i) ℓ F) : Prop :=
   ∃ P : ℓ → MvPolynomial (Fin s) F, LinearIndependent F P ∧
   ∀ x : (∀ i, S i), G x = MvPolynomial.eval (fun i ↦ (x i : F)) ∘ P
 
@@ -97,6 +98,133 @@ def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (
   ∀ U : ℓ → (ι → F), ∀ γ : I,
     Pr_{let x ←$ᵖ S}[(Condition G LC x U γ)] ≤ ENNReal.ofReal (ε_mca γ)
 
+
+open scoped ENNReal NNReal BigOperators
+
+
+/-! ## Schwartz-Zippel derived bound -/
+
+/-- Schwartz-Zippel bound in counting form, derived from the Mathlib version
+(`MvPolynomial.schwartz_zippel_sup_sum`).
+
+For a nonzero multivariate polynomial f of total degree at most d, evaluated over a
+product of finite subsets, each of cardinality at least m, the number of zeros
+times m is at most d times the total product size. -/
+theorem schwartz_zippel_counting
+    {F : Type*} [Field F] [DecidableEq F]
+    {s : ℕ}
+    (f : MvPolynomial (Fin s) F) (hf : f ≠ 0)
+    (S : Fin s → Finset F)
+    (d m : ℕ) (hd : f.totalDegree ≤ d) (hm_pos : 0 < m)
+    (hm : ∀ i, m ≤ (S i).card) :
+    (Finset.filter (fun x => MvPolynomial.eval x f = 0) (Fintype.piFinset S)).card * m
+    ≤ d * ∏ i, (S i).card := by
+  have h_schwartz_zippel : (Finset.card (Finset.filter (fun x => (MvPolynomial.eval x) f = 0)
+      (Fintype.piFinset S))) / (∏ i, (S i).card : ℝ≥0∞) ≤ d / (m : ℝ≥0∞) := by
+    convert MvPolynomial.schwartz_zippel_sup_sum hf S |> le_trans <| ?_ using 1
+    rotate_left
+    · exact d / m
+    · simp only [div_eq_mul_inv, mul_comm, Finset.sup_le_iff, MvPolynomial.mem_support_iff, ne_eq]
+      intro b hb
+      have h_deg : ∑ i, b i ≤ d := by
+        refine' le_trans _ hd
+        exact Finset.le_sup (f := fun s => Finsupp.sum s fun x e => e)
+          (MvPolynomial.mem_support_iff.mpr hb) |> le_trans (by simp +decide [Finsupp.sum_fintype])
+      refine' le_trans (Finset.sum_le_sum fun i _ =>
+        mul_le_mul_of_nonneg_right (inv_anti₀ (by positivity) (Nat.cast_le.mpr (hm i)))
+          (Nat.cast_nonneg _)) _
+      rw [← Finset.mul_sum _ _ _, mul_comm]; gcongr; norm_cast
+    · rw [← ENNReal.toReal_le_toReal] <;> norm_num
+      · rw [div_le_div_iff₀] <;> norm_cast <;> norm_num [Finset.prod_pos, hm_pos]
+        · rw [div_le_div_iff₀] <;> norm_cast; norm_num [Finset.prod_pos, hm_pos]
+          exact fun i => Finset.card_pos.mp (lt_of_lt_of_le hm_pos (hm i))
+        · exact fun i => Finset.card_pos.mp (lt_of_lt_of_le hm_pos (hm i))
+      · simp only [div_eq_top, ne_eq, Nat.cast_eq_zero, Finset.card_eq_zero,
+        Finset.filter_eq_empty_iff, Fintype.mem_piFinset, not_forall,
+        Decidable.not_not, natCast_ne_top, false_and, or_false, not_and, forall_exists_index]
+        exact fun x hx hx' => Finset.prod_ne_zero_iff.mpr fun i _ =>
+          Nat.cast_ne_zero.mpr (ne_of_gt (lt_of_lt_of_le hm_pos (hm i)))
+      · exact ENNReal.div_ne_top (by aesop) (by aesop)
+  rw [ENNReal.div_le_iff_le_mul] at h_schwartz_zippel
+  · rw [ENNReal.div_mul] at h_schwartz_zippel
+    · rw [ENNReal.le_div_iff_mul_le] at h_schwartz_zippel
+      · rw [mul_div, ENNReal.div_le_iff_le_mul] at h_schwartz_zippel <;> norm_cast at *
+        · exact Or.inl <| Finset.prod_ne_zero_iff.mpr fun i _ =>
+            ne_of_gt <| lt_of_lt_of_le hm_pos <| hm i
+        · exact Or.inl <| ENNReal.natCast_ne_top _
+      · simp only [ne_eq, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, hm_pos.ne', false_or]
+        exact Or.inl <| ENNReal.prod_ne_top fun i _ => ENNReal.natCast_ne_top _
+      · exact Or.inr (ENNReal.natCast_ne_top _)
+    · exact Or.inl (by positivity)
+    · exact Or.inl ENNReal.coe_ne_top
+  · exact Or.inr (ENNReal.div_ne_top (by aesop) (by aesop))
+  · exact Or.inl <| ENNReal.prod_ne_top fun i _ => ENNReal.natCast_ne_top _
+
+/-! ## Auxiliary lemmas -/
+
+/-- A nonzero linear combination of linearly independent vectors is nonzero. -/
+theorem linearCombination_ne_zero
+    {F : Type} [Field F] {ℓ : Type} [Fintype ℓ]
+    {M : Type} [AddCommMonoid M] [Module F M]
+    {P : ℓ → M} (hP : LinearIndependent F P)
+    {v : ℓ → F} (hv : v ≠ 0) :
+    ∑ j : ℓ, v j • P j ≠ 0 := by
+  have := @Fintype.linearIndependent_iff (ℓ) F M
+  contrapose! hv
+  contrapose! this
+  refine' ⟨_, _, _, _⟩
+  · all_goals try infer_instance
+  · exact Module.addCommMonoidToAddCommGroup F
+  · exact inferInstance
+  · refine ⟨P, inferInstance, Or.inl ⟨hP, v, hv, Function.ne_iff.mp this⟩⟩
+
+/-- The total degree of a linear combination is at most the maximum of the total degrees. -/
+theorem totalDegree_linearCombination_le
+    {F : Type} [Field F] {s : ℕ} {ℓ : Type} [Fintype ℓ]
+    (P : ℓ → MvPolynomial (Fin s) F) (v : ℓ → F) (d : ℕ)
+    (hd : ∀ j, (P j).totalDegree ≤ d) :
+    (∑ j : ℓ, v j • P j).totalDegree ≤ d := by
+  have h_total_degree_sum : ∀ (L : Finset ℓ) (f : ℓ → MvPolynomial (Fin s) F),
+      (∀ j ∈ L, (f j).totalDegree ≤ d) → (Finset.sum L (fun j => f j)).totalDegree ≤ d := by
+    exact fun L f a => MvPolynomial.totalDegree_finsetSum_le a
+  convert h_total_degree_sum Finset.univ (fun j => v j • P j) fun j _ => _
+  exact le_trans (MvPolynomial.totalDegree_smul_le _ _) (hd j)
+
+/-- The dot product ⟨G(x), v⟩ equals the evaluation of the linear combination ∑ v_j P_j
+when G is defined by polynomial evaluation. -/
+theorem dotProduct_eq_eval_linearCombination
+    {F : Type*} [Field F] {s : ℕ} {ℓ : Type*} [Fintype ℓ]
+    (P : ℓ → MvPolynomial (Fin s) F)
+    (x : Fin s → F) (v : ℓ → F) :
+    dotProduct (MvPolynomial.eval x ∘ P) v =
+    MvPolynomial.eval x (∑ j : ℓ, v j • P j) := by
+  simp [dotProduct, mul_comm]
+
+/-! ## Remark 3.20 -/
+
+lemma dm_in_unit_interval (d : ℕ) (m : ℕ) (hm_pos : 0 < m) (hdm : d ≤ m) : (d / m : ℝ) ∈ I := by
+  constructor
+  · exact div_nonneg (Nat.cast_nonneg d) (le_of_lt (Nat.cast_pos.mpr hm_pos))
+  · have hdm' : (d : ℝ) ≤ m := by exact_mod_cast hdm
+    have hm_pos' : (0 : ℝ) < m := by exact_mod_cast hm_pos
+    exact (div_le_one hm_pos').mpr hdm'
+
+
+/-- Here d should be the max of the total degree of the polynomials P : ℓ → MvPolynomial (Fin s) F
+that we can extract from (hG : IsPolynomialGenerator S G) and m is the minimum of the cardinality of
+each seed S i. Use schwartz_zippel_counting in the proof. -/
+ theorem remark_3_20'
+  {F : Type} [Field F] [Fintype F] [DecidableEq F]
+  {ℓ : Type} [Fintype ℓ] [DecidableEq ℓ]
+  {s : ℕ}
+  {S : Fin s → Set F} [∀ i, Fintype ↥(S i)] [∀ i, Nonempty ↥(S i)]
+  {G : Generator (∀ i, ↥(S i)) ℓ F} (hG : IsPolynomialGenerator S G) :
+    ∃ (d m : ℕ) (hm_pos : 0 < m) (hdm : d ≤ m),
+    IsZeroEvadingGenerator G ⟨(d : ℝ) / m, dm_in_unit_interval d m hm_pos hdm⟩ := by
+ sorry
+
+
+
 end CoreDefinitions
 
 end