The Exercise

A message of $k$ bits is sent through a noisy classical channel as a string of $n$ bits, and the channel flips some of the bits on the way. Sender and receiver agree beforehand on $2^k$ strings of $n$ bits, the codewords, one for each message and spaced so far apart that after any $t$ flips the receiver can still tell which codeword was sent.

The exercise asks for a guarantee on how many bits such a code can carry, for linear codes, those in which the bitwise sum modulo $2$ of two codewords is again a codeword: when $4t \le n$, a linear code of length $n$ that corrects $t$ errors exists for every $k$ up to a bound set by the binary entropy of the fraction $2t/n$.

Linear Codes

A linear code $C$ over a field $K$, with positions indexed by a set $\iota$, is a subspace of the space $K^{\iota}$ of words carrying a letter of $K$ at each position; its elements are its codewords. A binary linear code $C$ of length $n$ is a linear code over the field $\mathbb{Z}_2$ with $n$ positions, a subspace of $\mathbb{Z}_2^n$, and its dimension $\dim C$ over $\mathbb{Z}_2$ is the number of bits it carries.

The Hamming weight $\mathrm{wt}(c)$ of a word $c$ is the number of its nonzero entries. The minimum distance $d(C)$ of a linear code $C$ is the least Hamming weight of a nonzero codeword of $C$, $$d(C) = \min \{\, \mathrm{wt}(c) : c \in C,\ c \neq 0 \,\},$$(1)^✦ and the zero code, which has no nonzero codeword, has infinite minimum distance.

A linear code $C$ corrects $t$ errors when its minimum distance is at least $2t + 1$, $$d(C) \ge 2t + 1.$$(2)^✦

The Claim

The bound is written with the binary entropy $H(p) = -p \log_2 p - (1 - p) \log_2 (1 - p)$ of a probability $p$, in bits. The claim is the Gilbert-Varshamov bound.

What Is Checked

The claim is stated over the binary linear codes of length $n$, with their dimension, and over the condition (2) of correcting $t$ errors, built on the minimum distance (1).

What the library proves about these constructions is Theorem 1.