The minimum distance of a code

A code is a set C of words ∀ i, β i over the alphabets β i at the finitely many coordinates i : ι. Its minimum distance Cslib.Code.minDist C is the least Hamming distance between two distinct codewords, and ⊤ when C has at most one codeword MacWilliams and Sloane, Chapter 1. A bound d ≤ minDist C says exactly that distinct codewords differ on at least d coordinates (Cslib.Code.le_minDist_iff). When C has two distinct codewords the minimum is attained (Cslib.Code.exists_hammingDist_eq_minDist).

A word within distance e of two codewords determines them when 2 e < minDist C: the code uniquely decodes up to e errors (Cslib.Code.eq_of_hammingDist_le_of_two_mul_lt_minDist).

Main definitions

• Cslib.Code.minDist: the minimum distance of a code.

Main results

• Cslib.Code.le_minDist_iff, Cslib.Code.natCast_lt_minDist_iff: lower bounds on the minimum distance.
• Cslib.Code.minDist_eq_top_iff: the minimum distance is ⊤ exactly for codes with at most one word.
• Cslib.Code.exists_hammingDist_eq_minDist: the minimum distance is attained.
• Cslib.Code.eq_of_hammingDist_le_of_two_mul_lt_minDist: unique decoding below half the minimum distance.

References

• [F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes] [MWS77]

noncomputable def Cslib.Code.minDist {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : ℕ∞

The minimum distance of a code C: the least Hamming distance between two distinct codewords, or ⊤ when C has at most one codeword.

theorem Cslib.Code.le_minDist_iff {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} {d : ℕ∞} : d ≤ minDist C ↔ ∀ x ∈ C, ∀ y ∈ C, x ≠ y → d ≤ ↑(hammingDist x y)

The minimum distance is at least d iff distinct codewords differ on at least d coordinates.

theorem Cslib.Code.natCast_lt_minDist_iff {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} {r : ℕ} : ↑r < minDist C ↔ ∀ x ∈ C, ∀ y ∈ C, x ≠ y → r < hammingDist x y

The minimum distance exceeds r iff distinct codewords differ on more than r coordinates.

theorem Cslib.Code.minDist_le_hammingDist {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} {x y : (i : ι) → β i} (hx : x ∈ C) (hy : y ∈ C) (hxy : x ≠ y) : minDist C ≤ ↑(hammingDist x y)

Distinct codewords are separated by at least the minimum distance of the code.

theorem Cslib.Code.minDist_anti {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C D : Set ((i : ι) → β i)} (h : C ⊆ D) : minDist D ≤ minDist C

A subcode has at least the minimum distance of the code.

theorem Cslib.Code.minDist_eq_top_iff {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} : minDist C = ⊤ ↔ C.Subsingleton

The minimum distance is ⊤ exactly for codes with at most one codeword.

@[simp]

theorem Cslib.Code.minDist_empty {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] : minDist ∅ = ⊤

The empty code has minimum distance ⊤.

@[simp]

theorem Cslib.Code.minDist_singleton {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) : minDist {x} = ⊤

A singleton code has minimum distance ⊤.

theorem Cslib.Code.exists_hammingDist_eq_minDist {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (h : C.Nontrivial) : ∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ ↑(hammingDist x y) = minDist C

A code with two distinct codewords has two codewords at exactly the minimum distance.

theorem Cslib.Code.minDist_le_card {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (h : C.Nontrivial) : minDist C ≤ ↑(Fintype.card ι)

A code with two distinct codewords has minimum distance at most the number of coordinates.

theorem Cslib.Code.eq_of_hammingDist_le_of_two_mul_lt_minDist {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} {x y : (i : ι) → β i} {e : ℕ} (he : 2 * ↑e < minDist C) {w : (i : ι) → β i} (hx : x ∈ C) (hy : y ∈ C) (hxw : hammingDist x w ≤ e) (hyw : hammingDist y w ≤ e) : x = y

Unique decoding. If 2 e is less than the minimum distance, a word is within distance e of at most one codeword.