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

[aryaethn]

Closes #588. Corrects the statement of large_agreement_set_on_curve_implies_correlated_agreement
in ProximityGap/BCIKS20/Curves.lean — the two defects #588 reports (a vacuous ∃ v and a false
… = Finset.univ) are removed. The proof of the corrected lemma is left as sorry, exactly as it was
before this change (the sorry count is unchanged); #588 is about the statement being wrong, which
this fixes.

The current conclusion has two defects, both machine-checked in #588:

1. Vacuous ∃ v. v := u discharges the existential with no hypotheses
   (δᵣ(curve u z, curve u z) = 0 ≤ δ, and {x | ∃ i, u i x ≠ u i x} = ∅), so its only real
   content was the first conjunct.
2. False … = Finset.univ. rho occurs only in hδ and is otherwise unconstrained by V, so
   the statement is equivalent to its rho := 0 instance. Concretely (F = ZMod 5, n = 1, l = 2,
   V = {const 0, const 1, const 2}, δ = 1/2): S = {0,1,2}, so both hδ and hS (n·l = 2 < 3)
   hold while S ≠ univ. The counterexample in BCIKS20 large_agreement_set_on_curve_implies_correlated_agreement is false as stated (vacuous ∃ v, rho unlinked to V) #588 compiles and #print axioms reports only
   [propext, Classical.choice, Quot.sound].

This PR restates the lemma to mirror the correctly-shaped Johnson-regime sibling
large_agreement_set_on_curve_implies_correlated_agreement', sharing its conclusion, and keeping the
unique-decoding hypotheses (hδ : δ ≤ (1 - rho) / 2, hS : n * l < #S):

∃ v : Fin l → Fin n → F,
  ∀ i, v i ∈ V ∧
    (1 - δ) * n ≤ ({ x : Fin n | ∀ i, u i x = v i x } : Finset _).card

Notes:

• The sorry count is unchanged (the lemma was already sorry); no declaration consumes it, so no
  downstream code is affected. lake build / validate.sh green locally.
• Design question: the primed sibling also leaves rho unconnected to V. Should both lemmas
  additionally tie rho to V (e.g. V a rate-rho linear code, or (1 - rho) * n ≤ Code.dist V)
  so that δ ≤ (1 - rho)/2 sits inside V's unique-decoding radius? Glad to adjust to whatever shape
  you intend.

Happy to follow up with a proof of the unique-decoding regime once the target statement is confirmed.

[github-actions]

🤖 PR Summary

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

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	38
❌ Lines Removed	27

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff does not relate to the supplied review instructions. The instructions concern contribution guidelines, PR title/description format, and style/naming conventions for ArkLib; the diff only modifies two Lean theorems in a coding theory file. There is no PR description, title change, or style-guideline content to check against the instructions. Therefore the response is: No findings. (No findings.)

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean: The diff overhauls the file that formalizes Theorems 6.1 and 6.2 of the BCIKS20 proximity gap paper. The main change is that V is no longer an arbitrary Finset of words; it is now specifically the ReedSolomon.code determined by a domain embedding and a deg (degree). The definition coeffs_of_close_proximity_curve is rewritten to accept a Set instead of a Finset and to use Finset.filter on Finset.univ instead of Set.toFinset. The statement of large_agreement_set_on_curve_implies_correlated_agreement (Theorem 6.1) is completely changed: it now requires hδ : δ ≤ (1 - ρ(...))/2, uses (l - 1) * n instead of n * l in the cardinality assumption, and its conclusion is a triple conjunction and a ∀ z universal closeness claim, instead of a conjunction with coeffs_of_close_proximity_curve being the full set. Its comment is replaced by a detailed docstring noting it only holds for Reed-Solomon codes. The second theorem, large_agreement_set_on_curve_implies_correlated_agreement', similarly receives a domain and deg parameter; its cardinality assumption now uses (l - 1) instead of l, and its conclusion adds a condition (∀ i, v i ∈ ReedSolomon.code domain deg). Both theorems remain unfinished (sorry).

---

Last updated: 2026-07-10 13:18 UTC.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 3eb66cd13b

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".