[proofplan]
The proof is a volumetric packing argument. An $e$-error correcting code has the property that the closed Hamming balls of radius $e$ around distinct codewords are pairwise disjoint, because any point in such a ball is uniquely decodable to its centre. The total volume of these $|C|$ disjoint balls, each of size $V(n, e)$, cannot exceed the volume $2^n$ of the ambient space $\mathbb{F}_2^n$. Rearranging gives the claimed inequality.
[/proofplan]
[step:Define the closed Hamming balls around codewords]
Let $n \in \mathbb{N}$ be the blocklength and $C \subseteq \mathbb{F}_2^n$ a code. For $c \in \mathbb{F}_2^n$ and an integer $e \ge 0$, the **closed Hamming ball of radius $e$** centred at $c$ is
\begin{align*}
B(c, e) := \{x \in \mathbb{F}_2^n : d(x, c) \le e\},
\end{align*}
where $d$ denotes Hamming distance. Because $\mathbb{F}_2^n$ is homogeneous under coordinate translation by $c$ (the map $x \mapsto x + c$ is a bijection of $\mathbb{F}_2^n$ that sends $0$ to $c$ and preserves Hamming weight), the cardinality of $B(c, e)$ does not depend on the centre $c$ but only on $n$ and $e$. We denote this common cardinality by
\begin{align*}
V(n, e) := |B(c, e)| = \sum_{k=0}^{e} \binom{n}{k},
\end{align*}
counting all binary strings of length $n$ at distance $\le e$ from a fixed reference point.
[/step]
[step:Establish pairwise disjointness of the balls $\{B(c, e)\}_{c \in C}$]
We claim that for any two distinct codewords $c_1, c_2 \in C$,
\begin{align*}
B(c_1, e) \cap B(c_2, e) = \varnothing.
\end{align*}
Suppose for contradiction that some $x \in B(c_1, e) \cap B(c_2, e)$. Then $d(x, c_1) \le e$ and $d(x, c_2) \le e$. But an $e$-error correcting code has the property that, for every $x \in \mathbb{F}_2^n$, there is at most one codeword $c \in C$ with $d(x, c) \le e$; otherwise, if $x$ were received from the channel, minimum distance decoding could not uniquely determine the sender. More precisely, the defining property of an $e$-error correcting code is that the closed balls $\{B(c, e)\}_{c \in C}$ are pairwise disjoint — equivalently, the code has minimum distance at least $2e + 1$, as established in the [characterisation of error-correcting codes via minimum distance](/theorems/1638). Thus the existence of $x \in B(c_1, e) \cap B(c_2, e)$ with $c_1 \ne c_2$ contradicts the error-correcting hypothesis, proving disjointness.
[/step]
[step:Sum the ball volumes and compare to $|\mathbb{F}_2^n| = 2^n$]
Since the balls $\{B(c, e)\}_{c \in C}$ are pairwise disjoint subsets of $\mathbb{F}_2^n$, additivity of cardinality gives
\begin{align*}
\left| \bigsqcup_{c \in C} B(c, e) \right| = \sum_{c \in C} |B(c, e)| = \sum_{c \in C} V(n, e) = |C| \cdot V(n, e).
\end{align*}
This disjoint union is a subset of $\mathbb{F}_2^n$, so
\begin{align*}
|C| \cdot V(n, e) = \left| \bigsqcup_{c \in C} B(c, e) \right| \le |\mathbb{F}_2^n| = 2^n.
\end{align*}
[guided]
We have $|C|$ balls, each of size $V(n, e)$, and they are pairwise disjoint. How much room do they occupy? Exactly $|C| \cdot V(n, e)$, because disjointness is precisely the statement that the total cardinality of a union equals the sum of individual cardinalities. The union sits inside $\mathbb{F}_2^n$, which has $2^n$ elements (each coordinate independently chosen from $\{0, 1\}$, and there are $n$ coordinates).
Why does disjointness matter here? Without disjointness, we could double-count elements: an $x$ in two overlapping balls would be tallied twice by the sum $\sum_c |B(c, e)|$, but only once by the union. With disjointness the two quantities agree, and we obtain a legitimate bound
\begin{align*}
|C| \cdot V(n, e) \le 2^n.
\end{align*}
This is a classical **sphere-packing** inequality: non-overlapping balls cannot occupy more than the total volume. The inequality is the volumetric inequality that gives the Hamming bound its alternative name of "sphere-packing bound".
[/guided]
[/step]
[step:Divide by $V(n, e) > 0$ to conclude]
Because $V(n, e) = \sum_{k=0}^e \binom{n}{k} \ge \binom{n}{0} = 1 > 0$, we may divide both sides of the inequality $|C| \cdot V(n, e) \le 2^n$ by $V(n, e)$ to obtain
\begin{align*}
|C| \le \frac{2^n}{V(n, e)}.
\end{align*}
This is the Hamming bound, completing the proof.
[/step]
