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
If a code \(C\) has minimum distance \(d\), then \(d \le n\).
4.5 Additional declarations
If \(q \ge 2\), then \(q \gt 0\) as a real number.
If \(q \ge 2\), then \(1 \lt q\) as a real number.
If \(q \ge 2\), then \(0 \lt q - 1\) as a real number.
If \(q \ge 2\), then \(q \ne 1\) as a real number.
If \(p \lt 1\), then \(0 \lt 1 - p\).
If \(0 \lt p\) and \(p \lt 1\), then \(0 \lt p(1 - p)\).
If \(0 \lt q\) and \(p \le 1 - 1/q\), then \(p \lt 1\).