feat(proximity-gap): harden BCIKS20 curve regimes

[latifkasuli]

Summary

This is a stacked follow-up to #639. The new changes in commit 5901e0a9 harden the BCIKS20 Section 6 curve statements and add a kernel-checked degree-one case of Theorem 6.1.

• bind the Section 6 helpers to the actual Reed-Solomon code and its actual rate/radius instead of arbitrary V and free rho
• use Fin (l + 1) for the paper's degree-l curve convention
• include the missing requirement that reconstructed coefficients are Reed-Solomon codewords
• restrict the headline proximity-gap theorem to the proven open Johnson/Guruswami-Sudan regime 0 < delta < 1 - sqrt(rho)
• explicitly exclude BCIKS20's separate capacity-regime Conjecture 8.4
• prove the degree-one Theorem 6.1 bridge from polynomial curves to the existing affine-line joint-agreement result
• update STIR/Folding callers for the strict regime contract

Why the contract change is necessary

The previous general helper quantified over an arbitrary finite set V and an unconstrained rho. That is stronger than BCIKS20 and false in general: the source theorem fixes V to the Reed-Solomon code and uses its actual rate. The paper also uses l + 1 coefficient words for a degree-l curve.

This PR preserves BCIKS20's proved unique-decoding and sub-Johnson statements. It does not promote the later capacity conjecture that was refuted in IACR ePrint 2025/2046.

Verification

• lake build ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.Curves ArkLib.ProofSystem.Stir.Combine ArkLib.Data.CodingTheory.ProximityGap.Folding
• #print axioms ProximityGap.large_agreement_set_on_line_implies_correlated_agreement
  • [propext, Classical.choice, Quot.sound]
  • no sorryAx
• ./scripts/validate.sh
  • 4,048 build jobs completed
  • Data warning budget passed
  • umbrella imports passed
  • docs integrity passed
  • knowledge-base lint passed
• git diff --check

Honest boundary

Three admissions remain in Curves.lean: the full degree-l Theorem 6.1 helper, Theorem 6.2, and the headline correlated-agreement theorem. Consequently STIR combine_theorem remains readiness-blocked. This PR repairs their mathematical contracts and proves only the degree-one Theorem 6.1 case.

Stack

• depends on feat(proximity-gap): prove BCIKS20 curve agreement bounds #639 (agent/bciks20-affine-lines-list-decoding)
• review the final commit 5901e0a9 for this slice until feat(proximity-gap): prove BCIKS20 curve agreement bounds #639 merges

[github-actions]

🤖 PR Summary

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

The PR hardens the BCIKS20 Section 6 curve statements by specializing the proximity-gap helpers to the actual Reed‑Solomon code and its rate/radius, proving the degree‑one case of Theorem 6.1, and tightening the inequality contracts in callers. Three admissions remain in the degree‑l case, blocking STIR’s combine_theorem.

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	428
❌ Lines Removed	52

---

Lean Declarations

✏️ Added: 1 declaration(s)

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean (1)

• theorem large_agreement_set_on_line_implies_correlated_agreement {deg : ℕ}

✏️ Affected: 3 declaration(s) (line number changed)

• noncomputable def δ₀ (rho : ℝ) (m : ℕ) : ℝ in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean moved from L72 to L188
• theorem large_agreement_set_on_curve_implies_correlated_agreement {l deg : ℕ} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean moved from L56 to L167
• theorem large_agreement_set_on_curve_implies_correlated_agreement' {l deg : ℕ} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean moved from L78 to L199

---

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 primarily implements two core lemmas from BCIKS20 (Lemmas 7.5 and 7.6) in WeightedAgreement.lean, relaxes their hypotheses by removing redundant code-membership arguments, strengthens the statement of correlatedAgreement_affine_curves to require a strict inequality δ < 1 - √ρ, and adjusts dependent call-sites in Folding.lean and Combine.lean. One remaining sorry block is left in Curves.lean for the full Theorem 6.1. No violations of the style or naming guidelines were detected beyond the continued use of hδ where the guideline suggests hδ_pos; the diff itself introduces that pattern so it is not a regression. No deprecation notices, documentation gaps, or blueprint citation issues were introduced beyond the scope of the client's instructions. No findings specific to the provided workflow instructions (which focus on general contribution guidelines rather than a project-specific checklist).

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean: Added import AffineLines.JointAgreement and a new, fully-proved theorem large_agreement_set_on_line_implies_correlated_agreement (degree-one case of Theorem 6.1). Modified the (still sorry) theorems correlatedAgreement_affine_curves, large_agreement_set_on_curve_implies_correlated_agreement (Theorem6.1) and large_agreement_set_on_curve_implies_correlated_agreement' (Theorem6.2): their signatures now take an explicit domain and deg, the distance set V is specialized to ReedSolomon.toFinset domain deg, the type of δ changed from ℚ≥0 to ℝ≥0 also in the helper coeffs_of_close_proximity_curve, and the δ₀ function now takes ℝ instead of ℚ. The hδ hypotheses now refer to the code's relative unique-decoding radius (Code.relativeUniqueDecodingRadius) or its rate via LinearCode.rate, and the docstrings have been updated to reflect the Johnson/Guruswami-Sudan regime restriction.
• 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 were refactored: both removed the parameters k, deg, domain and the hypothesis hv (that each v i is a Reed‑Solomon codeword), making them purely combinatorial bounds that no longer require code‑membership. Their previously sorry proofs have been filled in – the first lemma now gives a full algebraic derivation of the strict inequality, and the second reduces to the first via a rational‑weight grid argument using the new condition on hμ and the existing cardinality condition hS'_card₁.
• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean: In folding_preserves_distance, tightened the hypothesis bound_tighter from (↑δ) ≤ 1 - ReedSolomon.sqrtRate ... to (↑δ) < 1 - ReedSolomon.sqrtRate ..., and added a new explicit argument (hδ_pos := δ_gt_0) to the call of correlatedAgreement_affine_curves. These changes strengthen the inequality required and supply a positivity condition for δ, likely aligning with updated assumptions in the invoked lemma.
• ArkLib/ProofSystem/Stir/Combine.lean: In combine_theorem (ArkLib/ProofSystem/Stir/Combine.lean), the argument to ProximityGap.correlatedAgreement_affine_curves that provides an inequality on δ was changed from a derived proof using le_of_lt to a direct use of the hypothesis hδPos. This makes the proof’s reliance on hδPos explicit, likely reflecting that the hypothesis is now an assumption of the theorem or a local context variable, simplifying the reasoning and aligning with upstream API changes.

---

Last updated: 2026-07-12 18:53 UTC.