Proximity and Correlated Agreement Results #105
Conversation
|
Haven't reviewed this at all yet, just checking in with the review bot |
|
/review External: Internal: Comments: |
🤖 AI Review (with external context)\n\nGenerating AI review...Hello! As an expert code reviewer, I've analyzed the pull request. Here is my review: High-level summaryThis pull request introduces significant new formalizations related to proximity gaps for Reed-Solomon codes, drawing from the Ben-Sasson et al. paper "Proximity Gaps for Reed–Solomon Codes". This includes definitions for divergence of sets, correlated agreement, and proximity gaps, along with statements of key theorems like the concentration bounds. Additionally, the PR includes refactoring and minor fixes in the Berlekamp-Welch decoder implementation, making the proofs cleaner and more explicit. A new notation While the additions are substantial and valuable, I've identified two major issues in the new definitions and a couple of potential off-by-one errors that need to be addressed. The rest of the changes are positive improvements. Major Issues1. Incorrect definition of
|
Julek
force-pushed
the
Katy/ProximityWIP
branch
3 times, most recently
from
10e6aa2 to
720ce0f
Compare
|
/review External: Internal: Comments: |
🤖 AI Review (with external context)\n\nGenerating AI review...Hello! As an expert code reviewer, I've analyzed the provided pull request. Here is my review: High-level summaryThis pull request introduces significant formalizations of key concepts and theorems from the paper "Proximity Gaps for Reed–Solomon Codes" [BCIKS20]. The author has done a great job laying the groundwork for proving these advanced results in Lean. Key additions include:
Overall, this is a high-quality contribution that moves the project forward significantly. I've identified a few areas for improvement, mainly concerning correctness of formalization against the reference document and some minor code quality issues. Formalization CorrectnessI've compared the formalizations against the reference document "[BCIKS20] Proximity Gaps for Reed–Solomon Codes". While most definitions and theorems are captured correctly, there are a couple of discrepancies that should be addressed.
Specific Feedback and Suggestions
I'm impressed with the progress and the quality of the formalization. Addressing these points will make this contribution even stronger. Keep up the excellent work |
|
@katyhr can you fix these errors? I think they are indeed errors. |
Julek
force-pushed
the
Katy/ProximityWIP
branch
from
720ce0f to
fd5a3d9
Compare
|
@quangvdao fixed Theorem 1.5 and amended @Julek fixed the |
refactor Q to Q>=0, fix proofs relHamming dist proofs minor cleanup more cleanups final minor cleanups ProximityGaps draft1 some stuff proximity wip line 257 WIP - thing3 + nonempty explicitly given fix decidable equality def generalProximityGap fix generalProximityGap or something like this latest WIP proximityGaps results cleanup proximity, reedsolomon, divergence and prelims fix the variable name minor edits, added authors in ProximityGap and linter error fixes filled in a small sorry fix of linter errors + other small fixes more linter fixes fixed order of imports Review of ProximityGap PR minor cleanup of comments Co-authored-by: Frantisek Silvasi <[email protected]> Co-authored-by: Julian Sutherland <[email protected]> Co-authored-by: Katerina Hristova <[email protected]>
Julek
force-pushed
the
Katy/ProximityWIP
branch
from
31cb2cd to
3be8f99
Compare
Co-authored-by: Katerina Hristova <[email protected]> Co-authored-by: Julian Sutherland <[email protected]>
Julek
force-pushed
the
Katy/ProximityWIP
branch
from
37ebe36 to
b5a5a1d
Compare
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
🤖 Gemini PR SummaryThis diff introduces a significant formalization of advanced coding theory concepts, particularly proximity gaps for Reed-Solomon codes, while also performing widespread code cleanup and refinement. Here are the key changes:
Analysis of Changes
Last updated: 2025-10-04 21:53 UTC. See the main CI run for build status. |
There was a problem hiding this comment.
Could we move this to the general ToMathLib folder to make it easier to keep track of?
| {p : Polynomial R} {f g : ℕ → R → S} | ||
| (h : ∀ i x, f i x = g i x) | ||
| : p.sum f = p.sum g := by | ||
| aesop (add simp [Polynomial.sum]) |
There was a problem hiding this comment.
Could replace this with simp_all only [Polynomial.sum] which is less likely to break if there are changes to aesop?
There was a problem hiding this comment.
(This is pretty optional, I realise there are many other aseop calls that could similarly be refactored, not sure if we have a consensus preference about this?)
| /-- `Corollary 1.3` (Concentration bounds) from [BCIKS20]. -/ | ||
| lemma concentration_bounds [Fintype F] [Field F] [Fintype ι] {deg : ℕ} {domain : ι ↪ F} | ||
| {U : AffineSubspace F (ι → F)} [Nonempty U] | ||
| (hdiv : (divergence U (RScodeSet domain deg) : ℝ≥0) ≤ 1 - ReedSolomonCode.sqrtRate deg domain) |
There was a problem hiding this comment.
Seems to be a small deviation from the paper here, as it uses δ* ∈ (0, 1 − √ρ) i.e. strict inequality.
| {F : Type*} | ||
|
|
||
| /-- `Definition 1.1` in [BCIKS20]. -/ | ||
| noncomputable def generalProximityGap {α : Type*} [DecidableEq α] [Nonempty α] |
There was a problem hiding this comment.
Based on the paper's wording
Definition 1.1 (Proximity gap). Let P ⊂ Σn be a property and C ⊂ 2Σn
be a collection of sets.
Let ∆ be a distance measure on Σn. We say that C displays a (δ, ε)-proximity gap with respect to P
under ∆ if every S ∈ C satisfies exactly one of the following:
- Pr s∈S[∆(s, P) ≤ δ] = 1.
- Pr s∈S[∆(s, P) ≤ δ] ≤ ε.
We call δ the proximity parameter and ε is the error parameter. By default, ∆ denotes the relative
Hamming distance measure.
Perhaps this should include some constraint like ε < 1 to avoid the case where ε =1 and both conditions are satisfied, or is it basically fine for both to be satisfied? (To some extent this is implicit in the paper as it only considers scenarios where ε is much smaller than 1.)
| {k : ℕ} | ||
|
|
||
| /-- Affine line between two vectors with coefficients in a semiring. -/ | ||
| def line [Ring F] (u v : ι → F) : Submodule F (ι → F) := |
There was a problem hiding this comment.
in #143 this is redefined as
def Affine.line {F : Type*} {ι : Type*} [Semiring F] (u v : ι → F) : Set (ι → F) :=
{x | ∃ a : F, x = u + a • v}
vectorSpan returns a submodule, the above returns a set, and it seems to be me we should also consider affineSpan which seems closer to what we want as it uses affine subspaces (which can be obtained from Submodules too) which show up in Sections 6 and 7 of the proximity gaps paper.
5 participants
We formalise the following definitions, statements and needed preliminaries thereof from [BCIKS20] refers to the paper "Proximity Gaps for Reed-Solomon Codes":
In
ProximityGap.leanDefinition 1.1(Proximity gaps);Theorem 1.2(Proximity gaps for Reed-Solomon codes);Theorem 1.4(Correlated agreement over affine lines),Theorem 1.5(Correlated agreement over low-degree parameterised curves), andTheorem 1.6(Correlated agreement over affine spaces).In
DivergenceOfSets.lean:Corollary 1.3(Concentration bounds);Additionally, there are linter error fixes.
Note
Introduce proximity gap framework with RS theorems (statements), divergence of sets, and supporting affine/curve, Reed–Solomon, and probability notation utilities, plus minor refactors/notation tweaks.
ProximityGapframework:proximityMeasure,proximityGap,correlatedAgreement(moved/namespaced),generalProximityGap, anderrorBoundfor RS.proximity_gap_RSCodes,correlatedAgreement_lines,correlatedAgreement_affine_curves,correlatedAgreement_affine_spaces.possibleDeltasanddivergence(nowℚ≥0); addconcentration_boundscorollary statement.neqCols, row/col spans/ranks, submatrix extractors) and rank lemmas (stated).parametrisedCurveand finite variants).ReedSolomonCode:RScodeSet,toFinset,sqrtRate.Pr_{...}[...]macro expansion and examples.Code.minDist/RScodeSet; minor doc cleanups.ρnotation scoped macro forLinearCode.rate.Combine.combine_theorem,blueprint/lean_decls) to new namespaces/defs.Written by Cursor Bugbot for commit ab20fe0. This will update automatically on new commits. Configure here.