Guruswami-Sudan divisibility

ArkLib.lean

@@ -30,6 +30,7 @@ import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
 import ArkLib.Data.CodingTheory.BerlekampWelch.ToMathlib
 import ArkLib.Data.CodingTheory.DivergenceOfSets
 import ArkLib.Data.CodingTheory.GuruswamiSudan
+import ArkLib.Data.CodingTheory.GuruswamiSudan.Basic
 import ArkLib.Data.CodingTheory.GuruswamiSudan.GuruswamiSudan
 import ArkLib.Data.CodingTheory.InterleavedCode
 import ArkLib.Data.CodingTheory.JohnsonBound.Basic

ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

@@ -1,24 +1,33 @@
 /-
 Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: František Silváši, Ilia Vlasov
+Authors: František Silváši, Ilia Vlasov, Stefano Rocca
 -/
 import Mathlib.Algebra.Field.Basic
 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
+import ArkLib.Data.CodingTheory.GuruswamiSudan.Basic
 
-namespace GuruswamiSudan
 
-variable {F : Type} [Field F]
-variable [DecidableEq F]
+open Finset Finsupp Polynomial Polynomial.Bivariate ReedSolomon
+
+--Let `F` be a field (finite).
+variable {F : Type} [Field F] [DecidableEq F]
+--Let `k + 1` be the **dimension** of the code.
+variable {k : ℕ}
+--Let `n` be the **blocklength** of the code.
 variable {n : ℕ}
+--Let `m` be a natural number, serving as the **multiplicity parameter**.
+variable {m : ℕ}
+--Let `ωs` be the **domain of evaluation**, i.e. the interpolation points.
+variable {ωs : Fin n ↪ F}
+--Let `f` be the **received word**, possibly corrupted.
+variable {f : Fin n → F}
 
-open Polynomial
+namespace GuruswamiSudan
 
+variable (k m) in
 /--
 Guruswami–Sudan conditions for the polynomial searched by the decoder.
 
@@ -28,30 +37,22 @@ at all interpolation points `(ωs i, f i)`. As in the Berlekamp–Welch
 case, this can be shown to be equivalent to solving a system of linear
 equations.
 
-Parameters:
-* `k : ℕ` — Message length parameter of the code.
-* `r : ℕ` — Multiplicity parameter; controls how many derivatives of `Q`
-  must vanish at each interpolation point.
-* `D : ℕ` — Degree bound for `Q` under the weighted degree measure.
-* `ωs : Fin n ↪ F` — The domain of evaluation.
-* `f : Fin n → F` — Received word (evaluation of the encoded polynomial,
-  possibly corrupted).
-* `Q : Polynomial (Polynomial F)` — The candidate bivariate polynomial
-  in variables `X` and `Y`.
+Here:
+* `D : ℕ` — the **degree bound** for `Q` under the weighted degree measure.
+* `ωs : Fin n ↪ F` — the **domain of evaluation**, i.e. the interpolation points.
+* `f : Fin n → F` — the **received word**.
+  It is the evaluation of the encoded polynomial, possibly corrupted.
+* `Q : F[X][Y]` — The candidate bivariate polynomial.
 -/
-structure Condition
-  (k r D : ℕ)
-  (ωs : Fin n ↪ F)
-  (f : Fin n → F)
-  (Q : Polynomial (Polynomial F)) where
+structure Conditions (D : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) (Q : F[X][Y]) where
   /-- Q ≠ 0 -/
   Q_ne_0 : Q ≠ 0
-  /-- Degree of the polynomial. -/
-  Q_deg : Bivariate.weightedDegree Q 1 (k-1) ≤ D
+  /-- (1, k-1)-weighted degree of the polynomial is bounded. -/
+  Q_deg : 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)
+  /-- Multiplicity of the roots is at least m. -/
+  Q_multiplicity : ∀ i, m ≤ rootMultiplicity Q (ωs i) (f i)
 
 /-- Guruswami-Sudan decoder. -/
 opaque decoder (k r D e : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) : List F[X] := sorry
@@ -68,8 +69,7 @@ theorem decoder_mem_impl_dist
   Δ₀(f, p.eval ∘ ωs) ≤ e := by sorry
 
 /-- If a codeword is e-far from the received message it appears in the output of
-the decoder.
--/
+    the decoder. -/
 theorem decoder_dist_impl_mem
   {k r D e : ℕ}
   (h_e : e ≤ n - Real.sqrt (k * n))
@@ -80,42 +80,21 @@ theorem decoder_dist_impl_mem
   :
   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 [BCIKS20].
