Proximity Generators Definitions

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

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

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