Implement GS decoder and prove soundness + completeness

[MavenRain]

Replace opaque decoder with noncomputable def using polySol roots filtered by Hamming distance. Prove soundness and completeness with zero sorry.

Fix hypothesis from e ≤ n - √(kn) to (e : ℝ) < n - √((k+1)n) to match the GS rate parameter ρ = (k+1)/n. Add h_deg : p.natDegree < k to completeness.

Closes #213, #233, #222.

[chatgpt-codex-connector]

Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits.
Credits must be used to enable repository wide code reviews.

[github-actions]

🤖 Gemini PR Summary

Guruswami-Sudan Implementation

• Decoder Implementation: Replaced opaque placeholders with a noncomputable def of the Guruswami-Sudan decoder utilizing polySol roots filtered by Hamming distance.
• Error Bound Refinement: Updated the error bound hypothesis from $e \le n - \sqrt{kn}$ to $(e : \mathbb{R}) &lt; n - \sqrt{(k+1)n}$ to match the rate parameter $\rho = (k+1)/n$.
• Interpolation Infrastructure: Added support for solving linearized systems of Hasse-derivative constraints for the bivariate interpolation step.
• Degree Constraints: Incorporated the hypothesis h_deg : p.natDegree < k into the completeness proof.
• Note: A discrepancy exists between the draft summary, which mentions a constructive computableDecoder, and the PR body, which specifies a noncomputable def.

Proof Completion

• Removal of Placeholders: Eliminated all sorry and admit placeholders within the Guruswami-Sudan implementation and associated proofs.
• Soundness and Completeness: Established formal proofs for the soundness and completeness of the decoder relative to the Johnson bound.

Infrastructure & Refactoring

• Bivariate Polynomial Bridging: Implemented "bridge lemmas" to facilitate conversion between computable coefficient vectors and standard Mathlib bivariate polynomials.
• Algorithmic Logic: Integrated polySol root-finding with Hamming distance filtering to identify valid codewords.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	952
❌ Lines Removed	54

---

Lean Declarations

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

• theorem decoder_dist_impl_mem 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

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

• 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 mem_decoder_of_dist in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• theorem dist_le_of_mem_decoder in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• theorem computableDecoder_mem_impl_dist in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• theorem computableDecoder_output_dist_le in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma guruswami_sudan_for_proximity_gap_existence 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 guruswami_sudan_for_proximity_gap_existence_strong in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• lemma guruswami_sudan_for_proximity_gap_property [Fintype F] {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

---

sorry Tracking

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

• theorem mem_decoder_of_dist in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean (L75)
• theorem dist_le_of_mem_decoder in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean (L64)
• opaque decoder (k r D e : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) : List F[X] in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean (L54)

---

🎨 **Style Guide Adherence**

The following violations of the style guide were identified:

• Documentation Standards: "Use backticks for Lean names: `List.map`." (23 violations)

  • Line 51: proximity_gap_johnson (should be `proximity_gap_johnson`)
  • Line 181: codewordToPoly (should be `codewordToPoly`)
  • Line 692: isWitnessC and isQRootRaw (should be `isWitnessC` and `isQRootRaw`)

• Naming Conventions (Dot Notation): "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)." (16 violations)

  • Line 183: Multiset.mem_toList.mpr (should be Iff.mpr Multiset.mem_toList)
  • Line 274: Finset.mem_singleton.mp hp (should be Iff.mp Finset.mem_singleton hp)
  • Line 662: (...).1 (should use Iff.mp or similar explicit namespace-based name)

• Variable Conventions: "α, β, γ, ... : Generic types" (10 violations)

  • Line 90: variable {F : Type} (should use α, β, or another generic Greek letter)
  • Line 203: def polynomialsDegreeLt (F : Type) ...
  • Line 289: (c : Fin (D + 1) × Fin (D + 1) → F)

• Theorem Naming Logic (Predicates): "Predicates: Generally use prefixes (e.g., isClosed_Icc not Icc_isClosed)." (6 violations)

  • Line 360: is_witness_c_nonzero (should be isWitnessC_nonzero)
  • Line 489: is_q_root_raw_iff_all_coeff_zero (should be isQRootRaw_iff_all_coeff_zero)
  • Line 680: coeff_vec_to_bivariate_ne_zero_of_is_witness_c (should be coeff_vec_to_bivariate_ne_zero_of_isWitnessC)

• Naming Conventions (Theorems and Proofs): "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)." (3 violations)

  • Line 538: mem_computableDecoder_imp (should be mem_computable_decoder_imp)
  • Line 545: computableDecoder_mem_impl_dist (should be computable_decoder_mem_impl_dist)
  • Line 549: computableDecoder_output_dist_le (should be computable_decoder_output_dist_le)

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean: This update replaces previous sorry placeholders with a complete implementation of the Guruswami-Sudan decoder, providing both a noncomputable specification and a constructive computableDecoder using CompPoly arithmetic. It introduces formal proofs for decoder soundness and completeness relative to the Johnson bound, alongside infrastructure for solving the linearized systems of Hasse-derivative constraints required for bivariate interpolation. The changes also establish bridge lemmas between computable coefficient vectors and classical Mathlib bivariate polynomials, with no new sorry placeholders introduced.

---

Last updated: 2026-04-05 16:30 UTC.

[alexanderlhicks]

Thanks for the PR! Please note #311, could you consider rebasing on top of that branch/PR?

[MavenRain]

#311

Sure . . . if this doesn't get too hairy, I'll give it a go