diff --git a/ArkLib.lean b/ArkLib.lean
index 74c7a6f3e..17fbb8f4b 100644
--- a/ArkLib.lean
+++ b/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
diff --git a/ArkLib/ProofSystem/Whir/BlockRelDistance.lean b/ArkLib/Data/CodingTheory/Distance/BlockRel.lean
similarity index 98%
rename from ArkLib/ProofSystem/Whir/BlockRelDistance.lean
rename to ArkLib/Data/CodingTheory/Distance/BlockRel.lean
index 2ffdd5de3..d11398973 100644
--- a/ArkLib/ProofSystem/Whir/BlockRelDistance.lean
+++ b/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
diff --git a/ArkLib/Data/CodingTheory/DivergenceOfSets.lean b/ArkLib/Data/CodingTheory/DivergenceOfSets.lean
index 28ff61cae..cf4d5c6e3 100644
--- a/ArkLib/Data/CodingTheory/DivergenceOfSets.lean
+++ b/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
diff --git a/ArkLib/ProofSystem/Stir/Folding.lean b/ArkLib/Data/CodingTheory/Folding/Stir.lean
similarity index 85%
rename from ArkLib/ProofSystem/Stir/Folding.lean
rename to ArkLib/Data/CodingTheory/Folding/Stir.lean
index 1d6065424..9be7ce5a3 100644
--- a/ArkLib/ProofSystem/Stir/Folding.lean
+++ b/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
 
diff --git a/ArkLib/ProofSystem/Whir/Folding.lean b/ArkLib/Data/CodingTheory/Folding/Whir.lean
similarity index 99%
rename from ArkLib/ProofSystem/Whir/Folding.lean
rename to ArkLib/Data/CodingTheory/Folding/Whir.lean
index 979a7e6cf..125eb4993 100644
--- a/ArkLib/ProofSystem/Whir/Folding.lean
+++ b/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
diff --git a/ArkLib/ProofSystem/Stir/Combine.lean b/ArkLib/Data/CodingTheory/Operations/Combine.lean
similarity index 97%
rename from ArkLib/ProofSystem/Stir/Combine.lean
rename to ArkLib/Data/CodingTheory/Operations/Combine.lean
index 72a47c03b..903732358 100644
--- a/ArkLib/ProofSystem/Stir/Combine.lean
+++ b/ArkLib/Data/CodingTheory/Operations/Combine.lean
@@ -1,7 +1,7 @@
 /-
 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
@@ -9,7 +9,7 @@ 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
diff --git a/ArkLib/ProofSystem/Stir/Quotienting.lean b/ArkLib/Data/CodingTheory/Operations/Quotienting.lean
similarity index 99%
rename from ArkLib/ProofSystem/Stir/Quotienting.lean
rename to ArkLib/Data/CodingTheory/Operations/Quotienting.lean
index b5c337a90..5b27f0fad 100644
--- a/ArkLib/ProofSystem/Stir/Quotienting.lean
+++ b/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)
diff --git a/ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean b/ArkLib/Data/CodingTheory/OutOfDomSmpl/Stir.lean
similarity index 100%
rename from ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean
rename to ArkLib/Data/CodingTheory/OutOfDomSmpl/Stir.lean
diff --git a/ArkLib/ProofSystem/Whir/OutofDomainSmpl.lean b/ArkLib/Data/CodingTheory/OutOfDomSmpl/Whir.lean
similarity index 100%
rename from ArkLib/ProofSystem/Whir/OutofDomainSmpl.lean
rename to ArkLib/Data/CodingTheory/OutOfDomSmpl/Whir.lean
diff --git a/ArkLib/ProofSystem/Stir/ProximityBound.lean b/ArkLib/Data/CodingTheory/Proximity/Bound.lean
similarity index 100%
rename from ArkLib/ProofSystem/Stir/ProximityBound.lean
rename to ArkLib/Data/CodingTheory/Proximity/Bound.lean
diff --git a/ArkLib/ProofSystem/Whir/ProximityGen.lean b/ArkLib/Data/CodingTheory/Proximity/Generator.lean
similarity index 100%
rename from ArkLib/ProofSystem/Whir/ProximityGen.lean
rename to ArkLib/Data/CodingTheory/Proximity/Generator.lean
diff --git a/ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean b/ArkLib/Data/CodingTheory/Proximity/MutualCorrAgreement.lean
similarity index 99%
rename from ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean
rename to ArkLib/Data/CodingTheory/Proximity/MutualCorrAgreement.lean
index 70c1b85bd..35c3e4cbf 100644
--- a/ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean
+++ b/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
 
 
 /-!
