= Solution
A <binary linear code> of length $n$ is a <vector subspace> $C\subseteq\mathbb F_2^n$. The <Hamming weight> of a word counts its nonzero coordinates, and the code weight is $w(C)=\min_{0\ne c\in C}\operatorname{wt}(c)$; for a <linear code> this equals its <minimum distance>. One may assign infinite minimum weight to the zero code when needed.
For length-$n$ codes with $C_2\subseteq C_1$, the <bar product of binary linear codes> is
$$
C_1|C_2=\{(u,u+v):u\in C_1,\ v\in C_2\}\subseteq\mathbb F_2^{2n}.
$$
It is a <linear code> because this map from $C_1\oplus C_2$ is linear and injective. For a nonzero <codeword>, if $v=0$ then $u\ne0$ and its weight is $2\operatorname{wt}(u)\geq2w(C_1)$. If $v\ne0$, every nonzero coordinate of $v$ makes exactly one of the corresponding coordinates of $u,u+v$ nonzero; hence
$$
\operatorname{wt}(u)+\operatorname{wt}(u+v)\geq\operatorname{wt}(v)\geq w(C_2).
$$
Taking the minimum gives
$$
\boxed{w(C_1|C_2)\geq\min\{2w(C_1),w(C_2)\}.}
$$
In fact equality holds when the codes are nonzero: minimum-weight words $(u,u)$ and $(0,v)$ attain the two candidate weights.
Back to article page
