minor fixes because I'm not competent enough to push review comments

[alexanderlhicks]

See comments in #105

[github-actions]

🤖 Gemini PR Summary

This diff refines several mathematical definitions and theorem statements for greater precision and correctness.

Here are the key changes:

• ProximityGap.lean: The generalProximityGap definition is strengthened by replacing a logical "or" (∨) with an exclusive "or" (Xor'). This enforces a stricter condition: the probability of a point being close to a code must be either exactly 1 or less than or equal to ε, but not both. This more accurately reflects the "gap" property.

• Prelims.lean: The definition of a line passing through two vectors is changed from a Submodule (using vectorSpan) to an AffineSubspace (using affineSpan). This is a more geometrically accurate and general definition, as an affine line does not need to pass through the origin.

• DivergenceOfSets.lean: The hypothesis for the concentration_bounds lemma is tightened. The previous non-strict inequality (≤) is now a strict inequality (<), and an additional condition is added to ensure the divergence is strictly positive. This refines the conditions under which the concentration bound holds.

---

Analysis of Changes

Metric	Count
📝 Files Changed	3
✅ Lines Added	7
❌ Lines Removed	5

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

Last updated: 2025-10-04 22:54 UTC. See the main CI run for build status.

[alexanderlhicks]

/review

External:
https://eprint.iacr.org/2020/654.pdf
https://cse.buffalo.edu/faculty/atri/courses/coding-theory/book/web-coding-book.pdf

Internal:
ArkLib/Data/CodingTheory/
ArkLib/ProofSystem/Fri

Comments:
Please review these changes for their correctness and accuracy with respect to source material.

[github-actions]

🤖 AI Review (with external context)\n\nGenerating AI review...

Excellent, thank you for providing the code and reference materials. I have performed a detailed review of the pull request. Here is my assessment:

High-Level Summary

This pull request introduces three important corrections to align the Lean formalization more closely with the source paper, "Proximity Gaps for Reed–Solomon Codes". The changes are:

1. Refining the definition of a proximity gap to correctly model the "exactly one of" condition.
2. Correcting the definition of an affine line from a linear subspace (vectorSpan) to a proper affine subspace (affineSpan).
3. Adjusting the bounds in the concentration_bounds lemma to match the strict inequalities specified in the paper.

All changes are accurate, improve the correctness of the formalization, and are well-justified by the source material. I recommend merging this pull request.

Detailed Review

Below are my file-by-file comments.

---

ArkLib/Data/CodingTheory/ProximityGap.lean

Change: The definition of generalProximityGap has been modified to use Xor' instead of ∨ (or).

-    Pr_{let x ← $ᵖ S}[Code.relHammingDistToCode x.1 P ≤ δ] = 1 ∨
-    Pr_{let x ← $ᵖ S}[Code.relHammingDistToCode x.1 P ≤ δ] ≤ ε
+  Xor'
+  ( Pr_{let x ← $ᵖ S}[Code.relHammingDistToCode x.1 P ≤ δ] = 1 )
+  ( Pr_{let x ← $ᵖ S}[Code.relHammingDistToCode x.1 P ≤ δ] ≤ ε )

Assessment: This is a great correction.

• Correctness: The source paper, in Definition 1.1, states that a set satisfies "exactly one of the following" two conditions. The logical ∨ operator allows for both conditions to be true simultaneously. While this is only possible if ε = 1 (making the property trivial), the use of Xor' (exclusive or) more precisely captures the mutual exclusivity implied by the paper's phrasing. In the contexts where this theorem is applied, ε is expected to be small (< 1), making the two conditions mutually exclusive. Using Xor' is therefore more precise and robust.

---

ArkLib/Data/CodingTheory/Prelims.lean

Change: The definition of Affine.line has been changed from a Submodule defined by vectorSpan to an AffineSubspace defined by affineSpan.

-def line [Ring F] (u v : ι → F) : Submodule F (ι → F) :=
-  vectorSpan _ {u, v}
+def line [Ring F] (u v : ι → F) : AffineSubspace F (ι → F) :=
+  affineSpan _ {u, v}

Assessment: This is a critical and correct change.

• Correctness: The previous definition was incorrect. vectorSpan _ {u, v} defines the linear span of u and v, which is the set of all linear combinations {a•u + b•v | a, b ∈ F}. This is typically a 2-dimensional plane passing through the origin, not an affine line.
• The new definition, affineSpan _ {u, v}, correctly defines the affine line passing through points u and v as the set of all affine combinations {a•u + b•v | a, b ∈ F, a + b = 1}. This corresponds to the mathematical concept of an affine line (e.g., {u + z•(v-u) | z ∈ F}) used throughout the reference paper (e.g., in Theorem 1.4 and Remark 1.1). This change fixes a fundamental definition to align with the source material.

---

ArkLib/Data/CodingTheory/DivergenceOfSets.lean

Change: The hypotheses for the concentration_bounds lemma have been updated. The single non-strict inequality ≤ has been replaced by two strict inequalities, 0 < ... and ... < 1 - ....

 lemma concentration_bounds {deg : ℕ} {domain : ι ↪ F}
   {U : AffineSubspace F (ι → F)} [Nonempty U]
-  (hdiv : (divergence U (RScodeSet domain deg) : ℝ≥0) ≤ 1 - ReedSolomonCode.sqrtRate deg domain)
+  (hdiv_pos : 0 < (divergence U (RScodeSet domain deg) : ℝ≥0))
+  (hdiv_lt : (divergence U (RScodeSet domain deg) : ℝ≥0) < 1 - ReedSolomonCode.sqrtRate deg domain)
   : let δ' := divergence U (RScodeSet domain deg)
     Pr_{let y ← $ᵖ U}[Code.relHammingDistToCode y (RScodeSet domain deg) ≠ δ']
     ≤ errorBound δ' deg domain := by sorry

Assessment: This is a correct and necessary refinement.

• Accuracy: The source paper's Corollary 1.3 states the condition for the concentration bound as δ* ∈ (0, 1 − √ρ). This is an open interval, meaning 0 < δ* and δ* < 1 - √ρ.
• The original formalization used ≤, which corresponds to a closed interval at the upper bound. The new hypotheses hdiv_pos and hdiv_lt correctly formalize the open interval (0, 1 - √ρ).
• The condition δ* > 0 is also important, as the proof of Corollary 1.3 in the paper relies on it to define an intermediate δ < δ*. If δ* were 0, the proof logic would not hold.

Conclusion

All three changes are accurate corrections that make the formalization more faithful to the source paper. I approve these changes.

[cloudflare-workers-and-pages]

Deploying arklib with    Cloudflare Pages

Latest commit:	3441bd5
Status:	✅  Deploy successful!
Preview URL:	https://0698e42d.arklib.pages.dev
Branch Preview URL:	https://minor-fixes-codingtheory.arklib.pages.dev

View logs