diff --git a/ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean b/ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
deleted file mode 100644
index 7db030e1c..000000000
--- a/ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
+++ /dev/null
@@ -1,89 +0,0 @@
-/-
-Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Katerina Hristova, František Silváši, Chung Thai Nguyen
--/
-
-import ArkLib.Data.CodingTheory.InterleavedCode
-import ArkLib.Data.Probability.Notation
-
-/-!
-## Main Definitions
-- Statements of proximity results for Reed Solomon codes (`Lemma 4.3`, `Lemma 4.4` and `Lemma 4.5`
-   from `[AHIV22]`
-
-## References
-
-* [Ames, S., Hazay, C., Ishai, Y., and Venkitasubramaniam, M., *Ligero: Lightweight sublinear
-    arguments without a trusted setup*][AHIV22]
-      * NB we use version 20221118:030830
--/
-
-noncomputable section
-
-open Code ProbabilityTheory
-
-variable {F : Type*} [Field F] [Finite F] [DecidableEq F]
-         {κ : Type*} [Fintype κ]
-         {ι : Type*} [Fintype ι]
-
-local instance : Fintype F := Fintype.ofFinite F
-
-/-- **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
-
-namespace ProximityToRS
-
-open ReedSolomonCode NNReal
-
-/-- The set of points on an affine line, which are within distance `e` from a Reed-Solomon code.
--/
-def closePtsOnAffineLine {ι : Type*} [Fintype ι]
-                         (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : Set (ι → F) :=
-  {x : ι → F | x ∈ Affine.affineLineAtOrigin (F := F) (origin := u) (direction := v)
-    ∧ Δ₀(x, ReedSolomon.code α deg) ≤ e}
-
-/-- The number of points on an affine line between, which are within distance `e` from a
-Reed-Solomon code.
--/
-def numberOfClosePts (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : ℕ :=
-  Fintype.card (closePtsOnAffineLine u v deg α e)
-
-/-- **Lemma 4.4, [AHIV22] (Combinatorial proximity gap for affine lines)**
-Let `L = RS_{𝔽, n, k, η}` be a Reed-Solomon code with minimal distance
-`d = n - k + 1`. Let `e` be a positive integer such that `e < d / 3`. Then for every two words
-`u, v ∈ 𝔽^n`, defining an affine line `ℓ_{u, v} = {u + α v : α ∈ 𝔽}`.
-**Either (i.e. mutually exclusive/XOR)**
-- (1) for every `x ∈ ℓ_{u, v}` we have `d(x, L) ≤ e`,
-- or (2) for at most `d` points `x ∈ ℓ_{u, v}` we have `d(x, L) ≤ e`.
-This is a concrete statement via cardinality of proximity gap for affine lines.
--/
-lemma e_leq_dist_over_3 [DecidableEq F] {deg : ℕ} {α : ι ↪ F} {e : ℕ} {u v : ι → F}
-  (he : (e : ℚ≥0) < ‖(RScodeSet α deg)‖₀ / 3) :
-  Xor'
-    (∀ x ∈ Affine.affineLineAtOrigin (F := F) u v, Δ₀(x, ReedSolomon.code α deg) ≤ e)
-    ((numberOfClosePts u v deg α e) ≤ ‖(RScodeSet α deg)‖₀) := by sorry
-
-/-- **`Lemma 4.5` from `[AHIV22]`.** Let `L = RS_{𝔽, n, k, η}` be a Reed-Solomon code with minimal
-distance `d = n - k + 1` and `e` a positive integer such that `e < d / 3`. Suppose `d(U⋆, L^m) > e`.
-Then, for a random `w⋆` in the row-span of `U⋆`, we have: `Pr[d(w⋆, L) ≤ e] ≤ d / |𝔽|` -/
-lemma probOfBadPts {deg : ℕ} {α : ι ↪ F} {e : ℕ} {U_star : WordStack (A := F) κ ι}
-  (he : (e : ℚ≥0) < ‖(RScodeSet α deg)‖₀ / 3)
-  (hU : e < Δ₀(⋈|U_star, (ReedSolomon.code α deg)^⋈κ)) :
-  (PMF.uniformOfFintype (Matrix.rowSpan U_star)).toOuterMeasure
-    {w_star | Δ₀(w_star, RScodeSet α deg) ≤ e} ≤ ‖(RScodeSet α deg)‖₀ /(Fintype.card F) := by
-  sorry
-
-end ProximityToRS
-end
diff --git a/ArkLib/Data/CodingTheory/ProximityGap/DG25.lean b/ArkLib/Data/CodingTheory/ProximityGap/Interleaved.lean
similarity index 98%
rename from ArkLib/Data/CodingTheory/ProximityGap/DG25.lean
rename to ArkLib/Data/CodingTheory/ProximityGap/Interleaved.lean
index 946d322d8..efb3a299f 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/DG25.lean
+++ b/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
diff --git a/ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean b/ArkLib/Data/CodingTheory/ProximityGap/ReedSolomon.lean
similarity index 93%
rename from ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
rename to ArkLib/Data/CodingTheory/ProximityGap/ReedSolomon.lean
index 5101d6d30..34df69996 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
+++ b/ArkLib/Data/CodingTheory/ProximityGap/ReedSolomon.lean
@@ -6,6 +6,7 @@ Authors: Quang Dao, Katerina Hristova, František Silváši, Julian Sutherland,
 -/
 
 import ArkLib.Data.CodingTheory.ProximityGap.Basic
+import ArkLib.Data.Probability.Notation
 
 /-!
   # Definitions and Theorems about Proximity Gaps
@@ -915,3 +916,57 @@ end WeightedAgreement
 end BCIKS20ProximityGapSection7
 
 end ProximityGap
+
+/-!
+## Combinatorial Proximity results from [AHIV22] (Ligero)
+-/
+
+namespace ProximityToRS
+
+noncomputable section
+variable {F : Type*} [Field F] [Finite F] [DecidableEq F]
+         {κ : Type*} [Fintype κ]
+         {ι : Type*} [Fintype ι]
+
+local instance : Fintype F := Fintype.ofFinite F
+
+open ReedSolomonCode Code
+
+/-- The set of points on an affine line, which are within distance `e` from a Reed-Solomon code.
+-/
+def closePtsOnAffineLine (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : Set (ι → F) :=
+  {x : ι → F | x ∈ Affine.affineLineAtOrigin (F := F) (origin := u) (direction := v)
+    ∧ Δ₀(x, ReedSolomon.code α deg) ≤ e}
+
+/-- The number of points on an affine line between, which are within distance `e` from a
+Reed-Solomon code.
+-/
+def numberOfClosePts (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : ℕ :=
+  Fintype.card (closePtsOnAffineLine u v deg α e)
+
+/-- **Lemma 4.4, [AHIV22] (Combinatorial proximity gap for affine lines)**
+Let `L = RS_{𝔽, n, k, η}` be a Reed-Solomon code with minimal distance
+`d = n - k + 1`. Let `e` be a positive integer such that `e < d / 3`. Then for every two words
+`u, v ∈ 𝔽^n`, defining an affine line `ℓ_{u, v} = {u + α v : α ∈ 𝔽}`.
+**Either (i.e. mutually exclusive/XOR)**
+- (1) for every `x ∈ ℓ_{u, v}` we have `d(x, L) ≤ e`,
+- or (2) for at most `d` points `x ∈ ℓ_{u, v}` we have `d(x, L) ≤ e`.
+This is a concrete statement via cardinality of proximity gap for affine lines.
+-/
+lemma e_leq_dist_over_3 [DecidableEq F] {deg : ℕ} {α : ι ↪ F} {e : ℕ} {u v : ι → F}
+  (he : (e : ℚ≥0) < ‖(RScodeSet α deg)‖₀ / 3) :
+  Xor'
+    (∀ x ∈ Affine.affineLineAtOrigin (F := F) u v, Δ₀(x, ReedSolomon.code α deg) ≤ e)
+    ((numberOfClosePts u v deg α e) ≤ ‖(RScodeSet α deg)‖₀) := by sorry
+
+/-- **`Lemma 4.5` from `[AHIV22]`.** Let `L = RS_{𝔽, n, k, η}` be a Reed-Solomon code with minimal
+distance `d = n - k + 1` and `e` a positive integer such that `e < d / 3`. Suppose `d(U⋆, L^m) > e`.
+Then, for a random `w⋆` in the row-span of `U⋆`, we have: `Pr[d(w⋆, L) ≤ e] ≤ d / |𝔽|` -/
+lemma probOfBadPts {deg : ℕ} {α : ι ↪ F} {e : ℕ} {U_star : WordStack (A := F) κ ι}
+  (he : (e : ℚ≥0) < ‖(RScodeSet α deg)‖₀ / 3)
+  (hU : e < Δ₀(⋈|U_star, (ReedSolomon.code α deg)^⋈κ)) :
+  (PMF.uniformOfFintype (Matrix.rowSpan U_star)).toOuterMeasure
+    {w_star | Δ₀(w_star, RScodeSet α deg) ≤ e} ≤ ‖(RScodeSet α deg)‖₀ /(Fintype.card F) := by
+  sorry
+
+end
diff --git a/ArkLib/ProofSystem/Stir.lean b/ArkLib/ProofSystem/Stir.lean
index bb3a65e4e..c60b5cacc 100644
--- a/ArkLib/ProofSystem/Stir.lean
+++ b/ArkLib/ProofSystem/Stir.lean
@@ -1,7 +1,6 @@
-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
diff --git a/ArkLib/ProofSystem/Stir/ProximityGap.lean b/ArkLib/ProofSystem/Stir/ProximityGap.lean
deleted file mode 100644
index 2ff401a24..000000000
--- a/ArkLib/ProofSystem/Stir/ProximityGap.lean
+++ /dev/null
@@ -1,47 +0,0 @@
-/-
-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)
--/
-
-import ArkLib.Data.CodingTheory.Basic
-import ArkLib.Data.CodingTheory.ReedSolomon
-import ArkLib.Data.Probability.Notation
-import ArkLib.ProofSystem.Stir.ProximityBound
-
-open NNReal ProbabilityTheory ReedSolomon
-
-namespace STIR
-
-/-!
-## References
-
-* [Ben-Sasson, E., Carmon, D., Ishai, Y., Kopparty, S., and Saraf, S., *Proximity Gaps
-    for Reed-Solomon Codes*][BCIKS20]
-* [Arnon, G., Chiesa, A., Fenzi, G., and Yogev, E., *STIR: Reed-Solomon proximity testing
-    with fewer queries*][ACFY24stir]
--/
-
-/-- Theorem 4.1[BCIKS20] from [ACFY24stir]
-  Let `C = RS[F, ι, degree]` be a ReedSolomon code with rate `degree / |ι|`
-  and let Bstar(ρ) = √ρ. For all `δ ∈ (0, 1 - Bstar(ρ))`, `f₁,...,fₘ : ι → F`, if
-  `Pr_{r ← F} [ δᵣ(rⱼ * fⱼ, C) ≤ δ] > err'(degree, ρ, δ, m)`
-  then ∃ S ⊆ ι, |S| ≥ (1 - δ) * |ι| and
-  ∀ i : m, ∃ u : C, u(S) = fᵢ(S) -/
-lemma proximity_gap
-  {F : Type} [Field F] [Fintype F] [DecidableEq F]
-  {ι : Type} [Fintype ι] [Nonempty ι] {φ : ι ↪ F}
-  {degree m : ℕ} {δ : ℝ≥0} {f : Fin m → ι → F} {GenFun : F → Fin m → F}
-  (h : ∀ (hδLe : δ < 1 - Bstar (LinearCode.rate (code φ degree))) {f : Fin m → ι → F},
-        Pr_{
-          let r ← $ᵖ F}[δᵣ((fun x => ∑ j : Fin m, (GenFun r j) * f j x), code φ degree) ≤ δ]
-            > ENNReal.ofReal (proximityError F degree (LinearCode.rate (code φ degree)) δ m)) :
-
-        ∃ S : Finset ι,
-          S.card ≥ (1 - δ) * (Fintype.card ι) ∧
-        ∃ u : (ι → F),
-          u ∈ (code φ degree) ∧ ∀ i : Fin m, ∀ x ∈ S, f i x = u x
-
-:= by sorry
-
-end STIR
diff --git a/ArkLib/ProofSystem/Stir/MainThm.lean b/ArkLib/ProofSystem/Stir/RBRSoundness.lean
similarity index 98%
rename from ArkLib/ProofSystem/Stir/MainThm.lean
rename to ArkLib/ProofSystem/Stir/RBRSoundness.lean
index 49b36c10b..f6b446a6c 100644
--- a/ArkLib/ProofSystem/Stir/MainThm.lean
+++ b/ArkLib/ProofSystem/Stir/RBRSoundness.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: Poulami Das (Least Authority)
+Authors: Poulami Das (Least Authority), Alexander Hicks
 -/
 
 import ArkLib.Data.CodingTheory.ListDecodability
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.OracleReduction.VectorIOR
-import ArkLib.ProofSystem.Stir.ProximityBound
+import ArkLib.Data.CodingTheory.Proximity.Bound
 
 /-!Section 5 ACFY24stir, Theorem 5.1 and Lemma 5.4
 
@@ -99,7 +99,7 @@ def stirRelation
   fun ⟨⟨_, oracle⟩, _⟩ => δᵣ(oracle (), ReedSolomon.code φ degree) ≤ err
 
 /-- Theorem 5.1 : STIR main theorem
-  Consider the following ingrediants,
+  Consider the following ingredients,
   a security parameter `secpar`
   a ReedSolomon code `RS[F, ι, degree]` with rate `ρ = degree/ |ι|`, where ι is a smooth domain
   a proximity parameter `δ ∈ (0, 1 - 1.05 * √ρ)`
@@ -119,7 +119,7 @@ theorem stir_main
   {k proofLen qNumtoInput qNumtoProofstr : ℕ}
   (hk : ∃ p, k = 2 ^ p) (hkGe : k ≥ 4)
   (δ : ℝ≥0) (hδub : δ < 1 - 1.05 * Real.sqrt (degree / Fintype.card ι))
-  (hF : Fintype.card F ≤
+  (hF : Fintype.card F ≥
         secpar * 2 ^ secpar * degree ^ 2 * (Fintype.card ι) ^ (7 / 2) /
           Real.log (1 / rate (code φ degree))) :
   ∃ n : ℕ,
diff --git a/ArkLib/ProofSystem/Whir.lean b/ArkLib/ProofSystem/Whir.lean
index 3d677f15c..646ba0827 100644
--- a/ArkLib/ProofSystem/Whir.lean
+++ b/ArkLib/ProofSystem/Whir.lean
@@ -1,6 +1,6 @@
-import ArkLib.ProofSystem.Whir.BlockRelDistance
-import ArkLib.ProofSystem.Whir.Folding
-import ArkLib.ProofSystem.Whir.MutualCorrAgreement
+import ArkLib.Data.CodingTheory.Distance.BlockRel
+import ArkLib.Data.CodingTheory.Folding.Whir
+import ArkLib.Data.CodingTheory.Proximity.MutualCorrAgreement
 import ArkLib.ProofSystem.Whir.RBRSoundness
-import ArkLib.ProofSystem.Whir.OutofDomainSmpl
-import ArkLib.ProofSystem.Whir.ProximityGen
+import ArkLib.Data.CodingTheory.OutOfDomSmpl.Whir
+import ArkLib.Data.CodingTheory.Proximity.Generator
diff --git a/ArkLib/ProofSystem/Whir/RBRSoundness.lean b/ArkLib/ProofSystem/Whir/RBRSoundness.lean
index ce18e9a0b..fc0ad6605 100644
--- a/ArkLib/ProofSystem/Whir/RBRSoundness.lean
+++ b/ArkLib/ProofSystem/Whir/RBRSoundness.lean
@@ -7,9 +7,9 @@ Authors: Poulami Das (Least Authority), Alexander Hicks
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.CodingTheory.ListDecodability
 import ArkLib.OracleReduction.VectorIOR
-import ArkLib.ProofSystem.Whir.BlockRelDistance
-import ArkLib.ProofSystem.Whir.MutualCorrAgreement
-import ArkLib.ProofSystem.Whir.ProximityGen
+import ArkLib.Data.CodingTheory.Distance.BlockRel
+import ArkLib.Data.CodingTheory.Proximity.MutualCorrAgreement
+import ArkLib.Data.CodingTheory.Proximity.Generator
 
 /-!
 # Round by round soundness theorem