4 Error-Correcting Codes — Core Definitions
4.1 Overview
This file documents the foundational definitions for \(q\)-ary block codes over a finite field alphabet \(\alpha \). Throughout, \(\alpha \) is a type carrying instances [Fintype α], [Field α], [DecidableEq α], and [Nonempty α].
4.2 Basic objects: codewords and codes
4.2.1 Codewords
A codeword of length \(n\) over alphabet \(\alpha \) is a function \(c : \mathrm{Fin}\, n \to \alpha \).
Pointwise addition, subtraction, and the all-zero codeword.
4.2.2 Codes and linear codes
A (block) code of length \(n\) over \(\alpha \) is a finite set (Finset) of codewords.
A code \(C\) is linear with generator matrix \(G\) (shape \(n\times m\)) if every message \(c':\mathrm{Fin}\, m\to \alpha \) maps to a codeword \(Gc'\in C\), and every codeword in \(C\) arises this way.
Existential version: there exists some \(m\) and generator matrix \(G\) witnessing linearity.
4.3 Distance, weight, and rate
Hamming distance between two codewords, wrapping Mathlib’s hammingDist.
distance C d holds when \(d\) is the minimum Hamming distance of \(C\): there exist distinct codewords at distance exactly \(d\), and no two distinct codewords are closer than \(d\).
The Hamming weight of \(c\) is \(d(c, \mathbf{0})\).
max_size n d A asserts existence of a code of size \(A\) and minimum distance \(d\) that is maximal among all such codes.
The Hamming ball of radius \(l\) around \(c\):
implemented as a Finset.
4.4 Basic lemma: distance vs. block length
Let \(C\) be a code of length \(n\) over an alphabet \(\alpha \) — that is, a finite set of codewords, each a function \(\mathrm{Fin}\, n \to \alpha \) — and let \(d\) be a natural number that is the minimum distance of \(C\): there exist two distinct codewords of \(C\) at Hamming distance exactly \(d\), and every pair of distinct codewords of \(C\) is at Hamming distance at least \(d\). Then \(d \le n\).
4.5 Additional declarations
Let \(q\) be a natural number with \(q \ge 2\). Then its image in the real numbers satisfies \(0 \lt q\).
For any natural number \(q\) with \(q \ge 2\), the image of \(q\) under the canonical embedding of the naturals into the reals satisfies \(1 \lt q\).
Let \(q\) be a natural number with \(q \ge 2\). Then, regarded as a real number, \(q - 1\) is strictly positive: \(0 \lt q - 1\).
Let \(q\) be a natural number with \(q \ge 2\). Then, regarded as a real number, \(q \ne 1\).
Let \(p\) be a real number with \(p \lt 1\). Then \(1 - p \gt 0\).
Let \(p\) be a real number with \(0 \lt p \lt 1\). Then \(p(1-p) \gt 0\).
Let \(q\) and \(p\) be real numbers with \(q \gt 0\). If \(p \le 1 - 1/q\), then \(p \lt 1\).