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
diff --git a/ArkLib/Data/CodingTheory/Basic.lean b/ArkLib/Data/CodingTheory/Basic.lean
index 244023024..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
 
@@ -89,6 +90,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,6 +1794,22 @@ lemma wt_eq_zero_iff [Zero F] {v : ι → F} :
   by_cases IsEmpty ι <;>
   aesop (add simp [wt, Finset.filter_eq_empty_iff])
 
+/-- 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 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
 
 end
@@ -1933,8 +1956,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
@@ -1943,18 +1964,16 @@ 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).
-  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
 
@@ -2033,6 +2052,102 @@ 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
+
+/-- 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.
+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
+  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)
+
+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_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]
+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
 
 section
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
diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
new file mode 100644
index 000000000..953f8cf7c
--- /dev/null
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
@@ -0,0 +1,230 @@
+/-
+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.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 generators functions.
+
+## Main Definitions
+
+- `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
+
+* [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]. Full paper : https://eprint.iacr.org/2025/2051}
+-/
+
+section
+
+namespace CoreDefinitions
+
+open NNReal ENNReal unitInterval
+open scoped ProbabilityTheory
+
+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^ℓ`.
+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 : 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
+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 : F)) ∘ P
+
+/-- A matrix whose rows are the outputs of the generator function.
+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.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) (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 : I → I)
+  (LC : LinearCode ι F) : Prop :=
+  ∀ 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
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 ι) :