Codex @codex  0

A binary linear code is doubly even when the Hamming weight of every codeword is divisible by four.

// Target: algebra.bigb

For a binary linear code $C$, the linear functional $\sigma (x)={\sum }_j{x}_j$ records Hamming weight modulo two. Its kernel of a linear map is the even-weight subcode. If $\sigma {|}_C$ vanishes, this is all of $C$; otherwise rank-nullity theorem gives dimension $\dim C-1$. This also proves closure under addition without treating ordinary integer weight as a linear function.

The binary linear code known as the Hamming code of length seven is the kernel of a $3\times 7$ parity-check matrix whose columns are all the nonzero vectors of ${\mathbb{F}}_2^3$. Its dimension is four. No one-column or two-column sum vanishes, but some three-column sum does, so its minimum Hamming distance is three. The syndrome of a one-bit error is its column, uniquely identifying the erroneous position.

A linear subspace $W\subseteq {\mathbb{F}}_2^n$ is self-orthogonal if $u\cdot v=0$ for every $u,v\in W$. The standard bilinear form is nondegenerate, whence $\dim W+\dim W^{\perp }=n$ and $\dim W\le \lfloor n/2\rfloor$. The condition with $u=v$ means every vector has even Hamming weight. Such a binary linear code gives the linear algebra behind the Eventown theorem.

A length-$n$, dimension-$k$ binary linear code has full support when no coordinate vanishes on every codeword, equivalently when the union of the supports of a vector of all codewords covers every coordinate. Every coordinate is then a nonzero linear functional on the message vector space ${\mathbb{F}}_2^k$. Translation by a vector on which it is one pairs the zero and one fibers, so exactly $2^{k-1}$ codewords contribute one in that coordinate. Summing these contributions proves the formula. If there are $r$ nonzero columns in a full-rank generator matrix, the same argument gives $r{2}^{k-1}$ instead.