feat(coding-theory): integrate CompPoly's executable Guruswami-Sudan decoder

[olympichek]

Overview

This PR connects ArkLib's Guruswami-Sudan development to the executable decoder recently added in CompPoly. It adds the translation layer needed to run the CompPoly decoder on ArkLib Reed-Solomon inputs and state the result in ArkLib's existing degree-and-distance specification.

This PR includes:

• A small wrapper around CompPoly's decoder parameters and selector interface.
• A bounded search for decoder parameters, with certificates for the conditions ArkLib needs.
• Conversions between ArkLib Reed-Solomon words and CompPoly's packed received-word format.
• Proofs that the executable decoder returns exactly the polynomials described by ArkLib's degree-and-distance specification.
• A bump to CompPoly v4.30.0-patch1, together with the new imports.

Correctness

The main theorem says that the executable output matches the ArkLib specification: returned polynomials have degree < k and are within the requested Hamming radius, and every polynomial with those properties appears in the output. There are also compatibility lemmas relating this statement to ArkLib's existing decoder under the Johnson-radius assumption.

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Formalizes exists_multiplicity_of_johnson to provide multiplicity and list size parameters based on the Johnson radius.
• Establishes soundness and completeness: proves the executable decoder output matches ArkLib’s degree-and-distance specification.
• Relates the executable decoder to ArkLib's existing decoder via compatibility lemmas under the Johnson-radius assumption.
• Proves the existence of interpolation witnesses using capacity bounds.

Executable Integration

• Integrates CompPoly's Guruswami-Sudan decoder and updates the library dependency to v4.30.0-patch1.
• Implements a certified parameter selector that performs a bounded search for valid decoding parameters.
• Adds a translation layer to convert between ArkLib Reed-Solomon words and CompPoly’s packed received-word format.
• Wraps CompPoly’s decoder parameters and selector into an ArkLib-compatible interface.

Refactoring and Infrastructure

• Reorganizes the Guruswami-Sudan module to separate the core algorithm, correctness proofs, and executable integration.
• Simplifies internal proofs within ArkLib/Data/CodingTheory/Prelims.lean to improve maintainability.

---

Statistics

Metric	Count
📝 Files Changed	8
✅ Lines Added	920
❌ Lines Removed	68

---

Lean Declarations

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

• def boundedSearchParamSelector {maxM maxW : Nat} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem agreement_card_add_hammingDist in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• noncomputable def johnsonParamSelector : GSParamSelector where in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decodeWithParams_iff_spec in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def RepresentsArkInput in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem interpolationMonomials_size (params : GSInterpParams) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma foldl_size_add {α β : Type*} (step : Array β → α → Array β) (d : α → Nat) in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def execParamsOfMultiplicityAndDegree in ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean
• private lemma foldl_push_size {α β : Type*} (g : Array β → α → β) in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem decode_complete in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem searchParamsUpTo_sound {maxM maxW k n e : Nat} {params : GSExecParams} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem toPoly_degree_lt_of_degreeLt in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• lemma exists_multiplicity_of_johnson {k n e : ℕ} in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• theorem candidateMismatchCount_represents_hammingDist in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decode_iff_mem_decoder_of_degree_lt in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decodeWithParams_iff_mem_decoder_of_degree_lt in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem toPoly_natDegree_lt_of_degreeLt in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem paramsCert_of_johnson {k n e : Nat} (hjohnson : JohnsonSpecCondition k n e) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def searchParamsUpTo in ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean
• private theorem cPolynomialOfPoly_toPoly (p : F[X]) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decode_iff_spec in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma sum_map_const {α : Type*} (l : List α) (c : Nat) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem decodeWithParams_sound in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma length_filter_ofFn_eq_card {α : Type*} {n : Nat} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma list_foldl_count_false {α : Type*} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma sum_range'_sub_two (m : Nat) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def GSSpecSet (k e : Nat) (ωs : Fin n ↪ F) (f : Fin n → F) : Set F[X] in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem interpolationConstraints_size {F : Type*} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private def cPolynomialOfPoly (p : F[X]) : CompPoly.CPolynomial F in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem decodeWithParams_complete in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma list_foldl_count_true {α : Type*} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def JohnsonSpecCondition (k n e : Nat) : Prop in ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean
• theorem passesCandidateDistance_represents_hammingDist in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def paramsPassIntegerChecks in ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean
• theorem matchingPointCount_represents_card in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private def constraintsFold {F : Type*} (points : Array (F × F)) (m : Nat) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private theorem degreeLt_cPolynomialOfPoly_of_degree_lt {p : F[X]} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem interpolationWitnessExists_of_capacity in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• example : GSParamCert 2 5 1 (execParamsOfMultiplicityAndDegree 2 1 1 3) in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem length_of_represents in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma mem_monomialGrid {D : Nat} {mm : Monomial} : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem paramsPassIntegerChecks_iff in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem distinctXCoordinates_of_represents in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decodeWithParams_iff_degree_and_distance in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem searchParamsUpTo_complete {maxM maxW k n e : Nat} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem decode_sound in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma interpolationConstraints_eq_fold {F : Type*} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Pull Request Guidelines

