Solution (source code)

= Solution

Work over the <finite field> $\mathbb F_2$. Reduce <polynomials> modulo $X_i^2-X_i$, so their monomials are square-free. The binary <Reed-Muller code> $\operatorname{RM}(r,m)$ consists of the evaluation vectors of <polynomials> of degree at most $r$ at all $2^m$ points of $\mathbb F_2^m$, in a fixed order. This is a <linear code> of length $2^m$ and dimension $\sum_{j=0}^r\binom mj$, for $0\leq r\leq m$. Square-free monomials give independent evaluation functions, as follows inductively by splitting according to the last variable.

The <minimum Hamming distance of a linear code> equals its least nonzero <Hamming weight>. The result is
$$
\boxed{d(\operatorname{RM}(r,m))=2^{m-r}\quad(0\leq r\leq m).}
$$
Here $r=0$ is the <repetition code>, while $r=m$ is the full binary vector space and has distance one. For the induction step, write $f(x,t)=u(x)+t v(x)$, where $\deg u\leq r$ and $\deg v\leq r-1$. Its evaluation vector is $(u,u+v)$, the <Reed-Muller bar-product recursion>. If $v=0$, its nonzero <Hamming weight> is at least $2d(r,m-1)=2^{m-r}$, with the full-space endpoint treated as above. If $v\ne0$, every position where $v=1$ contributes exactly one to the sum of the two weights; hence the weight is at least $\operatorname{wt}(v)\geq2^{(m-1)-(r-1)}=2^{m-r}$. The monomial $X_1\cdots X_r$ is one exactly on $2^{m-r}$ points, attaining the bound. Degrees greater than $m$ give the same full code; the zero code at negative degree has no nonzero word whose weight could define a finite minimum.