feat(guruswami-sudan): constructive decoder witness/filter correctness

[eliasjudin]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Implements constructive Guruswami-Sudan witness extraction in computeGsWitness via a normalized linear system solved by BerlekampWelch.linsolve, removing the brute-force fallback from the decoder path. It checks multiplicity by Hasse-derivative vanishing and performs computable CompPoly root filtering (Q(X, p(X)) = 0), with decoder soundness captured by decoder_mem_impl_dist; closes #213.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 Gemini PR Summary

Constructive Guruswami-Sudan Decoder

Transitions the Guruswami-Sudan (GS) decoder from a non-computable, existential formulation to a fully constructive and computable framework. This enables execution within Lean while maintaining rigorous mathematical soundness.

Implementation & Logic

• Constructive Witness Extraction: Implements computeGsWitness using a normalized linear system solved via BerlekampWelch.linsolve. This replaces "opaque" decoder logic and removes inefficient brute-force fallbacks.
• Multiplicity Verification: Employs Hasse-derivative vanishing to ensure the interpolation polynomial meets the required constraints at received data points.
• Computable Root Filtering: Introduces logic to verify the condition $Q(X, p(X)) = 0$, ensuring candidate polynomials extracted from the interpolation step are valid solutions.

Mathematical Soundness

• Decoder Soundness Theorem: Formalizes decoder_mem_impl_dist, proving that messages returned by the concrete implementation satisfy the specified Hamming distance bounds.
• Interpolation Correctness: Provides formal proofs verifying that the linearized system approach correctly satisfies the multiplicity requirements fundamental to the GS list-decoding algorithm.
• Computable Bridge: Replaces noncomputable definitions with active functions, improving the library's utility for program verification and code generation.

---

Related Issues: Closes #213
Co-authored-by: @Aristotle-Harmonic

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	739
❌ Lines Removed	58

---

Lean Declarations

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

• theorem decoder_dist_impl_mem in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

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

• lemma guruswami_sudan_for_proximity_gap_existence_strong in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma coeff_vec_to_bivariate_coeff (k D : ℕ) in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma guruswami_sudan_for_proximity_gap_property_strong [Fintype F] {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma mem_polynomials_degree_lt in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma coeff_vec_to_bivariate_ne_zero_of_is_witness_c in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• def polynomialsDegreeLt (F : Type) [CommSemiring F] [Fintype F] in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• theorem decoder_output_dist_le in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

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

• theorem decoder_mem_impl_dist in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean moved from L60 to L600
• def decoder [Fintype F] (k r D e : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) : in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean moved from L57 to L586
• lemma guruswami_sudan_for_proximity_gap_existence in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean moved from L103 to L717
• lemma guruswami_sudan_for_proximity_gap_property [Fintype F] {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean moved from L113 to L756

---

sorry Tracking

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

• lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• theorem decoder_mem_impl_dist in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• opaque decoder (k r D e : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) : List F[X] 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
• theorem decoder_dist_impl_mem in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

---

🎨 **Style Guide Adherence**

• Line 73: Q_multiplicity : ∀ i, r ≤ Bivariate.rootMultiplicity Q (ωs i) (f i) violates "Functions and Terms: lowerCamelCase (e.g., binarySearch, isPrime)".
• Line 77: {F : Type} violates "Variable Conventions: α, β, γ, ... : Generic types".
• Line 77: {p : F[X]} violates "Variable Conventions: x, y, z, ... : Elements of a generic type" (Note: p, q, r are reserved for Predicates and relations).
• Line 84: (lt_of_lt_of_le h (by exact_mod_cast Nat.le_of_not_lt ‹_›)) violates "Delimiters: Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting."
• Line 95: {p : F[X]} violates "Variable Conventions: x, y, z, ... : Elements of a generic type".
• Line 125: (fun acc i ↦ violates "Variable Conventions: m, n, k, ... : Natural numbers" (Note: i, j, k are reserved for Integers).
• Line 130: (fun b j ↦ violates "Variable Conventions: m, n, k, ... : Natural numbers".
• Line 166: {p : F[X]} violates "Variable Conventions: x, y, z, ... : Elements of a generic type".
• Line 196: (fun a1 j ↦ and (fun a2 i ↦ violate "Variable Conventions: m, n, k, ... : Natural numbers".
• Line 210: (fun a1 j ↦ and (fun a2 i ↦ violate "Variable Conventions: m, n, k, ... : Natural numbers".
• Line 224: (List.finRange r).all fun ab ↦ and (List.finRange (ab.val + 1)).all fun a ↦ violate "Variable Conventions: m, n, k, ... : Natural numbers" (Note: a, b, c are reserved for Propositions).
• Line 268: (fun j ↦ and Line 269: (fun i ↦ violate "Variable Conventions: m, n, k, ... : Natural numbers".
• Line 330: let i : Fin (D + 1) and Line 331: let j : Fin (D + 1) violate "Variable Conventions: m, n, k, ... : Natural numbers".
• Line 378: let a := rem / (r + 1) and Line 379: let b := rem % (r + 1) violate "Variable Conventions: m, n, k, ... : Natural numbers".
• Line 445: (p : F[X]) violates "Variable Conventions: x, y, z, ... : Elements of a generic type".
• Line 461: (fun acc j ↦ violates "Variable Conventions: m, n, k, ... : Natural numbers".
• Line 466: (fun a1 j ↦ and Line 467: (fun a2 i ↦ violate "Variable Conventions: m, n, k, ... : Natural numbers".
• Line 531: {p : F[X]} violates "Variable Conventions: x, y, z, ... : Elements of a generic type".
• Line 536: simp [hcw] at hp violates "Indentation: Use 2 spaces for indentation." (Indented 4 spaces relative to the pattern match).
• Lines 538-542: Indentation violates "Indentation: Use 2 spaces for indentation." (Indented 4 spaces relative to the pattern match).
• Line 670: ((coeffVecToBivariate k D c).coeff j.val).coeff i.val violates "Delimiters: Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting."
• Line 709: (...).1 hw violates "Naming Conventions: Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)." (Note: Projections like .1 should be replaced by Iff.mp for logical connectives).

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean: This update replaces the opaque Guruswami-Sudan decoder with a fully computable implementation based on linearized system solving and Hasse-derivative multiplicity checks, introducing several new definitions for witness searching and root extraction alongside theorems that verify their soundness and bridge them to classical formulations.

---

Last updated: 2026-03-03 11:29 UTC.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: abf6a7f5d2

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 8aa5bfba09

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[quangvdao]

You can use CompPoly now - probably after adding more supporting lemmas there

[eliasjudin]

You can use CompPoly now - probably after adding more supporting lemmas there

this is actually exactly what was needed for the computable definition, will update later

[eliasjudin]

still trying to write a constructive algorithm for computing a Guruswami–Sudan witness Q directly
(e.g. via linearized system solving over CompPoly) to replace the brute-force fallback

[eliasjudin]

@quangvdao @dhsorens some of this should probably go into CompPoly. let me know if you have any suggestions.