BCIKS20 `large_agreement_set_on_curve_implies_correlated_agreement` is false as stated (vacuous `∃ v`, `rho` unlinked to `V`)

[aryaethn]

File: ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean
(theorem large_agreement_set_on_curve_implies_correlated_agreement, currently ~L56–L69)

While studying the BCIKS20 Section-6 curve results I believe the statement of
large_agreement_set_on_curve_implies_correlated_agreement has two problems: one of its conclusions
is vacuous, and the remaining content is false as written. Both observations are machine-checked
against current main (b321c7ef, Lean v4.30.0). The sibling …_correlated_agreement' (Johnson
regime, ~L78–L92) looks correctly shaped and is the natural template for a fix. Filing for
coordination before anyone invests in a proof of the current statement.

The statement

theorem large_agreement_set_on_curve_implies_correlated_agreement {l : ℕ}
    {rho : ℚ≥0} {δ : ℚ≥0} {V : Finset (Fin n → F)}
    (hδ : δ ≤ (1 - rho) / 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 := sorry

Problem 1 — the ∃ v … conjunct is vacuous

v := u discharges it with no hypotheses: δᵣ(curve u z, curve u z) = 0 ≤ δ
(relHammingDist u u = hammingDist u u / _ = 0), and {x | ∃ i, u i x ≠ u i x} = ∅, whose card is
0 ≤ δ * n. So the existential carries no information, and the only real content of the conclusion is
coeffs_of_close_proximity_curve … = Finset.univ. The following compiles in the file's section
context (lake env lean, exit 0):

example {l : ℕ} {δ : ℚ≥0} {u : Fin l → Fin n → F} :
    ∃ 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
  refine ⟨u, fun z => ⟨?_, ?_⟩⟩
  · simp [relHammingDist]
  · simp

(The intended conclusion — cf. the primed sibling — is presumably that there are codewords v
from V with large agreement, e.g. ∀ i, v i ∈ V and a (1 - δ) * n ≤ |agree| bound.)

Problem 2 — the remaining content (S = Finset.univ) is false as stated

rho occurs only in hδ and is otherwise unconstrained, so the theorem is equivalent to its
rho := 0 instance, i.e. ∀ δ ≤ 1/2, …. In particular δ is never tied to the minimum distance of
V (no rate V = rho, no 2 * δ * n < Code.dist V), which the unique-decoding argument needs.

Counterexample. Take F = ZMod 5, n = 1, l = 2, rho = 0, δ = 1/2 (so hδ : 1/2 ≤ 1/2),
u 0 = fun _ => 0, u 1 = fun _ => 1 (so Curve.polynomialCurveEval u z = fun _ => z), and
V = {fun _ => 0, fun _ => 1, fun _ => 2} (|V| = 3). Since n = 1, δᵣ(·,·) ∈ {0,1}, so
δᵣ(curve z, V) ≤ 1/2 ⟺ curve z ∈ V ⟺ z ∈ {0,1,2} (here δᵣ(·, V) is the min relative distance to
V). Hence S := coeffs_of_close_proximity_curve δ u V = {0,1,2}, and:

• hS: n * l = 2 < 3 = |S| ✓ (both hypotheses hold)
• conclusion: S = Finset.univ, i.e. {0,1,2} = ZMod 5 ✗ (3, 4 ∉ S)

The threshold n * l and the bound on δ are both independent of |F| and of V's distance, so any
V with n * l < |V| < |F| and an injective curve refutes S = univ; the n = 1 instance is just
the minimal witness.

This is machine-checked: the script below compiles against current main and
#print axioms lemma_is_false reports only [propext, Classical.choice, Quot.sound] (no sorry,
no added axiom).

Full reproducible Lean script (drop into the ArkLib/ package, lake env lean)

import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves
import Mathlib.Algebra.Field.ZMod

open NNReal Finset Function
open scoped BigOperators
open Code ProximityGap

namespace BCIKS20CurvesCounterexample

instance : Fact (Nat.Prime 5) := ⟨by decide⟩

abbrev F := ZMod 5

/-- Curve coefficients: `u₀ ≡ 0`, `u₁ ≡ 1`, so `curve(z) = const z`. -/
def u : Fin 2 → Fin 1 → F := ![fun _ => 0, fun _ => 1]

/-- Three codewords. -/
def V : Finset (Fin 1 → F) := {fun _ => 0, fun _ => 1, fun _ => 2}

def δ : ℚ≥0 := 1/2

/-- Helper: the `ℚ≥0 → ENNReal` coercion of `1`. -/
lemma coe_qnn_one : ((1 : ℚ≥0) : ENNReal) = 1 := by
  rw [← ENNReal.coe_nnratCast]; norm_cast

/-- Helper: the `ℚ≥0 → ENNReal` coercion is monotone. -/
lemma coe_qnn_le {a b : ℚ≥0} (h : a ≤ b) : (a : ENNReal) ≤ (b : ENNReal) := by
  rw [← ENNReal.coe_nnratCast a, ← ENNReal.coe_nnratCast b]; exact_mod_cast h

lemma curve_eval (z : F) :
    Curve.polynomialCurveEval (F := F) (A := F) u z = (fun _ => z) := by
  funext x
  simp [Curve.polynomialCurveEval, Fin.sum_univ_two, u]

lemma mem_S_iff (z : F) :
    z ∈ coeffs_of_close_proximity_curve (F := F) δ u V ↔
      relDistFromCode (fun _ : Fin 1 => z) (V : Set (Fin 1 → F)) ≤ (δ : ENNReal) := by
  unfold coeffs_of_close_proximity_curve
  rw [Set.mem_toFinset, Set.mem_setOf_eq, curve_eval z]

