Basics of Coding Theory

We define a general code C to be a subset of n → R for some finite index set n and some target type R.

We can then specialize this notion to various settings. For [CommSemiring R], we define a linear code to be a linear subspace of n → R. We also define the notion of generator matrix and (parity) check matrix.

Naming conventions

1. suffix ': computable/instantiation of the corresponding mathematical generic definitions without such suffix (e.g. Δ₀'(u, C) vs Δ₀(u, C), δᵣ'(u, C) vs δᵣ(u, C), ...) - NOTE: The generic (non-suffixed) definitions (Δ₀, δᵣ, ...) are recommended to be used in generic security statements, and the suffixed definitions (Δ₀', δᵣ', ...) are used for proofs or in statements of lemmas that need smaller value range. - We usually prove the equality as a bridge from the suffixed definitions into the non-suffixed definitions (e.g. distFromCode'_eq_distFromCode, ...)

Main Definitions

1. Distance between two words: - hammingDist u v (Δ₀(u, v)): The Hamming distance between two words u and v - relHammingDist u v (δᵣ(u, v)): The relative Hamming distance between two words u and v
2. Distance of code: - dist C (‖"C‖₀): The Hamming distance of a code C, defined as the infimum (in ℕ∞) of the Hamming distances between any two distinct elements of C. This is noncomputable.
   • minDist C: another statement of dist C using equality, we have dist_eq_minDist - dist' C (‖C‖₀'): A computable version of dist C, assuming C is a Fintype.
3. Distance from a word to a code: - distFromCode u C (Δ₀(u, C)): The hamming distance from a word u to a code C
   • distFromCode_of_empty: Δ₀(u, ∅) = ⊤
   • distFromCode_eq_top_iff_empty: Δ₀(u, C) = ⊤ ↔ C = ∅ - distFromCode' u C (Δ₀'(u, C)): A computable version of distFromCode u C, assuming C is a Fintype.
   • distFromCode'_eq_distFromCode: Δ₀'(u, C) = Δ₀(u, C) - relDistFromCode u C (δᵣ(u, C)): The relative Hamming distance from a word u to a code C
   • relDistFromCode' u C (δᵣ'(u, C)): A computable version of relDistFromCode u C, assuming C is a Fintype and C is non-empty.
   • relDistFromCode'_eq_relDistFromCode: δᵣ'(u, C) = δᵣ(u, C)
4. Switching between different distance realms: - relDistFromCode_eq_distFromCode_div: δᵣ(u, C) = Δ₀(u, C) / |ι| - pairDist_eq_distFromCode_iff_eq_relDistFromCode_div: Δ₀(u, v) = Δ₀(u, C) ↔ δᵣ(u, v) = δᵣ(u, C) - relDistFromCode_le_relDist_to_mem: δᵣ(u, C) ≤ δᵣ(u, v) - relCloseToCode_iff_relCloseToCodeword_of_minDist: δᵣ(u, C) ≤ δ ↔ ∃ v ∈ C, δᵣ(u, v) ≤ δ - pairRelDist_le_iff_pairDist_le: (δᵣ(u, v) ≤ δ) ↔ (Δ₀(u, v) ≤ Nat.floor (δ * Fintype.card ι)) - distFromCode_le_iff_relDistFromCode_le: Δ₀(u, C) ≤ e ↔ δᵣ(u, C) ≤ (e : ℝ≥0) / (Fintype.card ι : ℝ≥0) - relDistFromCode_le_iff_distFromCode_le: δᵣ(u, C) ≤ δ ↔ Δ₀(u, C) ≤ Nat.floor (δ * Fintype.card ι) - relCloseToWord_iff_exists_possibleDisagreeCols - relCloseToWord_iff_exists_agreementCols - relDist_floor_bound_iff_complement_bound - distFromCode_le_dist_to_mem: Δ₀(u, C) ≤ Δ₀(u, v), given v ∈ C - distFromCode_le_card_index_of_Nonempty: Δ₀(u, C) ≤ |ι|, given C is non-empty
5. Unique decoding radius: - uniqueDecodingRadius C (UDR(C)): The unique decoding radius of a code C - relativeUniqueDecodingRadius C (relUDR(C)): The relative unique decoding radius of a code C - UDR_close_iff_exists_unique_close_codeword: Δ₀(u, C) ≤ UDR(C) ↔ ∃! v ∈ C, Δ₀(u, v) ≤ UDR(C) - UDRClose_iff_two_mul_proximity_lt_d_UDR: e ≤ UDR(C) ↔ 2 * e < ‖C‖₀ - eq_of_le_uniqueDecodingRadius - UDR_close_iff_relURD_close: Δ₀(u, C) ≤ UDR(C) ↔ δᵣ(u, C) ≤ relUDR(C) - dist_le_UDR_iff_relDist_le_relUDR: e ≤ UDR(C) ↔ (e : ℝ≥0) / (Fintype.card ι : ℝ≥0) ≤ relUDR(C)

