Change the Vandermonde def to the new mathlib one

[katyhr]

No description provided.

[github-actions]

🤖 Gemini PR Summary

Discrepancy Note

The PR title suggests a specific change to the Vandermonde definition, but the summary describes a broad refactor including trivariate polynomials, Hamming ball redefinitions, and significant namespace migrations across the library.

Mathematical Formalization

• Vandermonde Matrices: Refactors the Vandermonde matrix framework to align with Mathlib, adding support for rectangular matrices, rank calculations, submatrix properties, transposes, and polynomial evaluation.
• Trivariate Polynomials: Establishes a framework for trivariate polynomials with specialized notation ($X, Y, Z$) and evaluation homomorphisms for bivariate or rational function forms.
• Coding Theory: Redefines hammingBall and relHammingBall to incorporate code parameters directly. Includes lemmas for codeword density within these balls.
• Reed-Solomon Codes: Updates Reed-Solomon implementations and proximity gap results (referencing AHIV22, BCIKS20, and DG25) to utilize the new Vandermonde and Hamming ball definitions.

Refactoring and API Alignment

• Namespace Migration: Renames the ReedSolomonCode namespace to ReedSolomon across the library, impacting the Stir, Whir, and Binius modules.
• Standardization: Replaces closeCodewordsRel with relHammingBall throughout the codebase.
• Cleanup: Removes unused imports and redundant lemmas in the Fin and Matrix namespaces. Refines noncomputable markers.

Proof Status and Incompleteness

• CRITICAL: New sorry Placeholders: Introduces several sorry and admit placeholders, rendering portions of the library mathematically incomplete.
• Proof Regressions: In JohnsonBound/Lemmas.lean, the proofs for sum_choose_K' and d_eq_sum have been replaced with sorry.
• Unfinished Logic:
  • BCIKS20.lean: Contains sorry stubs for the Guruswami-Sudan algorithm.
  • R1CS.lean: Contains a sorry in pad_preserves_relation.
  • OracleInterface.lean: Includes a stop command mid-proof and an unproven multivariate polynomial bound.

---

Statistics

Metric	Count
📝 Files Changed	24
✅ Lines Added	577
❌ Lines Removed	762

---

Lean Declarations

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

• lemma subUpFull_of_vandermonde_is_vandermonde (h : n ≤ m) : 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
• lemma dotProduct_rightpad {R} [CommSemiring R] in ArkLib/Data/Matrix/Basic.lean
• theorem mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials in ArkLib/Data/CodingTheory/ReedSolomon.lean
• def closeCodewordsRel (C : Code ι F) (y : ι → F) (r : ℝ) : Set (ι → F) in ArkLib/Data/CodingTheory/ListDecodability.lean
• def nonsquare [Semiring F] (ι' : ℕ) (α : ι → F) : Matrix ι (Fin ι') F in ArkLib/Data/CodingTheory/ReedSolomon.lean
• theorem append_left_of_lt {u : Fin m → α} {v : Fin n → α} in ArkLib/Data/Fin/Basic.lean
• lemma rank_nonsquare_rows_eq_min (inj : Function.Injective α) : in ArkLib/Data/CodingTheory/ReedSolomon.lean
• theorem append_right_of_not_lt {u : Fin m → α} {v : Fin n → α} in ArkLib/Data/Fin/Basic.lean
• def nonsquareTranspose [Field F] (ι' : ℕ) (α : ι ↪ F) : Matrix (Fin ι') ι F in ArkLib/Data/CodingTheory/ReedSolomon.lean
• abbrev sqrtRate [Fintype ι] (deg : ℕ) (domain : ι ↪ F) : ℝ≥0 in ArkLib/Data/CodingTheory/ReedSolomon.lean
• instance interleavedCodeSet_fintype {A : Type*} {κ ι : Type*} in ArkLib/Data/CodingTheory/InterleavedCode.lean
• def finCarrier {ι : Type} [Fintype ι] in ArkLib/Data/CodingTheory/ReedSolomon.lean
• lemma subLeftFull_of_vandermonde_is_vandermonde (h : m ≤ n) : 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
• lemma nonsquare_mulVecLin [CommSemiring F] {ι' : ℕ} {α₁ : ι ↪ F} {α₂ : Fin ι' → F} {i : ι} : in ArkLib/Data/CodingTheory/ReedSolomon.lean
• instance instFintypeInterleavedModuleCode [Fintype A] : Fintype (MC ^⋈ κ) in ArkLib/Data/CodingTheory/InterleavedCode.lean
• def closeCodewords (C : Code ι F) (y : ι → F) (r : ℕ) : Set (ι → F) in ArkLib/Data/CodingTheory/ListDecodability.lean

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