/-- `hδ` is satisfiable. -/
lemma hδ_holds : δ ≤ (1 - (0:ℚ≥0)) / 2 := by norm_num [δ]

lemma mem_close (c : F) (hc : (fun _ => c) ∈ V) :
    c ∈ coeffs_of_close_proximity_curve (F := F) δ u V := by
  rw [mem_S_iff]
  calc relDistFromCode (fun _ : Fin 1 => c) (V : Set (Fin 1 → F))
      ≤ ((relHammingDist (fun _ : Fin 1 => c) (fun _ => c) : ℚ≥0) : ENNReal) :=
        relDistFromCode_le_relDist_to_mem _ _ (Finset.mem_coe.mpr hc)
    _ ≤ (δ : ENNReal) := by
        have h0 : relHammingDist (fun _ : Fin 1 => c) (fun _ => c) = 0 := by simp [relHammingDist]
        rw [h0]
        exact coe_qnn_le zero_le'

lemma card_ge : 3 ≤ (coeffs_of_close_proximity_curve (F := F) δ u V).card := by
  have h012 : ({0,1,2} : Finset F) ⊆ coeffs_of_close_proximity_curve (F := F) δ u V := by
    intro c hc
    fin_cases hc <;> · apply mem_close; decide
  calc (3 : ℕ) = ({0,1,2} : Finset F).card := by decide
    _ ≤ _ := Finset.card_le_card h012

/-- `hS` is satisfiable (`n * l = 1 * 2 = 2 < |S|`). -/
lemma hS_holds : (1 : ℕ) * 2 < (coeffs_of_close_proximity_curve (F := F) δ u V).card :=
  lt_of_lt_of_le (by norm_num) card_ge

lemma three_not_mem : (3 : F) ∉ coeffs_of_close_proximity_curve (F := F) δ u V := by
  rw [mem_S_iff]
  intro h
  have hlb : (1 : ENNReal) ≤ relDistFromCode (fun _ : Fin 1 => (3 : F)) (V : Set (Fin 1 → F)) := by
    unfold relDistFromCode
    apply le_sInf
    rintro d ⟨v, hv, hvd⟩
    have hv1 : relHammingDist (fun _ : Fin 1 => (3 : F)) v = 1 := by
      rw [Finset.mem_coe] at hv
      fin_cases hv <;>
      · rw [relHammingDist, show hammingDist (fun _ : Fin 1 => (3 : F)) _ = 1 from by decide]
        simp
    rw [hv1, coe_qnn_one] at hvd
    exact hvd
  have hlt : (δ : ENNReal) < 1 := by
    have hδr : (δ : ℝ≥0) < 1 := by unfold δ; norm_num
    calc (δ : ENNReal) = ((δ : ℝ≥0) : ENNReal) := rfl
      _ < 1 := by exact_mod_cast hδr
  exact absurd (le_trans hlb h) (not_le.mpr hlt)

/-- The conclusion `S = univ` fails. -/
lemma S_ne_univ : coeffs_of_close_proximity_curve (F := F) δ u V ≠ Finset.univ := by
  intro h
  exact three_not_mem (h ▸ Finset.mem_univ (3 : F))

/-- Both hypotheses (`hδ`, `hS`) hold for this instance, yet the conclusion
`coeffs_of_close_proximity_curve … = Finset.univ` fails. -/
theorem lemma_is_false :
    δ ≤ (1 - (0 : ℚ≥0)) / 2 ∧
    1 * 2 < (coeffs_of_close_proximity_curve (F := F) δ u V).card ∧
    coeffs_of_close_proximity_curve (F := F) δ u V ≠ Finset.univ :=
  ⟨hδ_holds, hS_holds, S_ne_univ⟩

end BCIKS20CurvesCounterexample

Suggested fix

Mirror the (correctly-shaped) …_correlated_agreement':

1. Tie rho/δ to V — either state the lemma about a concrete code (as the proven affine-line
   case RS_correlatedAgreement_affineLines_uniqueDecodingRegime does, directly over
   ReedSolomon.code domain deg), or add a hypothesis such as (1 - rho) * n ≤ Code.dist (V : Set _)
   / rho = LinearCode.rate V, so that δ ≤ (1 - rho)/2 lands inside V's unique-decoding radius.
2. Replace the vacuous ∃ v with the intended correlated-agreement conclusion (codewords + a
   genuine agreement/closeness bound), as in the primed version (∀ i, v i ∈ V, etc.).

I'd be happy to follow up with a corrected statement + a proof of the unique-decoding regime if
that's useful — it's the regime already handled for affine lines, so the coordinate-wise
polynomial-curve argument should go through.

Related (lower confidence, not part of this report's core claim)

• …_correlated_agreement' (~L78–L92) shares the rho-disconnected-from-V looseness (Problem 2),
  though its conclusion is correctly shaped (Problem 1 doesn't apply).
• ListDecoding/Guruswami.lean modified_guruswami_has_a_solution (Claim 5.4) has no hypotheses
  relating m, n, k; existence of a nonzero solution to the multiplicity system generally needs the
  degree bounds to dominate the constraints. Worth a separate look.

[aryaethn]

Hey everyone,

Any comments on this issue and its PR? Should I ping anyone specific?

[alexanderlhicks]

Thanks for the issue and PR! It took a while for me to get to it because it clashed with a long trip, sorry about that! Will take a look tomorrow.