δ must be positive in proximity gap theorems

[ElijahVlasov]

δ must be positive in proximity gap theorems and strictly less than the Johnson bound.

[chatgpt-codex-connector]

Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits.
Credits must be used to enable repository wide code reviews.

[github-actions]

🤖 Gemini PR Summary

Strengthens the hypotheses for proximity gap and correlated agreement theorems across affine spaces, curves, and Reed-Solomon codes. The proximity parameter $\delta$ is now required to satisfy $0 < \delta$ and remain strictly below relevant theoretical limits, such as the Johnson bound or the complement of the square root rate ($1 - \sqrt{R}$).

Technical Changes

• Hypothesis Tightening: Updates preconditions in AffineSpaces, Curves, and ReedSolomonGap to enforce strict inequalities for $\delta$, ensuring the soundness of proximity gap definitions.
• API Standardization: Aligning requirements for $\delta$ across geometric and algebraic contexts to provide a uniform interface for proximity-related proofs.

Proof Status

• CRITICAL: The following theorems are updated with the new hypotheses but remain incomplete and contain sorry placeholders:
  • correlatedAgreement_affine_spaces
  • correlatedAgreement_affine_curves

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	8
❌ Lines Removed	4

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following lines violate the style guide:

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/Main.lean:33: (hδPos : 0 < δ) violates "In assumptions, use x ≠ ⊥ (easier to check)." (Since 0 is the bottom element ⊥ for ℝ≥0, this should be δ ≠ 0).
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/Main.lean:34: (hδ : δ < 1 - (ReedSolomonCode.sqrtRate deg domain)) violates "Delimiters: Avoid parentheses where possible." (The parentheses around ReedSolomonCode.sqrtRate deg domain are unnecessary).
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean:34: (hδ : 0 < δ) violates "In assumptions, use x ≠ ⊥ (easier to check)."
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean:34: (hδ : 0 < δ) violates "Indentation: Use 2 spaces for indentation." (Indented 4 spaces).
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean:35: (hδ : δ < 1 - ReedSolomonCode.sqrtRate deg domain) : violates "Indentation: Use 2 spaces for indentation." (Indented 4 spaces).
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean:35: The use of the name hδ twice in the theorem signature (lines 34 and 35) violates the convention for distinct hypothesis naming ("h, h₁, ... : Assumptions/Hypotheses").
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:29: (hδPos : 0 < δ) violates "In assumptions, use x ≠ ⊥ (easier to check)."
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:29: (hδPos : 0 < δ) violates "Indentation: Use 2 spaces for indentation."
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:30: (hδ : δ < 1 - ReedSolomonCode.sqrtRate deg domain) : violates "Indentation: Use 2 spaces for indentation."
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ReedSolomonGap.lean:29: (hδPos : 0 < δ) violates "In assumptions, use x ≠ ⊥ (easier to check)."
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ReedSolomonGap.lean:29: (hδPos : 0 < δ) violates "Indentation: Use 2 spaces for indentation."
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ReedSolomonGap.lean:30: (hδ : δ < 1 - ReedSolomonCode.sqrtRate deg domain) : violates "Indentation: Use 2 spaces for indentation."

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean: This change refines the hypotheses of the correlatedAgreement_affine_spaces theorem by requiring the proximity parameter $\delta$ to be strictly positive and strictly less than the specified error bound. The theorem remains unimplemented and contains a sorry placeholder.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean: This update refines the hypotheses of the correlatedAgreement_affine_curves theorem by requiring the proximity parameter δ to be strictly positive and strictly less than the square-root rate bound. The theorem's proof remains incomplete and contains a sorry placeholder.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ReedSolomonGap.lean: This change modifies the proximity_gap_RSCodes theorem by strengthening the preconditions on the proximity parameter $\delta$, requiring it to be strictly positive and strictly less than the complement of the square root rate. No new definitions or sorry placeholders were introduced.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/Main.lean: This change refines the preconditions for the theorem RS_correlatedAgreement_affineLines by requiring the proximity parameter δ to be strictly positive and strictly less than the complement of the Reed-Solomon code's square root rate. No new theorems or sorry placeholders are introduced.

---

Last updated: 2026-03-23 13:18 UTC.

[Julek]

Small change requested, otherwise LGTM.

[alexanderlhicks]

maybe name both hypotheses differently 😅