Existence of separated Boolean codes

A maximum-cardinality code of a prescribed minimum distance covers the Boolean cube by balls of radius minimumDistance - 1. Counting that cover gives the finite Gilbert--Varshamov inequality. This is an existence theorem only; it does not supply an efficient encoder or decoder.

theorem Complexity.BooleanHamming.exists_isSeparated_and_covering (length minimumDistance : ℕ) : ∃ (code : Finset (Word length)), IsSeparated code minimumDistance ∧ ∀ (word : Word length), ∃ center ∈ code, distance word center ≤ minimumDistance - 1

Some code of minimum distance d covers the cube by radius-d-1 balls.

theorem Complexity.BooleanHamming.gilbertVarshamov_bound (length minimumDistance : ℕ) : ∃ (code : Finset (Word length)), IsSeparated code minimumDistance ∧ 2 ^ length ≤ code.card * volume length (minimumDistance - 1)

Finite Gilbert--Varshamov bound for Boolean codes.