The Singleton bound

Two distinct codewords of a code of minimum distance at least d differ on at least d coordinates, so they already differ on any set S of coordinates that leaves out fewer than d of them: the codewords are determined by their letters on S (Cslib.Code.injOn_restrict_of_card_lt_add). Taking n - d + 1 coordinates, a code of length n and minimum distance at least d over an alphabet of q letters has at most q ^ (n - d + 1) codewords: the Singleton bound (Cslib.Code.card_le_pow_of_le_minDist) [Sin64], [GRS19]. For a nonzero linear code over a field the same restriction is an injective linear map, so the dimension k satisfies k + d ≤ n + 1 (Cslib.Code.finrank_add_le_card_add_one). Codes meeting this bound, such as Reed–Solomon codes, are maximum distance separable.

Main results

• Cslib.Code.injOn_restrict_of_card_lt_add: codewords are determined by any n - d + 1 coordinates.
• Cslib.Code.card_le_pow_of_le_minDist: the Singleton bound.
• Cslib.Code.finrank_add_le_card_add_one: the Singleton bound for linear codes.

References

• R. C. Singleton, Maximum distance q-nary codes
• V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory

theorem Cslib.Code.injOn_restrict_of_card_lt_add {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} {d : ℕ} (hd : ↑d ≤ minDist C) {S : Finset ι} (hS : Fintype.card ι < S.card + d) : Set.InjOn S.restrict C

The codewords of a code of minimum distance at least d are determined by their letters on any set S of coordinates that leaves out fewer than d coordinates.

theorem Cslib.Code.card_le_pow_of_le_minDist {ι : Type u_1} [Fintype ι] {α : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] {C : Finset (ι → α)} {d : ℕ} (hd : ↑d ≤ minDist ↑C) : C.card ≤ Fintype.card α ^ (Fintype.card ι - d + 1)

The Singleton bound [Sin64]: a code of length n and minimum distance at least d over an alphabet of q letters has at most q ^ (n - d + 1) codewords.

theorem Cslib.Code.finrank_add_le_card_add_one {ι : Type u_1} [Fintype ι] {F : Type u_2} [Field F] [DecidableEq F] {C : Submodule F (ι → F)} (hC : C ≠ ⊥) {d : ℕ} (hd : ↑d ≤ minDist ↑C) : Module.finrank F ↥C + d ≤ Fintype.card ι + 1

The Singleton bound for linear codes: a nonzero linear code of length n over a field, with dimension k and minimum distance at least d, satisfies k + d ≤ n + 1.