Minimum Hamming distance

The minimum distance of a set of words is the least Hamming distance between distinct words, with value zero for a set containing at most one word. It agrees with Set.infsep after transport to Mathlib's Hamming metric space. For an additive code it is also the least weight of a nonzero word, so the same API applies to linear codes through their underlying additive subgroups.

The coordinate type is finite; the alphabets may depend on the coordinate and need not be finite, nor does the code. The attained minimum and its lower-bound characterization support parameter computations for explicit codes, while invariance under distance-preserving maps handles changes of coordinates.

Use C.hammingMinDist, or Set.hammingMinDist C, for a set of words C. Its defining equation is Set.hammingMinDist_def C.

The conventions follow Huffman and Pless, Fundamentals of Error-Correcting Codes, §§1.2–1.6. The unbundled minimum-distance design follows Cristina Dueñas Navarro's Mathlib PR #38014. This module generalizes its Fin n/Hamming-space interface to arbitrary finite coordinate types and dependent alphabets, with hammingMinDist_eq_infsep providing the explicit bridge.

noncomputable def Set.hammingMinDist {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : ℕ

The least distance between distinct words of C, or zero if there are no such words.

theorem Set.hammingMinDist_def {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : C.hammingMinDist = sInf {d : ℕ | ∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ hammingDist x y = d}

Minimum distance is the infimum of the Hamming distances between distinct codewords.

theorem Set.hammingMinDist_eq_zero_of_subsingleton {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Subsingleton) : C.hammingMinDist = 0

A code with at most one word has minimum distance zero.

@[simp]

theorem Set.hammingMinDist_empty {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] : ∅.hammingMinDist = 0

@[simp]

theorem Set.hammingMinDist_singleton {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) : {x}.hammingMinDist = 0

theorem Set.hammingMinDist_le {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} {x y : (i : ι) → β i} (hx : x ∈ C) (hy : y ∈ C) (hxy : x ≠ y) : C.hammingMinDist ≤ hammingDist x y

The minimum distance is bounded by the distance between any two distinct codewords.

theorem Set.exists_hammingDist_eq_hammingMinDist {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Nontrivial) : ∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ hammingDist x y = C.hammingMinDist

Every code with two distinct words attains its minimum distance.

theorem Set.le_hammingMinDist_iff {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Nontrivial) {d : ℕ} : d ≤ C.hammingMinDist ↔ ∀ x ∈ C, ∀ y ∈ C, x ≠ y → d ≤ hammingDist x y

Lower bounds for minimum distance are exactly lower bounds for all distinct pairs.

@[simp]

theorem Set.hammingMinDist_pos_iff {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} : 0 < C.hammingMinDist ↔ C.Nontrivial

Minimum distance is positive exactly when the code contains two distinct words.

@[simp]

theorem Set.hammingMinDist_eq_zero_iff {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} : C.hammingMinDist = 0 ↔ C.Subsingleton

Minimum distance is zero exactly when the code contains at most one word.

theorem Set.hammingMinDist_le_card {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} : C.hammingMinDist ≤ Fintype.card ι

The minimum distance never exceeds the number of coordinates.

theorem Set.hammingMinDist_le_of_subset {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C D : Set ((i : ι) → β i)} (hC : C.Nontrivial) (hCD : C ⊆ D) : D.hammingMinDist ≤ C.hammingMinDist

Inclusion reverses minimum distance when the smaller code has two distinct words.

theorem Set.hammingMinDist_eq_infsep {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} : ↑C.hammingMinDist = (⇑Hamming.toHamming '' C).infsep

The natural-number minimum distance equals metric infimum separation in Hamming space.

@[simp]

theorem Set.hammingMinDist_pair {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (x y : (i : ι) → β i) : {x, y}.hammingMinDist = hammingDist x y

The minimum distance of a two-word code is the distance between its words, including when the words coincide.

theorem Set.hammingMinDist_image {ι : Type u_1} {κ : Type u_2} {β : ι → Type u_3} {γ : κ → Type u_4} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} [Fintype κ] [(i : κ) → DecidableEq (γ i)] (f : ((i : ι) → β i) → (i : κ) → γ i) (hf : ∀ x ∈ C, ∀ y ∈ C, x ≠ y → hammingDist (f x) (f y) = hammingDist x y) : (f '' C).hammingMinDist = C.hammingMinDist

A map preserving distances between distinct codewords preserves minimum distance.

theorem Set.hammingMinDist_le_hammingNorm {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} [(i : ι) → Zero (β i)] {x : (i : ι) → β i} (h0 : 0 ∈ C) (hx : x ∈ C) (hx0 : x ≠ 0) : C.hammingMinDist ≤ hammingNorm x

In a code containing the zero word, the weight of any nonzero codeword bounds the minimum distance. This applies in particular to additive and linear codes.

theorem Set.hammingMinDist_eq_sInf_hammingNorm {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddGroup (β i)] {E : AddSubgroup ((i : ι) → β i)} : (↑E).hammingMinDist = sInf {d : ℕ | ∃ x ∈ E, x ≠ 0 ∧ hammingNorm x = d}

For an additive code, minimum distance is the least nonzero weight. For the zero code the indexing set is empty and both sides are zero.

theorem Set.exists_hammingNorm_eq_hammingMinDist {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddGroup (β i)] {E : AddSubgroup ((i : ι) → β i)} (hE : E ≠ ⊥) : ∃ x ∈ E, x ≠ 0 ∧ hammingNorm x = (↑E).hammingMinDist

A nonzero additive code attains its minimum distance at a nonzero codeword.

theorem Set.le_hammingMinDist_iff_hammingNorm {ι : Type u_1} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddGroup (β i)] {E : AddSubgroup ((i : ι) → β i)} (hE : E ≠ ⊥) {d : ℕ} : d ≤ (↑E).hammingMinDist ↔ ∀ x ∈ E, x ≠ 0 → d ≤ hammingNorm x

Weight lower bounds characterize the minimum distance of a nonzero additive code.