Skip to content

Hamming (7,4) code

DefinitionGenerator matrix of the Hamming (7,4) code#✓fully proved

\(G\) is the \(4 \times 7\) matrix over \(\mathbb{F}_2\), with columns indexed by the positions \(1, \dots, 7\), whose \(k\)-th row encodes the \(k\)-th message bit: if \(p\) is the \(k\)-th of the message positions \(3, 5, 6, 7\), the row has entry \(1\) at position \(p\) and at each of the parity positions \(1, 2, 4\) that occurs in the binary expansion of \(p\), and entry \(0\) elsewhere.

Explicitly, its rows are \(1110000\), \(1001100\), \(0101010\) and \(1101001\).

def G : Matrix (Fin 4) (Fin 7) (ZMod 2) :=
  !![1, 1, 1, 0, 0, 0, 0;
     1, 0, 0, 1, 1, 0, 0;
     0, 1, 0, 1, 0, 1, 0;
     1, 1, 0, 1, 0, 0, 1]
Used by 6
Used byEvery single-bit error is corrected · Encoder of the Hamming code · The generator matrix is orthogonal to the parity-check matrix · Minimum distance of the Hamming (7,4) code · The Hamming generator matrix generates the Hamming code · The Hamming bound is attained

DefinitionParity-check matrix of the Hamming (7,4) code#✓fully proved

\(H\) is the \(3 \times 7\) matrix over \(\mathbb{F}_2\), with columns indexed by the positions \(1, \dots, 7\), whose column at position \(p\) is the binary expansion of \(p\), least significant bit first: its entry in row \(i\), for \(i = 0, 1, 2\), is the \(i\)-th binary digit of \(p\).

def H : Matrix (Fin 3) (Fin 7) (ZMod 2) :=
  !![1, 0, 1, 0, 1, 0, 1;
     0, 1, 1, 0, 0, 1, 1;
     0, 0, 0, 1, 1, 1, 1]
Used by 9
Used byThe Hamming (7,4) code · Syndrome decoder of the Hamming code · The decoder corrects every error of weight at most 1 · The decoder always outputs a codeword · The syndrome of a single-bit error locates it · The generator matrix is orthogonal to the parity-check matrix · The Hamming decoder's syndrome table is correct · The Hamming generator matrix generates the Hamming code · The Hamming (7,4) code has minimum weight at least 3

DefinitionThe Hamming (7,4) code#✓fully proved

Let \(H\) be the \(3 \times 7\) matrix over \(\mathbb{F}_2\) whose column \(j\), for \(j = 1, \dots, 7\), is the binary expansion of \(j\), least significant bit first. The Hamming code is the binary linear code of length \(7\) with parity-check matrix \(H\): the words \(c \in \mathbb{F}_2^7\) with \(Hc = 0\).

def code : LinearCode (ZMod 2) (Fin 7) := ofParityCheck H
Uses 3 · Used by 10
Statement usesParity-check matrix of the Hamming (7,4) code · Linear code · Code with a given parity-check matrix
Used byThe decoder corrects every error of weight at most 1 · Every single-bit error is corrected · The decoder always outputs a codeword · The Hamming code is perfect · No codeword is closer than the Hamming decoder's output · Minimum distance of the Hamming (7,4) code · The Hamming generator matrix generates the Hamming code · The Hamming bound is attained · Hamming bound for the Hamming (7,4) code · The Hamming (7,4) code has minimum weight at least 3

DefinitionEncoder of the Hamming code#✓fully proved

Let \(G\) be the \(4 \times 7\) generator matrix over \(\mathbb{F}_2\) with rows \((1,1,1,0,0,0,0)\), \((1,0,0,1,1,0,0)\), \((0,1,0,1,0,1,0)\) and \((1,1,0,1,0,0,1)\). A message \(m \in \mathbb{F}_2^4\) is encoded as the word \(mG \in \mathbb{F}_2^7\), the combination of the rows of \(G\) with coefficients \(m\).

def encode (m : Fin 4 → ZMod 2) : Fin 7 → ZMod 2 := LinearCode.encode G m
Uses 2 · Used by 4
Statement usesGenerator matrix of the Hamming (7,4) code · Encoder of a generator matrix
Used byEvery single-bit error is corrected · Minimum distance of the Hamming (7,4) code · The Hamming generator matrix generates the Hamming code · The Hamming bound is attained

DefinitionMessage bits of a word#✓fully proved

The message of a word \(y = (y_1, \dots, y_7) \in \mathbb{F}_2^7\) is \((y_3, y_5, y_6, y_7) \in \mathbb{F}_2^4\), its bits at the positions that are not powers of two.

def message (y : Fin 7 → ZMod 2) : Fin 4 → ZMod 2 := ![y 2, y 4, y 5, y 6]
Used by 2
Used byThe Hamming generator matrix generates the Hamming code · The Hamming bound is attained

