Singleton Bound #
This file proves the Singleton bound: any code C of block-length n and minimum
distance d over an alphabet α satisfies
|C| ≤ |α|^(n - d + 1).
Main Result #
singleton_bound: formal statement of the Singleton bound.
References #
- R. Singleton, "Maximum distance q-nary codes", IEEE Trans. Inf. Theory 10(2):116–118, 1964.
theorem
CodingTheory.Codeword.singleton_bound
{α : Type u_1}
[Fintype α]
[Nonempty α]
[DecidableEq α]
[Field α]
{n : ℕ}
(C : Code n α)
(d : ℕ)
(h : distance C d)
(hα : Nontrivial α)
:
Singleton bound: every code of block-length n and minimum distance d has at most
|α|^(n - d + 1) codewords.
Proof sketch: project each codeword onto its first n - d + 1 coordinates.
Two distinct codewords in C must have distinct projections (otherwise their distance
would be less than d), so |C| is at most the number of possible projections.