Reed–Solomon codes

21 fully proved

The code

DefinitionReed-Solomon encoder#✓fully proved

For a field \(F\) and points \(\alpha_0, \dots, \alpha_{n-1} \in F\), the encoding of a polynomial \(p \in F[X]\) is the word \((p(\alpha_0), \dots, p(\alpha_{n-1}))\) in \(F^n\).

noncomputable def encode (α : Fin n → F) (p : F[X]) : Fin n → F := fun i ↦ p.eval (α i)

Used by 14

Used byBerlekamp-Welch decoder · Berlekamp-Welch corrects every error of weight at most \(\lfloor (n-k)/2 \rfloor\) · The decoder fails exactly when no codeword is close · What the decoder returns · The quotient of a key-equation solution is the message · Reed-Solomon encoder as a linear map · Every solution of the key equations reveals the message · A low-weight Reed-Solomon codeword · The key equations are solvable · The Reed-Solomon encoder is injective on low-degree polynomials · Nonzero Reed-Solomon codewords are heavy · Lower bound on the minimum distance of a Reed-Solomon code · Reed-Solomon codes are MDS · Reed-Solomon codes meet the Singleton bound

DefinitionReed-Solomon encoder as a linear map#✓fully proved

For a field \(F\) and points \(\alpha_0, \dots, \alpha_{n-1} \in F\), the \(F\)-linear map \(F[X] \to F^n\) sending a polynomial \(p\) to \((p(\alpha_0), \dots, p(\alpha_{n-1}))\).

noncomputable def encodeLin (α : Fin n → F) : F[X] →ₗ[F] (Fin n → F) where
  toFun := encode α
  map_add' p q := funext fun i ↦ eval_add
  map_smul' c p := funext fun i ↦ by simp [encode, smul_eq_C_mul]

Uses 1 · Used by 3

Statement usesReed-Solomon encoder

Used byReed-Solomon code · Dimension of a Reed-Solomon code · The Reed-Solomon encoder is injective on low-degree polynomials

DefinitionReed-Solomon code#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) and let \(k\) be a natural number. The Reed-Solomon code \(\mathrm{RS}(\alpha, k)\) is the linear code of length \(n\) over \(F\) consisting of the words \((p(\alpha_0), \dots, p(\alpha_{n-1}))\) for the polynomials \(p \in F[X]\) of degree less than \(k\).

noncomputable def code (α : Fin n → F) (k : ℕ) : LinearCode F (Fin n) :=
  (degreeLT F k).map (encodeLin α)

Uses 2 · Used by 4

Statement usesLinear code · Reed-Solomon encoder as a linear map

Used byDimension of a Reed-Solomon code · Lower bound on the minimum distance of a Reed-Solomon code · Reed-Solomon codes are MDS · Reed-Solomon codes meet the Singleton bound

TheoremRoot count at distinct points#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1}\) be pairwise distinct elements of \(F\), and let \(p \in F[X]\) be a nonzero polynomial. Then the number of indices \(i < n\) with \(p(\alpha_i) = 0\) is at most the degree of \(p\).

theorem card_eval_eq_zero_le {α : Fin n → F} (hα : Function.Injective α) {p : F[X]}
    (hp : p ≠ 0) : #{i | p.eval (α i) = 0} ≤ p.natDegree

Used by 2

Used byEvery solution of the key equations reveals the message · Nonzero Reed-Solomon codewords are heavy

TheoremNonzero Reed-Solomon codewords are heavy#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct and let \(k \le n\). For every nonzero polynomial \(p \in F[X]\) of degree less than \(k\), the encoding \((p(\alpha_0), \dots, p(\alpha_{n-1}))\) has at least \(n - k + 1\) nonzero coordinates.

theorem le_hammingNorm_encode {α : Fin n → F} (hα : Function.Injective α) (hkn : k ≤ n)
    {p : F[X]} (hp : p ≠ 0) (hdeg : p.degree < k) : n - k + 1 ≤ hammingNorm (encode α p)

Uses 2 · Used by 3

Statement usesReed-Solomon encoder

Proof usesRoot count at distinct points

