Proof obligation for `decoder_mem_impl_dist` in `ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean`

[alexanderlhicks]

A proof in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem states a key "soundness" property of the Guruswami-Sudan decoder. It guarantees that for any polynomial p found in the output list of the decoder, the corresponding Reed-Solomon codeword p.eval ∘ ωs is "close" to the received word f.

• Goal: The Hamming distance Δ₀ between the received word f and the codeword generated by p is at most e.
• Hypotheses:
  • p ∈ decoder ... f: The polynomial p is one of the candidates returned by the decoder.
  • h_e : e ≤ n - Real.sqrt (k * n): This is a condition on the number of tolerated errors e, related to the Johnson bound for list decoding, which ensures the decoder's parameters can be chosen correctly.

In essence, the theorem asserts that the decoder does not produce spurious results; every polynomial it outputs corresponds to a message that could have been the original, given up to e errors in transmission.

Context

This theorem, along with its converse decoder_dist_impl_mem, forms the complete functional specification of the Guruswami-Sudan decoder. While decoder_dist_impl_mem establishes "completeness" (any polynomial that is close enough will be found), this theorem establishes "soundness" (any polynomial that is found is close enough).

The proof is not self-contained but relies on the underlying principles of the Guruswami-Sudan algorithm, which is implemented inside the opaque decoder. The algorithm works in two main stages:

1. Interpolation: Construct a non-zero bivariate polynomial Q(X,Y) that passes through all points (ωs i, f i) with high multiplicity r. The properties of Q are described in the GuruswamiSudan.Condition structure.
2. Root-finding: Find all factors of Q of the form Y - p(X) where p has a degree less than k. The set of these polynomials p is the output of the decoder.

This theorem connects the algebraic property of p (being related to a factor of Q) to the combinatorial property of its codeword (being close to f).

Proof Suggestion

The proof should be based on the properties of the interpolation polynomial Q that is implicitly constructed by the decoder. Since the decoder is opaque, you must reason from the principles of the algorithm it represents.

1. Start by introducing the bivariate polynomial Q from the interpolation step of the Guruswami-Sudan algorithm. The hypothesis h_in implies that p is in the decoder's output, which means Y - p(X) (formally (X : F[X][X]) - C p) must be a factor of Q.
2. Let S be the other factor, so Q = (Y - p(X)) * S.
3. Let E be the set of indices i where the received word f disagrees with the codeword from p, i.e., f i ≠ (p.eval ∘ ωs) i. The size of this set is |E| = Δ₀(f, p.eval ∘ ωs). The goal is to show |E| ≤ e.
4. Recall that Q is constructed to have a root of multiplicity at least r at each point (ωs i, f i). For any i ∈ E, we have f i - (p.eval ∘ ωs) i ≠ 0.
5. Use the multiplicity property of Q at these error points. By applying the Leibniz rule (product rule for higher derivatives) to the derivatives of Q = (Y - p(X)) * S with respect to Y, show that S must also have a root of multiplicity at least r at (ωs i, f i) for each i ∈ E.
6. This gives you a polynomial S with many high-multiplicity roots. The next step is to find an upper bound on |E|. The weighted degree of S is bounded by the weighted degree of Q, which is at most D. A lemma establishing Bivariate.weightedDegree S 1 (k-1) ≤ D would be useful here.
7. A fundamental result, often seen as a generalization of the Schwartz-Zippel lemma, states that a non-zero polynomial cannot have too many roots, even when counted with multiplicity. This principle can be used to bound |E| * r in terms of the degrees of S.
8. This bound will lead to an inequality that constrains |E|. If you assume for contradiction that |E| > e, the number of constraints imposed on S by the high-multiplicity roots will exceed the number of its coefficients (determined by its weighted degree). This would force S to be the zero polynomial, which in turn implies Q is zero, contradicting the first step of the Guruswami-Sudan algorithm.
9. Conclude that the assumption |E| > e must be false, which proves the theorem.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem decoder_mem_impl_dist
  {k r D e : ℕ}
  (h_e : e ≤ n - Real.sqrt (k * n))
  {ωs : Fin n ↪ F}
  {f : Fin n → F}
  {p : F[X]}
  (h_in : p ∈ decoder k r D e ωs f)
  :
  Δ₀(f, p.eval ∘ ωs) ≤ e := by sorry

[FawadHa1der]

Me with some AI help is working on this one

[FawadHa1der]

Solution part of #298