Griesmer bound (source code)

= Griesmer bound
{c}
{wiki}

Every binary linear $[n,k,d]$ code satisfies
$$
n\geq\sum_{j=0}^{k-1}\left\lceil\frac d{2^j}\right\rceil.
$$
Puncturing on the support of a minimum-weight codeword reduces the rank by one and leaves minimum distance at least $\lceil d/2\rceil$, which proves the bound inductively.