Linear codes

AbbreviationLinear code#✓fully proved

Let \(F\) be a field and \(\iota\) an index set, not necessarily finite. A linear code over \(F\) with coordinates indexed by \(\iota\) is an \(F\)-linear subspace of the space of words, the functions \(\iota \to F\).

abbrev LinearCode (F : Type*) [Field F] (ι : Type*) := Submodule F (ι → F)

Used by 35

Used byThe Hamming (7,4) code · The decoder corrects every error of weight at most 1 · Every single-bit error is corrected · The decoder always outputs a codeword · The Hamming code is perfect · No codeword is closer than the Hamming decoder's output · Minimum distance of the Hamming (7,4) code · The Hamming generator matrix generates the Hamming code · The Hamming bound is attained · Hamming bound for the Hamming (7,4) code · The Hamming (7,4) code has minimum weight at least 3 · Number of codewords of a linear code · Dual code · Dual of the code generated by a matrix · Dual of the code with a given parity-check matrix · Dimension of the dual code · Singleton bound for linear codes, dimension form · Minimum distance · Minimum distance equals minimum weight · Minimum distance is at most the length · Singleton bound for linear codes · Minimum weight · Code generated by a matrix · Generator/parity-check duality · Code with a given parity-check matrix · Hamming bound for linear codes · The syndrome depends only on the error · Syndrome decoding corrects every error of weight at most \(t\) · Syndrome decoding up to half the minimum distance · Systematic generator and parity-check matrices · Reed-Solomon code · Dimension 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

29 fully proved

Generator and parity-check matrices

DefinitionEncoder of a generator matrix#✓fully proved

Let \(G\) be a \(\kappa \times \iota\) matrix over a field \(F\), with \(\kappa\) finite. The encoder of \(G\) sends a message \(m \in F^\kappa\) to the word \(mG \in F^\iota\) given by \((mG)_j = \sum_{k \in \kappa} m_k G_{kj}\), the combination of the rows of \(G\) with coefficients \(m\).

def encode (G : Matrix κ ι F) (m : κ → F) : ι → F := m ᵥ* G

Used by 8

Used byEvery single-bit error is corrected · Encoder of the Hamming code · Minimum distance of the Hamming (7,4) code · The Hamming generator matrix generates the Hamming code · Dual of the code generated by a matrix · The systematic encoder copies the message · Generator/parity-check duality · Systematic generator and parity-check matrices

DefinitionCode generated by a matrix#✓fully proved

Let \(F\) be a field, \(\kappa\) a finite index set, \(\iota\) any index set and \(G\) a \(\kappa \times \iota\) matrix over \(F\). The code generated by \(G\) is the linear code of all words \(m G\) with \(m : \kappa \to F\), the image of the encoder \(m \mapsto m G\); equivalently, the span of the rows of \(G\).

def ofGenerator (G : Matrix κ ι F) : LinearCode F ι := LinearMap.range G.vecMulLinear

Uses 1 · Used by 8

Statement usesLinear code

Used byEvery single-bit error is corrected · Minimum distance of the Hamming (7,4) code · The Hamming generator matrix generates the Hamming code · The Hamming bound is attained · Dual of the code generated by a matrix · Dual of the code with a given parity-check matrix · Generator/parity-check duality · Systematic generator and parity-check matrices

DefinitionSyndrome#✓fully proved

Let \(F\) be a field, \(\iota\) a finite set and \(\rho\) a set. For a matrix \(H \in F^{\rho \times \iota}\) (a parity-check matrix) and a word \(y \in F^\iota\), the syndrome of \(y\) is the vector \(Hy \in F^\rho\).

def syndrome (H : Matrix ρ ι F) (y : ι → F) : ρ → F := H *ᵥ y

Used by 13

Used bySyndrome decoder of the Hamming code · The decoder always outputs a codeword · The syndrome of a single-bit error locates it · The Hamming decoder's syndrome table is correct · The Hamming (7,4) code has minimum weight at least 3 · Dual of the code generated by a matrix · Existence of correct syndrome tables · Syndrome table correct up to a radius · Generator/parity-check duality · Syndrome table by exhaustive search · The syndrome depends only on the error · Syndrome decoding · Syndrome decoding corrects every error of weight at most \(t\)