Used byThe Reed-Solomon encoder is injective on low-degree polynomials · Lower bound on the minimum distance of a Reed-Solomon code · Reed-Solomon codes are MDS

TheoremThe Reed-Solomon encoder is injective on low-degree polynomials#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct and let \(k \le n\). If two polynomials \(p, q \in F[X]\) of degree less than \(k\) satisfy \(p(\alpha_i) = q(\alpha_i)\) for every \(i < n\), then \(p = q\).

theorem injOn_encode {α : Fin n → F} (hα : Function.Injective α) (hkn : k ≤ n) :
    Set.InjOn (encode α) (degreeLT F k : Set F[X])

Uses 3 · Used by 1

Statement usesReed-Solomon encoder

Proof usesReed-Solomon encoder as a linear map · Nonzero Reed-Solomon codewords are heavy

Used byDimension of a Reed-Solomon code

TheoremDimension of a Reed-Solomon code#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct and let \(k \le n\). The Reed-Solomon code of the points \(\alpha\) with parameter \(k\) has dimension \(k\) over \(F\).

theorem finrank_code {α : Fin n → F} (hα : Function.Injective α) (hkn : k ≤ n) :
    finrank F (code α k) = k

Uses 4 · Used by 1

Statement usesLinear code · Reed-Solomon code

Proof usesReed-Solomon encoder as a linear map · The Reed-Solomon encoder is injective on low-degree polynomials

Used byReed-Solomon codes meet the Singleton bound

TheoremLower bound on the minimum distance of a Reed-Solomon code#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct and let \(k \in \mathbb{N}\). The Reed-Solomon code of the points \(\alpha\) with parameter \(k\) has minimum distance at least \(\max(n - k, 0) + 1\).

theorem le_minDist_code {α : Fin n → F} (hα : Function.Injective α) :
    ((n - k + 1 : ℕ) : ℕ∞) ≤ (code α k).minDist

Uses 7 · Used by 2

Statement usesMinimum distance · Reed-Solomon code

Proof usesLinear code · Minimum distance equals minimum weight · Minimum weight · Reed-Solomon encoder · Nonzero Reed-Solomon codewords are heavy

Used byReed-Solomon codes are MDS · Reed-Solomon codes meet the Singleton bound

TheoremA low-weight Reed-Solomon codeword#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) (not necessarily distinct) and let \(1 \le k \le n\). There is a nonzero polynomial \(p \in F[X]\) of degree less than \(k\) whose encoding \((p(\alpha_0), \dots, p(\alpha_{n-1}))\) has at most \(n - k + 1\) nonzero coordinates.

One such polynomial is \(\prod_{j < k - 1} (X - \alpha_j)\).

theorem exists_codeword_hammingNorm_le (α : Fin n → F) (hk : 1 ≤ k) (hkn : k ≤ n) :
    ∃ p : F[X], p ≠ 0 ∧ p.degree < k ∧ hammingNorm (encode α p) ≤ n - k + 1

Uses 1 · Used by 1

Statement usesReed-Solomon encoder

Used byReed-Solomon codes are MDS

TheoremReed-Solomon codes are MDS#✓fully proved

Let \(F\) be a field (not necessarily finite), let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct and let \(1 \le k \le n\). The Reed-Solomon code of the points \(\alpha\) with parameter \(k\) has minimum distance exactly \(n - k + 1\).

The lower bound counts roots; the upper bound is attained by the encoding of \(\prod_{j < k - 1} (X - \alpha_j)\).

theorem minDist_code {α : Fin n → F} (hα : Function.Injective α) (hk : 1 ≤ k) (hkn : k ≤ n) :
    (code α k).minDist = (n - k + 1 : ℕ)

Uses 7

Statement usesMinimum distance · Reed-Solomon code

Proof usesLinear code · Reed-Solomon encoder · A low-weight Reed-Solomon codeword · Nonzero Reed-Solomon codewords are heavy · Lower bound on the minimum distance of a Reed-Solomon code

TheoremReed-Solomon codes meet the Singleton bound#✓fully proved

Let \(F\) be a finite field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct and let \(1 \le k \le n\). The Reed-Solomon code \(C\) of the points \(\alpha\) with parameter \(k\) has minimum distance \(d = n - \dim C + 1\), so the Singleton bound \(d \le n - \dim C + 1\) for linear codes holds with equality.