• Title Format: Ensure the PR title follows <type>(<optional-scope>): <subject>. For example: feat(GuruswamiSudan): add executable GS decoder and correctness proofs.

Style and Naming Guidelines

• Variable Conventions: The use of ωs and f in Correctness.lean is consistent with adjacent Reed-Solomon files, and the use of h prefixes for hypotheses (e.g., hrep, hparams) follows the h, h₁ convention.
• Naming Conventions: Types and Props such as GSParamCert, GSSpecSet, and RepresentsArkInput correctly use UpperCamelCase. Functions like paramsPassIntegerChecks correctly use lowerCamelCase.
• Theorem Naming Logic: Theorem names such as paramsPassIntegerChecks_iff and interpolationWitnessExists_of_capacity correctly use snake_case and follow the _iff and _of_ conventions.

Syntax and Formatting

• Line Length: Several lines in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean exceed the 100-character limit:
  • Line 126 (declaration of boundedSearchParamSelector): ~147 characters.
  • Line 149 (hypothesis hex in searchParamsUpTo_complete): ~172 characters.
  • Line 411 (declaration of mem_decodeWithParams_iff_degree_and_distance): ~120 characters.
  • Line 639 (hypothesis he in mem_decodeWithParams_iff_mem_decoder_of_degree_lt): ~115 characters.
• Functions: In Correctness.lean, the code uses fun x => ... (e.g., lines 23, 116, 222). Per guidelines, prefer the fun x ↦ ... syntax.
• Operators: Spaces around :, :=, and infix operators are correctly applied throughout the new files.

Documentation Standards

• Declaration Docstrings: Major theorems and definitions in Correctness.lean and Executable.lean have docstrings.
• Citations: The Guruswami-Sudan algorithm and the Johnson bound are referenced in text, but the new modules lack a ## References section in their headers with citation keys (e.g., [GS99]) and corresponding BibTeX entries as required by the Citation Standards for academic papers.
• Sectioning: The use of /-! ### Title -/ for structure is followed correctly in the new files.

---

📄 **Per-File Summaries**

• ArkLib.lean: This update expands the Guruswami-Sudan decoding module by adding imports for its correctness proofs and executable implementation. These changes integrate these submodules into the main library entry point.
• ArkLib/Data/CodingTheory/GuruswamiSudan.lean: This change updates the Guruswami-Sudan module by importing submodules for its executable implementation and correctness proofs, effectively aggregating the algorithm's definition and formal verification into a single entry point.
• ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean: This file establishes the formal correctness of the executable Guruswami-Sudan Reed-Solomon decoder by proving its soundness and completeness relative to the ArkLib specification. It introduces theorems connecting the computational backend to mathematical constraints, such as proving the existence of interpolation witnesses via capacity bounds and the availability of valid parameters within the Johnson radius. The file contains no sorry or admit placeholders.
• ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean: This new file establishes an integration layer between ArkLib and the CompPoly library for an executable Guruswami-Sudan decoder. It introduces definitions for parameter certification, search logic, and a certified parameter selector structure that includes soundness and completeness properties relative to the Johnson radius condition.
• ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean: Introduces the lemma exists_multiplicity_of_johnson to prove that a valid multiplicity parameter exists when the error count is within the Johnson radius. The proof of mem_decoder_of_dist is modified to utilize this new lemma, refactoring the previous inlined logic into a more modular structure.
• ArkLib/Data/CodingTheory/Prelims.lean: The changes in ArkLib/Data/CodingTheory/Prelims.lean simplify a proof step within the rank_eq_if_subUpFull_eq lemma by replacing a redundant use of Equiv.refl with the identity function. This modification streamlines the existing proof without introducing new theorems, definitions, or sorry placeholders.

