Guruswami-Sudan existence and divisibility

[ster-oc]

In this PR with @Aristotle-Harmonic, we prove the existence of a solution to the Guruswami-Sudan system and the fact that one such biviariate polynomial has divisibility property.

Depends on : #299
Closes : #221 #224

[github-actions]

🤖 Gemini PR Summary

This Pull Request formalizes the existence proofs and divisibility properties for the Guruswami-Sudan (GS) list decoding algorithm within ArkLib, bridging abstract coding theory with concrete bivariate polynomial requirements for Reed-Solomon decoding.

Mathematical Formalization

• Existence Proofs: Establishes that for specific Reed-Solomon parameters and agreement requirements, a non-zero interpolation polynomial exists satisfying all multiplicity constraints.
• Divisibility Lemma: Proves that for any valid codeword with sufficient agreement, the corresponding univariate polynomial is a root of the interpolated bivariate polynomial.
• Proximity Gap Completion: Replaces placeholders in the BCIKS20 module with rigorous proofs, solidifying the link between the GS system and proximity gap analysis.

Polynomial Theory Enhancements

• Root Multiplicity (Order of Vanishing): Redefines bivariate root multiplicity using a minimum-degree calculation to accurately represent the "order of vanishing" at a point.
• Shift Operator: Introduces a shift definition and associated lemmas to handle polynomial translations and facilitate analysis at specific coordinates.

Architectural Improvements

• Module Decoupling: Reorganizes the GS implementation into a dedicated GuruswamiSudan module, separating high-level algorithm logic from lower-level proximity gap proofs.
• Namespace Integration: Exports core GS definitions and theorems through the main ArkLib entry point for use in future decoding implementations.

Dependencies & Closures

• Depends on: Guruswami-Sudan existence #299
• Closes: Proof obligation for guruswami_sudan_for_proximity_gap_existence in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean #221, Proof obligation for guruswami_sudan_for_proximity_gap_property in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean #224

---

Analysis of Changes

Metric	Count
📝 Files Changed	5
✅ Lines Added	953
❌ Lines Removed	83

---

Lean Declarations

✏️ **Removed:** 2 declaration(s)

• lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F} : in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

✏️ **Added:** 43 declaration(s)

