[proofplan] The upper bound is a direct consequence of the [Hamming bound for $e$-error correcting codes](/theorems/1639) with $e = \lfloor (d-1)/2 \rfloor$, together with the fact that a code with minimum distance $d$ is $\lfloor (d-1)/2 \rfloor$-error correcting. The lower bound is a covering argument: a code $C$ of maximum size with minimum distance $d$ must leave no room outside the balls $\bigcup_{c \in C} B(c, d-1)$, since any uncovered point could be adjoined to $C$ while preserving minimum distance $d$, contradicting maximality. Volume considerations then force $|C| \cdot V(n, d-1) \ge 2^n$. [/proofplan]

[step:Derive the upper bound (Hamming bound) from error-correction capability] Let $C \subseteq \mathbb{F}_2^n$ be a code with $|C| = A(n, d)$ and minimum distance at least $d$. Set $e = \lfloor (d-1)/2 \rfloor$. By the [minimum-distance characterisation of error correction](/theorems/1638), a code with minimum distance at least $d$ is $e$-error correcting (because $2e \le d - 1$, so $2e + 1 \le d$). Applying the [Hamming bound for $e$-error correcting codes](/theorems/1639), \begin{align*} A(n, d) = |C| \le \frac{2^n}{V(n, e)} = \frac{2^n}{V\!\left(n, \left\lfloor \frac{d-1}{2} \right\rfloor\right)}. \end{align*} This is the right-hand inequality. [/step]

[step:Pick a maximum-size code $C$ with minimum distance $d$] For the lower bound, let $m = A(n, d)$ and choose $C \subseteq \mathbb{F}_2^n$ with $|C| = m$ and minimum distance at least $d$. By definition of $A(n, d)$ as the supremum, such a code exists, and by the maximality of $m$ no strictly larger code of blocklength $n$ with minimum distance $\ge d$ exists. [/step]

[step:Show that the balls $\{B(c, d-1)\}_{c \in C}$ cover $\mathbb{F}_2^n$]We claim \begin{align*} \mathbb{F}_2^n = \bigcup_{c \in C} B(c, d - 1). \end{align*} Let $x \in \mathbb{F}_2^n$ be arbitrary. We consider two cases. **Case 1**: $x \in C$. Then $d(x, x) = 0 \le d - 1$, so $x \in B(x, d-1) \subseteq \bigcup_{c \in C} B(c, d-1)$. **Case 2**: $x \notin C$. Suppose for contradiction that $d(x, c) \ge d$ for every $c \in C$. Then $C' := C \cup \{x\}$ is a set of $m + 1$ distinct elements of $\mathbb{F}_2^n$, and for every pair $c_1, c_2 \in C'$ with $c_1 \ne c_2$ we have $d(c_1, c_2) \ge d$: if both lie in $C$ this follows from the minimum distance of $C$, and if one is $x$ this follows from the supposition. Hence $C'$ is a code of blocklength $n$ with minimum distance at least $d$ and $|C'| = m + 1 > A(n, d)$, contradicting the definition of $A(n, d)$ as the supremum of such sizes. Therefore some $c \in C$ satisfies $d(x, c) \le d - 1$, i.e., $x \in B(c, d-1) \subseteq \bigcup_{c \in C} B(c, d-1)$. Combining the two cases, every $x \in \mathbb{F}_2^n$ lies in $\bigcup_{c \in C} B(c, d-1)$.[/step]

[guided]We want to argue that no point of $\mathbb{F}_2^n$ can be "far" from $C$. The key leverage is the maximality of $|C|$: if some point $x$ were at distance $\ge d$ from every codeword, then adjoining $x$ to $C$ would produce a strictly larger code with minimum distance still $\ge d$, contradicting that $C$ is already as large as possible. Formally, suppose $x \notin C$ and $d(x, c) \ge d$ for every $c \in C$. Consider $C' = C \cup \{x\}$. For any two distinct elements $c_1, c_2 \in C'$: - if $c_1, c_2 \in C$: then $d(c_1, c_2) \ge d$ because $C$ has minimum distance $\ge d$; - if one of them is $x$, say $c_1 = x$ and $c_2 \in C$: then $d(x, c_2) \ge d$ by our supposition. In either case $d(c_1, c_2) \ge d$, so $C'$ has minimum distance at least $d$. But $|C'| = |C| + 1 = m + 1 > m = A(n, d)$, violating the definition of $A(n, d)$ as the maximum. This contradiction forces some $c \in C$ with $d(x, c) < d$, i.e., $d(x, c) \le d - 1$, meaning $x \in B(c, d-1)$. Combined with the trivial case $x \in C$ (where $x \in B(x, d-1)$), every point of $\mathbb{F}_2^n$ lies in the union of the $(d-1)$-balls around codewords. This is a **covering** statement, dual to the *packing* statement used in the Hamming bound. Packing gives an upper bound on $|C|$ (the balls don't overlap, so they can't be too many); covering gives a lower bound on $|C|$ (the balls must fill the space, so there can't be too few).[/guided]

[step:Bound $2^n$ by the total ball volume via the union bound] Having established $\mathbb{F}_2^n = \bigcup_{c \in C} B(c, d - 1)$, we take cardinalities. By the union bound (subadditivity of cardinality for not-necessarily-disjoint unions), \begin{align*} 2^n = |\mathbb{F}_2^n| = \left| \bigcup_{c \in C} B(c, d - 1) \right| \le \sum_{c \in C} |B(c, d - 1)| = |C| \cdot V(n, d - 1), \end{align*} where the last equality uses the translation invariance of the Hamming ball cardinality: $|B(c, d-1)| = V(n, d-1)$ for every $c$. Note that no disjointness is assumed here — the balls of radius $d - 1$ can and do overlap (they have radius $d-1$, not $\lfloor (d-1)/2 \rfloor$). The inequality is in the correct direction because the union bound counts each element *at least* once in the sum. [/step]

[step:Divide by $V(n, d-1) > 0$ to conclude the GV bound] Because $V(n, d-1) = \sum_{k=0}^{d-1} \binom{n}{k} \ge \binom{n}{0} = 1 > 0$, we may divide the inequality $2^n \le |C| \cdot V(n, d-1)$ by $V(n, d-1)$ to obtain \begin{align*} |C| \ge \frac{2^n}{V(n, d-1)}. \end{align*} Since $|C| = A(n, d)$, this reads \begin{align*} A(n, d) \ge \frac{2^n}{V(n, d-1)}, \end{align*} which is the Gilbert–Varshamov bound. Combined with the Hamming bound from the first step, we obtain \begin{align*} \frac{2^n}{V(n, d-1)} \le A(n, d) \le \frac{2^n}{V\!\left(n, \left\lfloor \frac{d-1}{2} \right\rfloor\right)}, \end{align*} completing the proof. [/step]