diff --git a/ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean b/ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
index 5356a8425..396cb85cb 100644
--- a/ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
+++ b/ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
@@ -7,6 +7,13 @@ Authors: Quang Dao, Katerina Hristova, František Silváši, Julian Sutherland,
 
 import ArkLib.Data.CodingTheory.ProximityGap.Basic
 
+import Mathlib.Combinatorics.Pigeonhole
+import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
+import Mathlib.LinearAlgebra.Quotient.Basic
+import Mathlib.Algebra.Module.Torsion.Free
+import Mathlib.FieldTheory.Finiteness
+import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+import Mathlib.LinearAlgebra.Quotient.Card
 /-!
   # Definitions and Theorems about Proximity Gaps
 
@@ -808,38 +815,547 @@ theorem weighted_correlated_agreement_over_affine_spaces
     mu_set μ ι' ≥ α ∧
     ∀ i, ∀ x ∈ ι', u i x = v i x := by sorry
 
-open scoped ProbabilityTheory in
-open scoped Pointwise in
-open Uniform in
-/-- Weighted correlated agreement over affine spaces.
-Take a Reed-Solomon code of length `ι` and degree `deg`, a proximity-error parameter
-pair `(δ, ε)` and an affine space generated by vectors `u`, such that the probability that a random
-point from the space is `δ`-close to Reed-Solomon code is at most `ε`.
-Then, the words `u` have weighted correlated agreement.
+def WCA_affineSpace {F ι : Type} [Field F] [DecidableEq F] [Fintype ι]
+    {l : ℕ} (u : Fin (l + 2) → ι → F) : AffineSubspace F (ι → F) :=
+  Affine.affineSubspaceAtOrigin (F := F) (A := F) (origin := u 0) (directions := Fin.tail u)
+
+noncomputable abbrev WCA_bound (ι F : Type) [Fintype ι] [Fintype F]
+    (sr : ℝ≥0) (M m : ℕ) : ℝ :=
+  max
+    (((1 + 1 / (2 * m : ℝ))^7 * m^7 * (Fintype.card ι)^2) / ((3 * sr^3) * Fintype.card F))
+    (((max (2 * m + 3) 23) * (M * Fintype.card ι + 1)) / (sr * Fintype.card F))
+
+def WCA_good {F ι : Type} [Field F] [Fintype F] [DecidableEq F]
+    [Fintype ι] [Nonempty ι]
+    (μ : ι → Set.Icc (0 : ℚ) 1) (domain : ι ↪ F) (deg : ℕ) (α : ℝ≥0) : (ι → F) → Prop :=
+  fun x => agree_set μ x (finCarrier domain deg) ≥ α
+
+theorem agree_le_one {ι F : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι] [Field F] [DecidableEq F]
+  (μ : ι → Set.Icc (0 : ℚ) 1) (u v : ι → F) :
+  agree μ u v ≤ (1 : ℝ) := by
+  classical
+  unfold agree
+  let s : Finset ι := { i : ι | u i = v i }
+  have hμle : ∀ i : ι, (μ i).1 ≤ (1 : ℚ) := by
+    intro i
+    exact (μ i).2.2
+  have hsumQ : (∑ i ∈ s, (μ i).1) ≤ (Fintype.card ι : ℚ) := by
+    have h1 : (∑ i ∈ s, (μ i).1) ≤ (∑ i ∈ s, (1 : ℚ)) := by
+      refine Finset.sum_le_sum ?_
+      intro i hi
+      exact hμle i
+    have hcard : s.card ≤ Fintype.card ι := by
+      simpa using (Finset.card_le_univ s)
+    calc
+      (∑ i ∈ s, (μ i).1) ≤ (∑ i ∈ s, (1 : ℚ)) := h1
+      _ = (s.card : ℚ) := by
+        simp
+      _ ≤ (Fintype.card ι : ℚ) := by
+        exact_mod_cast hcard
+  have hsumR : (↑(∑ i ∈ s, (μ i).1) : ℝ) ≤ (Fintype.card ι : ℝ) := by
+    exact_mod_cast hsumQ
+  have hpos : 0 ≤ (1 / (Fintype.card ι : ℝ)) := by
+    positivity
+  have hmul : (1 / (Fintype.card ι : ℝ)) * (↑(∑ i ∈ s, (μ i).1) : ℝ)
+      ≤ (1 / (Fintype.card ι : ℝ)) * (Fintype.card ι : ℝ) :=
+    mul_le_mul_of_nonneg_left hsumR hpos
+  have hcard_ne : (Fintype.card ι : ℝ) ≠ 0 := by
+    exact_mod_cast (Fintype.card_ne_zero : Fintype.card ι ≠ 0)
+  calc
+    1 / (Fintype.card ι : ℝ) * (↑(∑ i with u i = v i, (μ i).1) : ℝ)
+        = 1 / (Fintype.card ι : ℝ) * (↑(∑ i ∈ s, (μ i).1) : ℝ) := by
+            simp [s]
+    _ ≤ 1 / (Fintype.card ι : ℝ) * (Fintype.card ι : ℝ) := hmul
+    _ = (1 : ℝ) := by
+        simpa using (one_div_mul_cancel hcard_ne)
+
+
+theorem agree_set_le_one {ι F : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι] [Field F] [DecidableEq F]
+  (μ : ι → Set.Icc (0 : ℚ) 1) (u : ι → F)
+  (V : Finset (ι → F)) [Nonempty V] :
+  agree_set μ u V ≤ (1 : ℝ) := by
+  classical
+  unfold agree_set
+  let S : Finset ℝ := Finset.image (agree μ u) V
+  have hS : S.Nonempty := by
+    rcases (show Nonempty V from inferInstance) with ⟨w⟩
+    refine ⟨agree μ u w.1, ?_⟩
+    exact Finset.mem_image.2 ⟨w.1, w.2, rfl⟩
+  have hgoal : S.max' hS ≤ (1 : ℝ) := by
+    refine (Finset.max'_le_iff (s := S) (H := hS) (x := (1 : ℝ))).2 ?_
+    intro y hy
+    rcases Finset.mem_image.1 hy with ⟨w, hwV, rfl⟩
+    simpa using (agree_le_one μ u w)
+  simpa [S] using hgoal
+
+
+instance instNonempty_WCA_affineSpace {F ι : Type} [Field F] [DecidableEq F] [Fintype ι]
+    {l : ℕ} (u : Fin (l + 2) → ι → F) : Nonempty (WCA_affineSpace u) := by
+  classical
+  -- `WCA_affineSpace u` is defined via `AffineSubspace.mk'`, hence nonempty.
+  simpa [WCA_affineSpace, Affine.affineSubspaceAtOrigin] using
+    (Affine.instNonemptyAffineSubspace_mk' (F := F) (V := (ι → F)) (p := u 0)
+      (direction := Submodule.span F (Finset.univ.image (Fin.tail u))))
+
+theorem mu_set_mono [Fintype ι] [DecidableEq ι]
+  (μ : ι → Set.Icc (0 : ℚ) 1) {s t : Finset ι} :
+  s ⊆ t → mu_set μ s ≤ mu_set μ t := by
+  intro hst
+  classical
+  unfold mu_set
+  -- compare the sums
+  have hsum : (∑ i ∈ s, (μ i).1) ≤ (∑ i ∈ t, (μ i).1) := by
+    -- use monotonicity of sum over subsets, weights are nonnegative
+    refine Finset.sum_le_sum_of_subset_of_nonneg hst ?_
+    intro i hi ht
+    -- show 0 ≤ (μ i).1
+    exact (μ i).2.1
+  have hscalar : 0 ≤ (1 / (Fintype.card ι : ℝ)) := by
+    positivity
+  -- multiply inequality by nonnegative scalar
+  -- note: `hsum` is in ℚ, coerces to ℝ
+  have := (mul_le_mul_of_nonneg_left (show (↑(∑ i ∈ s, (μ i).1) : ℝ) ≤ (↑(∑ i ∈ t, (μ i).1) : ℝ) from by
+      exact_mod_cast hsum) hscalar)
+  -- simplify
+  simpa [mul_assoc] using this
+
+theorem sum_ite_const_eq_card_subtype_mul {α : Type} [Fintype α] (P : α → Prop) [DecidablePred P] (c : ENNReal) :
+  (∑ a, (if P a then c else 0)) = (Fintype.card {a : α // P a} : ENNReal) * c := by
+  classical
+  calc
+    (∑ a : α, (if P a then c else 0))
+        = (Finset.univ.sum fun a : α => if P a then c else 0) := by
+            simp
+    _ = (Finset.univ.filter P).sum (fun _ : α => c) := by
+            simpa using
+              (Finset.sum_filter (s := (Finset.univ : Finset α)) (p := P) (f := fun _ : α => c)).symm
+    _ = ((Finset.univ.filter P).card : ENNReal) * c := by
+            simpa [Nat.nsmul_eq_mul] using (Finset.sum_const (s := Finset.univ.filter P) c)
+    _ = (Fintype.card {a : α // P a} : ENNReal) * c := by
+            simpa [Fintype.card_subtype]
+
+theorem pr_uniformOfFintype_eq_card {α : Type} [Fintype α] [Nonempty α] (P : α → Prop) [DecidablePred P] :
+  Pr_{let x ←$ᵖ α}[P x] = ((Fintype.card {x : α // P x} : ENNReal) / (Fintype.card α)) := by
+  classical
+  change (P <$> ($ᵖ α)) True =
+      ((Fintype.card { x : α // P x } : ENNReal) / (Fintype.card α))
+  -- Expand the probability computation for the uniform distribution.
+  simp [PMF.monad_map_eq_map, PMF.map_apply, div_eq_mul_inv]
+  -- Count the number of satisfying elements.
+  simpa using
+    (sum_ite_const_eq_card_subtype_mul (α := α) (P := P)
+      (c := (↑(Fintype.card α) : ENNReal)⁻¹))
+
+theorem wca_exists_base_with_many_good_on_line {F V : Type} [Field F] [Fintype F] [DecidableEq F]
+  [AddCommGroup V] [Module F V] [FiniteDimensional F V] [Fintype V] [DecidableEq V]
+  (U : AffineSubspace F V) [Nonempty U]
+  (Good : V → Prop) [DecidablePred Good]
+  (d : U.direction) (hd : (d : V) ≠ 0)
+  [Fintype (U.direction ⧸ Submodule.span F ({d} : Set U.direction))]
+  {T : ℕ}
+  (hGood : Fintype.card {x : U // Good x.1} > T * Fintype.card (U.direction ⧸ Submodule.span F ({d} : Set U.direction))) :
+  ∃ b : U, Fintype.card {z : F // Good ((z • (d : V)) +ᵥ (b : V))} > T := by
+  classical
+  -- Choose an arbitrary reference point in `U`.
+  let p : U := Classical.choice (inferInstance : Nonempty U)
+
+  -- Good points in `U`.
+  let α : Type := {x : U // Good x.1}
+
+  -- Quotient of the direction by the line spanned by `d`.
+  let P : Submodule F U.direction := Submodule.span F ({d} : Set U.direction)
+  let β : Type := (U.direction ⧸ P)
+
+  -- Displacement of a point from the reference point, viewed in `U.direction`.
+  let disp : α → U.direction := fun x =>
+    (⟨(x.1 : V) -ᵥ (p : V), U.vsub_mem_direction x.1.property p.property⟩ : U.direction)
+
+  -- Map to the quotient; fibers correspond to affine lines parallel to `d`.
+  let f : α → β := fun x => Submodule.Quotient.mk (p := P) (disp x)
+
+  -- Convert the hypothesis to the form needed for pigeonhole.
+  have hmul : Fintype.card β * T < Fintype.card α := by
+    have h' : T * Fintype.card β < Fintype.card α := by
+      simpa [α, β, P] using hGood
+    simpa [Nat.mul_comm] using h'
+
+  -- Get a large fiber of `f`.
+  rcases (Fintype.exists_lt_card_fiber_of_mul_lt_card (f := f) (n := T) hmul) with ⟨q, hq⟩
+
+  -- The fiber over `q`.
+  let fiber : Type := {x : α // f x = q}
+  have hfiber : T < Fintype.card fiber := by
+    -- `hq` is stated using `#{x | f x = q}`, i.e. the filtered-universe finset cardinality.
+    have hcard : Fintype.card fiber = #{x : α | f x = q} := by
+      simpa [fiber] using (Fintype.card_subtype (α := α) (p := fun x : α => f x = q))
+    simpa [hcard] using hq
+
+  -- Pick a base point `b` in this fiber.
+  have hfiber_pos : 0 < Fintype.card fiber :=
+    lt_of_le_of_lt (Nat.zero_le T) hfiber
+  have hfiber_nonempty : Nonempty fiber := (Fintype.card_pos_iff.1 hfiber_pos)
+  let bα : fiber := Classical.choice hfiber_nonempty
+  let b : U := bα.1.1
+
+  -- Any point in the fiber lies on the affine line through `b` in direction `d`.
+  have hx_on_line :
+      ∀ x : fiber, ∃ z : F, (x.1.1 : V) = (z • (d : V)) +ᵥ (b : V) := by
+    intro x
+
+    -- Points in the same fiber have equal image under `f`.
+    have hquot : f x.1 = f bα.1 := by
+      simpa [x.2, bα.2]
+
+    have hmemP : disp x.1 - disp bα.1 ∈ P := by
+      have : (Submodule.Quotient.mk (p := P) (disp x.1) : β) =
+            Submodule.Quotient.mk (p := P) (disp bα.1) := by
+        simpa [f] using hquot
+      exact (Submodule.Quotient.eq (p := P) (x := disp x.1) (y := disp bα.1)).1 this
+
+    -- Rewrite the difference of displacements as the displacement from `b`.
+    have hdir :
+        disp x.1 - disp bα.1 =
+          (⟨(x.1.1 : V) -ᵥ (b : V),
+            U.vsub_mem_direction x.1.1.property bα.1.1.property⟩ : U.direction) := by
+      ext
+      simp [disp, b, vsub_sub_vsub_cancel_right]
+
+    have hmem :
+        (⟨(x.1.1 : V) -ᵥ (b : V),
+          U.vsub_mem_direction x.1.1.property bα.1.1.property⟩ : U.direction) ∈ P := by
+      simpa [hdir] using hmemP
+
+    -- Membership in `span {d}` gives a scalar.
+    rcases
+        (Submodule.mem_span_singleton).1 (by simpa [P] using hmem) with ⟨z, hz⟩
+    refine ⟨z, ?_⟩
+
+    have hzV : (x.1.1 : V) -ᵥ (b : V) = z • (d : V) := by
+      have hz' := congrArg (fun (w : U.direction) => (w : V)) hz
+      simpa [b] using hz'.symm
+
+    -- Turn a `vsub` equation into the desired `vadd` equation.
+    exact (eq_vadd_iff_vsub_eq (p₁ := (x.1.1 : V)) (g := z • (d : V)) (p₂ := (b : V))).2 hzV
+
+  -- Define a map from the fiber to scalars witnessing goodness on this line.
+  let zOf : fiber → F := fun x => Classical.choose (hx_on_line x)
+  have hzOf_spec :
+      ∀ x : fiber, (x.1.1 : V) = (zOf x • (d : V)) +ᵥ (b : V) := by
+    intro x
+    simpa [zOf] using (Classical.choose_spec (hx_on_line x))
+
+  let γ : Type := {z : F // Good ((z • (d : V)) +ᵥ (b : V))}
+
+  let g : fiber → γ := fun x =>
+    ⟨zOf x, by
+      simpa [hzOf_spec x] using (x.1.2 : Good (x.1.1 : V))⟩
+
+  have hg_inj : Function.Injective g := by
+    intro x₁ x₂ h
+    have hz : zOf x₁ = zOf x₂ := congrArg Subtype.val h
+
+    have hxV : (x₁.1.1 : V) = (x₂.1.1 : V) := by
+      calc
+        (x₁.1.1 : V) = (zOf x₁ • (d : V)) +ᵥ (b : V) := hzOf_spec x₁
+        _ = (zOf x₂ • (d : V)) +ᵥ (b : V) := by simpa [hz]
+        _ = (x₂.1.1 : V) := (hzOf_spec x₂).symm
+
+    have hxU : (x₁.1.1 : U) = (x₂.1.1 : U) := by
+      ext
+      exact hxV
+
+    have hxα : (x₁.1 : α) = (x₂.1 : α) := by
+      apply Subtype.ext
+      exact hxU
+
+    apply Subtype.ext
+    exact hxα
+
+  have hcard : Fintype.card fiber ≤ Fintype.card γ :=
+    Fintype.card_le_of_injective g hg_inj
+
+  refine ⟨b, ?_⟩
+  exact lt_of_lt_of_le hfiber hcard
+
+
+theorem wca_exists_eq_of_cover_lt_fieldCard {F V : Type} [Field F] [Fintype F] [DecidableEq F]
+  [AddCommGroup V] [Module F V] [FiniteDimensional F V] [Fintype V] [DecidableEq V]
+  (U : AffineSubspace F V) [Nonempty U]
+  (L : Finset (AffineSubspace F V))
+  (hL : L.card < Fintype.card F)
+  (hsub : ∀ A ∈ L, A ≤ U)
+  (hnonempty : ∀ A ∈ L, Nonempty A)
+  (hcover : (U : Set V) ⊆ ⋃ A ∈ L, (A : Set V)) :
+  ∃ A ∈ L, A = U := by
+  classical
+  let q : ℕ := Fintype.card F
+  have hqpos : 0 < q := Fintype.card_pos
+
+  -- Split on `finrank` of the direction of `U`.
+  cases hdim : Module.finrank F U.direction with
+  | zero =>
+      -- If `U.direction` has finrank 0, then `U.direction = ⊥` and any nonempty `A ≤ U` must equal `U`.
+      let u0 : U := Classical.choice (inferInstance : Nonempty U)
+      have hu : (u0.1 : V) ∈ ⋃ A ∈ L, (A : Set V) := hcover u0.2
+      rcases Set.mem_iUnion.1 hu with ⟨A, huA⟩
+      rcases Set.mem_iUnion.1 huA with ⟨hAL, huA'⟩
+      refine ⟨A, hAL, ?_⟩
+      have hAle : A ≤ U := hsub A hAL
+      have hAne : (A : Set V).Nonempty := by
+        rcases hnonempty A hAL with ⟨a⟩
+        exact ⟨a.1, a.2⟩
+      have hUdir : U.direction = ⊥ :=
+        (Submodule.finrank_eq_zero (R := F) (S := U.direction)).1 hdim
+      have hAdir_le : A.direction ≤ U.direction := AffineSubspace.direction_le hAle
+      have hAdir : A.direction = ⊥ := by
+        have : A.direction ≤ (⊥ : Submodule F V) := by
+          simpa [hUdir] using hAdir_le
+        exact le_antisymm this bot_le
+      have hdirEq : A.direction = U.direction := by
+        simpa [hAdir, hUdir]
+      exact
+        AffineSubspace.eq_of_direction_eq_of_nonempty_of_le hdirEq hAne hAle
+
+  | succ d' =>
+      -- Main counting argument in positive dimension.
+      by_contra hex
+      have hne : ∀ A ∈ L, A ≠ U := by
+        intro A hA hEq
+        exact hex ⟨A, hA, hEq⟩
+
+      -- Cardinality of `U`.
+      let u0 : U := Classical.choice (inferInstance : Nonempty U)
+      have cardU : Fintype.card U = q ^ Nat.succ d' := by
+        have h1 : Fintype.card U = Fintype.card U.direction :=
+          Fintype.card_congr (Equiv.vaddConst u0).symm
+        have h2 : Fintype.card U.direction = q ^ Nat.succ d' := by
+          simpa [q, hdim] using (Module.card_eq_pow_finrank (K := F) (V := U.direction))
+        exact h1.trans h2
+
+      -- Surjection from the disjoint union of all `A ∈ L` onto `U`.
+      let g : (Σ A : L, A.1) → U := fun x =>
+        ⟨x.2.1, (hsub x.1.1 x.1.2) x.2.2⟩
+
+      have hg : Function.Surjective g := by
+        intro u
+        have hu : (u.1 : V) ∈ ⋃ A ∈ L, (A : Set V) := hcover u.2
+        rcases Set.mem_iUnion.1 hu with ⟨A, huA⟩
+        rcases Set.mem_iUnion.1 huA with ⟨hAL, huA'⟩
+        refine ⟨⟨⟨A, hAL⟩, ⟨u.1, huA'⟩⟩, ?_⟩
+        ext
+        rfl
+
+      have hcardU_le_sigma : Fintype.card U ≤ Fintype.card (Σ A : L, A.1) :=
+        Fintype.card_le_of_surjective g hg
+
+      have hcardSigma : Fintype.card (Σ A : L, A.1) = ∑ A : L, Fintype.card A.1 := by
+        simpa using (Fintype.card_sigma (β := fun A : L => A.1))
+
+      have hcardU_le_sum : Fintype.card U ≤ ∑ A : L, Fintype.card A.1 := by
+        simpa [hcardSigma] using hcardU_le_sigma
+
+      -- Uniform bound on the size of each `A ∈ L`.
+      let bound : ℕ := q ^ d'
+      have bound_pos : 0 < bound := by
+        dsimp [bound]
+        exact Nat.pow_pos hqpos
+
+      have hcardA_le : ∀ A : L, Fintype.card A.1 ≤ bound := by
+        intro A
+        have hAle : A.1 ≤ U := hsub A.1 A.2
+        have hAne : (A.1 : Set V).Nonempty := by
+          rcases hnonempty A.1 A.2 with ⟨a⟩
+          exact ⟨a.1, a.2⟩
+        have hAlt : A.1 < U := lt_of_le_of_ne hAle (hne A.1 A.2)
+        have hdirlt : A.1.direction < U.direction :=
+          AffineSubspace.direction_lt_of_nonempty hAlt hAne
+        have hfinrank_lt : Module.finrank F A.1.direction < Nat.succ d' := by
+          have : Module.finrank F A.1.direction < Module.finrank F U.direction :=
+            Submodule.finrank_lt_finrank_of_lt (K := F) (V := V) hdirlt
+          simpa [hdim] using this
+        have hle_exp : Module.finrank F A.1.direction ≤ d' := Nat.le_of_lt_succ hfinrank_lt
+
+        obtain ⟨p, hp⟩ := hAne
+        let pA : A.1 := ⟨p, hp⟩
+        letI : Nonempty A.1 := ⟨pA⟩
+
+        have hAcard : Fintype.card A.1 = Fintype.card A.1.direction :=
+          Fintype.card_congr (Equiv.vaddConst pA).symm
+
+        have card_dir : Fintype.card A.1.direction = q ^ Module.finrank F A.1.direction := by
+          simpa [q] using (Module.card_eq_pow_finrank (K := F) (V := A.1.direction))
+
+        have cardA_eq : Fintype.card A.1 = q ^ Module.finrank F A.1.direction :=
+          hAcard.trans card_dir
+
+        have hpow_le : q ^ Module.finrank F A.1.direction ≤ q ^ d' :=
+          Nat.pow_le_pow_right hqpos hle_exp
+
+        simpa [bound, cardA_eq] using hpow_le
+
+      have hsum_le : (∑ A : L, Fintype.card A.1) ≤ Fintype.card L * bound := by
+        classical
+        simpa using
+          (Finset.sum_le_card_nsmul (s := (Finset.univ : Finset L))
+            (f := fun A : L => Fintype.card A.1) (n := bound) (by
+              intro A _
+              exact hcardA_le A))
+
+      have hL' : Fintype.card L < q := by
+        simpa [q] using hL
+
+      have hstrict_prod : Fintype.card L * bound < q * bound :=
+        Nat.mul_lt_mul_of_pos_right hL' bound_pos
+
+      have hqmul : q * bound = q ^ Nat.succ d' := by
+        dsimp [bound]
+        -- `q^(d'+1) = q^d' * q`
+        simpa [Nat.pow_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
+
+      have hprod_lt_cardU : Fintype.card L * bound < Fintype.card U := by
+        have : Fintype.card L * bound < q ^ Nat.succ d' :=
+          lt_of_lt_of_eq hstrict_prod hqmul
+        simpa [cardU] using this
+
+      have : Fintype.card U < Fintype.card U := by
+        have h1 : Fintype.card U ≤ ∑ A : L, Fintype.card A.1 := hcardU_le_sum
+        have h2 : (∑ A : L, Fintype.card A.1) ≤ Fintype.card L * bound := hsum_le
+        have h3 : Fintype.card L * bound < Fintype.card U := hprod_lt_cardU
+        exact lt_of_le_of_lt (le_trans h1 h2) h3
+
+      exact lt_irrefl _ this
+
+
+theorem wca_ratio_bound_implies_exists_v [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F}
+  {deg : ℕ} {domain : ι ↪ F}
+  {μ : ι → Set.Icc (0 : ℚ) 1}
+  {α : ℝ≥0}
+  {M m : ℕ}
+  [DecidablePred (fun x : (WCA_affineSpace u) =>
+    WCA_good (F := F) (ι := ι) μ domain deg α x.1)]
+  (hm : 3 ≤ m)
+  (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ))
+  (sr : ℝ≥0)
+  (hsr : sr = ReedSolomonCode.sqrtRate deg domain) :
+  (0 : ℝ≥0) < sr →
+  (sr * (1 + 1 / (2 * m : ℝ)) ≤ α) →
+  (α < 1) →
+  ((Fintype.card {x : (WCA_affineSpace u) //
+        WCA_good (F := F) (ι := ι) μ domain deg α x.1} : ENNReal) /
+      (Fintype.card (WCA_affineSpace u))) >
+    ENNReal.ofReal (WCA_bound ι F sr M m) →
+  ∃ v : Fin (l + 2) → ι → F,
+    (∀ i, v i ∈ ReedSolomon.code domain deg) ∧
+    mu_set μ {i : ι | ∀ j, u j i = v j i} ≥ α := by
+  -- This lemma is the core combinatorial lift (BCIKS20 §6.3/§7.3) from a lower bound on the density of `Good` points in the affine space `U := WCA_affineSpace u` to a global correlated-agreement witness.
+  -- 
+  -- Recommended skeleton:
+  -- - Work with `U := WCA_affineSpace u` and `Good := WCA_good μ domain deg α`.
+  -- - Split on `U.direction = ⊥` vs `≠ ⊥`.
+  --   * `direction = ⊥`: `U` is a singleton; use the ratio bound to show the unique point is good and pick witnesses directly.
+  --   * `direction ≠ ⊥`: implement the BCIKS20 minimizer/list/cover/collapse argument.
+  -- 
+  -- Nontrivial case outline:
+  -- 1. Choose `u* : U` minimizing `agree_set μ (↑u*) (finCarrier domain deg)` (finite min exists).
+  -- 2. Let `α*` be that minimum; show `α* ≥ α`.
+  -- 3. Define the candidate list `V* := {v ∈ finCarrier domain deg | agree μ (↑u*) v ≥ α*}`.
+  -- 4. Use the *max-right* part of `WCA_bound` to show `V*.card < Fintype.card F`.
+  -- 5. For each `v ∈ V*`, build an affine subspace `A_v ≤ U` (nonempty, contains `u*`) such that
+  --    `⋃ v∈V*, A_v` covers `U`.
+  --    (This uses the line theorem `weighted_correlated_agreement_for_parameterized_curves'` with `l := 0` on lines from `u*` to arbitrary points.)
+  -- 6. Apply `wca_exists_eq_of_cover_lt_fieldCard` to the cover to get some `v` with `A_v = U`.
+  -- 7. From `A_v = U`, extract codewords for each generator `u j` agreeing on a common domain of μ-measure ≥ α, and finish with `mu_set_mono`.
+  -- 
+  -- Tips:
+  -- - You already have the geometric collapse lemma `wca_exists_eq_of_cover_lt_fieldCard`; focus on constructing the cover and proving the card bound.
+  -- - Keep ENNReal/ℝ coercions localized; switch to Nat-card inequalities only when applying `wca_exists_base_with_many_good_on_line` or similar pigeonhole steps.
+  sorry
 
-Version with different bounds.
--/
-theorem weighted_correlated_agreement_over_affine_spaces'
-  [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F}
+theorem weighted_correlated_agreement_over_affine_spaces'_direct [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F}
+  {deg : ℕ} {domain : ι ↪ F}
+  {μ : ι → Set.Icc (0 : ℚ) 1}
+  {α : ℝ≥0}
+  {M m : ℕ}
+  (hm : 3 ≤ m)
+  (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ))
+  (sr : ℝ≥0)
+  (hsr : sr = ReedSolomonCode.sqrtRate deg domain)
+  (pr : ENNReal)
+  (hpr : pr = Pr_{let x ←$ᵖ (WCA_affineSpace u)}[WCA_good (F := F) (ι := ι) μ domain deg α x]) :
+  (0 : ℝ≥0) < sr →
+  (sr * (1 + 1 / (2 * m : ℝ)) ≤ α) →
+  (α < 1) →
+  pr > ENNReal.ofReal (WCA_bound ι F sr M m) →
+  ∃ v : Fin (l + 2) → ι → F,
+    (∀ i, v i ∈ ReedSolomon.code domain deg) ∧
+    mu_set μ {i : ι | ∀ j, u j i = v j i} ≥ α := by
+  classical
+  intro hsr_pos hα hα₁ hpr_bound
+
+  -- Provide decidability for the "good" predicate on the affine space.
+  haveI : DecidablePred (fun x : (WCA_affineSpace u) =>
+      WCA_good (F := F) (ι := ι) μ domain deg α x.1) :=
+    Classical.decPred _
+
+  -- Rewrite the probability bound using `hpr`.
+  have hpr_bound' :
+      Pr_{let x ←$ᵖ (WCA_affineSpace u)}[WCA_good (F := F) (ι := ι) μ domain deg α x] >
+        ENNReal.ofReal (WCA_bound ι F sr M m) := by
+    simpa [hpr] using hpr_bound
+
+  -- Convert probability to a counting ratio.
+  have hPr :
+      Pr_{let x ←$ᵖ (WCA_affineSpace u)}[WCA_good (F := F) (ι := ι) μ domain deg α x] =
+        ((Fintype.card {x : (WCA_affineSpace u) //
+              WCA_good (F := F) (ι := ι) μ domain deg α x.1} : ENNReal) /
+          (Fintype.card (WCA_affineSpace u))) := by
+    simpa using
+      (pr_uniformOfFintype_eq_card (α := (WCA_affineSpace u))
+        (P := fun x : (WCA_affineSpace u) =>
+          WCA_good (F := F) (ι := ι) μ domain deg α x.1))
+
+  have hratio :
+      ((Fintype.card {x : (WCA_affineSpace u) //
+            WCA_good (F := F) (ι := ι) μ domain deg α x.1} : ENNReal) /
+          (Fintype.card (WCA_affineSpace u))) >
+        ENNReal.ofReal (WCA_bound ι F sr M m) := by
+    -- Rewrite only the LHS of `hpr_bound'` and avoid simplifying the `max` inside `WCA_bound`.
+    have h := hpr_bound'
+    rw [hPr] at h
+    exact h
+
+  -- Now apply the packaged affine-space→line reduction.
+  exact
+    wca_ratio_bound_implies_exists_v (F := F) (ι := ι) (k := k)
+      (hm := hm) (hμ := hμ) (sr := sr) (hsr := hsr)
+      hsr_pos hα hα₁ hratio
+
+theorem weighted_correlated_agreement_over_affine_spaces' [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F}
   {deg : ℕ} {domain : ι ↪ F}
   {μ : ι → Set.Icc (0 : ℚ) 1}
   {α : ℝ≥0}
   {M m : ℕ}
   (hm : 3 ≤ m)
   (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ)) :
-  letI sqrtRate := ReedSolomonCode.sqrtRate deg domain
+  letI sr := ReedSolomonCode.sqrtRate deg domain
+  (hsr_pos : (0 : ℝ≥0) < sr) →
   letI pr :=
-    Pr_{let u ←$ᵖ (u 0 +ᵥ affineSpan F (Finset.univ.image (Fin.tail u)).toSet)
-    }[agree_set μ u (finCarrier domain deg) ≥ α]
-  (hα : sqrtRate * (1 + 1 / (2 * m : ℝ)) ≤ α) →
+    Pr_{let x ←$ᵖ (WCA_affineSpace u)}[agree_set μ x (finCarrier domain deg) ≥ α]
+  (hα : sr * (1 + 1 / (2 * m : ℝ)) ≤ α) →
+  (hα₁ : α < 1) →
   letI numeratorl : ℝ := (1 + 1 / (2 * m : ℝ))^7 * m^7 * (Fintype.card ι)^2
-  letI denominatorl : ℝ := (3 * sqrtRate^3) * Fintype.card F
-  letI numeratorr : ℝ := (2 * m + 1) * (M * Fintype.card ι + 1)
-  letI denominatorr : ℝ := sqrtRate * Fintype.card F
+  letI denominatorl : ℝ := (3 * sr^3) * Fintype.card F
+  letI numeratorr : ℝ := (max (2 * m + 3) 23) * (M * Fintype.card ι + 1)
+  letI denominatorr : ℝ := sr * Fintype.card F
   pr > ENNReal.ofReal (max (numeratorl / denominatorl) (numeratorr / denominatorr)) →
   ∃ v : Fin (l + 2) → ι → F,
     (∀ i, v i ∈ ReedSolomon.code domain deg) ∧
-    mu_set μ {i : ι | ∀ j, u j i = v j i} ≥ α := by sorry
+    mu_set μ {i : ι | ∀ j, u j i = v j i} ≥ α := by
+  classical
+  simpa using
+    (weighted_correlated_agreement_over_affine_spaces'_direct (F := F) (ι := ι) (k := k) (l := l) (u := u)
+      (deg := deg) (domain := domain) (μ := μ) (α := α) (M := M) (m := m) hm hμ)
+
 
 /--
 Lemma 7.5 in [BCIKS20].