• lemma natWeightedDegree_add_le (p q : F[X][Y]) (u v : ℕ) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma eval_shifted_eq_shifted_eval (Q : F[X][Y]) (P : F[X]) (x y : F) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma interpolate_eq_of_degree_lt (q : F[X]) (hq : q.natDegree < n) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma linearIndependent_monomials : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma polySol_weightedDegree_le : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma shift_eq_zero_iff {F : Type} [Field F] (f : F[X][Y]) (x y : F) : shift f x y = 0 ↔ f = 0 in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma roots_le_degree_of_deg_lt_roots (R : F[X]) (m : ℕ) (A : Finset (Fin n)) in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma sufficient_multiplicity_bound {dist : ℕ} in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• theorem dvd_property [DecidableEq F] (hk : k + 1 ≤ n) (hm : 1 ≤ m) (p : code ωs k) in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma natWeightedDegree_monomial (i j u v : ℕ) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma numVars_lower_bound_tight {D : ℕ} (hk : 1 < k) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma polySol_multiplicity [DecidableEq F] (i : Fin n) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma coeff_linearCombination_monomial (c : ℕ × ℕ →₀ F) (i j : ℕ) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• theorem proximity_gap_existence (k n : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) (hm : 1 ≤ m) : in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• def weigthBoundIndices (k D : ℕ) : Finset (ℕ × ℕ) in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma polySol_ne_zero : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• theorem proximity_gap_divisibility (hk : k + 1 ≤ n) (hm : 1 ≤ m) (p : code ωs k) in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma exists_nonzero_solution (k n m : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma rootMultiplicity_le_of_coeff_ne_zero [DecidableEq F] {Q : F[X][Y]} {x y : F} {s t : ℕ} in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma numVars_gt_numConstraints (k n m : ℕ) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma polySol_roots {ωs : Fin n ↪ F} {f : Fin n → F} (hm : 1 ≤ m) (i : Fin n) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• def numVars (k D : ℕ) : ℕ in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• def constraintIndices (m : ℕ) : Finset (ℕ × ℕ) in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma eval_eq_zero_of_constraint_zero {f : F[X][Y]} {x y : F} {m : ℕ} (hm : 1 ≤ m) in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma rootMultiplicity_ge_of_shift_zero [DecidableEq F] {f : F[X][Y]} {x y : F} in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma degree_eval_le_weightedDegree (Q : F[X][Y]) (P : F[X]) (k : ℕ) (hP : P.natDegree ≤ k - 1) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma proximity_gap_degree_bound_sq_gt (hn : n ≠ 0) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma numVars_eq_sq {k D : ℕ} (hk : k ≤ 1) : numVars k D = (D + 1) ^ 2 in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma natWeightedDegree_monomial_eq (i j u v : ℕ) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma card_constraintIndices (m : ℕ) : (constraintIndices m).card = m * (m + 1) / 2 in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma card_weigthBoundIndices_eq_sum (D : ℕ) (hk : 1 < k) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma list_min_le_of_mem {l : List ℕ} {a m : ℕ} (h_min : l.min? = some m) (h_mem : a ∈ l) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma dvd_eval_of_rootMultiplicity_zero (Q : F[X][Y]) (P : F[X]) (m : ℕ) in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma codewordToPoly_degree_le (hk : k + 1 ≤ n) (p : code ωs k) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• def HasOrderAt (Q : F[X][Y]) (x y : F) (m : ℕ) : Prop in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• def numConstraints (n m : ℕ) : ℕ in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma natWeightedDegree_smul_le {F : Type} [Semiring F] (a : F) (p : F[X][Y]) (u v : ℕ) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma natWeightedDegree_sum_le {ι : Type*} (s : Finset ι) (f : ι → F[X][Y]) (u v : ℕ) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma numVars_eq_of_gt_one {D : ℕ} (hk : 1 < k) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma natWeightedDegree_coeffsToPoly_le (k D : ℕ) (c : (weigthBoundIndices k D) → F) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma numVars_gt_numConstraints_of_gt_one (hn : n ≠ 0) (hk : 1 < k) (hm : 1 ≤ m) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
• lemma weightedDegree_ne_none {F : Type} [Semiring F] (f : F[X][Y]) (u v : ℕ) : in ArkLib/Data/Polynomial/Bivariate.lean
• lemma orderAt_eval_ge (Q : F[X][Y]) (P : F[X]) (x : F) (m : ℕ) in ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean

✏️ **Affected:** 1 declaration(s) (line number changed)

• lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L176 to L176

---

sorry Tracking

✅ **Removed:** 4 `sorry`(s)

• lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F} : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F} : in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean

---

🎨 **Style Guide Adherence**

Based on the provided style guide, the following violations were identified:

ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean

