Proximity Gaps + Coding Theory Cleanup and Refactor

[katyhr]

Refactor of Proximity Gap definitions and cleanup of Coding Theory

[github-actions]

🤖 Gemini PR Summary

Refactors Proximity Gap definitions and standardizes Coding Theory modules to enhance modularity, naming consistency, and mathematical generalization.

Coding Theory & Namespace Refactoring

• Namespace Standardization: Renamed ReedSolomonCode to ReedSolomon and updated all references across the Binius proof system and Proximity Gap modules (DG25, AHIV22, BCIKS20).
• Explicit Scoping: Removed the ReedSolomon namespace from the global scope in Prelude.lean. Primitives now require explicit qualification (e.g., ReedSolomon.code), preventing namespace pollution in complex proofs.

Mathematical Formalization

• Vandermonde Matrices: Moved matrix logic to ArkLib/Data/Matrix/Vandermonde.lean. Introduced definitions for non-square Vandermonde matrices and established formal links between their rank and polynomial evaluation properties.
• Trivariate Polynomials: Added a new interface for trivariate polynomials, including evaluation homomorphisms that map to bivariate forms and rational function domains.
• Proximity Gap Generalization: Generalized the AHIV22 combinatorial proximity gap lemma for affine lines by removing the DecidableEq requirement, expanding its applicability in diverse algebraic contexts.

Modularity and Code Health

• Decoupling: Extracted matrix logic from ReedSolomon.lean and removed the Trivariate namespace from ProximityGap/Basic.lean to improve separation of concerns.
• Import Optimization: Streamlined InterleavedCode.lean and RationalFunctions.lean by removing redundant imports and unused typeclass constraints.
• Noncomputability Scoping: Narrowed the noncomputable modifier in the Interleaved Code module from the file level to specific instances, clarifying where classical logic is required.
• Architectural Foundation: Decoupling Vandermonde logic from Reed-Solomon codes ensures a modular foundation for future zero-knowledge proof constructions and minimizes naming collisions between different code types.

---

Analysis of Changes

Metric	Count
📝 Files Changed	12
✅ Lines Added	359
❌ Lines Removed	423

---

Lean Declarations

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

• lemma rank_nonsquare_rows_eq_min (inj : Function.Injective α) : in ArkLib/Data/CodingTheory/ReedSolomon.lean
• lemma rank_nonsquare_eq_deg_of_ι_le (inj : Function.Injective α) (h : m ≤ n) : in ArkLib/Data/CodingTheory/ReedSolomon.lean
• def nonsquareTranspose [Field F] (ι' : ℕ) (α : ι ↪ F) : Matrix (Fin ι') ι F in ArkLib/Data/CodingTheory/ReedSolomon.lean
• def finCarrier {ι : Type} [Fintype ι] in ArkLib/Data/CodingTheory/ReedSolomon.lean
• instance instFintypeInterleavedModuleCode [Fintype A] : Fintype (MC ^⋈ κ) in ArkLib/Data/CodingTheory/InterleavedCode.lean
• lemma subUpFull_of_vandermonde_is_vandermonde (h : n ≤ m) : in ArkLib/Data/CodingTheory/ReedSolomon.lean
• theorem mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials in ArkLib/Data/CodingTheory/ReedSolomon.lean
• lemma subLeftFull_of_vandermonde_is_vandermonde (h : m ≤ n) : in ArkLib/Data/CodingTheory/ReedSolomon.lean
• instance interleavedCodeSet_fintype {A : Type*} {κ ι : Type*} in ArkLib/Data/CodingTheory/InterleavedCode.lean
• def nonsquare [Semiring F] (ι' : ℕ) (α : ι → F) : Matrix ι (Fin ι') F in ArkLib/Data/CodingTheory/ReedSolomon.lean
• lemma nonsquare_mulVecLin [CommSemiring F] {ι' : ℕ} {α₁ : ι ↪ F} {α₂ : Fin ι' → F} {i : ι} : in ArkLib/Data/CodingTheory/ReedSolomon.lean
• abbrev sqrtRate [Fintype ι] (deg : ℕ) (domain : ι ↪ F) : ℝ≥0 in ArkLib/Data/CodingTheory/ReedSolomon.lean
• def toFinset (domain : ι ↪ F) (deg : ℕ) : Finset (ι → F) in ArkLib/Data/CodingTheory/ReedSolomon.lean
• lemma rank_nonsquare_eq_deg_of_deg_le (inj : Function.Injective α) (h : n ≤ m) : in ArkLib/Data/CodingTheory/ReedSolomon.lean

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

