WIP

Author: ElijahVlasov

ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

@@ -8,9 +8,10 @@ import Mathlib.Algebra.Polynomial.Basic
 import Mathlib.Data.Real.Sqrt
 
 import ArkLib.Data.CodingTheory.Basic
+import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.Polynomial.Bivariate
 
-namespace GuruswamiSudan 
+namespace GuruswamiSudan
 
 variable {F : Type} [Field F]
 variable [DecidableEq F]
@@ -20,55 +21,86 @@ open Polynomial
 
 /--
 Guruswami-Sudan conditions for the polynomial searched by the decoder.
-As in the Berlekamp-Welch case, this can be shown to be equivalent to a 
+As in the Berlekamp-Welch case, this can be shown to be equivalent to a
 a system of linear equations.
 -/
-structure GuruswamiSudanCondition (k r D : ℕ) (ωs f : Fin n → F) (Q : Polynomial (Polynomial F)) where 
+structure Condition
+  (k r D : ℕ)
+  (ωs : Fin n ↪ F)
+  (f : Fin n → F)
+  (Q : Polynomial (Polynomial F)) where
   /-- Q ≠ 0 -/
   Q_ne_0 : Q ≠ 0
   /-- Degree of the polynomial. -/
-  Q_deg : Bivariate.weightedDegree Q 1 (k-1) ≤ D 
+  Q_deg : Bivariate.weightedDegree Q 1 (k-1) ≤ D
   /-- (ωs i, f i) must be root of the polynomial Q. -/
   Q_roots : ∀ i, (Q.eval (C <| f i)).eval (ωs i) = 0
   /-- Multiplicity of the roots is at least r. -/
   Q_multiplicity : ∀ i, r ≤ Bivariate.rootMultiplicity Q (ωs i) (f i)
 
 /-- Guruswami-Sudan decoder. -/
-opaque decoder (k r D e : ℕ) (ωs f : Fin n → F) : List F[X] := sorry
+opaque decoder (k r D e : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) : List F[X] := sorry
 
 /-- Each decoded codeword has to be e-far from the received message. -/
-theorem decoder_mem_impl_dist {k r D e : ℕ} {ωs f : Fin n → F} {p : F[X]}
-  (h_in : p ∈ decoder k r D e ωs f)
+theorem decoder_mem_impl_dist
+  {k r D e : ℕ}
   (h_e : e ≤ n - Real.sqrt (k * n))
+  {ωs : Fin n ↪ F}
+  {f : Fin n → F}
+  {p : F[X]}
+  (h_in : p ∈ decoder k r D e ωs f)
   :
   Δ₀(f, p.eval ∘ ωs) ≤ e := by sorry
 
-/-- If a codeword is e-far from the received message it appears in the output of 
+/-- If a codeword is e-far from the received message it appears in the output of
 the decoder.
 -/
-theorem decoder_dist_impl_mem {k r D e : ℕ} {ωs f : Fin n → F} {p : F[X]}
+theorem decoder_dist_impl_mem
+  {k r D e : ℕ}
   (h_e : e ≤ n - Real.sqrt (k * n))
+  {ωs : Fin n ↪ F}
+  {f : Fin n → F}
+  {p : F[X]}
   (h_dist : Δ₀(f, p.eval ∘ ωs) ≤ e)
   :
-  p ∈ decoder k r D e ωs f := by sorry 
+  p ∈ decoder k r D e ωs f := by sorry
 
+/-- The degree bound (a.k.a. `D_X`) for instantiation of Guruswami-Sudan 
+    in lemma 5.3 of the Proximity Gap paper.
+    D_X(m) = (m + 1/2)√ρn.
+-/
 noncomputable def proximity_gap_degree_bound (k m : ℕ) : ℕ :=
   let rho := (k + 1 : ℚ) / n
   Nat.floor ((((m : ℚ) + (1 : ℚ)/2)*(Real.sqrt rho))*n)
 
+/-- The ball radius from lemma 5.3 of the Proximity Gap paper,
+    which follows from the Johnson bound.
+    δ₀(ρ, m) = 1 - √ρ - √ρ/2m.
+-/ 
 noncomputable def proximity_gap_johnson (k m : ℕ) : ℕ :=
   let rho := (k + 1 : ℚ) / n
   Nat.floor ((1 : ℝ) - Real.sqrt rho - Real.sqrt rho / (2 * m))
 
-/-- Lemma 5.3 from the Proximity gap paper -/ 
-lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs f : Fin n → F} :
-  ∃ Q, GuruswamiSudanCondition k m (proximity_gap_degree_bound (n := n) k m) ωs f Q := by
+/-- The first part of lemma 5.3 from the Proximity gap paper. 
+    Given the D_X (`proximity_gap_degree_bound`) and δ₀ (`proximity_gap_johnson`),
+    a solution to Guruswami-Sudan system exists.
+-/
+lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F}:
+  ∃ Q, Condition k m (proximity_gap_degree_bound (n := n) k m) ωs f Q := by
   sorry
 
-lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs f : Fin n → F} 
-  {Q : F[X][X]} {p : F[X]} 
-  (h : Δ₀(f, p.eval ∘ f) ≤ proximity_gap_johnson (n := n) k m)
+/-- The second part of lemma 5.3 from the Proximity gap paper.
+    For any solution Q of the Guruswami-Sudan system, and for any
+    polynomial P ∈ RS[n, k, ρ] such that Δ(w, P) ≤ δ₀(ρ, m), 
+    we have that Y - P(X) divides Q(X, Y) in the polynomial ring
+    F[X][Y].
+-/
+lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F}
+  {f : Fin n → F}
+  {Q : F[X][X]} 
+  {p : ReedSolomon.code ωs n}
+  (h : Δ₀(f, (ReedSolomon.codeWordToPoly p).eval ∘ f) ≤ proximity_gap_johnson (n := n) k m)
   :
-  ((X : F[X][X]) - C p) ∣ Q := by sorry 
+  ((X : F[X][X]) - C (ReedSolomon.codeWordToPoly p)) ∣ Q := by sorry
 
-end GuruswamiSudan 
+end GuruswamiSudan

ArkLib/Data/CodingTheory/ReedSolomon.lean

@@ -39,6 +39,11 @@ def evalOnPoints : F[X] →ₗ[F] (ι → F) where
 def code (deg : ℕ) : Submodule F (ι → F) :=
   (Polynomial.degreeLT F deg).map (evalOnPoints domain)
 
+def codeWordToPoly 
+  [Fintype ι] [Field F] [DecidableEq ι] 
+  {deg : ℕ} {domain : ι ↪ F} (f : code domain deg) : F[X] :=
+  sorry
+
 /-- The generator matrix of the Reed-Solomon code of degree `deg` and evaluation points `domain`. -/
 def genMatrix (deg : ℕ) : Matrix (Fin deg) ι F :=
   .of fun i j => domain j ^ (i : ℕ)