• Line 1: Missing module docstring (violates "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references").
• Line 1: Missing References section (violates "Each file that cites papers should have a ## References section in its docstring header").
• Line 19: Variable F violates naming convention "α, β, γ, ... : Generic types".
• Line 24: Docstring math notation does not use LaTeX (violates "Use LaTeX for math: $ f(x) = y $").
• Line 25: proximity_gap_degree_bound violates naming convention "Functions and Terms: lowerCamelCase".
• Line 30: Docstring math notation does not use LaTeX (violates "Use LaTeX for math: $ f(x) = y $").
• Line 31: proximity_gap_johnson violates naming convention "Functions and Terms: lowerCamelCase".
• Line 38: Section numVars missing sectioning comment (violates "Use /-! ### Title -/ to structure large files into sections").
• Line 41: weigthBoundIndices missing declaration docstring (violates "Every definition and major theorem should have a docstring").
• Line 41: weigthBoundIndices is misspelled (violates "Use American English for declaration names").
• Line 41: weigthBoundIndices violates naming convention "Functions and Terms: lowerCamelCase".
• Line 45: numVars missing declaration docstring (violates "Every definition and major theorem should have a docstring").
• Line 47: card_weigthBoundIndices_eq_sum is misspelled (violates "Use American English for declaration names").
• Line 50: Indentation of 4 spaces violates "Use 2 spaces for indentation".
• Line 80: Lemma name numVars_eq_of_gt_one violates "Avoid ≥ (ge) and > (gt) in theorem statements".
• Line 113: Section numConstraints missing sectioning comment.
• Line 115: constraintIndices missing declaration docstring.
• Line 120: numConstraints missing declaration docstring.
• Line 138: Section numVars_gt_numConstraints missing sectioning comment.
• Line 144: Lemma name proximity_gap_degree_bound_sq_gt violates "Avoid ≥ (ge) and > (gt) in theorem statements".
• Line 145: Theorem statement uses > instead of < (violates "standardize on ≤ (le) and < (lt). Avoid ≥ (ge) and > (gt)").
• Line 161: Lemma name numVars_gt_numConstraints_of_gt_one violates "Avoid ≥ (ge) and > (gt) in theorem statements".
• Line 162: Theorem statement uses > instead of <.
• Line 183: Lemma name numVars_gt_numConstraints violates "Avoid ≥ (ge) and > (gt) in theorem statements".
• Line 184: Theorem statement uses > instead of <.
• Line 212: Section solution missing sectioning comment.
• Line 214: coeffsToPoly missing declaration docstring.
• Line 221: evalConstraint missing declaration docstring.
• Line 227: constraintMap missing declaration docstring.
• Line 235: Use of rfl violates "Use manual dot notation for logical connectives and equality (e.g., ... Eq.refl)".
• Line 257: polySol missing declaration docstring.
• Line 262: Section neZero missing sectioning comment.
• Line 297: Section weightedDegree missing sectioning comment.
• Line 389: Section roots missing sectioning comment.
• Line 412: Section multiplicity missing sectioning comment.
• Line 432: Use of rfl violates "Use manual dot notation for logical connectives and equality (e.g., ... Eq.refl)".
• Line 453: Use of rfl violates "Use manual dot notation for logical connectives and equality (e.g., ... Eq.refl)".
• Line 538: Section divisibility missing sectioning comment.
• Line 583: Section multiplicity missing sectioning comment.
• Line 585: HasOrderAt violates naming convention "Functions and Terms: lowerCamelCase" (Prop-valued term is not a class).
• Line 585: HasOrderAt missing declaration docstring.
• Line 608: Section roots_le_degree_of_deg_lt_roots missing sectioning comment.
• Line 626: Section interpolate_eq_of_degree_lt missing sectioning comment.
• Line 644: Section codewordToPoly_degree_le missing sectioning comment.
• Line 659: Section sufficient_multiplicity_bound missing sectioning comment.
• Line 674: Section dvd_property missing sectioning comment.

ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

• Line 12: Missing module docstring.
• Line 43: k-1 violates "Put spaces on both sides of ... infix operators".
• Line 58: decoder missing declaration docstring.

ArkLib/Data/Polynomial/Bivariate.lean

• Line 472: shift missing declaration docstring.

---

📄 **Per-File Summaries**

• ArkLib.lean: This update integrates basic definitions and theorems related to the Guruswami-Sudan algorithm into the main ArkLib library.
• ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean: Refactor the Guruswami-Sudan implementation by moving core definitions to a dedicated module and updating the existence and divisibility theorems for the proximity gap.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean: This change completes the proofs of the Guruswami-Sudan existence and property lemmas for proximity gaps by replacing sorry placeholders with applications of established coding theory results and refining lemma hypotheses.
• ArkLib/Data/Polynomial/Bivariate.lean: This update redefines bivariate root multiplicity to correctly represent the order of vanishing by switching to a minimum-degree calculation and introduces the shift definition along with supporting lemmas.
• ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean: This file formalizes the core components of the Guruswami-Sudan list decoding algorithm for Reed-Solomon codes, introducing new definitions for decoding parameters and the interpolation polynomial along with theorems establishing its existence, multiplicity properties, and divisibility by valid codewords.