The upper bound is the Singleton bound for linear codes; the lower bound counts roots.

theorem minDist_code_eq_singleton [Finite F] {α : Fin n → F} (hα : Function.Injective α)
    (hk : 1 ≤ k) (hkn : k ≤ n) :
    (code α k).minDist = (n - finrank F (code α k) + 1 : ℕ)

Uses 7

Statement usesLinear code · Minimum distance · Reed-Solomon code

Proof usesSingleton bound for linear codes · Reed-Solomon encoder · Dimension of a Reed-Solomon code · Lower bound on the minimum distance of a Reed-Solomon code

Berlekamp-Welch decoding

DefinitionBerlekamp-Welch key equations#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\), let \(k, e \in \mathbb{N}\) and let \(y \in F^n\) be a received word. A pair of polynomials \((Q, E)\) over \(F\) solves the key equations for \(y\) when \(E\) is monic of degree \(e\), \(Q\) has degree less than \(e + k\), and \(Q(\alpha_i) = y_i E(\alpha_i)\) for every \(i < n\).

def IsKeySolution (α : Fin n → F) (k e : ℕ) (y : Fin n → F) (Q E : F[X]) : Prop :=
  E.Monic ∧ E.natDegree = e ∧ Q.degree < (e + k : ℕ) ∧ ∀ i, Q.eval (α i) = y i * E.eval (α i)

Used by 6

Used byWhat the decoder returns · The quotient of a key-equation solution is the message · Every solution of the key equations reveals the message · The key equations are solvable · Solver for the key equations · A key-equation solver by choice

TheoremThe key equations are solvable#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) and let \(p \in F[X]\) have degree less than \(k\). If a received word \(y \in F^n\) differs from the encoding \((p(\alpha_0), \dots, p(\alpha_{n-1}))\) in at most \(e\) coordinates, then the Berlekamp-Welch key equations for \(y\) with parameters \(k\) and \(e\) have a solution \((Q, E)\).

A solution is the error locator polynomial, padded to degree \(e\), together with \(Q = pE\).

theorem exists_isKeySolution (α : Fin n → F) {p : F[X]} (hp : p.degree < k) {y : Fin n → F}
    (he : hammingDist y (encode α p) ≤ e) : ∃ Q E, IsKeySolution α k e y Q E

Uses 2 · Used by 1

Statement usesBerlekamp-Welch key equations · Reed-Solomon encoder

Used byWhat the decoder returns

TheoremEvery solution of the key equations reveals the message#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct and let \(k, e\) be natural numbers with \(2e + k \le n\). Let \(p \in F[X]\) have degree less than \(k\), and let \(y \in F^n\) be within Hamming distance \(e\) of \((p(\alpha_0), \dots, p(\alpha_{n-1}))\). If \((Q, E)\) solves the key equations for \(y\) (\(E\) is monic of degree \(e\), \(\deg Q < e + k\), and \(Q(\alpha_i) = y_i E(\alpha_i)\) for all \(i < n\)), then \(Q = pE\).

The difference \(Q - pE\) has degree less than \(e + k\) and vanishes at the at least \(n - e \ge e + k\) error-free points.

theorem eq_mul_of_isKeySolution {α : Fin n → F} (hα : Function.Injective α) (h2e : 2 * e + k ≤ n)
    {p : F[X]} (hp : p.degree < k) {y : Fin n → F} (he : hammingDist y (encode α p) ≤ e)
    {Q E : F[X]} (hsol : IsKeySolution α k e y Q E) : Q = p * E

Uses 3 · Used by 1

Statement usesBerlekamp-Welch key equations · Reed-Solomon encoder

Proof usesRoot count at distinct points

Used byThe quotient of a key-equation solution is the message

TheoremThe quotient of a key-equation solution is the message#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct and let \(k, e\) be natural numbers with \(2e + k \le n\). Let \(p \in F[X]\) have degree less than \(k\), and let \(y \in F^n\) be within Hamming distance \(e\) of \((p(\alpha_0), \dots, p(\alpha_{n-1}))\). If \((Q, E)\) solves the key equations for \(y\) (\(E\) is monic of degree \(e\), \(\deg Q < e + k\), and \(Q(\alpha_i) = y_i E(\alpha_i)\) for all \(i < n\)), then the quotient of \(Q\) by \(E\) is \(p\).