We define the block length, rate, and distance of C. We prove simple properties of linear codes such as the singleton bound.

TODOs

• Implement ENNRat (ℚ≥0∞), for usage in relDistFromCode and relDistFromCode', as counterpart of ENat (ℕ∞) in distFromCode and distFromCode'.

def Code.«termΔ₀(_,_)» : Lean.ParserDescr

def Code.«term‖_‖₀» : Lean.ParserDescr

noncomputable def Code.dist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ℕ

The Hamming distance of a code C is the minimum Hamming distance between any two distinct elements of the code. We formalize this as the infimum sInf over all d : ℕ such that there exist u v : n → R in the code with u ≠ v and hammingDist u v ≤ d. If none exists, then we define the distance to be 0.

@[implicit_reducible]

instance Code.instEDistForall_starlib {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : EDist (n → R)

@[implicit_reducible]

instance Code.instDistForall_starlib {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : Dist (n → R)

noncomputable def Code.eCodeDistNew {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ENNReal

noncomputable def Code.codeDistNew {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ℝ

def Code.«term‖_‖₀_1» : Lean.ParserDescr

noncomputable def Code.distFromCode {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) (C : Set (n → R)) : ℕ∞

The distance from a vector u to a code C is the minimum Hamming distance between u and any element of C.

def Code.«termΔ₀(_,_)_1» : Lean.ParserDescr

theorem Code.distFromCode_le_dist_to_mem {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) {C : Set (n → R)} (v : n → R) (hv : v ∈ C) : Δ₀(u, C) ≤ ↑Δ₀(u, v)

The distance to a code is at most the distance to any specific codeword.

theorem Code.pairDist_ge_code_mindist_of_ne {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} {u v : n → R} (hu : u ∈ C) (hv : v ∈ C) (h_ne : u ≠ v) : Δ₀(u, v) ≥ ‖C‖₀

If u and v are distinct members of a code C, their distance is at least ‖C‖₀.

noncomputable def Code.minDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ℕ

@[simp]

theorem Code.dist_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : ‖∅‖₀ = 0

@[simp]

theorem Code.dist_subsingleton {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Subsingleton ↑C] : ‖C‖₀ = 0

@[simp]

theorem Code.dist_le_card {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ‖C‖₀ ≤ Fintype.card n

theorem Code.dist_eq_minDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) : ‖C‖₀ = minDist C

theorem Code.dist_pos_of_Nontrivial {ι : Type u_3} [Fintype ι] {F : Type u_4} (C : Set (ι → F)) [DecidableEq F] (hC : C.Nontrivial) : ‖C‖₀ > 0

A non-trivial code (a code with at least two distinct codewords) must have a minimum distance greater than 0.

theorem Code.exists_closest_codeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : ∃ M ∈ C, ↑Δ₀(u, M) = Δ₀(u, C)

noncomputable def Code.pickClosestCodeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : ↑C

theorem Code.distFromPickClosestCodeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : Δ₀(u, C) = ↑Δ₀(u, ↑(pickClosestCodeword_of_Nonempty_Code C u))

theorem Code.closeToWord_iff_exists_possibleDisagreeCols {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u v : ι → F) (e : ℕ) : Δ₀(u, v) ≤ e ↔ ∃ (D : Finset ι), D.card ≤ e ∧ ∀ colIdx ∉ D, u colIdx = v colIdx

theorem Code.closeToWord_iff_exists_agreementCols {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u v : ι → F) (e : ℕ) : Δ₀(u, v) ≤ e ↔ ∃ (S : Finset ι), Fintype.card ι - e ≤ S.card ∧ ∀ (colIdx : ι), (colIdx ∈ S → u colIdx = v colIdx) ∧ (u colIdx ≠ v colIdx → colIdx ∉ S)

theorem Code.eq_of_lt_dist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} {u v : n → R} (hu : u ∈ C) (hv : v ∈ C) (huv : Δ₀(u, v) < ‖C‖₀) : u = v

If u and v are two codewords of C with distance less than dist C, then they are the same.

@[simp]

theorem Code.distFromCode_of_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) : Δ₀(u, ∅) = ⊤

theorem Code.distFromCode_eq_top_iff_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) (C : Set (n → R)) : Δ₀(u, C) = ⊤ ↔ C = ∅

theorem Code.distFromCode_le_card_index_of_Nonempty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) {C : Set (n → R)} [Nonempty ↑C] : Δ₀(u, C) ≤ ↑(Fintype.card n)