-    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 [BCIKS20],
-    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))
-
-/-- The first part of lemma 5.3 from [BCIKS20].
-    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
+/-- Existence of a solution to the Guruswami-Sudan decoder.
+    It is the first part of Lemma 5.3 from [BCIKS20]. -/
+theorem proximity_gap_existence (k n : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) (hm : 1 ≤ m) :
+    ∃ Q, Conditions k m (proximity_gap_degree_bound k n m) ωs f Q := by
+  use polySol k n m ωs f
+  exact ⟨polySol_ne_zero, polySol_weightedDegree_le, polySol_roots hm, polySol_multiplicity⟩
 
-/-- The second part of lemma 5.3 from [BCIKS20].
-    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 (ReedSolomon.codewordToPoly p)) ∣ Q := by sorry
+/-- Given any Reed-Solomon code `p`, any solution of the Guruswami-Sudan decoder is
+    divisible by `Y - P(X)`, where `P(X)` is the polynomial corresponding to the codeword `p`.
+    It is the first part of Lemma 5.3 from [BCIKS20]. -/
+theorem proximity_gap_divisibility (hk : k + 1 ≤ n) (hm : 1 ≤ m) (p : code ωs k)
+    {Q : F[X][Y]} (hQ : Conditions k m (proximity_gap_degree_bound k n m) ωs f Q)
+    (h_dist : (hammingDist f (fun i ↦ (codewordToPoly p).eval (ωs i)) : ℝ) / n <
+      proximity_gap_johnson k n m) :
+    X - C (codewordToPoly p) ∣ Q :=
+  dvd_property (f := f) hk hm p hQ.Q_ne_0 hQ.Q_deg hQ.Q_multiplicity h_dist
 
 end GuruswamiSudan

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean

@@ -174,7 +174,7 @@ noncomputable def proximity_gap_johnson (rho : ℚ) (m : ℕ) : ℝ :=
     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 + 1) m ((proximity_gap_degree_bound ((k + 1 : ℚ) / n) m n)) ωs f Q := by
+  ∃ Q, Conditions (k + 1) m ((proximity_gap_degree_bound ((k + 1 : ℚ) / n) m n)) ωs f Q := by
   sorry
 
 open Polynomial in
@@ -188,7 +188,7 @@ open Polynomial in
 lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F}
   {w : Fin n → F}
   {Q : F[X][Y]}
-  (cond : Condition (k + 1) m (proximity_gap_degree_bound ((k + 1 : ℚ) / n) m n) ωs w Q)
+  (cond : Conditions (k + 1) m (proximity_gap_degree_bound ((k + 1 : ℚ) / n) m n) ωs w Q)
   {p : ReedSolomon.code ωs n}
   (h : δᵣ(w, p) ≤ proximity_gap_johnson ((k + 1 : ℚ) / n) m)
   :

ArkLib/Data/List/Lemmas.lean