---

Last updated: 2026-02-27 21:28 UTC.

[ster-oc]

I see a problem with the definition of proximity_gap_johnson.
In particular, I believe that in Lemma 5.3 of [BCIKS20] the second part of the statement really asks to bound the Hamming distance with the real number δ₀(ρ, m) and not with its floor as per the definition in GuruswamiSudan.lean.

The relative radius δ₀(ρ, m) is always <1, which means that its floor is always 0.
This means that in [BCIKS20] Δ is the relative Hamming distance and not the absolute one

[alexanderlhicks]

Hello! Thanks for the PR and sorry for the delay in getting to this. I'll be merging the 4.26 PR soon, which might break a few things, and get back to all the other PRs including this one.

[ster-oc]

I realized that the definition of rootMultiplicity₀ was not correct, with essentially a List.max? to be replaced by a List.min?.
(An example is the polynomial p(x) := X + Y² which has a zero of order 1 at (0,0), but List.max would give order 2 because of the monomial Y²)

This fix together with the correct hypothesis on the relative Hamming distance should now be fine for everything to go through.

There is still a sorry left because some code broke after changing rootMultiplicity.

[ster-oc]

Guruswami-Sudan is now sorry free!

I see you opened PR #306, be mindful that I put some of the new definitions in Bivariate.lean✌️

[alexanderlhicks]

/review

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

Internal:
ArkLib/Data/CodingTheory/
ArkLib/Data/Polynomial

Comments:
Please review for correctness with respect to ArkLib internals and the external reference papers.

[github-actions]

🤖 AI Review (with external context)

🤖 AI Review

Overall Summary:
The pull request contains critical logical errors that render parts of the formalization incorrect, specifically within Bivariate.lean (where the shift function is defined incorrectly and a lemma fails for the zero polynomial) and GuruswamiSudan.lean (where theorems are false for $k=1$). Additionally, there is a pervasive inconsistency regarding whether the parameter k represents the code dimension or maximum degree, which currently leads to suboptimal bounds and documentation conflicts. I recommend blocking the merge until these logic errors are fixed and the parameter semantics are standardized across the library.

---

📄 **Review for `ArkLib.lean`**

Review of ArkLib.lean

Verdict: Correct

Implementation Analysis

The file ArkLib.lean serves as the top-level entry point for the library, aggregating various modules via import statements. The provided diff adds a single line:

import ArkLib.Data.CodingTheory.GuruswamiSudan.Basic

This change exports the definitions and theorems contained within the GuruswamiSudan.Basic module to users importing ArkLib. This is standard practice for library organization in Lean projects. Given the global context involving updates to Reed-Solomon proximity gaps and Guruswami-Sudan decoding, exposing the basic definitions of this theory is appropriate.

Misformalization Check

As this file contains only import statements:

• There are no logical definitions or theorems to check for correctness errors (Off-by-One, recursion, etc.).
• Since the code compiles, the module path is valid and does not introduce circular dependencies.

The change correctly updates the library interface.

📄 **Review for `ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean`**

Review of ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean

Verdict: Correct with Minor Issues

The formalization correctly implements the algebraic core of the Guruswami-Sudan list decoding algorithm, specifically the interpolation step and the divisibility argument (Theorem dvd_property). The logic aligns with the standard proofs in the literature (and the referenced paper [BCIKS20]), ensuring that if a nonzero polynomial $Q$ with sufficient root multiplicity is found, any codeword $P$ sufficiently close to the received word $f$ will satisfy $Y - P(X) \mid Q(X, Y)$.

Findings:

1. Parameter Inconsistency (Minor):

   • Observation: There is a discrepancy between the documentation/definitions and the usage of the parameter k.
     • The top-level comment states: variable {k : ℕ} -- Let k + 1 be the dimension of the code.
     • The definition proximity_gap_degree_bound calculates rho := (k + 1 : ℚ) / n.
     • However, the code usage consistently treats k as the dimension (max degree k-1). For example:
       • weigthBoundIndices uses weight (1, k - 1).
       • codewordToPoly_degree_le asserts natDegree ≤ k - 1 for p : code ωs k.
   • Impact: If k is indeed the dimension (as implied by code ωs k), then rho should technically be k / n (or the theorem statement should clarify parameters). Calculating rho as (k+1)/n results in a slightly larger rate, which leads to a smaller Johnson radius proximity_gap_johnson. Using a smaller radius makes the theorem condition h_dist stricter than necessary (requires closer proximity). Thus, the theorem remains true (the condition implies the result), but it is slightly weaker than the optimal statement for a code of dimension k.
   • Recommendation: Clarify the definition of k. If code ωs k represents a code of dimension k, update the comment and consider changing rho to k / n or updating proximity_gap_degree_bound logic to match the dimension k exactly.

2. Definition of weigthBoundIndices (Minor):

   • In weigthBoundIndices, the weight constraint is x.1 + (k - 1) * x.2 ≤ D. This is consistent with k being the dimension (max degree k-1). If k were the max degree, this would likely be x.1 + k * x.2. This confirms the inconsistency noted above but is internally consistent with the proofs in the file.

General Assessment:
The file is well-structured. The proofs for variable counting, existence of the solution (exists_nonzero_solution), and the algebraic divisibility argument (dvd_property) are rigorous. The handling of Hasse derivatives and root multiplicities via evalConstraint and rootMultiplicity_le_of_coeff_ne_zero is correct. The off-by-one checks in range calculations appear correct. The formalization is safe to merge, subject to clarifying the parameter k.

📄 **Review for `ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean`**

Review of ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

Verdict: Incorrect

Critical Issues:

1. Missing Hypothesis / Incorrect Degree Weight for k=1:
   • Observation: The structure Conditions defines the degree constraint as weightedDegree Q 1 (k - 1) ≤ D. If k represents the dimension of the code (as implied by the usage p : code ωs k), then k=1 corresponds to a code of constant polynomials. In this case, k - 1 = 0.
   • Impact: A weight of 0 for $Y$ means weightedDegree imposes no constraint on the degree of $Q$ with respect to $Y$. For example, $Q(X, Y) = Y^{100}$ would have weighted degree 0 (assuming $X$ degree is 0) and satisfy the bound $D$.
   • Consequence: The theorem proximity_gap_divisibility becomes false for k=1. One can construct a $Q$ (e.g., with very high $Y$-degree) that satisfies the Conditions but is not divisible by $Y - P(X)$ for the codeword $P$. The Guruswami-Sudan algorithm and the reference paper [BCI+20] typically assume the degree parameter $k_{paper}$ (where dimension is $k_{paper}+1$) is $\ge 1$, i.e., dimension $\ge 2$.
   • Correction: You must either require 2 ≤ k in the theorems proximity_gap_existence and proximity_gap_divisibility, or adjust the weight definition to handle k=1 (though the latter might not align with the paper's specific bounds which divide by $k$).

Major Issues:

1. Documentation Contradiction:
   • Observation: The comment line 17 states: --Let k + 1 be the **dimension** of the code. However, the code uses variable {k : ℕ} and p : code ωs k. In ArkLib (and standard mathlib patterns), code ωs k typically creates a code of dimension k.
   • Evidence: The use of weightedDegree ... (k-1) is consistent with k being the dimension (so polynomials have degree $\le k-1$, matching the weight). If k+1 were the dimension, the max degree would be k, and the weight should be k.
   • Correction: Update the comment to reflect that k is the dimension, e.g., --Let k be the **dimension** of the code.

Minor Issues:

1. Variable Shadowing:
   • In proximity_gap_existence, the arguments (k n : ℕ) shadow the section variables {k : ℕ} and {n : ℕ}. While valid Lean, this can be confusing, especially since ωs depends on the section's n. It is cleaner to use the section variables implicitly or explicitly {k n} without redeclaring them as explicit arguments (k n : ℕ).

Corrected Code Snippet (Suggestion):

-- ... inside namespace GuruswamiSudan

/-- ... -/
-- Ensure k matches the intended semantics (Dimension).
-- Adjust Condition to handle k=1 or enforce k \ge 2 in theorems.
-- Assuming enforcing k \ge 2 is the intended fix based on the paper's assumptions:

theorem proximity_gap_divisibility (hk : 2 ≤ k) (hkn : k + 1 ≤ n) (hm : 1 ≤ m) (p : code ωs k)
    {Q : F[X][Y]} (hQ : Conditions k m (proximity_gap_degree_bound k n m) ωs f Q)
    (h_dist : (hammingDist f (fun i ↦ (codewordToPoly p).eval (ωs i)) : ℝ) / n <
      proximity_gap_johnson k n m) :
    X - C (codewordToPoly p) ∣ Q :=
  -- ... implementation

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean`**

Analysis of Implementation:

The changes in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean consist entirely of renaming the identifier Condition to Conditions.

1. Hunk 1: In guruswami_sudan_for_proximity_gap_existence, the return type is changed from ∃ Q, Condition ... to ∃ Q, Conditions .... This reflects a renaming of the predicate checking the Guruswami-Sudan conditions (likely degree bounds and multiplicity constraints). The parameters (k + 1) m ... are preserved correctly.
2. Hunk 2: In guruswami_sudan_for_proximity_gap_property, the hypothesis cond has its type updated from Condition ... to Conditions .... The arguments match the previous version.

Conformance with Specification:
The rename from singular Condition to plural Conditions is semantically appropriate for the Guruswami-Sudan algorithm, which imposes multiple constraints (weighted degree bound on $Q$ and root multiplicity at interpolation points). This aligns with the mathematical description in the referenced paper [BCI+20] (Section 5.1).

Check for Misformalization:

• Logic: The change is a syntactic rename. Given that the code compiles, the definition Conditions exists and is compatible with the usage.
• Off-by-One/Indices: The arguments (k + 1) and m are preserved. The use of k+1 (presumably dimension) vs k (degree bound) was pre-existing and is not altered by this diff.
• Types: The usage of Conditions as a Prop (implied by ∃ and hypothesis usage) is correct.

Observation (Contextual):
In guruswami_sudan_for_proximity_gap_property, the variable p has type ReedSolomon.code ωs n. Typically, an RS code is parameterized by dimension $k$ (or $k+1$). If n here represents the block length, p would be a member of the full space $F^n$, or the code of dimension $n$. For the Guruswami-Sudan property to hold (specifically, that $Y - p(X)$ divides $Q(X, Y)$), $p$ usually must satisfy the degree bound $k$ used to construct $Q$. If ReedSolomon.code ωs n implies degree $<n$ rather than $< k+1$, the theorem might be stated too weakly or incorrectly in the context. However, this is outside the scope of the provided diff (it is context), and the rename itself is correct.

Verdict:
The formalization changes in this diff are correct.

Feedback:

1. Rename Verification: The renaming of Condition to Conditions is correct and improves readability, aligning with the multiple constraints involved in the Guruswami-Sudan algorithm.
2. Contextual Note (Minor): Please verify the type of p in guruswami_sudan_for_proximity_gap_property. It is currently ReedSolomon.code ωs n. Ensure this restricts p to the dimension k+1 (or degree k) assumed by the Conditions on Q. If n is the block length and $n > k+1$, p might have too high a degree for the conclusion to hold.

📄 **Review for `ArkLib/Data/List/Lemmas.lean`**

Based on the review of the provided diff in ArkLib/Data/List/Lemmas.lean against the general requirements of Lean formalization and the provided context:

Verdict:
The formalization is Correct.

Analysis:

1. Logic and Correctness: The lemma min?_filterMap_ge asserts that if every value k produced by applying f to elements of list l satisfies m ≤ k, then the minimum of the resulting filtered list (if it exists) must also be at least m. This is logically sound. If (l.filterMap f).min? = some k, then k must be an element of the filtered list. By the hypothesis h, any element in that list satisfies the lower bound m. Thus m ≤ k.
2. Proof Script: The proof uses List.min?_eq_some_iff to expose the fact that k is a member of the list, and then uses aesop to perform the necessary logical deduction involving List.mem_filterMap and the hypothesis h. This is a standard and robust proof technique in Lean 4.
3. Context: While the external references discuss advanced coding theory, this file contains utility lemmas for lists. This lemma likely supports operations involving degrees or weights (natural numbers) of elements in a list, fitting the broader context.

Feedback/Minor Suggestions:

• Universe Polymorphism: The type parameter α is declared as Type (which is Type 0). While ℕ is fixed in Type 0, the input list l could theoretically contain elements from a higher universe (e.g., Type u). The existing code in the file uses Type _ (universe polymorphic). It would be more consistent and general to use {α : Type*} or {α : Type u} instead of {α : Type}, though this does not affect the correctness of the lemma as stated for Type 0 types.

Diff Review:

• The added lemma min?_filterMap_ge is correctly defined and proved.
• No off-by-one errors or misuse of Prop/Type were found.
• Assumptions are appropriate for the conclusion.

📄 **Review for `ArkLib/Data/Polynomial/Bivariate.lean`**

Review of ArkLib/Data/Polynomial/Bivariate.lean

The changes in this file introduce two critical issues regarding formalization correctness, despite valid refactoring and corrections to rootMultiplicity.

1. Incorrect Lemma: weightedDegree_ne_none

The new lemma weightedDegree_ne_none claims that weightedDegree f u v is never none for any bivariate polynomial f.

lemma weightedDegree_ne_none {F : Type} [Semiring F] (f : F[X][Y]) (u v : ℕ) :
    weightedDegree f u v ≠ none := by
  unfold weightedDegree; aesop

• Issue: This lemma is false for the zero polynomial (f = 0). In standard libraries and the context of this file (see rootMultiplicity₀ handling none), weightedDegree 0 is defined as none (representing $-\infty$).
• Proof of falsity: If f = 0, weightedDegree 0 u v = none. The lemma asserts none ≠ none.
• Correction: The lemma requires the hypothesis f ≠ 0.

lemma weightedDegree_ne_none {F : Type} [Semiring F] (f : F[X][Y]) (u v : ℕ) (hf : f ≠ 0) :
    weightedDegree f u v ≠ none := ...

2. Incorrect Definition: shift

The function shift is intended to map $f(X, Y)$ to $f(X+x, Y+y)$.

noncomputable def shift {F : Type} [Field F] (f : F[X][Y]) (x y : F) : F[X][Y] :=
  (f.comp (X + C (C y))).map ((X + C x).compRingHom)

• Issue: The expression f.comp (X + C (C y)) substitutes the outer variable Y with X + y. This transforms $f(X, Y)$ into $f(X, X+y)$ (before the X-shift), which is not a coordinate translation but a substitution onto a line.
• Context: In rootMultiplicity (lines 150-151), the correct variable Y is used: f.comp (Y + C (C y)). The usage of X in shift appears to be a typo confusing the inner variable X with the outer variable Y.
• Correction: Use Y instead of X in the composition.

noncomputable def shift {F : Type} [Field F] (f : F[X][Y]) (x y : F) : F[X][Y] :=
  (f.comp (Y + C (C y))).map ((X + C x).compRingHom)

3. Other Changes

• rootMultiplicity fix: The logic change from List.max? to List.min? correctly changes the calculation from computing the degree to computing the multiplicity (order of vanishing). This fixes a prior misformalization.
• Formatting: Minor formatting changes in monomialY, monomialXY, and degreesY_nonempty are correct.

Verdict:
The formalization contains Critical errors in the new additions (weightedDegree_ne_none and shift). The logic fix in rootMultiplicity is correct.

[eliasjudin]

Opened a follow-up integration PR against the head repository branch to make merge/cherry-pick easier: ster-oc#1