@[simp]

theorem Code.distFromCode_of_mem {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) {u : n → R} (h : u ∈ C) : Δ₀(u, C) = 0

theorem Code.distFromCode_eq_zero_iff_mem {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (u : n → R) : Δ₀(u, C) = 0 ↔ u ∈ C

theorem Code.distFromCode_eq_of_lt_half_dist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (u : n → R) {v w : n → R} (hv : v ∈ C) (hw : w ∈ C) (huv : Δ₀(u, v) < ‖C‖₀ / 2) (hvw : Δ₀(u, w) < ‖C‖₀ / 2) : v = w

theorem Code.closeToCode_iff_closeToCodeword_of_minDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] {C : Set (ι → F)} (u : ι → F) (e : ℕ) : Δ₀(u, C) ≤ ↑e ↔ ∃ v ∈ C, Δ₀(u, v) ≤ e

def Code.dist' {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) [Fintype ↑C] : ℕ∞

Computable version of the Hamming distance of a code C, assuming C is a Fintype.

The return type is ℕ∞ since we use Finset.min.

def Code.«term‖_‖₀'» : Lean.ParserDescr

@[simp]

theorem Code.dist'_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : ‖∅‖₀' = ⊤

@[simp]

theorem Code.codeDist'_subsingleton {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Fintype ↑C] [Subsingleton ↑C] : ‖C‖₀' = ⊤

theorem Code.dist'_eq_dist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Fintype ↑C] : ‖C‖₀'.toNat = ‖C‖₀

def Code.possibleDistsToCode {α : Type u_3} {F : Type u_4} {ι : Type u_5} (w : ι → F) (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) : Set α

The set of possible distances δf from a vector w to a code C.

theorem Code.possibleDistsToCode_nonempty_iff {α : Type u_6} {F : Type u_7} {ι : Type u_8} {w : ι → F} {C : Set (ι → F)} {δf : (ι → F) → (ι → F) → α} : (possibleDistsToCode w C δf).Nonempty ↔ (C \ {w}).Nonempty

def Code.possibleDists {α : Type u_3} {F : Type u_4} {ι : Type u_5} (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) : Set α

The set of possible distances δf between distinct codewords in a code C.

• TODO: This allows us to express distance in non-ℝ, which is quite convenient. Extending to (E)Dist forces this into ℝ; give some thought.

noncomputable def Code.distToCode {α : Type u_3} {F : Type u_4} {ι : Type u_5} [LinearOrder α] [Zero α] (w : ι → F) (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) (h : (possibleDistsToCode w C δf).Finite) : WithTop α

A generalisation of distFromCode for an arbitrary distance function δf.

theorem Code.distToCode_of_nonempty {α : Type u_3} [LinearOrder α] [Zero α] {ι : Type u_4} {F : Type u_5} {w : ι → F} {C : Set (ι → F)} {δf : (ι → F) → (ι → F) → α} (h₁ : (possibleDistsToCode w C δf).Finite) (h₂ : (possibleDistsToCode w C δf).Nonempty) : distToCode w C δf h₁ = ↑((possibleDistsToCode w C δf).toFinset.min' ⋯)

def Code.distFromCode' {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) [Fintype ↑C] (u : n → R) : ℕ∞

Computable version of the distance from a vector u to a finite code C.

def Code.«termΔ₀'(_,_)» : Lean.ParserDescr

theorem Code.distFromCode'_eq_distFromCode {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) [Fintype ↑C] (u : n → R) : Δ₀'(u, C) = Δ₀(u, C)

For finite nonempty codes, the computable distance equals the noncomputable distance.