feat(proximity-gap): prove BCIKS20 curve agreement bounds

[latifkasuli]

Summary

• prove BCIKS20 Lemma 7.5 (list_agreement_on_curve_implies_correlated_agreement_bound)
• prove its integral-weight strengthening, BCIKS20 Lemma 7.6 (sufficiently_large_list_agreement_on_curve_implies_correlated_agreement)
• formalize the coefficient-difference polynomial root bound and weighted double-counting argument
• derive Lemma 7.6 by placing the minimum curve agreement and correlated agreement on the common 1 / (M * |ι|) grid
• remove Reed–Solomon membership parameters that neither combinatorial lemma needs

These are two genuine prerequisites in the BCIKS20 affine-lines list-decoding chain. This PR does not claim to prove Theorem 1.4, RS_correlatedAgreement_affineLines, or STIR's Combine.combine_theorem; those remain blocked by other admitted prerequisites.

Trust and verification

• both declarations build with the real Lean kernel
• #print axioms reports only propext, Classical.choice, and Quot.sound for each declaration (no sorryAx)
• ./scripts/validate.sh passes: full build, Data warning budget, umbrella imports, docs integrity, and knowledge-base lint
• git diff --check passes
• no in-repository caller uses the removed irrelevant parameters

The optional repository-wide style lint still reports ArkLib's existing style backlog. The only finding when the modified file is checked directly is its pre-existing missing module-docstring exception; the new proofs add no style finding.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Prove BCIKS20 curve agreement bounds

sorry delta: -2 (2 removed) — net proof progress

Mathematical Formalization

• Proves BCIKS20 Lemma 7.5 (list_agreement_on_curve_implies_correlated_agreement_bound) and Lemma 7.6 (sufficiently_large_list_agreement_on_curve_implies_correlated_agreement), establishing combinatorial bounds on curve agreement and correlated agreement.
• The core argument formalizes the coefficient‑difference polynomial root bound and a weighted double‑counting argument, then derives Lemma 7.6 by placing the minimum curve agreement and correlated agreement on a common 1 / (M * |ι|) grid.

Proof Completion (sorries removed)

• Both lemmas previously contained sorry placeholders; these have been replaced with complete proofs. The #print axioms output confirms no sorryAx (only propext, Classical.choice, Quot.sound), so all placeholders are resolved.

Refactoring

• The parameters k, deg, and domain were removed from both lemmas, along with the hypothesis hv : ∀ i, v i ∈ ReedSolomon.code domain deg. The proofs demonstrate that Reed–Solomon code membership is unnecessary for the combinatorial root‑counting arguments. No in‑repository callers used the removed parameters, so the change is safe and simplifies the API.
• Corresponding doc‑comments were updated to reflect the new, weaker hypotheses.

Infrastructure / CI

• ./scripts/validate.sh passes (full build, data warning budget, umbrella imports, docs integrity, knowledge‑base lint).
• git diff --check passes (no whitespace errors).
• Style lint (optional) reports only pre‑existing issues; the new proofs add no style findings.

Documentation

• The doc‑comments in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/WeightedAgreement.lean were updated to reflect the removal of Reed–Solomon membership parameters.

All changes are contained in that single file.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	266
❌ Lines Removed	14

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

✅ Removed: 2 `sorry`(s)

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/WeightedAgreement.lean (2)

• lemma list_agreement_on_curve_implies_correlated_agreement_bound (L192)
• lemma sufficiently_large_list_agreement_on_curve_implies_correlated_agreement (L232)

---

📋 **Additional Analysis**

The diff makes progress on the active formalization of BCIKS20 by providing proofs for Lemmas 7.5 and 7.6. The primary change is the removal of the hv (Reed-Solomon code membership) parameter from both lemmas, allowing them to be stated as purely combinatorial results. This is consistent with the blueprint principles for large contributions. The proofs are completed. There is a minor naming inconsistency (agreementPoints, difference_degree) against the style guide and one place where lim (summation) abbreviation usage is ambiguous versus using Finset.sum directly. The remaining items (docstring updates, citation, deprecation, deprecation policy) are not applicable. Overall, the diff aligns with the project's roadmap and style guide with minor adjustments needed.

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/WeightedAgreement.lean: The lemmas list_agreement_on_curve_implies_correlated_agreement_bound and sufficiently_large_list_agreement_on_curve_implies_correlated_agreement (Lemmas 7.5 and 7.6 in [BCIKS20]) have been given complete proofs, replacing the previous sorry placeholders. Both statements were refactored: the parameters k, deg, and domain were removed, and the hypothesis hv : ∀ i, v i ∈ ReedSolomon.code domain deg was deleted, because the proofs now show that code membership is not required for the combinatorial root‑counting arguments. The doc‑comments were updated to reflect this change.

---

Last updated: 2026-07-11 18:42 UTC.

[alexanderlhicks]

Thanks!