[proofplan]
We show that any code achieving the maximum size $A(n, d+1)$ for minimum distance $d+1$ can be modified to produce a code with minimum distance $d$ and the same size, so the maximum size for minimum distance $d$ is at least $A(n, d+1)$. The modification picks two codewords $c_1, c_2$ realising the minimum distance $d+1$ and flips a single bit of $c_1$ in a coordinate where $c_1$ and $c_2$ differ, yielding a new word $c_1'$ at distance $d$ from $c_2$. The triangle inequality bounds the distance from $c_1'$ to every other codeword below by $d$, so replacing $c_1$ with $c_1'$ produces a valid $[n, A(n, d+1), d]$-code.
[/proofplan]
[step:Set up the extremal code with minimum distance $d+1$]
Let $m = A(n, d+1)$. By definition of $A(n, d+1)$ as the largest size of an $[n, \cdot, d+1]$-code (a binary code of blocklength $n$ and minimum distance at least $d+1$), there exists a code $C \subseteq \mathbb{F}_2^n$ of size $|C| = m$ and minimum distance exactly $d+1$ (if the minimum distance were strictly greater, we could artificially enlarge and still have distance $\ge d+1$; but we are interested in a concrete witness, and a maximal such code has minimum distance exactly $d+1$ when $d+1 \le n$ is achievable, which is implicit in the statement).
Let $c_1, c_2 \in C$ be a pair of codewords realising the minimum distance:
\begin{align*}
d(c_1, c_2) = d + 1.
\end{align*}
Such a pair exists because the minimum is attained. Let $i_0 \in \{1, \dots, n\}$ be any coordinate in which $c_1$ and $c_2$ differ; there are exactly $d + 1 \ge 1$ such coordinates, so at least one exists.
[/step]
[step:Define the modified codeword $c_1'$ by flipping one disagreement coordinate of $c_1$]
Define $c_1' \in \mathbb{F}_2^n$ by
\begin{align*}
(c_1')_i = \begin{cases} (c_1)_i + 1 \pmod{2} & \text{if } i = i_0 \\ (c_1)_i & \text{if } i \ne i_0, \end{cases}
\end{align*}
so $c_1'$ agrees with $c_1$ in every coordinate except $i_0$, where it has been flipped. Then $d(c_1, c_1') = 1$, and $(c_1')_{i_0} = (c_1)_{i_0} + 1 = (c_2)_{i_0}$ (using that $(c_1)_{i_0} \ne (c_2)_{i_0}$ in $\mathbb{F}_2$). Consequently $c_1'$ and $c_2$ agree at coordinate $i_0$ but still differ at the remaining $d$ coordinates in which $c_1$ and $c_2$ differed, so
\begin{align*}
d(c_1', c_2) = d.
\end{align*}
[/step]
[step:Use the triangle inequality to bound distances from $c_1'$ to other codewords]
We claim: for every $c \in C \setminus \{c_1\}$,
\begin{align*}
d(c_1', c) \ge d.
\end{align*}
Let $c \in C \setminus \{c_1\}$. By the Hamming triangle inequality applied to the triple $(c, c_1, c_1')$,
\begin{align*}
d(c, c_1) \le d(c, c_1') + d(c_1', c_1),
\end{align*}
equivalently $d(c, c_1') \ge d(c, c_1) - d(c_1', c_1)$. Because $c, c_1 \in C$ are distinct codewords and $C$ has minimum distance $d + 1$, we have $d(c, c_1) \ge d + 1$. Because $d(c_1', c_1) = 1$ by construction,
\begin{align*}
d(c, c_1') \ge (d + 1) - 1 = d,
\end{align*}
as claimed.
[guided]
Why does the triangle inequality give us the bound we need? We want to control $d(c_1', c)$ for every other codeword $c$. We know a lot about $c_1$: it is at distance $\ge d+1$ from every other codeword. And $c_1'$ is close to $c_1$ — at distance exactly $1$. So intuitively $c_1'$ should be at distance roughly $\ge d+1 - 1 = d$ from every other codeword.
The triangle inequality makes this precise. The inequality
\begin{align*}
d(c, c_1) \le d(c, c_1') + d(c_1', c_1)
\end{align*}
says "the detour from $c$ to $c_1$ via $c_1'$ is at least as long as the direct path". Rearranging,
\begin{align*}
d(c, c_1') \ge d(c, c_1) - d(c_1', c_1).
\end{align*}
Now we plug in the known bounds:
- $d(c, c_1) \ge d + 1$ because $c \ne c_1$ are two codewords of a minimum-distance-$(d+1)$ code,
- $d(c_1', c_1) = 1$ by our explicit construction of $c_1'$ as a single bit-flip of $c_1$.
The result is $d(c, c_1') \ge (d+1) - 1 = d$. The bound is achieved by $c = c_2$, where $d(c_2, c_1') = d$ exactly.
What if we had flipped a bit in a coordinate where $c_1$ and $c_2$ *agree*? Then $c_1'$ and $c_2$ would disagree on the flipped coordinate *plus* all $d+1$ coordinates of original disagreement, so $d(c_1', c_2) = d + 2$. We wouldn't have achieved the target distance $d$, and the modification would not lower the minimum distance. This is why the construction specifically picks a coordinate in which $c_1$ and $c_2$ differ.
[/guided]
[/step]
[step:Form the replacement code and verify its minimum distance is exactly $d$]
Define
\begin{align*}
C' := (C \setminus \{c_1\}) \cup \{c_1'\}.
\end{align*}
We check that $C'$ is a well-defined code, i.e., that $c_1' \notin C \setminus \{c_1\}$. If $c_1' \in C$ and $c_1' \ne c_1$, then $c_1$ and $c_1'$ would be two distinct codewords of $C$ with $d(c_1, c_1') = 1 < d + 1$, contradicting the minimum distance hypothesis on $C$. Hence $c_1' \notin C \setminus \{c_1\}$, and
\begin{align*}
|C'| = |C \setminus \{c_1\}| + 1 = (m - 1) + 1 = m.
\end{align*}
The minimum distance of $C'$ is computed over distinct pairs in $C'$. There are two cases:
- Both codewords lie in $C \setminus \{c_1\}$: they are distinct codewords of $C$, so their distance is $\ge d + 1 > d$.
- One codeword is $c_1'$ and the other is some $c \in C \setminus \{c_1\}$: by the previous step, $d(c_1', c) \ge d$.
So every pair of distinct codewords in $C'$ has distance $\ge d$, and the pair $(c_1', c_2)$ achieves distance $d$ exactly. Hence the minimum distance of $C'$ is exactly $d$. In particular, $C'$ is a code with blocklength $n$, size $m$, and minimum distance at least $d$ — i.e., an $[n, m, d]$-code in the relaxed sense that $d(C') \ge d$.
[/step]
[step:Conclude the monotonicity inequality]
We have exhibited an $[n, m, d]$-code $C'$ with $m = A(n, d+1)$. By definition $A(n, d)$ is the supremum of $|C'|$ over codes $C'$ of blocklength $n$ with minimum distance at least $d$. Hence
\begin{align*}
A(n, d) \ge |C'| = m = A(n, d+1),
\end{align*}
which is the claimed inequality $A(n, d+1) \le A(n, d)$. This completes the proof.
[/step]