---

Last updated: 2026-06-16 14:12 UTC.

[olympichek]

@MavenRain thank you for your review of this PR! I just pushed a pair of new commits to address issues/gaps you pointed out

[Abraxas1010]

Coordination note (complementary lane, no file overlap intended): we are preparing the encoder-side executable bridge — a theorem that CompPoly's Univariate.ReedSolomon.encode output, read through the embedding induced by Domain.node_injective, is a member of ArkLib's ReedSolomon.code (with the messagePoly.toPoly / messagePoly_degree_lt / eval_toPoly witness chain), followed by the NTT fast-encoder equality via forwardImpl_eq_evalOnDomain. Statement-level typing is validated against ArkLib main.

Two touch points with this PR:

1. CompPoly pin: ArkLib's pinned rev 18c1613 predates CompPoly/Univariate/ReedSolomon.lean, and this PR already carries a manifest bump — we plan to base on (or land after) your bump rather than race it.
2. Conversions: if your ArkLib↔CompPoly received-word conversion layer is the intended canonical one, we'll consume it for the codeword direction rather than adding a parallel one — happy to adjust to whatever shape lands here.

Placement guidance welcome (ArkLib/ToCompPoly/CodingTheory/ vs alongside this PR's files).

The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[Abraxas1010]

This is showing as conflicting, so I resolved it locally and build-verified the result — offering the resolution here since we contributed the sibling decoder work in CompPoly (#267) and know that side of the dependency.

The conflict is narrower than it looks. Only two files actually conflict: lakefile.toml and lake-manifest.json, both on the dependency pins. Every Lean file in the PR auto-merges — ArkLib.lean, GuruswamiSudan.lean and Prelims.lean all merge without intervention. The substance is:

	this branch	main
lean-toolchain	v4.30.0	v4.31.0
CompPoly pin	v4.30.0-patch1	v4.31.0

So the resolution is to take main's side on both files (the branch never edited lean-toolchain, so that one resolves itself) and then check whether the Lean side survives the CompPoly 4.30 → 4.31 bump.

It survives, with one repair. After taking main's pins, exactly one proof breaks:

ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean:442:2
Type mismatch: After simplification, term
  List.nodup_ofFn.mpr (Function.Embedding.injective ωs)
has type
  @List.Nodup F (List.ofFn ⇑ωs)
but is expected to have type
  @List.Nodup F (List.ofFn ((fun point ↦ point.1) ∘ fun i ↦ (ωs i, f i)))

simp no longer unfolds the composition to its pointwise form here, so distinctXCoordinates_of_represents no longer closes. One-line fix:

-  simpa using (List.nodup_ofFn.2 ωs.injective)
+  simpa [Function.comp_def] using (List.nodup_ofFn.2 ωs.injective)

That is the whole repair — nothing mathematical changed, and Executable.lean, GuruswamiSudan.lean and Basic.lean all build unchanged against CompPoly v4.31.0.

Verified: merge main taking its pins, apply the one-line change above, then full lake build ArkLib completes green at Lean 4.31 (4238 jobs), including GuruswamiSudan.Basic, .GuruswamiSudan, .Executable and .Correctness.

Happy to open a PR against formal-land:guruswami-sudan with exactly that, or to just leave it here if you would rather apply it yourself — it is three lines of work now that the diagnosis is done.

The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[github-actions]

🤖 PR Summary

This PR integrates ArkLib's existing Guruswami–Sudan specification with CompPoly's executable decoder, establishing a certified translation layer that lets the concrete decoder run on ArkLib Reed–Solomon inputs and proves its output matches the previously purely existential degree-and-distance specification.

Mathematical Formalization

• GuruswamiSudan.lean (refactor): Extracts the existential argument from mem_decoder_of_dist into a new standalone lemma exists_multiplicity_of_johnson. This lemma states that under the Johnson radius condition e < n - √((k+1)·n) there exists a positive multiplicity m such that e/n < proximity_gap_johnson k n m. The body of mem_decoder_of_dist is now a one‑line call to this lemma. No sorry or admit were added.

• Correctness.lean (new): Proves the executable decoder matches the ArkLib specification.

  • Defines RepresentsArkInput and GSSpecSet to relate runtime inputs to the semantic specification.
  • Establishes paramsPassIntegerChecks_iff for parameter certificates.
  • Constructs boundedSearchParamSelector (computable) and johnsonParamSelector (non‑computable, relies on the Johnson‑radius lemma).
  • Proves interpolationWitnessExists_of_capacity and counting lemmas (interpolationMonomials_size, interpolationConstraints_size) to discharge the interpolation‑existence hypothesis.
  • Core membership characterizations:
    • mem_decodeWithParams_iff_degree_and_distance
    • mem_decodeWithParams_iff_spec
    • mem_decode_iff_spec
  • Soundness/completeness corollaries: decodeWithParams_sound, decodeWithParams_complete, decode_sound, decode_complete.
  • Compatibility theorems mem_decodeWithParams_iff_mem_decoder_of_degree_lt and mem_decode_iff_mem_decoder_of_degree_lt that relate this decoder’s output to the existing specification decoder under an explicit degree bound.
  • No sorry or admit are present.

Protocols / Soundness

• Executable.lean (new): Provides the ArkLib integration layer for the CompPoly decoder.
  • Defines GSParamCert — a certificate that executable parameters satisfy message degree, Hamming radius, multiplicity positivity, interpolation capacity, and enough agreement bound.
  • Defines JohnsonSpecCondition (proposition for the Johnson‑radius condition).
  • Defines paramsPassIntegerChecks (boolean check), execParamsOfMultiplicityAndDegree (constructor), searchParamsUpTo (bounded search), and GSParamSelector (structure with soundness and completeness conditions).
  • No sorry or admit are present.

Infrastructure / CI

• Bumps the CompPoly dependency to v4.30.0-patch1 and adds the required imports.

Refactoring

• In GuruswamiSudan.lean, the existential argument is extracted to a reusable lemma; the original theorem becomes a one‑liner that delegates to it. No semantic change.

---

Note: The PR body describes a small wrapper and a bounded search; the actual substance is concentrated in Correctness.lean (the major new proof file) and Executable.lean (the integration layer). All new code is fully proven — no sorry or admit remain.
}

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	916
❌ Lines Removed	64

---

Lean Declarations

✏️ Added: 47 declaration(s)

ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean (42)

• def GSSpecSet (k e : Nat) (ωs : Fin n ↪ F) (f : Fin n → F) : Set F[X]
• def RepresentsArkInput
• def boundedSearchParamSelector {maxM maxW : Nat}
• example : GSParamCert 2 5 1 (execParamsOfMultiplicityAndDegree 2 1 1 3)
• noncomputable def johnsonParamSelector : GSParamSelector where
• private def cPolynomialOfPoly (p : F[X]) : CompPoly.CPolynomial F
• private def constraintsFold {F : Type*} (points : Array (F × F)) (m : Nat) :
• private lemma foldl_push_size {α β : Type*} (g : Array β → α → β)
• private lemma foldl_size_add {α β : Type*} (step : Array β → α → Array β) (d : α → Nat)
• private lemma interpolationConstraints_eq_fold {F : Type*}
• private lemma length_filter_ofFn_eq_card {α : Type*} {n : Nat}
• private lemma list_foldl_count_false {α : Type*}
• private lemma list_foldl_count_true {α : Type*}
• private lemma mem_monomialGrid {D : Nat} {mm : Monomial} :
• private lemma sum_map_const {α : Type*} (l : List α) (c : Nat) :
• private lemma sum_range'_sub_two (m : Nat) :
• private theorem cPolynomialOfPoly_toPoly (p : F[X]) :
• private theorem degreeLt_cPolynomialOfPoly_of_degree_lt {p : F[X]}
• theorem agreement_card_add_hammingDist
• theorem candidateMismatchCount_represents_hammingDist
• theorem decodeWithParams_complete
• theorem decodeWithParams_sound
• theorem decode_complete
• theorem decode_sound
• theorem distinctXCoordinates_of_represents
• theorem interpolationConstraints_size {F : Type*}
• theorem interpolationMonomials_size (params : GSInterpParams) :
• theorem interpolationWitnessExists_of_capacity
• theorem length_of_represents
• theorem matchingPointCount_represents_card
• theorem mem_decodeWithParams_iff_degree_and_distance
• theorem mem_decodeWithParams_iff_mem_decoder_of_degree_lt
• theorem mem_decodeWithParams_iff_spec
• theorem mem_decode_iff_mem_decoder_of_degree_lt
• theorem mem_decode_iff_spec
• theorem paramsCert_of_johnson {k n e : Nat} (hjohnson : JohnsonSpecCondition k n e) :
• theorem paramsPassIntegerChecks_iff
• theorem passesCandidateDistance_represents_hammingDist
• theorem searchParamsUpTo_complete {maxM maxW k n e : Nat}
• theorem searchParamsUpTo_sound {maxM maxW k n e : Nat} {params : GSExecParams}
• theorem toPoly_degree_lt_of_degreeLt
• theorem toPoly_natDegree_lt_of_degreeLt

ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean (4)

• def JohnsonSpecCondition (k n e : Nat) : Prop
• def execParamsOfMultiplicityAndDegree
• def paramsPassIntegerChecks
• def searchParamsUpTo

ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean (1)

• lemma exists_multiplicity_of_johnson {k n e : ℕ}

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean: This new file, Correctness.lean, provides the correctness proofs connecting the executable CompPoly‑backed Guruswami–Sudan decoder to the ArkLib Reed–Solomon specification. It defines RepresentsArkInput and GSSpecSet to relate runtime input to the semantic specification, establishes the equivalence paramsPassIntegerChecks_iff for parameter certificates, and constructs both a bounded‑search and a non‑computable GSParamSelector (boundedSearchParamSelector, johnsonParamSelector). It proves interpolationWitnessExists_of_capacity and various counting lemmas (e.g., interpolationMonomials_size, interpolationConstraints_size) that discharge the interpolation‑existence hypothesis. The core results are the membership characterizations mem_decodeWithParams_iff_degree_and_distance, mem_decodeWithParams_iff_spec, mem_decode_iff_spec, and the corresponding soundness/completeness corollaries (decodeWithParams_sound, decodeWithParams_complete, decode_sound, decode_complete). Finally, compatibility theorems mem_decodeWithParams_iff_mem_decoder_of_degree_lt and mem_decode_iff_mem_decoder_of_degree_lt relate the decoder’s output to the existing specification decoder under an explicit degree bound.
• ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean: This new file adds the ArkLib integration layer for the CompPoly Guruswami-Sudan decoder. It defines the GSParamCert structure (certifying that executable parameters satisfy message degree, radius, multiplicity positivity, interpolation capacity, and enough agreement bound), the JohnsonSpecCondition proposition (Johnson-radius condition), the paramsPassIntegerChecks boolean, the execParamsOfMultiplicityAndDegree constructor, the searchParamsUpTo bounded search, and the GSParamSelector structure with soundness and completeness conditions. No sorry or admit are present.
• ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean: This diff extracts the existential argument from inside mem_decoder_of_dist into a new standalone lemma exists_multiplicity_of_johnson which states that under the Johnson radius condition e < n - √((k+1)·n) there exists a positive multiplicity m such that e/n < proximity_gap_johnson k n m. The body of mem_decoder_of_dist is then simplified to a one-line call to this new lemma, with a comment noting the delegation. All proofs are complete (no sorry or admit are added).
• 2 file(s) filtered as noise (lockfiles, generated, or trivial): ArkLib.lean, ArkLib/Data/CodingTheory/GuruswamiSudan.lean

---

Last updated: 2026-07-28 16:35 UTC.

[olympichek]

Happy to open a PR against formal-land:guruswami-sudan with exactly that, or to just leave it here if you would rather apply it yourself — it is three lines of work now that the diagnosis is done.

I just rebased the branch and applied your suggestions