DefinitionCode with a given parity-check matrix#✓fully proved

Let \(F\) be a field, \(\iota\) a finite index set, \(\rho\) any index set and \(H\) a \(\rho \times \iota\) matrix over \(F\). The code with parity-check matrix \(H\) is the linear code of all words \(c : \iota \to F\) whose syndrome \(H c\) is zero, that is, the kernel of \(c \mapsto H c\).

def ofParityCheck (H : Matrix ρ ι F) : LinearCode F ι := LinearMap.ker H.mulVecLin

Uses 1 · Used by 9

Statement usesLinear code

Used byThe Hamming (7,4) code · The Hamming generator matrix generates the Hamming code · Dual of the code generated by a matrix · Dual of the code with a given parity-check matrix · Generator/parity-check duality · The syndrome depends only on the error · Syndrome decoding corrects every error of weight at most \(t\) · Syndrome decoding up to half the minimum distance · Systematic generator and parity-check matrices

TheoremThe syndrome depends only on the error#✓fully proved

Let \(F\) be a field, \(\iota\) a finite set and \(H\) a parity-check matrix over \(F\) with columns indexed by \(\iota\). If \(c \in F^\iota\) is a codeword of the code with parity-check matrix \(H\) and \(e \in F^\iota\) is any word, then the received word \(c + e\) has the same syndrome as \(e\), that is, \(H(c + e) = He\).

theorem syndrome_add_of_mem {H : Matrix ρ ι F} {c : ι → F} (hc : c ∈ ofParityCheck H)
    (e : ι → F) : syndrome H (c + e) = syndrome H e

Uses 3 · Used by 1

Statement usesLinear code · Code with a given parity-check matrix · Syndrome

Used bySyndrome decoding corrects every error of weight at most \(t\)

TheoremGenerator/parity-check duality#✓fully proved

Let \(F\) be a field, \(\kappa\) and \(\iota\) finite index sets and \(\rho\) any index set, and let \(G\) be a \(\kappa \times \iota\) matrix and \(H\) a \(\rho \times \iota\) matrix over \(F\). The code generated by \(G\) equals the code with parity-check matrix \(H\) if and only if \(G H^{\mathsf{T}} = 0\) and \(\operatorname{rank} G + \operatorname{rank} H\) equals \(|\iota|\), the length of the code.

theorem ofGenerator_eq_ofParityCheck_iff {G : Matrix κ ι F}
    {H : Matrix ρ ι F} :
    ofGenerator G = ofParityCheck H ↔ G * Hᵀ = 0 ∧ G.rank + H.rank = Fintype.card ι

Uses 5 · Used by 2

Statement usesLinear code · Code generated by a matrix · Code with a given parity-check matrix

Proof usesEncoder of a generator matrix · Syndrome

Used byThe Hamming generator matrix generates the Hamming code · Systematic generator and parity-check matrices

Systematic form

TheoremThe systematic encoder copies the message#✓fully proved

Let \(F\) be a field, \(\kappa\) a finite set and \(A\) a \(\kappa \times \rho\) matrix over \(F\). For the systematic generator matrix \(G = [I \mid A]\), whose columns are indexed by the disjoint union \(\kappa \sqcup \rho\), the encoding \(mG\) of every message \(m \in F^\kappa\) agrees with \(m\) on the coordinates in \(\kappa\): \((mG)_i = m_i\) for every \(i \in \kappa\).

theorem encode_fromCols_one_inl (A : Matrix κ ρ F) (m : κ → F) (i : κ) :
    encode (fromCols 1 A) m (Sum.inl i) = m i

Uses 1 · Used by 1

Statement usesEncoder of a generator matrix

Used bySystematic generator and parity-check matrices

TheoremSystematic generator and parity-check matrices#✓fully proved

Let \(F\) be a field, \(\kappa\) and \(\rho\) finite sets, and \(A\) a \(\kappa \times \rho\) matrix over \(F\). Then the code generated by \(G = [I_\kappa \mid A]\) equals the code with parity-check matrix \(H = [-A^{\mathsf{T}} \mid I_\rho]\), both being codes whose coordinates are indexed by the disjoint union of \(\kappa\) and \(\rho\).

