Polynomial Generators have MCA for RSCodes

ArkLib.lean

@@ -102,8 +102,10 @@ import ArkLib.Data.CodingTheory.ProximityGap.DG25.Basic
 import ArkLib.Data.CodingTheory.ProximityGap.DG25.MainResults
 import ArkLib.Data.CodingTheory.ProximityGap.DG25.ReedSolomon
 import ArkLib.Data.CodingTheory.ProximityGap.Folding
-import ArkLib.Data.CodingTheory.ProximityGap.MCAGenerator
-import ArkLib.Data.CodingTheory.ProximityGap.ProximityGenerators
+import ArkLib.Data.CodingTheory.ProximityGenerator.AffineGenerator
+import ArkLib.Data.CodingTheory.ProximityGenerator.Basic
+import ArkLib.Data.CodingTheory.ProximityGenerator.MCAGenerator
+import ArkLib.Data.CodingTheory.ProximityGenerator.PolynomialGenerator
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.CodingTheory.ReedSolomon.Multilinear
 import ArkLib.Data.Domain.CosetFftDomain.Block

ArkLib/Data/CodingTheory/Basic/LinearCode.lean

@@ -257,17 +257,51 @@ scoped macro_rules
 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.7 [BCGM25]. -/
-def projectedWord (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c
-
-notation:60 c "|[" T "]" => projectedWord c T
+def projectedWord [Fintype ι] (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c
 
 /-- 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.7 [BCGM25]. -/
-def projectedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
-  {w | ∃ c ∈ C, w = c|[T]}
-
-notation:60 C "|[" T "]" => projectedCode C T
+def projectedCode [Fintype ι] (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
+  {w | ∃ c ∈ C, w = projectedWord c T}
+
+open Submodule
+
+def projectedCode_submod
+    [Field F]
+    [Fintype ι]
+    (LC : LinearCode ι F)
+    (T : Finset ι) :
+    Submodule F (T → F) :=
+{
+  carrier := projectedCode (LC.carrier) T,
+  zero_mem' := by
+    unfold projectedCode projectedWord
+    simp only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq]
+    use 0
+    exact And.intro (Submodule.zero_mem LC) (List.map_inj.mp rfl)
+
+  add_mem' := by
+    unfold projectedCode projectedWord
+    intros x y hx hy
+    simp_all only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq]
+    rcases hx with ⟨cx, hx⟩
+    rcases hy with ⟨cy, hy⟩
+    use (cx + cy)
+    apply And.intro ((Submodule.add_mem_iff_right LC hx.1).mpr hy.1)
+    ext i
+    simp [hx.2, hy.2]
+
+  smul_mem' := by
+    unfold projectedCode projectedWord
+    intros m x hx
+    simp_all only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq]
+    rcases hx with ⟨cx,hx⟩
+    use m • cx
+    apply And.intro (smul_mem LC m hx.1)
+    ext i
+    simp [hx.2]
+}
 
 /-- Let `T` be a finite subset of `ι`. If every word in a collection lies in the projected code
 `C|[T]`, then so do all `F`-linear combinations of these. -/

ArkLib/Data/CodingTheory/Prelims.lean

@@ -10,6 +10,7 @@ import Mathlib.LinearAlgebra.AffineSpace.Pointwise
 import Mathlib.LinearAlgebra.AffineSpace.Combination
 import Mathlib.RingTheory.Henselian
 
+
 /-! # Coding-Theory Preliminaries -/
 
 section TensorCombination
@@ -34,6 +35,7 @@ def multilinearCombine {ϑ : ℕ} {ι : Type*}
     (u : (Fin (2 ^ ϑ)) → ι → A) (r : Fin ϑ → F) : (ι → A) :=
   fun colIdx => ∑ rowIdx : Fin (2^ϑ), ((multilinearWeight r rowIdx) : F) • ((u rowIdx colIdx) : A)
 notation:20 r " |⨂| " u => multilinearCombine (u := u) (r := r)
+
 end TensorCombination
 noncomputable section
 
@@ -297,6 +299,29 @@ instance instNonemptyAffineSubspace_mk' {V : Type*} [AddCommGroup V] [Module F V
     (p : V) (direction : Submodule F V) : Nonempty (AffineSubspace.mk' p direction) :=
   nonempty_subtype.mpr ⟨p, AffineSubspace.self_mem_mk' p direction⟩
 
+/-- The affine-space combination of codewords `U` at seed `x`:
+`U 0 + ∑ i, x i • U (i+1)`, i.e. `vecMul (1, x) U`. -/
+abbrev affineComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (x : Fin s → F) : ι → F :=
+  Matrix.vecMul (Fin.cons 1 x) U
+
+/-- The linear combination `∑ i, l i • U (i+1)` of the "direction" codewords. -/
+abbrev linComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (l : Fin s → F) : ι → F :=
+  fun k => ∑ i, l i * U i.succ k
+
+omit [Fintype ι] [DecidableEq F] [Fintype F] in
+/-- The affine combination along the line `x ↦ v + t • lam` in seed space. -/
+lemma affineComb_line {s : ℕ} (U : Fin (s + 1) → (ι → F)) (v lam : Fin s → F) (t : F) :
+    affineComb U (v + t • lam) = affineComb U v + t • (linComb U lam) := by
+  have hsplit : (Fin.cons 1 (v + t • lam) : Fin (s + 1) → F) =
+      Fin.cons 1 v + t • (Fin.cons (0 : F) lam : Fin (s + 1) → F) := by
+    ext i
+    refine Fin.cases ?_ ?_ i <;> simp
+  have hlin : Matrix.vecMul (Fin.cons (0 : F) lam : Fin (s + 1) → F) U = linComb U lam := by
+    ext k
+    simp [Matrix.vecMul, dotProduct, Fin.sum_univ_succ, linComb]
+  change Matrix.vecMul (Fin.cons 1 (v + t • lam) : Fin (s + 1) → F) U = _
+  rw [hsplit, Matrix.add_vecMul, Matrix.smul_vecMul, hlin]
+
 end
 end Affine