theorem divByMonic_eq_of_isKeySolution {α : Fin n → F} (hα : Function.Injective α)
    (h2e : 2 * e + k ≤ n) {p : F[X]} (hp : p.degree < k) {y : Fin n → F}
    (he : hammingDist y (encode α p) ≤ e) {Q E : F[X]} (hsol : IsKeySolution α k e y Q E) :
    Q /ₘ E = p

Uses 3 · Used by 1

Statement usesBerlekamp-Welch key equations · Reed-Solomon encoder

Proof usesEvery solution of the key equations reveals the message

Used byWhat the decoder returns

StructureSolver for the key equations#✓fully proved

For a field \(F\), points \(\alpha_0, \dots, \alpha_{n-1} \in F\) and parameters \(k, e \in \mathbb{N}\), a solver for the Berlekamp-Welch key equations is a procedure that takes a received word \(y \in F^n\) and either returns a pair of polynomials \((Q, E)\) over \(F\) or reports failure, such that every returned pair solves the key equations for \(y\), and a pair is returned whenever the key equations for \(y\) have a solution.

(The key equations are a linear system in the coefficients of \(Q\) and of \(E\); Gaussian elimination is a solver.)

structure KeySolver (α : Fin n → F) (k e : ℕ) where
  /-- The solving procedure. -/
  solve : (Fin n → F) → Option (F[X] × F[X])
  /-- Returned pairs solve the key equations. -/
  sound : ∀ y QE, solve y = some QE → IsKeySolution α k e y QE.1 QE.2
  /-- A solution is returned whenever one exists. -/
  complete : ∀ y, (∃ Q E, IsKeySolution α k e y Q E) → (solve y).isSome

Uses 1 · Used by 5

Statement usesBerlekamp-Welch key equations

Used byBerlekamp-Welch decoder · Berlekamp-Welch corrects every error of weight at most \(\lfloor (n-k)/2 \rfloor\) · The decoder fails exactly when no codeword is close · What the decoder returns · A key-equation solver by choice

DefinitionA key-equation solver by choice#✓fully proved

For points \(\alpha_0, \dots, \alpha_{n-1}\) in a field \(F\) and natural numbers \(k\) and \(e\), this is the solver for the key equations that, on a received word \(y \in F^n\), returns a pair \((Q, E)\) of polynomials solving the key equations for \(y\) (that is, \(E\) is monic of degree \(e\), \(\deg Q < e + k\) and \(Q(\alpha_i) = y_i E(\alpha_i)\) for all \(i\)), picked by the axiom of choice, whenever such a pair exists, and reports failure otherwise.

noncomputable def KeySolver.ofChoice (α : Fin n → F) (k e : ℕ) : KeySolver α k e where
  solve y := by
    classical
    exact if h : ∃ Q E, IsKeySolution α k e y Q E then some (h.choose, h.choose_spec.choose)
      else none
  sound y QE h := by
    classical
    split_ifs at h with hex
    · cases h
      exact hex.choose_spec.choose_spec
  complete y hex := by
    classical
    simp [hex]

Uses 2

Statement usesBerlekamp-Welch key equations · Solver for the key equations

DefinitionBerlekamp-Welch decoder#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\), let \(k, e\) be natural numbers and let \(S\) be a solver for the key equations with error budget \(e\). On a received word \(y \in F^n\) the decoder runs \(S\) on \(y\) and reports failure if \(S\) returns nothing. If \(S\) returns a pair \((Q, E)\) (the solver guarantees that \(E\) is monic), let \(q\) be the quotient of \(Q\) by \(E\); the decoder returns \(q\) if \(q\) has degree less than \(k\) and the Hamming distance between \(y\) and \((q(\alpha_0), \dots, q(\alpha_{n-1}))\) is at most \(e\), and reports failure otherwise.

Its only nontrivial step is the solver.