theorem systematic_eq [Fintype ρ] [DecidableEq ρ] (A : Matrix κ ρ F) :
    ofGenerator (fromCols (1 : Matrix κ κ F) A) =
      ofParityCheck (fromCols (-Aᵀ) (1 : Matrix ρ ρ F))

Uses 6

Statement usesLinear code · Code generated by a matrix · Code with a given parity-check matrix

Proof usesEncoder of a generator matrix · The systematic encoder copies the message · Generator/parity-check duality

The dual code

AbbreviationDot product bilinear form#✓fully proved

Let \(F\) be a field and \(\iota\) a finite set. The dot product form is the bilinear form on \(F^\iota\) that sends a pair of words \((x, y)\) to \(x \cdot y = \sum_{i \in \iota} x_i y_i\).

abbrev _root_.Cslib.CodingTheory.dotForm : LinearMap.BilinForm F (ι → F) := dotProductBilin F F

Used by 4

Used byDual code · Dual of the code generated by a matrix · Dual of the code with a given parity-check matrix · Dimension of the dual code

DefinitionDual code#✓fully proved

Let \(F\) be a field and \(\iota\) a finite set. The dual \(C^\perp\) of a linear code \(C \subseteq F^\iota\) is the linear code of all words \(x \in F^\iota\) with \(x \cdot c = \sum_{i \in \iota} x_i c_i = 0\) for every codeword \(c \in C\).

noncomputable def dual (C : LinearCode F ι) : LinearCode F ι := dotForm.orthogonal C

Uses 2 · Used by 3

Statement usesLinear code · Dot product bilinear form

Used byDual of the code generated by a matrix · Dual of the code with a given parity-check matrix · Dimension of the dual code

TheoremDimension of the dual code#✓fully proved

Let \(F\) be a field and \(\iota\) a finite set. For every linear code \(C \subseteq F^\iota\), \(\dim C + \dim C^\perp = |\iota|\), where \(C^\perp\) is the dual code.

theorem finrank_add_finrank_dual (C : LinearCode F ι) :
    finrank F C + finrank F (dual C) = Fintype.card ι

Uses 3

Statement usesLinear code · Dual code

Proof usesDot product bilinear form

TheoremDual of the code generated by a matrix#✓fully proved

Let \(G\) be a matrix over a field \(F\) with finitely many rows and finitely many columns. Then the dual of the code generated by \(G\) (the span of its rows) is the code with parity-check matrix \(G\) (the words \(x\) with \(Gx = 0\)).

theorem dual_ofGenerator [Fintype κ] (G : Matrix κ ι F) :
    dual (ofGenerator G) = ofParityCheck G

Uses 7 · Used by 1

Statement usesLinear code · Dual code · Code generated by a matrix · Code with a given parity-check matrix

Proof usesEncoder of a generator matrix · Syndrome · Dot product bilinear form

Used byDual of the code with a given parity-check matrix

TheoremDual of the code with a given parity-check matrix#✓fully proved

Let \(H\) be a matrix over a field \(F\) with finitely many rows and finitely many columns. Then the dual of the code with parity-check matrix \(H\) (the words \(x\) with \(Hx = 0\)) is the code generated by \(H\) (the span of its rows).

theorem dual_ofParityCheck [Fintype ρ] (H : Matrix ρ ι F) :
    dual (ofParityCheck H) = ofGenerator H

Uses 6

Statement usesLinear code · Dual code · Code generated by a matrix · Code with a given parity-check matrix

Proof usesDual of the code generated by a matrix · Dot product bilinear form

Minimum distance and minimum weight

DefinitionMinimum distance#✓fully proved

The minimum distance of a linear code \(C\) of finite length is the least Hamming distance (number of coordinates where they differ) between two distinct codewords of \(C\), taken in \(\mathbb{N} \cup \{\infty\}\); it is \(\infty\) if \(C\) has at most one codeword.

noncomputable def minDist (C : LinearCode F ι) : ℕ∞ :=
  ⨅ (c₁ ∈ C) (c₂ ∈ C) (_ : c₁ ≠ c₂), (hammingDist c₁ c₂ : ℕ∞)

Uses 1 · Used by 14

