Refactoring Coding Theory

ArkLib.lean

@@ -39,10 +39,9 @@ import ArkLib.Data.CodingTheory.JohnsonBound.Lemmas
 import ArkLib.Data.CodingTheory.ListDecodability
 import ArkLib.Data.CodingTheory.PolishchukSpielman
 import ArkLib.Data.CodingTheory.Prelims
-import ArkLib.Data.CodingTheory.ProximityGap.AHIV22
-import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20
+import ArkLib.Data.CodingTheory.ProximityGap.ReedSolomon
 import ArkLib.Data.CodingTheory.ProximityGap.Basic
-import ArkLib.Data.CodingTheory.ProximityGap.DG25
+import ArkLib.Data.CodingTheory.ProximityGap.Interleaved
 import ArkLib.Data.CodingTheory.ReedMuller
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.EllipticCurve.BN254
@@ -187,22 +186,21 @@ import ArkLib.ProofSystem.Fri.Spec.SingleRound
 import ArkLib.ProofSystem.Plonk.Basic
 import ArkLib.ProofSystem.Spartan.Basic
 import ArkLib.ProofSystem.Stir
-import ArkLib.ProofSystem.Stir.Combine
-import ArkLib.ProofSystem.Stir.Folding
-import ArkLib.ProofSystem.Stir.MainThm
-import ArkLib.ProofSystem.Stir.OutOfDomSmpl
-import ArkLib.ProofSystem.Stir.ProximityBound
-import ArkLib.ProofSystem.Stir.ProximityGap
-import ArkLib.ProofSystem.Stir.Quotienting
+import ArkLib.Data.CodingTheory.Operations.Combine
+import ArkLib.Data.CodingTheory.Folding.Stir
+import ArkLib.ProofSystem.Stir.RBRSoundness
+import ArkLib.Data.CodingTheory.OutOfDomSmpl.Stir
+import ArkLib.Data.CodingTheory.Proximity.Bound
+import ArkLib.Data.CodingTheory.Operations.Quotienting
 import ArkLib.ProofSystem.Sumcheck.Impl.Basic
 import ArkLib.ProofSystem.Sumcheck.Spec.General
 import ArkLib.ProofSystem.Sumcheck.Spec.SingleRound
 import ArkLib.ProofSystem.Whir
-import ArkLib.ProofSystem.Whir.BlockRelDistance
-import ArkLib.ProofSystem.Whir.Folding
-import ArkLib.ProofSystem.Whir.MutualCorrAgreement
-import ArkLib.ProofSystem.Whir.OutofDomainSmpl
-import ArkLib.ProofSystem.Whir.ProximityGen
+import ArkLib.Data.CodingTheory.Distance.BlockRel
+import ArkLib.Data.CodingTheory.Folding.Whir
+import ArkLib.Data.CodingTheory.Proximity.MutualCorrAgreement
+import ArkLib.Data.CodingTheory.OutOfDomSmpl.Whir
+import ArkLib.Data.CodingTheory.Proximity.Generator
 import ArkLib.ProofSystem.Whir.RBRSoundness
 import ArkLib.ToMathlib.BigOperators.Fin
 import ArkLib.ToMathlib.Data.IndexedBinaryTree.Basic

ArkLib/ProofSystem/Whir/BlockRelDistance.lean → ArkLib/Data/CodingTheory/Distance/BlockRel.lean