• def listOfCloseCodewords (C : Code ι F) (y : ι → F) (r : ℕ) : ℕ in ArkLib/Data/CodingTheory/ListDecodability.lean
• def listOfCloseCodewordsRel (C : Code ι F) (y : ι → F) (r : ℝ) : ℕ in ArkLib/Data/CodingTheory/ListDecodability.lean
• theorem mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials in ArkLib/Data/Matrix/Vandermonde.lean
• lemma nonsquare_mulVecLin [CommRing F] {ι' : ℕ} {α₁ : ι ↪ F} {α₂ : Fin ι' → F} {i : ι} : in ArkLib/Data/Matrix/Vandermonde.lean
• lemma listOfCloseCodewordsRel_eq_zero : in ArkLib/Data/CodingTheory/ListDecodability.lean
• lemma listOfCloseCodewords_eq_zero : in ArkLib/Data/CodingTheory/ListDecodability.lean
• def nonsquare [CommRing F] (ι' : ℕ) (α : ι → F) : Matrix ι (Fin ι') F in ArkLib/Data/Matrix/Vandermonde.lean
• lemma rank_nonsquare_rows_eq_min (inj : Function.Injective α) : in ArkLib/Data/Matrix/Vandermonde.lean
• lemma subLeftFull_of_vandermonde_is_vandermonde (h : m ≤ n) : 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 rank_nonsquare_eq_deg_of_ι_le (inj : Function.Injective α) (h : m ≤ n) : in ArkLib/Data/Matrix/Vandermonde.lean
• lemma subUpFull_of_vandermonde_is_vandermonde (h : n ≤ m) : in ArkLib/Data/Matrix/Vandermonde.lean
• def nonsquareTranspose [Field F] (ι' : ℕ) (α : ι ↪ F) : Matrix (Fin ι') ι F in ArkLib/Data/Matrix/Vandermonde.lean

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

• 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 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 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
• 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_factors_with_large_common_root_set (δ : ℚ) (x₀ : F) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L366 to L329
• 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
• def hammingBall (C : Code ι F) (y : ι → F) (r : ℕ) : Set (ι → F) in ArkLib/Data/CodingTheory/ListDecodability.lean moved from L22 to L23
• def relHammingBall (C : Code ι F) (y : ι → F) (r : ℝ) : Code ι F in ArkLib/Data/CodingTheory/ListDecodability.lean moved from L27 to L29
• def δ_ε_multilinearCorrelatedAgreement [CommRing F] [Module F A] in ArkLib/Data/CodingTheory/ProximityGap/Basic.lean moved from L141 to L119

---

sorry Tracking

❌ **Added:** 1 `sorry`(s)

• theorem pad_preserves_relation (sz₁ sz₂ : Size) in ArkLib/ProofSystem/ConstraintSystem/R1CS.lean (L90)

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