@@ -194,4 +194,10 @@ lemma zipWith_const {α β : Type _} {f : α → β → β} {l₁ : List α} {l
   | nil => rcases l₂ <;> aesop
   | cons _ _ _ => rcases l₂ <;> aesop
 
+/-- If every element produced by filterMap is at least m, then the minimum of the result
+    is at least m. -/
+lemma min?_filterMap_ge {α : Type} {l : List α} {f : α → Option ℕ} {m : ℕ}
+    (h : ∀ x ∈ l, ∀ k, f x = some k → m ≤ k) : ∀ k, (l.filterMap f).min? = some k → m ≤ k :=
+  fun k hk ↦ by rw [List.min?_eq_some_iff] at hk; aesop
+
 end List

ArkLib/Data/Polynomial/Bivariate.lean

@@ -79,7 +79,7 @@ def natDegreeY (f : F[X][Y]) : ℕ := Polynomial.natDegree f
 /-- The set of `Y`-degrees is non-empty. -/
 lemma degreesY_nonempty {f : F[X][Y]} (hf : f ≠ 0) : (f.toFinsupp.support).Nonempty :=
   Finsupp.support_nonempty_iff.mpr
-    fun h ↦ hf (Polynomial.ext (fun n => by rw [←Polynomial.toFinsupp_apply, h]; rfl))
+    fun h ↦ hf (Polynomial.ext (fun n => by rw [← Polynomial.toFinsupp_apply, h]; rfl))
 
 /-- The `X`-degree of a bivariate polynomial. -/
 def degreeX (f : F[X][Y]) : ℕ := f.support.sup (fun n => (f.coeff n).natDegree)
@@ -100,6 +100,11 @@ def natWeightedDegree.{u} {F : Type u} [Semiring F] (f : F[X][Y]) (u v : ℕ) :
 
 variable {f : F[X][Y]}
 
+/-- The weighted degree is always defined (never none). -/
+lemma weightedDegree_ne_none {F : Type} [Semiring F] (f : F[X][Y]) (u v : ℕ) :
+    weightedDegree f u v ≠ none := by
+  unfold weightedDegree; aesop
+
 @[grind _=_]
 lemma weightedDegree_eq_natWeightedDegree {u v : ℕ} :
   f ≠ 0 → weightedDegree f u v = natWeightedDegree f u v := by
@@ -133,16 +138,17 @@ def rootMultiplicity₀.{u} {F : Type u} [Semiring F] [DecidableEq F] (f : F[X][
   let deg := weightedDegree f 1 1
   match deg with
   | none => none
-  | some deg => List.max?
-    (List.map
-      (fun x => if coeff f x.1 x.2 ≠ 0 then x.1 + x.2 else 0)
-      (List.product (List.range deg.succ) (List.range deg.succ)))
-
-/-- The multiplicity of a pair `(x,y)` of a bivariate polynomial `f`. -/
+  | some deg => List.min?
+    (List.filterMap
+      (fun p ↦ if coeff f p.1 p.2 = 0 then none else some (p.1 + p.2))
+        (List.product (List.range deg.succ) (List.range deg.succ)))
+
+/-- Root multiplicity (order of vanishing) of a bivariate polynomial at `(x,y)`.
+It is the smallest total degree `s+t` of a nonzero coefficient after shifting
+the root to `(0,0)`. The zero polynomial has multiplicity `none`. -/
 def rootMultiplicity.{u} {F : Type u} [CommSemiring F] [DecidableEq F]
-  (f : F[X][Y]) (x y : F) : Option ℕ :=
-  let X := (Polynomial.X : Polynomial F)
-  rootMultiplicity₀ (F := F) ((f.comp (Y + (C (C y)))).map (Polynomial.compRingHom (X + C x)))
+    (f : F[X][Y]) (x y : F) : Option ℕ :=
+  rootMultiplicity₀ <| (f.comp (Y + C (C y))).map (Polynomial.compRingHom (X + C x))
 
 /-- If the multiplicity of a pair `(x,y)` is non-negative, then the pair is a root of `f`. -/
 lemma rootMultiplicity_some_implies_root {F : Type} [CommSemiring F] [DecidableEq F]
@@ -371,16 +377,19 @@ polynomial in `Y`. -/
 def monomialY (n : ℕ) : F[X] →ₗ[F[X]] F[X][Y] where
   toFun t := ⟨Finsupp.single n t⟩
   map_add' x y := by rw [Finsupp.single_add]; aesop
-  map_smul' r x := by simp; rw[smul_monomial]; aesop
+  map_smul' r x := by
+    simp only [smul_eq_mul, ofFinsupp_single, RingHom.id_apply]
+    rw [smul_monomial]
+    aesop
 
 /-- Definition of the bivariate monomial `X^n * Y^m` -/
 def monomialXY (n m : ℕ) : F →ₗ[F] F[X][Y] where
   toFun t := ⟨Finsupp.single m ⟨(Finsupp.single n t)⟩⟩
   map_add' x y := by
-    simp only [ofFinsupp_single, Polynomial.monomial_add, Polynomial.monomial_add]
+    simp only [ofFinsupp_single, map_add, map_add]
   map_smul' x y := by
     simp only [smul_eq_mul, ofFinsupp_single, RingHom.id_apply]
-    rw[smul_monomial, smul_monomial]
+    rw [smul_monomial, smul_monomial]
     simp
 
 /-- The bivariate monomial is well-defined. -/
@@ -459,5 +468,9 @@ lemma degreeY_monomialXY {n m : ℕ} {a : F} (ha : a ≠ 0) :
 def weightedDegreeMonomialXY {n m : ℕ} (a b t : ℕ) : ℕ :=
   a * (degreeX (monomialXY n m t)) + b * natDegreeY (monomialXY n m t)
 
+/-- Shift a bivariate polynomial by (x, y). -/
+noncomputable def shift {F : Type} [Field F] (f : F[X][Y]) (x y : F) : F[X][Y] :=
+  (f.comp (X + C (C y))).map ((X + C x).compRingHom)
+
 end
 end Polynomial.Bivariate

lake-manifest.json

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "375ddc485afeff3ee67816f1c3218dab120a600b",
+   "rev": "17a4da01b95f9fe92a361c38f039fea674ab1ade",
    "name": "VCVio",
    "manifestFile": "lake-manifest.json",
    "inputRev": "pfunction-4-26",