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.

A (block) code of length \(n\) over \(\alpha \) is a finite set () 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.

Hamming distance between two codewords, wrapping Mathlib’s .

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})\).

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 .