• lemma rank_nonsquare_eq_deg_of_ι_le (inj : Function.Injective α) (h : m ≤ n) : in ArkLib/Data/Matrix/Vandermonde.lean
• theorem mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials in ArkLib/Data/Matrix/Vandermonde.lean
• def nonsquare [Semiring F] (ι' : ℕ) (α : ι → F) : Matrix ι (Fin ι') F in ArkLib/Data/Matrix/Vandermonde.lean
• lemma subLeftFull_of_vandermonde_is_vandermonde (h : m ≤ n) : in ArkLib/Data/Matrix/Vandermonde.lean
• def nonsquareTranspose [Field F] (ι' : ℕ) (α : ι ↪ F) : Matrix (Fin ι') ι F in ArkLib/Data/Matrix/Vandermonde.lean
• lemma rank_nonsquare_eq_deg_of_deg_le (inj : Function.Injective α) (h : n ≤ m) : in ArkLib/Data/Matrix/Vandermonde.lean
• lemma nonsquare_mulVecLin [CommSemiring F] {ι' : ℕ} {α₁ : ι ↪ F} {α₂ : Fin ι' → F} {i : ι} : in ArkLib/Data/Matrix/Vandermonde.lean
• lemma rank_nonsquare_rows_eq_min (inj : Function.Injective α) : in ArkLib/Data/Matrix/Vandermonde.lean
• lemma subUpFull_of_vandermonde_is_vandermonde (h : n ≤ m) : in ArkLib/Data/Matrix/Vandermonde.lean

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