DefinitionError position of a syndrome#✓fully proved

For a syndrome \(s = (s_0, s_1, s_2) \in \mathbb{F}_2^3\), read its entries as bits of the number \(p = s_0 + 2s_1 + 4s_2 \in \{0, \dots, 7\}\). If \(p = 0\) there is no error position; otherwise the error position is \(p - 1 \in \{0, \dots, 6\}\).

def errorPos (s : Fin 3 → ZMod 2) : Option (Fin 7) :=
  let p := (s 0).val + 2 * (s 1).val + 4 * (s 2).val
  have hp : p - 1 < 7 := by
    have := ZMod.val_lt (s 0)
    have := ZMod.val_lt (s 1)
    have := ZMod.val_lt (s 2)
    omega
  if p = 0 then none else some ⟨p - 1, hp⟩
Used by 2
Used byThe syndrome of a single-bit error locates it · Syndrome table of the Hamming (7,4) code

DefinitionSyndrome table of the Hamming (7,4) code#✓fully proved

Number the positions of a word in \(\mathbb{F}_2^7\) as \(1, \dots, 7\). For a syndrome \(s = (s_0, s_1, s_2) \in \mathbb{F}_2^3\), read each \(s_i\) as \(0\) or \(1\) and let \(p = s_0 + 2 s_1 + 4 s_2\). The table sends \(s\) to the zero word if \(p = 0\), and otherwise to the word whose only nonzero entry is a \(1\) at position \(p\).

The Hamming decoder subtracts from a received word the table entry of its syndrome; over \(\mathbb{F}_2\) this flips the bit at the position the syndrome names.

def table (s : Fin 3 → ZMod 2) : Fin 7 → ZMod 2 :=
  match errorPos s with
  | none => 0
  | some p => Pi.single p 1
Uses 1 · Used by 3
Statement usesError position of a syndrome
Used bySyndrome decoder of the Hamming code · The decoder corrects every error of weight at most 1 · The Hamming decoder's syndrome table is correct

DefinitionSyndrome decoder of the Hamming code#✓fully proved

Let \(H\) be the \(3 \times 7\) parity-check matrix of the Hamming code over \(\mathbb{F}_2\), whose column \(j\), for \(j = 1, \dots, 7\), is the binary expansion of \(j\), least significant bit first. Given a word \(y \in \mathbb{F}_2^7\), compute its syndrome \(s = (s_0, s_1, s_2) = Hy \in \mathbb{F}_2^3\). If \(s = 0\), return \(y\). Otherwise read the entries of \(s\) as bits of the number \(p = s_0 + 2s_1 + 4s_2 \in \{1, \dots, 7\}\) and return \(y\) with its \(p\)-th bit flipped, counting positions from \(1\).

def decode (y : Fin 7 → ZMod 2) : Fin 7 → ZMod 2 := y - table (syndrome H y)
Uses 3 · Used by 6
Statement usesParity-check matrix of the Hamming (7,4) code · Syndrome table of the Hamming (7,4) code · Syndrome
Used byThe decoder corrects every error of weight at most 1 · Every single-bit error is corrected · The decoder always outputs a codeword · The Hamming code is perfect · No codeword is closer than the Hamming decoder's output · The Hamming decoder changes at most one bit

TheoremThe syndrome of a single-bit error locates it#✓fully proved

Let \(H\) be the parity-check matrix of the Hamming (7,4) code, and index the coordinates of words in \(\mathbb{F}_2^7\) by \(0, \dots, 6\), so that index \(i\) is position \(i + 1\). For each index \(i\), let \(e_i \in \mathbb{F}_2^7\) be the word with entry \(1\) at index \(i\) and \(0\) elsewhere. Then the error position of the syndrome \(He_i\) is defined and equals \(i\).

theorem errorPos_syndrome_single (i : Fin 7) :
    errorPos (syndrome H (Pi.single i 1)) = some i
Uses 3
Statement usesParity-check matrix of the Hamming (7,4) code · Error position of a syndrome · Syndrome

TheoremThe Hamming decoder's syndrome table is correct#✓fully proved

Let \(H\) be the parity-check matrix of the Hamming (7,4) code and \(T\) the syndrome table of its decoder. Then \(T\) is a correct syndrome table up to radius \(1\) for \(H\): for every word \(e \in \mathbb{F}_2^7\) of Hamming weight at most \(1\), the word \(T(He)\) has Hamming weight at most \(1\) and the same syndrome as \(e\), that is, \(H \, T(He) = He\).

theorem isSyndromeTable_table : IsSyndromeTable H 1 table
Uses 4 · Used by 1
Statement usesParity-check matrix of the Hamming (7,4) code · Syndrome table of the Hamming (7,4) code · Syndrome table correct up to a radius
Proof usesSyndrome
Used byThe decoder corrects every error of weight at most 1
22 fully proved

