Reed–Solomon list decoding with a hint

List decoding a Reed–Solomon codeword from a small fraction of agreements returns several candidate polynomials. In local list decoding of Reed–Muller codes [STV01] the right candidate is singled out by its value a = P(τ) at one further point, supplied as advice. This module computes the value P(0) of that candidate from the received word, τ and a alone, with linear algebra and Newton iteration, and no root finding or factoring.

Let Q be the Sudan interpolant of least Y-degree of the received word (Cslib.Code.Sudan.interpolant). If P has degree at most d and more than D agreements, then Q = (Y - P) * S with S(X, P(X)) ≠ 0 of degree at most D - d (Cslib.Code.Sudan.exists_eq_mul_eval_ne_zero), so for all but D - d points τ the root P is simple at (τ, P(τ)): ∂Q/∂Y (τ, P(τ)) = S(τ, P(τ)) ≠ 0. Then the Taylor coefficients of P at τ are determined one at a time by Newton's (Hensel's) rule: if A has degree less than k ≤ d and agrees with P(X + τ) below degree k, then the coefficient of X ^ k in P(X + τ) is -[X ^ k] Q(X + τ, A(X)) / ∂Q/∂Y (τ, a) (Cslib.Code.henselCoeff_eq). The coefficient [X ^ k] Q(X + τ, A(X)) is a fixed linear combination of the values Q(s + τ, A(s)) for s ∈ F (Cslib.Code.sum_coeffWeight_mul_eval), because this polynomial has degree at most D < |F|. So the whole computation Cslib.Code.hintDecode is an arithmetic computation on the received word, the hint and fixed constants, with no other branching than the tests for zero in the elimination; the decoded value is correct for all but D - d of the hint points (Cslib.Code.card_hintDecode_ne_le).

Main definitions

• Cslib.Code.coeffWeight: the weights extracting a coefficient from the values on all of F.
• Cslib.Code.henselCoeff: the coefficient chosen by one Newton step.
• Cslib.Code.henselTrunc: the Newton iteration from a hint.
• Cslib.Code.henselSeq: the coefficients chosen by the Newton iteration.
• Cslib.Code.henselValue: the value at 0 of the lifted root.
• Cslib.Code.hintDecode: Sudan decoding with a hint.

Main results

• Cslib.Code.sum_coeffWeight_mul_eval: coefficients from values.
• Cslib.Code.henselValue_eq: Newton iteration recovers a simple root of degree at most d.
• Cslib.Code.card_hintDecode_ne_le: decoding with a hint is correct at all but D - d hint points.

References

• [M. Sudan, L. Trevisan, S. Vadhan, Pseudorandom generators without the XOR lemma] [STV01]
• M. Sudan, Decoding of Reed Solomon codes beyond the error-correction bound

Coefficients from values

noncomputable def Cslib.Code.coeffWeight {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (k : ℕ) (s : F) : F

The weights extracting the coefficient of X ^ k from the values at all points of F: the coefficients of the Lagrange basis polynomials of F.

theorem Cslib.Code.sum_coeffWeight_mul_eval {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {R : Polynomial F} (hR : R.natDegree < Fintype.card F) (k : ℕ) : ∑ s : F, coeffWeight k s * Polynomial.eval s R = R.coeff k

Coefficients from values. A polynomial of degree less than |F| has coefficient ∑ s, coeffWeight k s * R(s) at X ^ k.

Newton iteration

noncomputable def Cslib.Code.henselCoeff {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Q : Polynomial (Polynomial F)) (τ lam : F) (A : Polynomial F) (k : ℕ) : F

The coefficient chosen by one Newton step: -[X ^ k] Q(X + τ, A(X)) / λ, computed from the values of Q(X + τ, A(X)) on F.

noncomputable def Cslib.Code.henselTrunc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Q : Polynomial (Polynomial F)) (τ a lam : F) : ℕ → Polynomial F

Newton iteration from a hint. Starting from the constant a, the step to k + 1 adds the monomial henselCoeff Q τ lam A (k + 1) * X ^ (k + 1).

noncomputable def Cslib.Code.henselSeq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Q : Polynomial (Polynomial F)) (τ a lam : F) : ℕ → F

The coefficients chosen by the Newton iteration: a and then the successive steps.

theorem Cslib.Code.henselTrunc_eq_sum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Q : Polynomial (Polynomial F)) (τ a lam : F) (k : ℕ) : henselTrunc Q τ a lam k = ∑ i ∈ Finset.range (k + 1), Polynomial.C (henselSeq Q τ a lam i) * Polynomial.X ^ i