• def δ_ε_multilinearCorrelatedAgreement [CommRing F] [Module F A] in ArkLib/Data/CodingTheory/ProximityGap/Basic.lean moved from L141 to L119
• lemma approximate_solution_is_exact_solution_coeffs (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L413 to L360
• lemma exists_factors_with_large_common_root_set (δ : ℚ) (x₀ : F) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L366 to L329
• lemma irreducible_H (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) : Irreducible (H k δ x₀ h_gs) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L400 to L354
• lemma irreducible_factorization_of_gs_solution {k : ℕ} (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L342 to L306
• lemma exists_a_set_and_a_matching_polynomial (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L317 to L286
• lemma modified_guruswami_has_a_solution {m n k : ℕ} {ωs : Fin n ↪ F} {u₀ u₁ : Fin n → F} : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L259 to L243

---

sorry Tracking

✏️ **Affected:** 5 `sorry`(s) (line number changed)

• lemma exists_factors_with_large_common_root_set (δ : ℚ) (x₀ : F) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L378 to L340
• theorem correlatedAgreement_affine_spaces {k : ℕ} [NeZero k] {u : Fin (k + 1) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L137 to L136
• lemma exists_a_set_and_a_matching_polynomial (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L324 to L292
• theorem correlatedAgreement_affine_curves [DecidableEq ι] {k : ℕ} {u : Fin k → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L120 to L119
• lemma modified_guruswami_has_a_solution {m n k : ℕ} {ωs : Fin n ↪ F} {u₀ u₁ : Fin n → F} : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L264 to L245

---

🎨 **Style Guide Adherence**

The following lines violate the provided style guide:

• ArkLib/Data/CodingTheory/InterleavedCode.lean

  • Line 656: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 656: "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering." (Uses ≥).
  • Line 774: "Every definition and major theorem should have a docstring." (Missing docstring for relHammingBallInterleavedCode).

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean

  • Line 60: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." and "Theorems and Proofs: snake_case." (Uses RSCodes, should be rs_codes).
  • Line 70: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 74: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 111: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 133: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 143: "Functions and Terms: lowerCamelCase." (Uses D_X).
  • Line 153: "Functions and Terms: lowerCamelCase." (Uses proximity_gap_degree_bound).
  • Line 161: "Functions and Terms: lowerCamelCase." (Uses proximity_gap_johnson).
  • Line 168: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 206: "Functions and Terms: lowerCamelCase." (Uses D_Y).
  • Line 206: "Every definition and major theorem should have a docstring." (Uses -- instead of /-- ... -/).
  • Line 209: "Functions and Terms: lowerCamelCase." (Uses D_YZ).
  • Line 209: "Every definition and major theorem should have a docstring." (Uses -- instead of /-- ... -/).
  • Line 255: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 274: "Functions and Terms: lowerCamelCase." (Uses coeffs_of_close_proximity).
  • Line 310: "Functions and Terms: lowerCamelCase." (Uses matching_set).
  • Line 313: "Every definition and major theorem should have a docstring." (Missing docstring for matching_set_is_a_sub_of_coeffs_of_close_proximity).
  • Line 335: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 344: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 349: "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering." (Uses ≥).
  • Line 350: "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering." (Uses >).
  • Line 354: "Functions and Terms: lowerCamelCase." (Uses R).
  • Line 358: "Functions and Terms: lowerCamelCase." (Uses H).
  • Line 372: "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering." (Uses ≥).
  • Line 532: "Every definition and major theorem should have a docstring." (Missing docstring for exists_polynomial_on_curve_of_large_agreement).
  • Line 549: "Every definition and major theorem should have a docstring." (Missing docstring for large_agreement_set_on_curve_implies_correlated_agreement').
  • Line 605: "Every definition and major theorem should have a docstring." (Missing docstring for weightedCorrelatedAgreement).
  • Line 621: "Every definition and major theorem should have a docstring." (Missing docstring for weighted_correlated_agreement_for_parameterized_curves).
  • Line 657: "Every definition and major theorem should have a docstring." (Missing docstring for weighted_correlated_agreement_for_parameterized_curves').
  • Line 685: "Every definition and major theorem should have a docstring." (Missing docstring for weighted_correlated_agreement_over_affine_spaces).
  • Line 724: "Every definition and major theorem should have a docstring." (Missing docstring for weighted_correlated_agreement_over_affine_spaces').

• ArkLib/Data/CodingTheory/ProximityGap/Basic.lean

  • Line 139: "Every definition and major theorem should have a docstring." (Missing docstring for δ_ε_multilinearCorrelatedAgreement).
  • Line 151: "Use 2 spaces for indentation." (Indented 4 spaces).
  • Line 162: "Use 2 spaces for indentation." (Indented 4 spaces).

• ArkLib/Data/CodingTheory/ReedSolomon.lean

  • Line 84: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Uses RScodeSet, should be rsCodeSet).
  • Line 288: "Theorems and Proofs: snake_case." (Uses minDist).
  • Line 323: "Theorems and Proofs: snake_case." (Uses minDist').
  • Line 350: "Theorems and Proofs: snake_case." and "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Uses uniqueDecodingRadius_RS_eq', should be unique_decoding_radius_rs_eq').
  • Line 365: "Theorems and Proofs: snake_case." and "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Uses relativeUniqueDecodingRadius_RS_eq', should be relative_unique_decoding_radius_rs_eq').
  • Line 478: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Uses decodeLT, should be decodeLt).
  • Line 516: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Uses mVdecode, should be mvDecode).

• ArkLib/Data/Matrix/Vandermonde.lean

  • Line 80: "Theorems and Proofs: snake_case." (Uses mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials, which contains camelCase).

• ArkLib/Data/Polynomial/RationalFunctions.lean

  • Line 20: "Format: * [Author Last Name, First Initial, *Title*][citation_key]." (Reference block does not follow the specific mandated asterisk/bracket format).
  • Line 164: "Functions and Terms: lowerCamelCase." (Uses weight_Λ).
  • Line 175: "Functions and Terms: lowerCamelCase." (Uses weight_Λ_over_𝒪).
  • Line 183: "Functions and Terms: lowerCamelCase." (Uses S_β).

• ArkLib/Data/Polynomial/Trivariate.lean

  • Line 38: "Functions and Terms: lowerCamelCase." (Uses eval_on_Z₀).
  • Line 52: "Functions and Terms: lowerCamelCase." (Uses eval_on_Z).

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/InterleavedCode.lean: The changes streamline the file by removing redundant imports and narrowing the scope of the noncomputable modifier to specific instances.
• ArkLib/Data/CodingTheory/ProximityGap/Basic.lean: Clean up the file by removing unused imports, redundant typeclass constraints, and the unrelated Trivariate namespace.
• ArkLib/Data/Polynomial/RationalFunctions.lean: Streamlined imports and improved code formatting and documentation for better readability.
• ArkLib/Data/Polynomial/Trivariate.lean: Defines an interface and notation for trivariate polynomials, including evaluation homomorphisms to bivariate polynomials and rational function domains.
• ArkLib.lean: This change expands the library's core exports by adding imports for Vandermonde matrices and trivariate polynomials.
• ArkLib/Data/CodingTheory/ProximityGap/DG25.lean: This PR modifies existing proofs by updating theorem references to reflect a namespace change from ReedSolomonCode to ReedSolomon.
• ArkLib/Data/CodingTheory/DivergenceOfSets.lean: This change updates the concentration_bounds lemma and namespace declarations to reflect the renaming of ReedSolomonCode to ReedSolomon.
• ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean: This update adjusts Reed-Solomon library references and generalizes the combinatorial proximity gap lemma for affine lines by removing an unnecessary DecidableEq typeclass requirement.
• ArkLib/Data/Matrix/Vandermonde.lean: This new file introduces definitions and theorems for non-square Vandermonde matrices, specifically characterizing their rank and establishing their relationship to polynomial evaluation.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean: This change removes the ReedSolomon namespace from the global scope and modifies a proof by explicitly qualifying references to ReedSolomon.code and ReedSolomon.evalOnPoints.
• ArkLib/Data/CodingTheory/ReedSolomon.lean: This change refactors the library by moving Vandermonde matrix logic to a dedicated module and updating various Reed-Solomon definitions and proofs for improved modularity and consistency.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean: This change refactors the file to align with renamed ReedSolomon library components, streamlines imports and namespaces, and improves the documentation and formatting of existing proximity gap theorems and definitions.

---

Last updated: 2026-03-02 19:11 UTC.