• 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
• lemma exists_factors_with_large_common_root_set (δ : ℚ) (x₀ : F) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L375 to L336
• lemma exists_factors_with_large_common_root_set (δ : ℚ) (x₀ : F) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L378 to L340
• 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
• theorem correlatedAgreement_affine_spaces {k : ℕ} [NeZero k] {u : Fin (k + 1) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L137 to L136

---

🎨 **Style Guide Adherence**

The code changes contain more than 20 style guide violations, primarily related to naming conventions for definitions and variables. They are grouped by rule below:

• Rule: Functions and Terms must use lowerCamelCase (25 violations)

  • noncomputable def D_X (ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean:148)
  • noncomputable def proximity_gap_degree_bound (ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean:151)
  • noncomputable def weight_Λ (ArkLib/Data/Polynomial/RationalFunctions.lean:155)
  • noncomputable def Pz (ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean:280)
  • noncomputable def δ_ε_correlatedAgreementCurves (ArkLib/Data/CodingTheory/ProximityGap/Basic.lean:162)
  • noncomputable def eval_on_Z₀ (ArkLib/Data/Polynomial/Trivariate.lean:38)

• Rule: Elements of a generic type must use x, y, z, ... (2 violations)

  • set X₁ : ℚ := ... (ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean:71)
  • set X₂ := ... (ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean:73)

• Rule: Assumptions/Hypotheses must use h, h₁, ... (4 violations)

  • have X₁h : X₁ ≠ 0 := ... (ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean:72)
  • have hF2 : (2 : ℕ) ≤ Fintype.card F := ... (ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean:1063)
  • have hC_nonneg : (0 : ℚ) ≤ 2 * E1 - frac * E1 ^ 2 (ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean:971)

• Rule: Indentation: Use 2 spaces for indentation (2 violations)

  • The second line of the variable block is aligned with the previous parameters rather than using a 2-space indent (ArkLib/Data/CodingTheory/InterleavedCode.lean:584).
  • The jointAgreement block uses a 4-space indent for the logical expression (ArkLib/Data/CodingTheory/InterleavedCode.lean:656).

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/DivergenceOfSets.lean: This change updates references from the ReedSolomonCode namespace to ReedSolomon within the concentration_bounds lemma. The lemma, which addresses probability bounds for code distances, currently contains a sorry placeholder.
• ArkLib.lean: This update expands the library's top-level exports by importing newly implemented modules for Vandermonde matrices and trivariate polynomials. No sorry or admit placeholders are introduced.
• ArkLib/Data/CodingTheory/InterleavedCode.lean: This PR cleans up the file by removing numerous unused imports and replacing the file-wide noncomputable section with specific noncomputable modifiers for Fintype instances. The changes focus on improving dependency management and code organization without introducing new logic or sorry placeholders.
• ArkLib/Data/CodingTheory/ProximityGap/DG25.lean: This change updates namespace references and theorem calls from ReedSolomonCode to ReedSolomon within existing proofs for Reed-Solomon proximity gap results. It modifies the implementation of several theorems to reflect this naming shift without introducing new theorems or sorry placeholders.
• ArkLib/Data/CodingTheory/ProximityGap/Basic.lean: This PR refactors the file by removing unused imports and deleting the Trivariate namespace. It also streamlines type signatures for core proximity gap and correlated agreement definitions by removing redundant constraints and parameters. No new theorems, proofs, or sorry placeholders were introduced.
• ArkLib/Data/CodingTheory/ListDecodability.lean: This refactor redefines hammingBall and relHammingBall to directly incorporate the code $C$, replacing previous set-intersection definitions with new functions listOfCloseCodewords and listOfCloseCodewordsRel based on Nat.card. The changes update the listDecodable predicate accordingly and introduce two new lemmas characterizing when the number of codewords in a ball is zero. No sorry or admit placeholders were added.
• ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean: This change updates the file's imports and namespace references to align with a refactoring of the ReedSolomon library. Additionally, it optimizes typeclass requirements by omitting an unnecessary DecidableEq constraint for the proof of Lemma 4.4.
• ArkLib/Data/Matrix/Basic.lean: This change removes the dotProduct_rightpad lemma, which related the dot product of two right-padded vectors to the dot product of the original vectors. No new theorems or definitions were added in this update.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean: This file refines the formalization of proximity gaps and correlated agreement for Reed-Solomon codes based on the BCIKS20 paper, primarily by updating the namespace from ReedSolomonCode to ReedSolomon. It introduces several definitions and lemma stubs related to the Guruswami-Sudan algorithm and trivariate polynomials, though most major theorems and lemmas currently contain sorry placeholders.
• ArkLib/Data/Fin/Basic.lean: This change removes the append_left_of_lt and append_right_of_not_lt theorems, which provided simplification rules for evaluating Fin.append based on index comparisons. No new definitions, theorems, or sorry placeholders are introduced.
• ArkLib/Data/Polynomial/Trivariate.lean: This new file defines a framework for trivariate polynomials, providing specialized notation for variables $X$, $Y$, and $Z$ and their respective polynomial rings. It introduces new definitions and homomorphisms to evaluate trivariate polynomials into bivariate forms and convert them into bivariate polynomials over rational functions. No theorems or sorry placeholders are included.
• ArkLib/Data/CodingTheory/ReedSolomon.lean: This refactoring moves Vandermonde matrix definitions and lemmas into a dedicated module, ArkLib.Data.Matrix.Vandermonde, and cleans up the ReedSolomon namespace. The changes also include adding noncomputable qualifiers to several definitions, improving documentation for Reed-Solomon code variants, and updating proofs to use standard library lemmas. No sorry or admit placeholders were introduced.
• ArkLib/Data/Polynomial/RationalFunctions.lean: This maintenance update streamlines the file by removing unused imports, refining open statements, and reformatting docstrings and definitions to improve readability and style. The changes are purely structural and documentation-based, introducing no new theorems or proof modifications and containing no sorry placeholders.
• ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean: This update refactors several proofs in JohnsonBound/Lemmas.lean to standardize variable naming and streamline tactic applications using aesop and grind. However, the changes introduce numerous sorry placeholders, leaving several previously completed or partially completed proofs—such as those for sum_choose_K', F2i_card, and d_eq_sum—incomplete.
• ArkLib/Data/Matrix/Vandermonde.lean: This new file introduces definitions and theorems for rectangular (non-square) Vandermonde matrices. It provides formalizations for their rank, submatrix properties, and transposes, as well as a theorem relating matrix-vector multiplication to polynomial evaluation.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean: This change refines the uniqueClosestCodeword proof by replacing the global ReedSolomon namespace opening with explicit references to ReedSolomon.code and ReedSolomon.evalOnPoints within a simp tactic. No new theorems, definitions, or sorry placeholders are introduced.
• ArkLib/OracleReduction/OracleInterface.lean: This change refactors the proof of distanceLE_polynomial_degreeLE to use direct degree and root counting arguments, though it currently includes a stop command mid-proof. It also simplifies the stated bound for multivariate polynomials in distanceLE_mvPolynomial_degreeLE, which remains unproven with a sorry.
• ArkLib/ProofSystem/ConstraintSystem/R1CS.lean: This change simplifies the statement of the pad_preserves_relation theorem by removing several size-related hypotheses. Notably, the previous detailed proof has been replaced with a sorry placeholder, leaving the theorem currently unverified.
• ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean: This change updates the listDecodingCollisionProbability definition by replacing the closeCodewordsRel relation with relHammingBall to specify codeword proximity. It modifies an existing definition and introduces no new theorems or sorry placeholders.
• ArkLib/ProofSystem/Stir/Quotienting.lean: This change updates the quotienting lemma by replacing the reference to closeCodewordsRel with relHammingBall. This refactor ensures the theorem statement aligns with updated naming conventions for relative Hamming balls in the library.
• ArkLib/ProofSystem/Whir/BlockRelDistance.lean: This change modifies the listBlock_subset_listHamming lemma by introducing a necessary bound on the relative distance parameter ($\delta \le 1$) and updating the target set to use relHammingBall instead of closeCodewordsRel. The update ensures the lemma correctly characterizes the subset relationship between block relative distance and relative Hamming balls under standard constraints.
• ArkLib/ProofSystem/Whir/Folding.lean: This change updates the folding_listdecoding_if_genMutualCorrAgreement theorem by replacing the use of closeCodewordsRel with relHammingBall. This modification aligns the theorem's proof with updated naming conventions or API structures for Hamming distance relations within the library.
• ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean: This update modifies the proximityListDecodingCondition definition by renaming closeCodewordsRel to relHammingBall, likely to align with updated naming conventions in the library. The change is purely a refactor of an existing definition and does not introduce any new theorems or sorry placeholders.
• ArkLib/ProofSystem/Whir/OutofDomainSmpl.lean: This refactor replaces the closeCodewordsRel definition with relHammingBall across several lemmas to align with updated library terminology. The changes modify the statements of existing theorems regarding out-of-domain sampling, one of which maintains a sorry placeholder.

---

Last updated: 2026-03-05 23:06 UTC.