Statement usesLinear code

Used byThe Hamming code is perfect · No codeword is closer than the Hamming decoder's output · Minimum distance of the Hamming (7,4) code · Hamming bound for the Hamming (7,4) code · Singleton bound for linear codes, dimension form · Minimum distance equals minimum weight · Minimum distance is at most the length · Singleton bound for linear codes · Hamming bound for linear codes · Syndrome decoding corrects every error of weight at most \(t\) · Syndrome decoding up to half the minimum distance · Lower bound on the minimum distance of a Reed-Solomon code · Reed-Solomon codes are MDS · Reed-Solomon codes meet the Singleton bound

DefinitionMinimum weight#✓fully proved

The minimum weight of a linear code \(C\) of finite length is the least weight of a nonzero codeword of \(C\), where the weight of a word is its number of nonzero coordinates; it is taken in \(\mathbb{N} \cup \{\infty\}\) and is \(\infty\) if \(C\) has no nonzero codeword.

noncomputable def minWeight (C : LinearCode F ι) : ℕ∞ :=
  ⨅ (c ∈ C) (_ : c ≠ 0), (hammingNorm c : ℕ∞)

Uses 1 · Used by 5

Statement usesLinear code

Used byMinimum distance of the Hamming (7,4) code · The Hamming (7,4) code has minimum weight at least 3 · Minimum distance equals minimum weight · Syndrome decoding corrects every error of weight at most \(t\) · Lower bound on the minimum distance of a Reed-Solomon code

TheoremHamming distance is the weight of the difference#✓fully proved

Let \(F\) be a field and \(\iota\) a finite set. For all words \(x, y \in F^\iota\), the Hamming distance between \(x\) and \(y\) (the number of coordinates where they differ) equals the Hamming weight of \(x - y\) (its number of nonzero coordinates).

theorem _root_.Cslib.CodingTheory.hammingDist_eq_hammingNorm_sub (x y : ι → F) :
    hammingDist x y = hammingNorm (x - y)

Used by 3

Used byMinimum distance equals minimum weight · Syndrome decoding corrects every error of weight at most \(t\) · Berlekamp-Welch corrects every error of weight at most \(\lfloor (n-k)/2 \rfloor\)

TheoremMinimum distance equals minimum weight#✓fully proved

For a linear code of finite length over a field, the minimum distance equals the minimum weight.

theorem minDist_eq_minWeight (C : LinearCode F ι) : C.minDist = C.minWeight

Uses 4 · Used by 3

Statement usesLinear code · Minimum distance · Minimum weight

Proof usesHamming distance is the weight of the difference

Used byMinimum distance of the Hamming (7,4) code · Syndrome decoding corrects every error of weight at most \(t\) · Lower bound on the minimum distance of a Reed-Solomon code

Syndrome decoding

DefinitionSyndrome decoding#✓fully proved

Syndrome decoding with a lookup table from syndromes to error patterns: subtract the error pattern the table assigns to the syndrome of the received word.

def syndromeDecode (H : Matrix ρ ι F) (table : (ρ → F) → ι → F) (y : ι → F) : ι → F :=
  y - table (syndrome H y)

Uses 1 · Used by 2

Statement usesSyndrome

Used bySyndrome decoding corrects every error of weight at most \(t\) · Syndrome decoding up to half the minimum distance

DefinitionSyndrome table correct up to a radius#✓fully proved

Let \(H\) be a \(\rho \times \iota\) matrix over a field \(F\), with \(\iota\) finite, and let \(t\) be a natural number. A syndrome table for \(H\), that is, a map \(T\) from syndromes \(s \in F^\rho\) to error patterns \(T(s) \in F^\iota\), is correct up to radius \(t\) when, for every word \(e \in F^\iota\) of Hamming weight at most \(t\), the word \(T(He)\) has the same syndrome as \(e\), that is \(H \, T(He) = He\), and has Hamming weight at most \(t\).

This is weaker than asking for minimum-weight coset leaders, and equivalent to it inside the radius when \(2t < d\), where \(d\) is the minimum distance of the code with parity-check matrix \(H\) (each coset then holds at most one word of weight at most \(t\)). Outside the radius the table is unconstrained, so for heavier errors the decoder's output need not even be a codeword.