The code

TheoremThe generator matrix is orthogonal to the parity-check matrix#✓fully proved

Let \(G\) be the generator matrix and \(H\) the parity-check matrix of the Hamming (7,4) code over \(\mathbb{F}_2\). Then \(G H^{\mathsf{T}} = 0\), the \(4 \times 3\) zero matrix: every row of \(G\) is orthogonal to every row of \(H\), so every row of \(G\) satisfies the parity checks given by \(H\).

theorem G_mul_H_transpose : G * Hᵀ = 0
Uses 2 · Used by 1
Statement usesGenerator matrix of the Hamming (7,4) code · Parity-check matrix of the Hamming (7,4) code
Used byThe Hamming generator matrix generates the Hamming code

TheoremThe Hamming generator matrix generates the Hamming code#✓fully proved

The code generated by the generator matrix \(G\), that is, the set of words \(mG\) for \(m \in \mathbb{F}_2^4\), equals the Hamming (7,4) code, the set of words \(c \in \mathbb{F}_2^7\) with \(Hc = 0\) for the parity-check matrix \(H\).

theorem ofGenerator_G_eq_code : ofGenerator G = code
Uses 11 · Used by 3
Statement usesGenerator matrix of the Hamming (7,4) code · The Hamming (7,4) code · Linear code · Code generated by a matrix
Proof usesThe generator matrix is orthogonal to the parity-check matrix · Parity-check matrix of the Hamming (7,4) code · Encoder of the Hamming code · Message bits of a word · Encoder of a generator matrix · Generator/parity-check duality · Code with a given parity-check matrix
Used byEvery single-bit error is corrected · Minimum distance of the Hamming (7,4) code · The Hamming bound is attained

TheoremThe Hamming (7,4) code has minimum weight at least 3#✓fully proved

Every nonzero codeword of the Hamming (7,4) code over \(\mathbb{F}_2\) has at least \(3\) nonzero coordinates; that is, the minimum weight of the code is at least \(3\).

theorem three_le_minWeight_code : 3 ≤ code.minWeight
Uses 5 · Used by 1
Statement usesThe Hamming (7,4) code · Minimum weight
Proof usesParity-check matrix of the Hamming (7,4) code · Linear code · Syndrome
Used byMinimum distance of the Hamming (7,4) code

TheoremMinimum distance of the Hamming (7,4) code#✓fully proved

The minimum distance of the Hamming (7,4) code is \(3\).

theorem minDist_code : code.minDist = 3
Uses 11 · Used by 4
Statement usesThe Hamming (7,4) code · Minimum distance
Proof usesGenerator matrix of the Hamming (7,4) code · Encoder of the Hamming code · The Hamming generator matrix generates the Hamming code · The Hamming (7,4) code has minimum weight at least 3 · Linear code · Encoder of a generator matrix · Minimum distance equals minimum weight · Minimum weight · Code generated by a matrix
Used byThe decoder corrects every error of weight at most 1 · The Hamming code is perfect · No codeword is closer than the Hamming decoder's output · Hamming bound for the Hamming (7,4) code

Decoding

TheoremThe decoder corrects every error of weight at most 1#✓fully proved

For every codeword \(c\) of the Hamming code and every word \(e \in \mathbb{F}_2^7\) of Hamming weight at most \(1\), decoding \(c + e\) returns \(c\).

theorem decode_add {c e : Fin 7 → ZMod 2} (hc : c ∈ code) (he : hammingNorm e ≤ 1) :
    decode (c + e) = c
Uses 8 · Used by 1
Statement usesThe Hamming (7,4) code · Syndrome decoder of the Hamming code · Linear code
Proof usesParity-check matrix of the Hamming (7,4) code · The Hamming decoder's syndrome table is correct · Minimum distance of the Hamming (7,4) code · Syndrome table of the Hamming (7,4) code · Syndrome decoding up to half the minimum distance
Used byEvery single-bit error is corrected

TheoremEvery single-bit error is corrected#✓fully proved

For every message \(m \in \mathbb{F}_2^4\) and every position \(i\) among the \(7\), flipping bit \(i\) of the encoding of \(m\) and then decoding returns the encoding of \(m\).

theorem decode_encode_add_single (m : Fin 4 → ZMod 2) (i : Fin 7) :
    decode (encode m + Pi.single i 1) = encode m
Uses 9
Statement usesSyndrome decoder of the Hamming code · Encoder of the Hamming code
Proof usesGenerator matrix of the Hamming (7,4) code · The Hamming (7,4) code · The decoder corrects every error of weight at most 1 · The Hamming generator matrix generates the Hamming code · Linear code · Encoder of a generator matrix · Code generated by a matrix

