fix(BCIKS20): correct false/vacuous statement of large_agreement_set_on_curve_implies_correlated_agreement

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean

@@ -44,50 +44,61 @@ variable {n : ℕ} [NeZero n]
 /-- The parameters for which the curve points are `δ`-close to a set `V`
 (typically, a linear code). This is the set `S` from the proximity gap paper. -/
 noncomputable def coeffs_of_close_proximity_curve {l : ℕ}
-    (δ : ℚ≥0) (u : Fin l → Fin n → F) (V : Finset (Fin n → F)) : Finset F :=
-  have : Fintype { z | δᵣ(Curve.polynomialCurveEval (F := F) (A := F) u z, V) ≤ δ } := by
-    infer_instance
-  @Set.toFinset _ { z | δᵣ(Curve.polynomialCurveEval (F := F) (A := F) u z, V) ≤ δ } this
-
-/-- If the set of points `δ`-close to the code `V` has at least `n * l + 1` points, then
-there exists a curve defined by vectors `v` from `V` such that the points of `curve u`
-and `curve v` are `δ`-close with the same parameters. Moreover, `u` and `v` differ at
-at most `δ * n` positions. -/
+    (δ : ℚ≥0) (u : Fin l → Fin n → F) (V : Set (Fin n → F)) : Finset F :=
+  Finset.filter (fun z : F => δᵣ(Curve.polynomialCurveEval (F := F) (A := F) u z, V) ≤ δ)
+    Finset.univ
+
+/-- Unique-decoding regime (`δ ≤ (1 - ρ) / 2`); companion of
+`large_agreement_set_on_curve_implies_correlated_agreement'` (Johnson regime). This is
+Theorem 6.1 of [BCIKS20]. `V` must be an actual Reed-Solomon code (of rate `ρ`, tied to `V` via
+its degree/domain) rather than an arbitrary set of words: the conclusion is false for a `V` with
+no algebraic structure connecting its elements, e.g. a `V` that is merely a "coincidentally
+close" `Finset` unrelated to `ρ`. If more than `(l - 1) * n` points on the curve defined by `u`
+are `δ`-close to `V`, then: every point of the curve is `δ`-close to `V`; there exist vectors `v`
+from `V` such that every point of the `v`-curve is `δ`-close to the corresponding point of the
+`u`-curve; and `u`, `v` agree outside a `δ`-fraction of coordinates. -/
 theorem large_agreement_set_on_curve_implies_correlated_agreement {l : ℕ}
-    {rho : ℚ≥0}
+    {deg : ℕ}
+    {domain : Fin n ↪ F}
     {δ : ℚ≥0}
-    {V : Finset (Fin n → F)}
-    (hδ : δ ≤ (1 - rho) / 2)
+    (hδ : δ ≤ (1 - ρ (ReedSolomon.code domain deg)) / 2)
     {u : Fin l → Fin n → F}
-    (hS : n * l < (coeffs_of_close_proximity_curve (F := F) δ u V).card) :
-    coeffs_of_close_proximity_curve (F := F) δ u V = Finset.univ ∧
-      ∃ v : Fin l → Fin n → F,
-        ∀ z,
-          δᵣ(Curve.polynomialCurveEval (F := F) (A := F) u z,
-            Curve.polynomialCurveEval (F := F) (A := F) v z) ≤ δ ∧
-          ({ x : Fin n | ∃ i, u i x ≠ v i x } : Finset _).card ≤ δ * n := by
+    (hS : (l - 1) * n <
+      (coeffs_of_close_proximity_curve (F := F) δ u (ReedSolomon.code domain deg)).card) :
+    (∀ z : F, δᵣ(Curve.polynomialCurveEval (F := F) (A := F) u z,
+      ReedSolomon.code domain deg) ≤ δ) ∧
+    ∃ v : Fin l → Fin n → F,
+      (∀ i, v i ∈ ReedSolomon.code domain deg) ∧
+      (∀ z, δᵣ(Curve.polynomialCurveEval (F := F) (A := F) u z,
+        Curve.polynomialCurveEval (F := F) (A := F) v z) ≤ δ) ∧
+      ({ x : Fin n | ∃ i, u i x ≠ v i x } : Finset _).card ≤ δ * n := by
   sorry
 
 /-- The distance bound from [BCIKS20]. -/
 noncomputable def δ₀ (rho : ℚ) (m : ℕ) : ℝ :=
   1 - Real.sqrt rho - Real.sqrt rho / (2 * m)
 
-/-- If the set of points on the curve defined by `u` close to `V` has at least
-`((1 + 1 / (2 * m)) ^ 7 * m ^ 7) / (3 * (Real.rpow rho (3 / 2 : ℚ))) * n ^ 2 * l + 1`
+/-- Johnson regime; Theorem 6.2 of [BCIKS20]. As in the unique-decoding companion
+`large_agreement_set_on_curve_implies_correlated_agreement`, `V` must be an actual Reed-Solomon
+code (of rate `ρ`) rather than an arbitrary set of words. If the set of points on the curve
+defined by `u` close to `V` has more than
+`((1 + 1 / (2 * m)) ^ 7 * m ^ 7) / (3 * (Real.rpow ρ (3 / 2 : ℚ))) * n ^ 2 * (l - 1)`
 points, then there exist vectors `v` from `V` that are `(1 - δ) * n` close to `u`. -/
 theorem large_agreement_set_on_curve_implies_correlated_agreement' {l : ℕ}
     [Finite F]
     {m : ℕ}
-    {rho : ℚ≥0}
+    {deg : ℕ}
+    {domain : Fin n ↪ F}
     {δ : ℚ≥0}
     (hm : 3 ≤ m)
-    {V : Finset (Fin n → F)}
-    (hδ : δ ≤ δ₀ rho m)
+    (hδ : δ ≤ δ₀ (ρ (ReedSolomon.code domain deg)) m)
     {u : Fin l → Fin n → F}
-    (hS : ((1 + 1 / (2 * m)) ^ 7 * m ^ 7) / (3 * (Real.rpow rho (3 / 2 : ℚ)))
-      * n ^ 2 * l < (coeffs_of_close_proximity_curve (F := F) δ u V).card) :
+    (hS : ((1 + 1 / (2 * m)) ^ 7 * m ^ 7) /
+        (3 * (Real.rpow (ρ (ReedSolomon.code domain deg)) (3 / 2 : ℚ)))
+      * n ^ 2 * (l - 1) <
+      (coeffs_of_close_proximity_curve (F := F) δ u (ReedSolomon.code domain deg)).card) :
     ∃ v : Fin l → Fin n → F,
-      ∀ i, v i ∈ V ∧
+      (∀ i, v i ∈ ReedSolomon.code domain deg) ∧
         (1 - δ) * n ≤ ({ x : Fin n | ∀ i, u i x = v i x } : Finset _).card := by
   sorry