@@ -131,7 +131,8 @@ lemma blockRelDistance_eq_relHammingDist_of_k_eq_i -- Renamed for clarity
   (hS' : S' = Finset.univ) -- This now works.
   (φ' : (indexPowT S φ i) ↪ F)
   [h_dec : DecidableBlockDisagreement i i f S' φ'] [DecidableEq (indexPowT S φ i)] :
-  Δᵣ(i, i, f, S', φ', g) = δᵣ(f, g) := by sorry
+  Δᵣ(i, i, f, S', φ', g) = δᵣ(f, g) := by
+  sorry
 
 /-- For the set S ⊆ F^ι, we define the minimum block relative distance wrt set S. -/
 noncomputable def minBlockRelDistance
@@ -175,7 +176,8 @@ lemma relHammingDist_le_blockRelDistance
   [h_fintype : ∀ i : ℕ, Fintype (indexPowT S φ i)]
   [DecidableEq (indexPowT S φ i)] [Smooth φ']
   [h_dec : DecidableBlockDisagreement i k f S' φ'] :
-  δᵣ(f, g) ≤ Δᵣ(i, k, f, S', φ', g) := by sorry
+  δᵣ(f, g) ≤ Δᵣ(i, k, f, S', φ', g) := by
+  sorry
 
 /-- Claim 4.19, Part 2
   As a consequence of `relHammingDist_le_blockRelDistance`, the list of codewords
@@ -190,7 +192,8 @@ lemma listBlock_subset_listHamming
   (C : Set ((indexPowT S φ i) → F)) (hcode : C = smoothCode φ' m)
   [h_dec : DecidableBlockDisagreement i k f S' φ']
   (δ : ℝ≥0) (hδLe : δ ≤ 1) :
-  Λᵣ(i, k, f, S', C, hcode, δ) ⊆ relHammingBall C f δ := by sorry
+  Λᵣ(i, k, f, S', C, hcode, δ) ⊆ relHammingBall C f δ := by
+  sorry
 
 
 end BlockRelDistance

ArkLib/Data/CodingTheory/DivergenceOfSets.lean

@@ -6,7 +6,7 @@ Authors: Katerina Hristova, František Silváši, Julian Sutherland
 
 import ArkLib.Data.CodingTheory.Basic
 import ArkLib.Data.CodingTheory.ProximityGap.Basic
-import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20
+import ArkLib.Data.CodingTheory.ProximityGap.ReedSolomon
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.Probability.Notation
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

ArkLib/ProofSystem/Stir/Folding.lean → ArkLib/Data/CodingTheory/Folding/Stir.lean

@@ -1,13 +1,13 @@
 /-
 Copyright (c) 2025 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mirco Richter, Poulami Das (Least Authority)
+Authors: Mirco Richter, Poulami Das (Least Authority), Alexander Hicks
 -/
 
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.CodingTheory.ListDecodability
 import ArkLib.Data.Probability.Notation
-import ArkLib.ProofSystem.Stir.ProximityBound
+import ArkLib.Data.CodingTheory.Proximity.Bound
 
 import Mathlib.Algebra.MvPolynomial.Basic
 import Mathlib.Algebra.MvPolynomial.Degrees
@@ -113,14 +113,14 @@ lemma exists_unique_bivariate
   (hdeg_q_max : qPoly.natDegree < Fintype.card F) (fPoly : Polynomial F) :
     -- Q ∈ 𝔽[X,Y]
     ∃! Q : MvPolynomial (Fin 2) F,
-      -- deg_x(Q) = Floor ( deg(fPoly) / deg(qPoly) )
+      -- deg_y(Q) = Floor ( deg(fPoly) / deg(qPoly) )
       -- This is natural number division towards zero, which is floor
-      (MvPolynomial.degreeOf 0 Q = (Polynomial.natDegree fPoly) / (Polynomial.natDegree qPoly)) ∧
-      -- deg_y(Q) < deg (q)
-      (MvPolynomial.degreeOf 1 Q < Polynomial.natDegree qPoly) ∧
-      -- point‑wise equality on F: f(z) = Q(q(z), z)
-      (∀ z : F, Polynomial.eval z fPoly = evalBivar Q (Polynomial.eval z qPoly) z) ∧
-      (∀ t : ℕ, fPoly.natDegree < t * qPoly.natDegree → MvPolynomial.degreeOf 0 Q < t) :=
+      (MvPolynomial.degreeOf 1 Q = (Polynomial.natDegree fPoly) / (Polynomial.natDegree qPoly)) ∧
+      -- deg_x(Q) < deg (q)
+      (MvPolynomial.degreeOf 0 Q < Polynomial.natDegree qPoly) ∧
+      -- point‑wise equality on F: f(z) = Q(z, q(z))
+      (∀ z : F, Polynomial.eval z fPoly = evalBivar Q z (Polynomial.eval z qPoly)) ∧
+      (∀ t : ℕ, fPoly.natDegree < t * qPoly.natDegree → MvPolynomial.degreeOf 1 Q < t) :=
   /- The proof can follow `def polyQ` using the properties guranteed
   from MonomialOrder.div from Mathlib.RingTheory.MvPolynomial.Groebner -/
   by sorry
@@ -131,15 +131,28 @@ lemma degree_bound_bivariate
   (hdeg_q_min : qPoly.natDegree > 0)
   (hdeg_q_max : qPoly.natDegree < Fintype.card F)
   {t : ℕ} (Q : MvPolynomial (Fin 2) F)
-  (hdegX : MvPolynomial.degreeOf 0 Q < t)
-  (hdegY : MvPolynomial.degreeOf 1 Q < qPoly.natDegree) :
+  (hdegX : MvPolynomial.degreeOf 0 Q < qPoly.natDegree)
+  (hdegY : MvPolynomial.degreeOf 1 Q < t) :
   (MvPolynomial.eval₂Hom (Polynomial.C : F →+* Polynomial F)
-      (fun i : Fin 2 => if i = 0 then qPoly else Polynomial.X) Q).natDegree < t * qPoly.natDegree :=
+      (fun i : Fin 2 => if i = 0 then Polynomial.X else qPoly) Q).natDegree < t * qPoly.natDegree :=
     by sorry
 
 /-- Definition 4.7
   `polyFold(f, k, r)` "folds" the polynomial `f`
-  producing a new polynomial of deree  `< degree(f)/k`. -/
+  producing a new polynomial of deree  `< degree(f)/k`.
+
+  **Note on Variable Mapping:**
+  The `polyQ` function uses `MonomialOrder.lex` on `Fin 2` to decompose `f`.
+  In Mathlib's `lex`, `X 0 > X 1`. The division reduces the "leading" variable `X 0` (index 0)
+  replacing `(X 0)^k` with `X 1` (index 1).
+  Therefore:
+  * Index 0 (`X 0`) represents the remainder/fiber variable (`Y` in STIR paper), with degree `< k`.
+  * Index 1 (`X 1`) represents the quotient/folded variable (`Z` in STIR paper).
+
+  To implement folding ($f(X) \to \sum r^j G_j(X)$), we must map:
+  * `X 0` (fiber) $\to$ randomness `r`
+  * `X 1` (folded) $\to$ new variable `X`
+-/
 noncomputable def polyFold
   [DecidableEq F] (fPoly : Polynomial F)
   (k : ℕ) (hk0 : 0 < k) (hkfin : k < Fintype.card F)
@@ -151,7 +164,7 @@ noncomputable def polyFold
     let Q : MvPolynomial (Fin 2) F := polyQ fPoly qPoly
     MvPolynomial.eval₂Hom
       (Polynomial.C : F →+* Polynomial F)
-      (fun i : Fin 2 => if i = 0 then Polynomial.X else Polynomial.C r) Q
+      (fun i => if i = 0 then Polynomial.C r else Polynomial.X) Q
 
 open Domain
 

ArkLib/ProofSystem/Whir/Folding.lean → ArkLib/Data/CodingTheory/Folding/Whir.lean

@@ -6,8 +6,8 @@ Authors: Poulami Das, Miguel Quaresma (Least Authority), Alexander Hicks
 
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.MvPolynomial.LinearMvExtension
-import ArkLib.ProofSystem.Whir.BlockRelDistance
-import ArkLib.ProofSystem.Whir.MutualCorrAgreement
+import ArkLib.Data.CodingTheory.Distance.BlockRel
+import ArkLib.Data.CodingTheory.Proximity.MutualCorrAgreement
 
 /-!
 # Folding

ArkLib/ProofSystem/Stir/Combine.lean → ArkLib/Data/CodingTheory/Operations/Combine.lean

@@ -1,15 +1,15 @@
 /-
 Copyright (c) 2025 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mirco Richter, Poulami Das (Least Authority)
+Authors: Mirco Richter, Poulami Das (Least Authority), Alexander Hicks
 -/
 
 import Mathlib.Tactic.FieldSimp
 
 import ArkLib.Data.CodingTheory.ProximityGap.Basic
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.Probability.Notation
-import ArkLib.ProofSystem.Stir.ProximityBound
+import ArkLib.Data.CodingTheory.Proximity.Bound
 
 /-! Section 4.5 from STIR [ACFY24stir]
 
@@ -48,7 +48,7 @@ def ri (dstar : ℕ) (degs : Fin m → ℕ) (r : F) (i : Fin m) : F :=
           match i.1 with
           | 0 => 1
           | .succ i' =>
-            let exp := i' + ∑ j < i, (dstar - degs j)
+            let exp := i.1 + ∑ j < i, (dstar - degs j)
             r ^ exp
 
 /-- Definition 4.11.1

ArkLib/ProofSystem/Stir/Quotienting.lean → ArkLib/Data/CodingTheory/Operations/Quotienting.lean

@@ -22,7 +22,7 @@ variable {n : ℕ}
 noncomputable def ansPoly (S : Finset F) (Ans : S → F) : Polynomial F :=
   Lagrange.interpolate S.attach (fun i => (i : F)) Ans
 
-/-- VanishingPoly is the vanishing polynomial on S, i.e. the unique polynomial of degree |S|+1
+/-- VanishingPoly is the vanishing polynomial on S, i.e. the unique polynomial of degree |S|
     that is 0 at each s ∈ S and is not the zero polynomial. That is V(X) = ∏(s ∈ S) (X - s). -/
 noncomputable def vanishingPoly (S : Finset F) : Polynomial F :=
   ∏ s ∈ S, (Polynomial.X - Polynomial.C s)

ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean → ArkLib/Data/CodingTheory/Proximity/MutualCorrAgreement.lean

@@ -8,7 +8,7 @@ import ArkLib.Data.Probability.Notation
 import ArkLib.Data.CodingTheory.ListDecodability
 import ArkLib.Data.CodingTheory.InterleavedCode
 import ArkLib.Data.CodingTheory.ReedSolomon
-import ArkLib.ProofSystem.Whir.ProximityGen
+import ArkLib.Data.CodingTheory.Proximity.Generator
 
 
 /-!

ArkLib/Data/CodingTheory/ProximityGap/DG25.lean → ArkLib/Data/CodingTheory/ProximityGap/Interleaved.lean

@@ -1,13 +1,13 @@
 /-
 Copyright (c) 2024 - 2025 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors : Chung Thai Nguyen, Quang Dao
+Authors : Chung Thai Nguyen, Quang Dao, Katerina Hristova, František Silváši
 -/
 import ArkLib.Data.Nat.Bitwise
 import ArkLib.Data.CodingTheory.Basic
 import ArkLib.Data.CodingTheory.InterleavedCode
 import ArkLib.Data.CodingTheory.ReedSolomon
-import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20
+import ArkLib.Data.CodingTheory.ProximityGap.ReedSolomon
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
 import ArkLib.Data.Probability.Instances
 import ArkLib.Data.CodingTheory.Prelims
@@ -2107,3 +2107,26 @@ theorem reedSolomon_multilinearCorrelatedAgreement [Nontrivial (ReedSolomon.code
   exact h_CA_Nat
 
 end RSCode_Corollaries
+
+variable {F : Type*} [Field F] [Finite F] [DecidableEq F]
+         {κ : Type*} [Fintype κ]
+         {ι : Type*} [Fintype ι]
+
+local instance : Fintype F := Fintype.ofFinite F
+/-!
+## Proximity results from [AHIV22] (Ligero)
+-/
+
+/-- **Lemma 4.3, [AHIV22]**. Let `L` be an `[n, k, d]`-linear code over `𝔽`, `U⋆` be a WordStack in
+`(𝔽ᵐ)ⁿ`. Let `e` be a positive integer such that `e < d/3` and `|𝔽| ≥ e`.
+Suppose `d(U⋆, L^⋈m) > e`. Then, there exists `v⋆ ∈ L⋆` such that `d(v⋆, L) > e`, where `L⋆` is the
+row-span of `U⋆`. -/
+lemma distInterleavedCodeToCodeLB
+  {L : LinearCode ι F} {U_star : WordStack (A := F) κ ι}
+  {e : ℕ} -- Might change e to ℕ+ if really needed
+  (hF : Fintype.card F ≥ e)
+  (he : (e : ℚ≥0) < ‖(L : Set (ι → F))‖₀ / 3) -- `e < d/3`
+  (hU : e < Δ₀(⋈|U_star, L^⋈κ)) : -- `d(U⋆, L^⋈ m) > e`, here we interleave U
+    -- before using `Δ₀` for correct symbol specification
+  ∃ v ∈ Matrix.rowSpan U_star , e < Δ₀(v, L) := by
+  sorry