def IsSyndromeTable (H : Matrix ρ ι F) (t : ℕ) (table : (ρ → F) → ι → F) : Prop :=
  ∀ e : ι → F, hammingNorm e ≤ t →
    syndrome H (table (syndrome H e)) = syndrome H e ∧ hammingNorm (table (syndrome H e)) ≤ t

Uses 1 · Used by 4

Statement usesSyndrome

Used byThe Hamming decoder's syndrome table is correct · Existence of correct syndrome tables · Syndrome decoding corrects every error of weight at most \(t\) · Syndrome decoding up to half the minimum distance

TheoremSyndrome decoding corrects every error of weight at most \(t\)#✓fully proved

Let \(H\) be a parity-check matrix over a field \(F\), let \(C\) be the code with parity-check matrix \(H\), let \(d \in \mathbb{N} \cup \{\infty\}\) be its minimum distance, and let \(t \in \mathbb{N}\) with \(2t < d\). If a syndrome table is correct up to radius \(t\) for \(H\), then for every codeword \(c \in C\) and every word \(e\) of Hamming weight at most \(t\), syndrome decoding with this table sends the received word \(c + e\) to \(c\).

The error pattern the table returns differs from the true error by a codeword of weight at most \(2t\), which must be zero.

theorem syndromeDecode_add_of_hammingNorm_le {H : Matrix ρ ι F} {t : ℕ} {table : (ρ → F) → ι → F}
    (hT : IsSyndromeTable H t table) (ht : (2 * t : ℕ∞) < (ofParityCheck H).minDist)
    {c e : ι → F} (hc : c ∈ ofParityCheck H) (he : hammingNorm e ≤ t) :
    syndromeDecode H table (c + e) = c

Uses 10 · Used by 1

Statement usesLinear code · Syndrome table correct up to a radius · Minimum distance · Code with a given parity-check matrix · Syndrome decoding

Proof usesMinimum distance equals minimum weight · Minimum weight · Syndrome · The syndrome depends only on the error · Hamming distance is the weight of the difference

Used bySyndrome decoding up to half the minimum distance

TheoremSyndrome decoding up to half the minimum distance#✓fully proved

Let \(H\) be a parity-check matrix over a field \(F\) such that the code \(C\) with parity-check matrix \(H\) has finite minimum distance \(d\), and let \(t = \lfloor (d - 1)/2 \rfloor\). If a syndrome table is correct up to radius \(t\) for \(H\), then for every codeword \(c \in C\) and every word \(e\) of Hamming weight at most \(t\), syndrome decoding with this table sends the received word \(c + e\) to \(c\).

theorem syndromeDecode_add_of_minDist_eq {H : Matrix ρ ι F} {d : ℕ}
    (hd : (ofParityCheck H).minDist = d) {table : (ρ → F) → ι → F}
    (hT : IsSyndromeTable H ((d - 1) / 2) table) {c e : ι → F} (hc : c ∈ ofParityCheck H)
    (he : hammingNorm e ≤ (d - 1) / 2) : syndromeDecode H table (c + e) = c

Uses 6 · Used by 1

Statement usesLinear code · Syndrome table correct up to a radius · Minimum distance · Code with a given parity-check matrix · Syndrome decoding

Proof usesSyndrome decoding corrects every error of weight at most \(t\)

Used byThe decoder corrects every error of weight at most 1

TheoremExistence of correct syndrome tables#✓fully proved

Let \(H\) be a matrix over a field \(F\) whose columns are indexed by a finite set. For every natural number \(t\) there is a syndrome table for \(H\) that is correct up to radius \(t\).

theorem exists_isSyndromeTable (H : Matrix ρ ι F) (t : ℕ) : ∃ table, IsSyndromeTable H t table

Uses 2

Statement usesSyndrome table correct up to a radius

Proof usesSyndrome

DefinitionSyndrome table by exhaustive search#✓fully proved

Let \(F\) be a field, \(\iota\) and \(\rho\) finite sets, \(H\) a \(\rho \times \iota\) parity-check matrix over \(F\), and \(t \in \mathbb{N}\), where the words \(F^\iota\) come with a fixed enumeration. The search table sends a syndrome \(s \in F^\rho\) to the first word \(e \in F^\iota\) in the enumeration with Hamming weight at most \(t\) and syndrome \(He = s\), and to \(0\) if there is no such word.