The code is perfect

TheoremThe decoder always outputs a codeword#✓fully proved

For every word \(y \in \mathbb{F}_2^7\), the decoding of \(y\) belongs to the Hamming code.

theorem decode_mem_code (y : Fin 7 → ZMod 2) : decode y ∈ code
Uses 5 · Used by 2
Statement usesThe Hamming (7,4) code · Syndrome decoder of the Hamming code · Linear code
Proof usesParity-check matrix of the Hamming (7,4) code · Syndrome
Used byThe Hamming code is perfect · No codeword is closer than the Hamming decoder's output

TheoremThe Hamming decoder changes at most one bit#✓fully proved

Let \(D\) be the Hamming (7,4) decoder. For every word \(y \in \mathbb{F}_2^7\), the Hamming distance between \(y\) and \(D(y)\) is at most \(1\).

theorem hammingDist_decode_le_one (y : Fin 7 → ZMod 2) : hammingDist y (decode y) ≤ 1
Uses 1 · Used by 2
Statement usesSyndrome decoder of the Hamming code
Used byThe Hamming code is perfect · No codeword is closer than the Hamming decoder's output

TheoremThe Hamming code is perfect#✓fully proved

Every word lies within distance 1 of exactly one codeword.

theorem existsUnique_hammingDist_le_one (y : Fin 7 → ZMod 2) :
    ∃! c, c ∈ code ∧ hammingDist y c ≤ 1
Uses 7
Statement usesThe Hamming (7,4) code · Linear code
Proof usesSyndrome decoder of the Hamming code · The decoder always outputs a codeword · The Hamming decoder changes at most one bit · Minimum distance of the Hamming (7,4) code · Minimum distance

TheoremNo codeword is closer than the Hamming decoder's output#✓fully proved

Let \(D\) be the Hamming (7,4) decoder and \(C \subseteq \mathbb{F}_2^7\) the Hamming code. For every word \(y \in \mathbb{F}_2^7\) and every codeword \(c \in C\), the Hamming distance between \(y\) and \(D(y)\) is at most the Hamming distance between \(y\) and \(c\).

Since \(D(y)\) is itself a codeword, the decoder returns a nearest codeword.

theorem hammingDist_decode_le (y : Fin 7 → ZMod 2) {c : Fin 7 → ZMod 2} (hc : c ∈ code) :
    hammingDist y (decode y) ≤ hammingDist y c
Uses 7
Statement usesThe Hamming (7,4) code · Syndrome decoder of the Hamming code · Linear code
Proof usesThe decoder always outputs a codeword · The Hamming decoder changes at most one bit · Minimum distance of the Hamming (7,4) code · Minimum distance

TheoremHamming bound for the Hamming (7,4) code#✓fully proved

Let \(k\) be the dimension of the Hamming (7,4) code over \(\mathbb{F}_2\). Then \(2^k \cdot \sum_{i=0}^{1} \binom{7}{i} (2 - 1)^i \le 2^7\).

This is the Hamming bound for codes correcting one error, obtained from the general Hamming bound for linear codes, which applies because the minimum distance \(3\) exceeds \(2\).

theorem pow_finrank_mul_sum_le :
    Fintype.card (ZMod 2) ^ Module.finrank (ZMod 2) code *
        ∑ i ∈ Finset.range (1 + 1), (7 : ℕ).choose i * (Fintype.card (ZMod 2) - 1) ^ i ≤
      Fintype.card (ZMod 2) ^ 7
Uses 5
Statement usesThe Hamming (7,4) code · Linear code
Proof usesMinimum distance of the Hamming (7,4) code · Minimum distance · Hamming bound for linear codes

TheoremThe Hamming bound is attained#✓fully proved

Let \(k\) be the dimension of the Hamming (7,4) code over \(\mathbb{F}_2\). Then \(2^k \cdot \sum_{i=0}^{1} \binom{7}{i} (2 - 1)^i = 2^7\): the Hamming bound for one error holds with equality.

Since \(k = 4\), this reads \(2^4 \cdot (1 + 7) = 2^7\), so the radius-\(1\) Hamming balls around the codewords fill \(\mathbb{F}_2^7\).

theorem pow_finrank_mul_sum_eq :
    Fintype.card (ZMod 2) ^ Module.finrank (ZMod 2) code *
        ∑ i ∈ Finset.range (1 + 1), (7 : ℕ).choose i * (Fintype.card (ZMod 2) - 1) ^ i =
      Fintype.card (ZMod 2) ^ 7
Uses 7
Statement usesThe Hamming (7,4) code · Linear code
Proof usesGenerator matrix of the Hamming (7,4) code · Encoder of the Hamming code · Message bits of a word · The Hamming generator matrix generates the Hamming code · Code generated by a matrix

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.