Griesmer bound
= 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.