def searchTable [FinEnum (ι → F)] [Fintype ρ] (H : Matrix ρ ι F) (t : ℕ) (s : ρ → F) : ι → F :=
  ((FinEnum.toList (ι → F)).find? fun e ↦ decide (hammingNorm e ≤ t ∧ syndrome H e = s)).getD 0

Uses 1

Statement usesSyndrome

The Singleton and Hamming bounds for linear codes

TheoremNumber of codewords of a linear code#✓fully proved

If \(C\) is a linear code of length \(n\) over a finite field \(F\), then exactly \(|F|^{\dim C}\) of the \(|F|^n\) words of length \(n\) lie in \(C\), where \(\dim C\) is the dimension of \(C\) over \(F\).

theorem card_filter_mem (C : LinearCode F (Fin n)) [DecidablePred (· ∈ C)] :
    (Finset.univ.filter (· ∈ C)).card = Fintype.card F ^ finrank F C

Uses 1 · Used by 2

Statement usesLinear code

Used bySingleton bound for linear codes, dimension form · Hamming bound for linear codes

TheoremSingleton bound for linear codes, dimension form#✓fully proved

Let \(C\) be a linear code of length \(n\) over a finite field \(F\), and let \(d \le n\) be a natural number that is at most the minimum distance of \(C\). Then \(\dim C + d \le n + 1\).

The hypothesis \(d \le n\) matters only for the zero code, whose minimum distance is \(\infty\).

theorem finrank_add_le_of_le_minDist [Finite F] {C : LinearCode F (Fin n)} {d : ℕ}
    (hdn : d ≤ n) (hd : (d : ℕ∞) ≤ C.minDist) : finrank F C + d ≤ n + 1

Uses 4 · Used by 1

Statement usesLinear code · Minimum distance

Proof usesNumber of codewords of a linear code · Singleton bound

Used bySingleton bound for linear codes

TheoremMinimum distance is at most the length#✓fully proved

If \(C\) is a linear code of length \(n\) over a field and \(C\) is not the zero subspace, then the minimum distance of \(C\) is finite and at most \(n\).

theorem minDist_le_length {C : LinearCode F (Fin n)} (hC : C ≠ ⊥) : C.minDist ≤ n

Uses 2 · Used by 1

Statement usesLinear code · Minimum distance

Used bySingleton bound for linear codes

TheoremSingleton bound for linear codes#✓fully proved

Let \(F\) be a finite field and \(C\) a linear code of length \(n\) and dimension \(k\) over \(F\) that is not the zero subspace. Then the minimum distance of \(C\) is at most \(n - k + 1\).

theorem minDist_le_of_ne_bot [Finite F] {C : LinearCode F (Fin n)} (hC : C ≠ ⊥) :
    C.minDist ≤ (n - finrank F C + 1 : ℕ)

Uses 4 · Used by 1

Statement usesLinear code · Minimum distance

Proof usesSingleton bound for linear codes, dimension form · Minimum distance is at most the length

Used byReed-Solomon codes meet the Singleton bound

TheoremHamming bound for linear codes#✓fully proved

Let \(F\) be a finite field with \(q\) elements and \(C\) a linear code of length \(n\) and dimension \(k\) over \(F\). If \(t\) is a natural number such that \(2t\) is less than the minimum distance of \(C\), then

\[q^k \sum_{i=0}^{t} \binom{n}{i} (q-1)^i \le q^n.\]

theorem pow_finrank_mul_sum_le_of_lt_minDist {C : LinearCode F (Fin n)} {t : ℕ}
    (ht : (2 * t : ℕ∞) < C.minDist) :
    Fintype.card F ^ finrank F C *
        ∑ i ∈ Finset.range (t + 1), n.choose i * (Fintype.card F - 1) ^ i ≤
      Fintype.card F ^ n

Uses 4 · Used by 1

Statement usesLinear code · Minimum distance

Proof usesNumber of codewords of a linear code · Hamming bound

Used byHamming bound for the Hamming (7,4) code

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.