The iterate to degree k is the polynomial with the first k + 1 chosen coefficients.

theorem Cslib.Code.eval_henselTrunc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Q : Polynomial (Polynomial F)) (τ a lam : F) (k : ℕ) (s : F) : Polynomial.eval s (henselTrunc Q τ a lam k) = ∑ i ∈ Finset.range (k + 1), henselSeq Q τ a lam i * s ^ i

The value at s of the iterate to degree k.

noncomputable def Cslib.Code.henselValue {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Q : Polynomial (Polynomial F)) (τ a : F) (d : ℕ) : F

The value at 0 of the root lifted from the hint a at τ, to degree d.

theorem Cslib.Code.henselCoeff_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d D : ℕ} {Q : Polynomial (Polynomial F)} (hQ : ∀ (a b : ℕ), (Q.coeff b).coeff a ≠ 0 → a + d * b ≤ D) (hD : D < Fintype.card F) {P : Polynomial F} (hQP : Polynomial.eval P Q = 0) {τ : F} (hlam : Polynomial.evalEval τ (Polynomial.eval τ P) (Polynomial.derivative Q) ≠ 0) {A : Polynomial F} {k : ℕ} (hk : k < d) (hA : A.natDegree ≤ k) (hAP : ∀ i ≤ k, A.coeff i = ((Polynomial.taylor τ) P).coeff i) : henselCoeff Q τ (Polynomial.evalEval τ (Polynomial.eval τ P) (Polynomial.derivative Q)) A (k + 1) = ((Polynomial.taylor τ) P).coeff (k + 1)

One Newton step. Let Q(X, P(X)) = 0 with P of degree at most d, let the monomials of Q have (1, d)-weighted degree at most D < |F|, and let λ = ∂Q/∂Y (τ, P(τ)) ≠ 0. If A has degree at most k < d and agrees with P(X + τ) below degree k + 1, then the Newton step returns the coefficient of X ^ (k + 1) in P(X + τ).

theorem Cslib.Code.henselValue_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d D : ℕ} {Q : Polynomial (Polynomial F)} (hQ : ∀ (a b : ℕ), (Q.coeff b).coeff a ≠ 0 → a + d * b ≤ D) (hD : D < Fintype.card F) {P : Polynomial F} (hP : P.natDegree ≤ d) (hQP : Polynomial.eval P Q = 0) {τ : F} (hlam : Polynomial.evalEval τ (Polynomial.eval τ P) (Polynomial.derivative Q) ≠ 0) : henselValue Q τ (Polynomial.eval τ P) d = Polynomial.eval 0 P

Newton iteration recovers a simple root. Let Q(X, P(X)) = 0 with P of degree at most d, let the monomials of Q have (1, d)-weighted degree at most D < |F|, and let ∂Q/∂Y (τ, P(τ)) ≠ 0. Then Newton iteration from the hint P(τ) returns P(0).

theorem Cslib.Code.evalEval_derivative_bivariateOf {F : Type u_1} [Field F] (M : Finset (ℕ × ℕ)) (c : ℕ × ℕ → F) (x y : F) : Polynomial.evalEval x y (Polynomial.derivative (Sudan.bivariateOf M c)) = ∑ m ∈ M, c m * (↑m.2 * x ^ m.1 * y ^ (m.2 - 1))

The derivative in Y of bivariateOf M c at (x, y).

Decoding with a hint

noncomputable def Cslib.Code.hintDecode {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {ι : Type u_2} [Fintype ι] (α w : ι → F) (d D : ℕ) (τ a : F) : F

Sudan decoding with a hint. The value at 0 of the root of the least-Y-degree Sudan interpolant of the received word w (with evaluation points α), lifted by Newton iteration from the hint a at τ.

theorem Cslib.Code.card_hintDecode_ne_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {ι : Type u_2} [Fintype ι] {α w : ι → F} {d D : ℕ} (hα : Function.Injective α) (hd : 1 ≤ d) (hn : Fintype.card ι < (Sudan.monomials d D).card) (hD : D < Fintype.card F) {P : Polynomial F} (hP : P.natDegree ≤ d) (hagree : D < {i : ι | Polynomial.eval (α i) P = w i}.card) : {τ : F | hintDecode α w d D τ (Polynomial.eval τ P) ≠ Polynomial.eval 0 P}.card ≤ D - d

Decoding with a hint is correct at almost every hint point. With distinct points, d ≥ 1, more monomials of (1, d)-weighted degree at most D than points, and D < |F|: if P has degree at most d and agrees with the received word at more than D points, then hintDecode α w d D τ (P τ) = P 0 for all but at most D - d points τ.