noncomputable def decode {α : Fin n → F} (S : KeySolver α k e) (y : Fin n → F) : Option F[X] :=
  (S.solve y).bind fun QE ↦
    if (QE.1 /ₘ QE.2).degree < k ∧ hammingDist y (encode α (QE.1 /ₘ QE.2)) ≤ e then
      some (QE.1 /ₘ QE.2)
    else none

Uses 2 · Used by 3

Statement usesSolver for the key equations · Reed-Solomon encoder

Used byBerlekamp-Welch corrects every error of weight at most \(\lfloor (n-k)/2 \rfloor\) · The decoder fails exactly when no codeword is close · What the decoder returns

TheoremWhat the decoder returns#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct, let \(k, e\) be natural numbers with \(2e + k \le n\) (the unique-decoding regime), and let \(S\) be a solver for the key equations with error budget \(e\). For every polynomial \(p \in F[X]\) and every received word \(y \in F^n\), the Berlekamp-Welch decoder with solver \(S\) returns \(p\) on \(y\) if and only if \(p\) has degree less than \(k\) and the Hamming distance between \(y\) and \((p(\alpha_0), \dots, p(\alpha_{n-1}))\) is at most \(e\).

theorem decode_eq_some_iff {α : Fin n → F} (hα : Function.Injective α) (h2e : 2 * e + k ≤ n)
    (S : KeySolver α k e) {p : F[X]} {y : Fin n → F} :
    decode S y = some p ↔ p.degree < k ∧ hammingDist y (encode α p) ≤ e

Uses 6 · Used by 2

Statement usesSolver for the key equations · Berlekamp-Welch decoder · Reed-Solomon encoder

Proof usesBerlekamp-Welch key equations · The quotient of a key-equation solution is the message · The key equations are solvable

Used byBerlekamp-Welch corrects every error of weight at most \(\lfloor (n-k)/2 \rfloor\) · The decoder fails exactly when no codeword is close

TheoremThe decoder fails exactly when no codeword is close#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct, let \(k, e\) be natural numbers with \(2e + k \le n\), and let \(S\) be a solver for the key equations with error budget \(e\). For every received word \(y \in F^n\), the Berlekamp-Welch decoder with solver \(S\) reports failure on \(y\) if and only if, for every polynomial \(p \in F[X]\) of degree less than \(k\), the Hamming distance between \(y\) and \((p(\alpha_0), \dots, p(\alpha_{n-1}))\) is greater than \(e\).

theorem decode_eq_none_iff {α : Fin n → F} (hα : Function.Injective α) (h2e : 2 * e + k ≤ n)
    (S : KeySolver α k e) {y : Fin n → F} :
    decode S y = none ↔ ∀ p : F[X], p.degree < k → e < hammingDist y (encode α p)

Uses 4

Statement usesSolver for the key equations · Berlekamp-Welch decoder · Reed-Solomon encoder

Proof usesWhat the decoder returns

TheoremBerlekamp-Welch corrects every error of weight at most \(\lfloor (n-k)/2 \rfloor\)#✓fully proved

Let \(F\) be a field, let \(\alpha_0, \dots, \alpha_{n-1} \in F\) be pairwise distinct, let \(k \le n\), put \(t = \lfloor (n-k)/2 \rfloor\), and let \(S\) be a solver for the key equations with error budget \(t\). For every polynomial \(p \in F[X]\) of degree less than \(k\) and every error word \(\varepsilon \in F^n\) with at most \(t\) nonzero entries, the Berlekamp-Welch decoder with solver \(S\), run on the received word \((p(\alpha_0) + \varepsilon_0, \dots, p(\alpha_{n-1}) + \varepsilon_{n-1})\), returns \(p\).

theorem decode_encode_add {α : Fin n → F} (hα : Function.Injective α) (hkn : k ≤ n)
    (S : KeySolver α k ((n - k) / 2)) {p : F[X]} (hp : p.degree < k) {err : Fin n → F}
    (herr : hammingNorm err ≤ (n - k) / 2) : decode S (encode α p + err) = some p

Uses 5

Statement usesSolver for the key equations · Berlekamp-Welch decoder · Reed-Solomon encoder

Proof usesWhat the decoder returns · Hamming distance is the weight of the difference

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.