A number that knows when it is wrong
A librarian in Kampala types the 13-digit number from the back of a new book. A cashier in Lima scans a packet of rice; the scanner misreads one bar. A student in Seoul types her card number into a website and swaps two digits. In each case the computer answers at once: that number is not valid — please check it.
How can a computer know that a number is wrong without knowing what the right number was? The trick is to add one extra digit — a check digit — calculated from all the others. If any digit is typed wrongly, the calculation no longer comes out right. The calculation is clock arithmetic, from the previous lesson, and the reason it works is a small, beautiful theorem about the number 11.
A digit that summarises the others
Here is a first attempt. Add up the digits of a number, and choose one extra digit so that the total ends in — that is, so that the digit sum is a multiple of . For the number the digit sum is , so we append and send (total ).
- If one digit is mistyped, say , the total becomes . It no longer ends in : caught. Changing one digit changes the total by a number between and that is not , so the total can never land on another multiple of .
- If two neighbouring digits are swapped, , the total is still . A plain sum does not care about order: missed.
Swapping neighbours is one of the most common mistakes people make when they copy numbers. To catch it, the check must notice where each digit is. The idea: multiply each digit by a weight that depends on its position before adding up. Then moving a digit changes its weight, and so changes the total. But which weights, and which modulus? That is where the mathematics comes in.
Definitions
Definition— check digit
A check digit is an extra digit computed from the other digits of a code number so that certain errors can be detected. A code number is valid if its check digit is the right one.
Definition— ISBN-10
An ISBN-10 (International Standard Book Number, used until 2006) has ten digits with
The check digit can be , which is printed as X (the Roman numeral for ten).
Some books state the rule with the weights in the other order, . The two rules accept exactly the same numbers, because the two sums add up to , a multiple of 11.
Definition— ISBN-13
An ISBN-13 (used since 2007; the same system as the EAN-13 barcodes on shop goods) has thirteen digits with weights alternating :
Definition— parity bit
A message of bits (0s and 1s) is protected by a parity bit: one extra bit chosen so that the total number of 1s is even. The receiver counts the 1s; an odd count means something went wrong.
Worked examples
Example— Computing an ISBN-10 check digit
The first nine digits of a sample ISBN are . The weighted sum of these nine is
We need to be a multiple of 11. Since , this says , so (as ). The check digit is , printed X: the full ISBN is 3-16-148410-X. Check: . ✓
In general, the ISBN-10 check digit is the weighted sum of the first nine digits, modulo 11.
Example— Verifying an ISBN-13
For 978-3-16-148410-0:
a multiple of 10. Valid. If the librarian types 978-3-16-148710-0 instead (a in a weight-3 position became ), the sum grows by to , which is not a multiple of 10: caught.
Example— A swap that ISBN-13 cannot see
Swap the neighbouring digits and of 978-3-16-148410-0 to get 978-3-61-148410-0. Positions 5 and 6 have weights and , so their contribution changes from to : down by . The total becomes , still a multiple of 10. The wrong number is accepted! The same swap in the ISBN-10, 3-61-148410-X, is caught: its sum is .
Example— A parity bit
The 7-bit message contains four 1s, an even number, so its parity bit is and we send . If noise flips one bit and arrives, it has three 1s — odd — and the receiver asks for the message again. But if two bits flip, say , the count is again even and the damage goes unnoticed.
What each scheme catches, and why
All the proofs below use one observation: if two code numbers are both valid, the difference of their check sums is a multiple of the modulus. So to show that an error is always caught, we show that it changes the check sum by something that is not a multiple of the modulus.
Theorem— Theorem 1 (ISBN-10 catches every single-digit error)
If one digit of a valid ISBN-10 is changed, the result is not a valid ISBN-10.
Proof
Suppose the digit in position changes from to . Only one term of the check sum changes, from to , so the sum changes by . If the new number were valid too, 11 would divide . Now and , so neither factor is a multiple of 11. Because 11 is prime, it divides a product only if it divides one of the factors (Euclid's lemma). So 11 does not divide , and the error is caught. (Without Euclid's lemma: the multiplication table modulo 11 has no outside row and column — every non-zero row is a shuffle, as you can check in the explorer below.)
∎
Theorem— Theorem 2 (ISBN-10 catches every swap of neighbours)
If two different neighbouring digits of a valid ISBN-10 are swapped, the result is not a valid ISBN-10.
Proof
Let the neighbours be in position and in position , with . Their contribution to the sum is before the swap and after. The difference is
and , so it is not a multiple of 11. The swap is caught.
∎
In fact ISBN-10 catches the swap of any two different digits, neighbours or not: swapping positions and changes the sum by , and the argument of Theorem 1 applies to this product.
Theorem— Theorem 3 (ISBN-13 catches every single-digit error)
If one digit of a valid ISBN-13 is changed, the result is not a valid ISBN-13.
Proof
Changing to changes the sum by (weight 1) or by (weight 3), where . In the first case the change is not a multiple of 10. In the second case, suppose were a multiple of 10. Then so would be , and hence itself — impossible. (We used that is the partner of modulo : .)
∎
Theorem— Theorem 4 (the ISBN-13 blind spot)
Swapping two neighbouring digits of a valid ISBN-13 gives another valid ISBN-13 exactly when and differ by .
Proof
Neighbouring positions have weights and (in some order). Say has weight 1 and weight 3. The contribution changes from to , a change of . This is a multiple of 10 exactly when is a multiple of 5, that is (for digits ) when . The other order of weights gives the change and the same conclusion.
∎
Theorem— Theorem 5 (parity bits)
A parity bit detects every error in which an odd number of bits are flipped, and no error in which an even number are flipped.
Proof
Flipping one bit changes the number of 1s by exactly one (up or down), so it changes the count from even to odd or from odd to even. Flipping bits changes the parity times. The sent word has an even number of 1s; the received word therefore has an odd number of 1s exactly when is odd. The receiver rejects exactly those words.
∎
Detecting is not correcting
When a number fails the test, can the computer work out what it should have been? With one check digit, no. Suppose 3-26-148410-X arrives. It fails the ISBN-10 test (its sum is ). It could be 3-16-148410-X with the second digit mistyped — but it could equally be 1-26-148410-X with the first digit mistyped, and that is also a valid ISBN-10. In general, for an invalid number, almost every position has some digit that would make it valid again.
Mathematicians measure this with the Hamming distance: the number of positions in which two code numbers differ. Theorem 1 says any two valid ISBN-10s are at distance at least 2. That is enough to notice one error, but a damaged number can sit at distance 1 from two valid ones, so there is no way to choose. To correct one error, valid code numbers must be at distance at least 3 from each other. Codes with that property exist — Richard Hamming and Marcel Golay published early examples around 1950 — but they need more than one check symbol (see information theory).
Bank cards and phones: Luhn's scheme
Bank card numbers, and the 15-digit IMEI number that identifies every mobile phone, end in a check digit computed by the Luhn scheme, patented by Hans Peter Luhn of IBM (filed 1954). Reading from the right, leave the last digit alone, double the next one, leave the next, double the next, and so on; whenever doubling gives a two-digit number, add its digits (). The number is valid if the total is a multiple of 10.
Example— The Luhn test
For , from the right: ; ; ; ; ; ; ; ; ; ; . The total is : valid.
Doubling-and-adding-digits sends the digits to — a shuffle, with no two digits landing on the same value. That is why Luhn's scheme catches every single-digit error. Neighbour swaps are caught too, with exactly one exception: swapping and () leaves the total unchanged. Neither ISBN-13 nor Luhn catches swaps of digits two places apart, because those positions get the same treatment; ISBN-10 does.
Check digits in Lean
A code number is a list of digits. Everything rests on one definition and one lemma: a weighted sum, and what happens to it when one digit in the middle of the list changes.
/-- The weighted sum of a list of digits: the digit in position `k` is multiplied by `w k`.
`wsum w k ds` starts counting positions at `k`. -/
def wsum (w : Nat → Nat) : Nat → List Nat → Nat
| _, [] => 0
| k, d :: ds => w k * d + wsum w (k + 1) ds/-- **Splitting a check sum at one digit.** If a code is `pre ++ x :: post` (some digits, then
the digit `x`, then more digits), its weighted sum is the sum over `pre`, plus `x` times its
weight, plus the sum over `post`. So when only `x` changes, only the middle term changes.
Proof by induction on the digits before `x`. -/
theorem wsum_append_cons (w : Nat → Nat) (pre post : List Nat) (x k : Nat) :
wsum w k (pre ++ x :: post) =
wsum w k pre + w (k + pre.length) * x + wsum w (k + pre.length + 1) post := by
induction pre generalizing k with
| nil => simp [wsum]
| cons d ds ih =>
simp only [List.cons_append, wsum, ih, List.length_cons]
have h1 : k + 1 + ds.length = k + (ds.length + 1) := by omega
rw [h1]
omegaThen ISBN-10: the definition, our example, the recipe for the check digit, and Theorems 1 and 2 for every ISBN-10. The finite fact “a non-zero weight can be cancelled modulo 11” is checked by decide, which tries all cases.
/-- The ISBN-10 check sum `1·d₁ + 2·d₂ + ⋯ + 10·d₁₀` (the weight of position `k` is `k`). -/
def isbn10Sum (ds : List Nat) : Nat := wsum (fun k => k) 1 ds/-- A valid ISBN-10: ten digits (the last may be `10`, printed `X`) whose check sum is a
multiple of `11`. -/
abbrev ValidISBN10 (ds : List Nat) : Prop := ds.length = 10 ∧ isbn10Sum ds % 11 = 0/-- The sample number `3-16-148410-X` is a valid ISBN-10 (`X` stands for `10`):
`1·3 + 2·1 + 3·6 + 4·1 + 5·4 + 6·8 + 7·4 + 8·1 + 9·0 + 10·10 = 231 = 21 · 11`. -/
theorem example_isbn10 : ValidISBN10 [3, 1, 6, 1, 4, 8, 4, 1, 0, 10] := by decide/-- **How to compute the check digit.** For any nine digits, appending
`(1·d₁ + ⋯ + 9·d₉) mod 11` gives a valid ISBN-10.
Proof: if the first nine digits have sum `S`, the full sum is `S + 10 · (S mod 11)`. Writing
`S = 11q + r`, this is `11q + 11r`, a multiple of 11. (Because `10 ≡ -1 (mod 11)`.) -/
theorem isbn10_check_digit (ds : List Nat) (h : ds.length = 9) :
ValidISBN10 (ds ++ [isbn10Sum ds % 11]) := by
refine ⟨by simp [h], ?_⟩
have hsplit := wsum_append_cons (fun k => k) ds [] (isbn10Sum ds % 11) 1
simp only [wsum, Nat.add_zero, h] at hsplit
show wsum (fun k => k) 1 (ds ++ [isbn10Sum ds % 11]) % 11 = 0
rw [hsplit]
-- `S + 10 · (S mod 11)` is a multiple of 11.
show (isbn10Sum ds + (1 + 9) * (isbn10Sum ds % 11)) % 11 = 0
omega/-- Modulo the prime `11`, a non-zero weight can be cancelled: if `w ≠ 0` and
`w · x ≡ w · y (mod 11)` for remainders `x, y`, then `x = y`. In words, each non-zero row of
the multiplication table modulo 11 is a shuffle. `decide` checks all `11³` cases. -/
theorem cancel_mod_eleven : ∀ w, w < 11 → ∀ x, x < 11 → ∀ y, y < 11 → w ≠ 0 →
(w * x) % 11 = (w * y) % 11 → x = y := by decide/-- **ISBN-10 detects every single-digit error.** If two ISBN-10s are identical except for
one digit (`x` in one, `y` in the other) and both are valid, then `x = y`.
Proof: by `wsum_append_cons` the two sums differ only in the term `w · x` versus `w · y`, where
the weight `w` is the position, between 1 and 10. Both sums are multiples of 11, so
`w · x ≡ w · y (mod 11)`, and `cancel_mod_eleven` gives `x = y`. -/
theorem isbn10_single_error (pre post : List Nat) (x y : Nat) (hx : x ≤ 10) (hy : y ≤ 10)
(h₁ : ValidISBN10 (pre ++ x :: post)) (h₂ : ValidISBN10 (pre ++ y :: post)) : x = y := by
obtain ⟨hlen, hs₁⟩ := h₁
obtain ⟨_, hs₂⟩ := h₂
simp only [List.length_append, List.length_cons] at hlen
unfold isbn10Sum at hs₁ hs₂
rw [wsum_append_cons] at hs₁ hs₂
-- Name the weight and the two middle terms, so that only linear arithmetic remains.
generalize hu : (1 + pre.length) * x = u at hs₁
generalize hv : (1 + pre.length) * y = v at hs₂
have huv : u % 11 = v % 11 := by omega
rw [← hu, ← hv] at huv
exact cancel_mod_eleven (1 + pre.length) (by omega) x (by omega) y (by omega) (by omega) huv/-- **ISBN-10 detects every swap of two neighbouring digits.** If `… x y …` and `… y x …` are
both valid ISBN-10s, then `x = y` (so nothing was really swapped).
Proof: neighbouring positions have weights `w` and `w + 1`, so the two sums are
`… + w·x + (w+1)·y + …` and `… + w·y + (w+1)·x + …`. Their difference is `y - x`, which lies
strictly between `-11` and `11`; it is a multiple of 11 only when `x = y`. -/
theorem isbn10_adjacent_swap (pre post : List Nat) (x y : Nat) (hx : x ≤ 10) (hy : y ≤ 10)
(h₁ : ValidISBN10 (pre ++ x :: y :: post)) (h₂ : ValidISBN10 (pre ++ y :: x :: post)) :
x = y := by
obtain ⟨_, hs₁⟩ := h₁
obtain ⟨_, hs₂⟩ := h₂
unfold isbn10Sum at hs₁ hs₂
simp only [wsum_append_cons, wsum] at hs₁ hs₂
-- The two middle terms: `w·x + (w+1)·y` and `w·y + (w+1)·x`, with `w = 1 + pre.length`.
rw [Nat.add_mul (1 + pre.length) 1 y] at hs₁
rw [Nat.add_mul (1 + pre.length) 1 x] at hs₂
generalize (1 + pre.length) * x = u at hs₁ hs₂
generalize (1 + pre.length) * y = v at hs₁ hs₂
omega/-- Swapping the neighbouring digits `1` and `6` in `3-16-148410-X` gives `3-61-148410-X`,
which is **not** a valid ISBN-10: the error is caught. -/
theorem swap_caught_by_isbn10 : ¬ ValidISBN10 [3, 6, 1, 1, 4, 8, 4, 1, 0, 10] := by decideISBN-13: Theorem 3 for every ISBN-13, and Theorem 4 checked for all 100 pairs of digits, with the swap from our example.
/-- ISBN-13 weights: positions `1, 3, 5, …` have weight `1`, positions `2, 4, 6, …` weight `3`. -/
def isbn13Weight (k : Nat) : Nat := if k % 2 = 1 then 1 else 3/-- A valid ISBN-13: thirteen digits whose weighted sum `d₁ + 3d₂ + d₃ + 3d₄ + ⋯ + d₁₃` is a
multiple of `10`. -/
abbrev ValidISBN13 (ds : List Nat) : Prop :=
ds.length = 13 ∧ wsum isbn13Weight 1 ds % 10 = 0/-- `978-3-16-148410-0` is a valid ISBN-13: its weighted sum is `100`. -/
theorem example_isbn13 : ValidISBN13 [9, 7, 8, 3, 1, 6, 1, 4, 8, 4, 1, 0, 0] := by decide/-- The weight `3` can be cancelled modulo 10: `3 · x ≡ 3 · y (mod 10)` forces `x = y` for
digits `x, y`. (The row of `3` in the multiplication table modulo 10 is a shuffle, because
`3` has the partner `7`.) `decide` checks all 100 pairs. -/
theorem cancel_three_mod_ten : ∀ x, x < 10 → ∀ y, y < 10 →
(3 * x) % 10 = (3 * y) % 10 → x = y := by decide/-- **ISBN-13 detects every single-digit error.** Same structure as for ISBN-10: the two sums
differ only in `w · x` versus `w · y`, the weight `w` is `1` or `3`, and both can be cancelled
modulo 10 (`cancel_three_mod_ten`). -/
theorem isbn13_single_error (pre post : List Nat) (x y : Nat) (hx : x ≤ 9) (hy : y ≤ 9)
(h₁ : ValidISBN13 (pre ++ x :: post)) (h₂ : ValidISBN13 (pre ++ y :: post)) : x = y := by
obtain ⟨_, hs₁⟩ := h₁
obtain ⟨_, hs₂⟩ := h₂
rw [wsum_append_cons] at hs₁ hs₂
unfold isbn13Weight at hs₁ hs₂
-- The weight of the changed position is `1` or `3` (the same in both codes).
split at hs₁ <;> split at hs₂
· -- weight 1: the sums differ by `y - x` itself.
omega
· omega
· omega
· -- weight 3: cancel the 3.
generalize hu : 3 * x = u at hs₁
generalize hv : 3 * y = v at hs₂
have huv : u % 10 = v % 10 := by omega
rw [← hu, ← hv] at huv
exact cancel_three_mod_ten x (by omega) y (by omega) huv/-- **Which neighbouring swaps does ISBN-13 miss?** Swapping neighbours `a, b` (weights `1` and
`3`) leaves the check sum unchanged modulo 10 exactly when `a = b` or the digits differ by 5.
`decide` checks all 100 pairs of digits. -/
theorem isbn13_swap_rule : ∀ a, a < 10 → ∀ b, b < 10 →
((a + 3 * b) % 10 = (b + 3 * a) % 10 ↔ (a = b ∨ a + 5 = b ∨ b + 5 = a)) := by
decide/-- A swap ISBN-13 cannot see: `978-3-16-148410-0` and the same digits with the neighbours `1`
and `6` swapped are **both** valid, because `6 - 1 = 5`. -/
theorem isbn13_missed_swap :
ValidISBN13 [9, 7, 8, 3, 1, 6, 1, 4, 8, 4, 1, 0, 0] ∧
ValidISBN13 [9, 7, 8, 3, 6, 1, 1, 4, 8, 4, 1, 0, 0] := by decideisbn13_swap_rule is about the two neighbouring digits only; combined with wsum_append_cons it gives Theorem 4 for whole code numbers, a step we explain in words rather than formalise. The Luhn scheme, with its two key facts checked over all pairs of digits:
/-- Luhn's doubling: double the digit, and if the result has two digits, add them
(`2·7 = 14 → 1 + 4 = 5`). For a digit `d` this is `2d` if `d < 5` and `2d - 9` otherwise. -/
def luhnDouble (d : Nat) : Nat := if d < 5 then 2 * d else 2 * d - 9/-- The Luhn sum, reading the digits **from the right**: the last digit is added as it is, the
next one doubled with `luhnDouble`, the next added as it is, and so on. A number passes the
Luhn test when this sum is a multiple of 10. (`luhnSumRev` takes the digits right to left.) -/
def luhnSumRev : Bool → List Nat → Nat
| _, [] => 0
| dbl, d :: ds => (if dbl then luhnDouble d else d) + luhnSumRev (!dbl) ds/-- The number `7992 7398 713` passes the Luhn test: its Luhn sum is `70`. -/
theorem example_luhn : luhnSumRev false [7, 9, 9, 2, 7, 3, 9, 8, 7, 1, 3].reverse % 10 = 0 := by
decide/-- Luhn's doubling sends different digits to different digits (`0,1,…,9 ↦ 0,2,4,6,8,1,3,5,7,9`),
so a single wrong digit always changes the Luhn sum by something that is not a multiple of 10.
`decide` checks all pairs. -/
theorem luhn_double_shuffle : ∀ a, a < 10 → ∀ b, b < 10 →
luhnDouble a = luhnDouble b → a = b := by decide/-- **The one swap Luhn misses.** Swapping neighbours `a, b` (one of them doubled) leaves the Luhn
sum unchanged modulo 10 exactly when `a = b` or the pair is `0, 9` or `9, 0`. -/
theorem luhn_swap_rule : ∀ a, a < 10 → ∀ b, b < 10 →
((a + luhnDouble b) % 10 = (b + luhnDouble a) % 10 ↔
(a = b ∨ (a = 0 ∧ b = 9) ∨ (a = 9 ∧ b = 0))) := by
decideParity bits (Theorem 5), proved by induction on the list of bits:
/-- The parity of a list of bits: `true` if it contains an odd number of `1`s (`true`s),
`false` if an even number. (`xor` is "exactly one of the two".) -/
def parity : List Bool → Bool
| [] => false
| b :: bs => xor b (parity bs)/-- The parity of two blocks of bits put together is the `xor` of their parities.
Proof by induction on the first block. -/
theorem parity_append (l₁ l₂ : List Bool) : parity (l₁ ++ l₂) = xor (parity l₁) (parity l₂) := by
induction l₁ with
| nil => simp [parity]
| cons a as ih => simp [parity, ih]/-- **Adding a parity bit.** Appending the parity of a message to the message always gives an
even number of `1`s in total: `parity (bs ++ [parity bs]) = false`. -/
theorem add_parity_bit (bs : List Bool) : parity (bs ++ [parity bs]) = false := by
rw [parity_append]
simp [parity]/-- Flipping any one bit flips the parity. Proof by induction on the bits before it. -/
theorem parity_flip (pre post : List Bool) (b : Bool) :
parity (pre ++ (!b) :: post) = !parity (pre ++ b :: post) := by
induction pre with
| nil => simp [parity]
| cons a as ih => simp [parity, ih]/-- **A parity bit detects any single flipped bit**: if the sent word had even parity, the
received word with one bit flipped has odd parity, so the receiver knows something went wrong. -/
theorem single_flip_detected (pre post : List Bool) (b : Bool)
(h : parity (pre ++ b :: post) = false) : parity (pre ++ (!b) :: post) = true := by
rw [parity_flip, h]
rfl/-- **… but never two.** Flipping two bits (`a` and, further on, `b`) leaves the parity exactly
as it was, so the error passes unnoticed. Two uses of `parity_flip`. -/
theorem double_flip_undetected (pre mid post : List Bool) (a b : Bool) :
parity (pre ++ (!a) :: (mid ++ (!b) :: post)) = parity (pre ++ a :: (mid ++ b :: post)) := by
rw [parity_flip]
have h : pre ++ a :: (mid ++ (!b) :: post) = (pre ++ a :: mid) ++ (!b) :: post := by simp
have h' : pre ++ a :: (mid ++ b :: post) = (pre ++ a :: mid) ++ b :: post := by simp
rw [h, h', parity_flip]
simpAnd the reason a check digit cannot correct:
/-- Two codes are *one digit apart* if they agree everywhere except in one position. -/
def OneDigitApart (c₁ c₂ : List Nat) : Prop :=
∃ pre post : List Nat, ∃ x y : Nat, x ≠ y ∧ c₁ = pre ++ x :: post ∧ c₂ = pre ++ y :: post/-- **A check digit cannot tell you which digit is wrong.** The received number `3-26-148410-X`
is invalid, and it is one digit away from **two different** valid ISBN-10s, `3-16-148410-X`
and `1-26-148410-X`. So the scheme detects the error but cannot correct it. -/
theorem cannot_correct :
¬ ValidISBN10 [3, 2, 6, 1, 4, 8, 4, 1, 0, 10] ∧
ValidISBN10 [3, 1, 6, 1, 4, 8, 4, 1, 0, 10] ∧
ValidISBN10 [1, 2, 6, 1, 4, 8, 4, 1, 0, 10] ∧
OneDigitApart [3, 2, 6, 1, 4, 8, 4, 1, 0, 10] [3, 1, 6, 1, 4, 8, 4, 1, 0, 10] ∧
OneDigitApart [3, 2, 6, 1, 4, 8, 4, 1, 0, 10] [1, 2, 6, 1, 4, 8, 4, 1, 0, 10] := by
refine ⟨by decide, by decide, by decide, ?_, ?_⟩
· exact ⟨[3], [6, 1, 4, 8, 4, 1, 0, 10], 2, 1, by decide, rfl, rfl⟩
· exact ⟨[], [2, 6, 1, 4, 8, 4, 1, 0, 10], 3, 1, by decide, rfl, rfl⟩All of these are proved here (core Lean only); none quotes a library theorem about codes. In Mathlib, ZMod 11 is the field of remainders modulo 11 and hammingDist is the Hamming distance.
Every typo, counted
"""Which typing errors do check digits catch? Every typo of 300 codes, counted.
For four schemes - ISBN-10 (weights 1..10, mod 11), ISBN-13 (weights 1, 3,
mod 10), Luhn (bank cards and phone IMEIs) and a naive "digit sum mod 10" -
the experiment makes 300 valid code numbers from seeded random digits, then
applies every possible single-digit error, every swap of neighbouring digits
and every swap of digits two apart ("jump" swaps, abc -> cba), and counts how
many of the damaged numbers are rejected. The counts are exact for this sample
of codes; the lesson proves which errors are always caught.
"""
import random
def isbn10_check(first9):
"""ISBN-10 check digit (10 means X) for nine digits, weights 1..9."""
return sum((i + 1) * d for i, d in enumerate(first9)) % 11
def isbn10_valid(code):
"""Ten digits (last may be 10) with 1*d1 + ... + 10*d10 = 0 mod 11."""
return len(code) == 10 and sum((i + 1) * d for i, d in enumerate(code)) % 11 == 0
def isbn13_valid(code):
"""Thirteen digits with d1 + 3*d2 + d3 + 3*d4 + ... = 0 mod 10."""
total = sum(d * (1 if i % 2 == 0 else 3) for i, d in enumerate(code))
return len(code) == 13 and total % 10 == 0
def isbn13_check(first12):
"""The ISBN-13 check digit for twelve digits."""
total = sum(d * (1 if i % 2 == 0 else 3) for i, d in enumerate(first12))
return (-total) % 10
def luhn_double(d):
"""Double a digit and add the digits of the result."""
return 2 * d if d < 5 else 2 * d - 9
def luhn_sum(code):
"""Luhn sum: from the right, every second digit is doubled."""
return sum(luhn_double(d) if i % 2 == 1 else d
for i, d in enumerate(reversed(code)))
def luhn_valid(code):
"""A number passes the Luhn test when its Luhn sum is a multiple of 10."""
return luhn_sum(code) % 10 == 0
def luhn_check(payload):
"""The digit to append so that payload + [digit] passes the Luhn test."""
return (-luhn_sum(list(payload) + [0])) % 10
def digitsum_valid(code):
"""Naive scheme: the plain digit sum is a multiple of 10."""
return sum(code) % 10 == 0
def make_codes(scheme, count, seed=2026):
"""``count`` valid codes for ``scheme`` from seeded random digits."""
rng = random.Random(seed)
codes = []
for _ in range(count):
if scheme == "ISBN-10":
body = [rng.randrange(10) for _ in range(9)]
codes.append(body + [isbn10_check(body)])
elif scheme == "ISBN-13":
body = [rng.randrange(10) for _ in range(12)]
codes.append(body + [isbn13_check(body)])
elif scheme == "Luhn":
body = [rng.randrange(10) for _ in range(15)]
codes.append(body + [luhn_check(body)])
else:
body = [rng.randrange(10) for _ in range(9)]
codes.append(body + [(-sum(body)) % 10])
return codes
VALID = {"ISBN-10": isbn10_valid, "ISBN-13": isbn13_valid,
"Luhn": luhn_valid, "digit sum": digitsum_valid}
def errors(code, kind, isbn10=False):
"""All damaged versions of ``code`` with one error of the given kind."""
out = []
n = len(code)
if kind == "single":
for i in range(n):
top = 11 if (isbn10 and i == n - 1) else 10
out += [code[:i] + [v] + code[i + 1:] for v in range(top)
if v != code[i]]
else:
gap = 1 if kind == "neighbour swap" else 2
for i in range(n - gap):
if code[i] != code[i + gap]:
c = list(code)
c[i], c[i + gap] = c[i + gap], c[i]
out.append(c)
return out
def detection(scheme, kind, codes):
"""(caught, total) over every error of ``kind`` applied to ``codes``."""
valid = VALID[scheme]
caught = total = 0
for code in codes:
for bad in errors(code, kind, isbn10=(scheme == "ISBN-10")):
total += 1
caught += not valid(bad)
return caught, total
def main():
kinds = ["single", "neighbour swap", "jump swap"]
print("Share of damaged codes rejected (300 valid codes per scheme)")
print(f"{'scheme':<10}" + "".join(f"{k:>22}" for k in kinds))
for scheme in VALID:
codes = make_codes(scheme, 300)
assert all(VALID[scheme](c) for c in codes)
cells = []
for kind in kinds:
caught, total = detection(scheme, kind, codes)
cells.append(f"{100 * caught / total:6.1f}% of {total:>5}")
print(f"{scheme:<10}" + "".join(f"{c:>22}" for c in cells))
print()
print("Swaps count only when the two digits differ. A 'jump swap' exchanges")
print("digits two places apart: in ISBN-13 and Luhn those positions have the")
print("same weight, so such swaps are never caught; ISBN-10 catches them all.")
print()
print("Epistemic status: exact counts for every error of three kinds applied")
print("to these 300 codes per scheme. The percentages for ISBN-13 and Luhn")
print("swaps depend on which digit pairs occur; that ISBN-10 catches every")
print("single error and every neighbour swap is a theorem, proved in the")
print("lesson for all ISBN-10s, not just these.")
if __name__ == "__main__":
main()The table agrees with the theorems: ISBN-10 rejects every damaged number; ISBN-13 lets through about one neighbour swap in nine (those of digits five apart); Luhn lets through only ; the plain digit sum catches every single error but no swap at all. The percentages for ISBN-13 and Luhn are exact counts for this sample, not universal constants — they depend on which digit pairs happen to occur.
"""A parity bit on a noisy line: simulation next to the exact probabilities.
Each word is 7 data bits plus 1 parity bit, so every word sent has an even
number of 1s. The channel flips each of the 8 bits independently with
probability p. The receiver accepts a word with an even number of 1s and
rejects one with an odd number. A seeded simulation of 10,000 words per value
of p is compared with exact formulas: a word arrives intact with probability
(1 - p)^8, is rejected exactly when an odd number of bits flipped, and slips
through damaged when an even number (2, 4, 6 or 8) flipped.
"""
import math
import random
BITS = 8 # 7 data bits + 1 parity bit
def with_parity(data):
"""Append a parity bit so that the number of 1s is even."""
return list(data) + [sum(data) % 2]
def accepted(word):
"""The receiver's test: an even number of 1s."""
return sum(word) % 2 == 0
def exact_probabilities(p, n=BITS):
"""(intact, rejected, undetected) probabilities for n bits, flip prob p."""
flips = [math.comb(n, k) * p ** k * (1 - p) ** (n - k) for k in range(n + 1)]
intact = flips[0]
rejected = sum(flips[k] for k in range(1, n + 1, 2))
undetected = sum(flips[k] for k in range(2, n + 1, 2))
return intact, rejected, undetected
def simulate(p, words, seed):
"""Counts (intact, rejected, undetected) for ``words`` random words."""
rng = random.Random(seed)
intact = rejected = undetected = 0
for _ in range(words):
sent = with_parity([rng.randrange(2) for _ in range(BITS - 1)])
got = [b ^ (rng.random() < p) for b in sent]
if got == sent:
intact += 1
elif accepted(got):
undetected += 1
else:
rejected += 1
return intact, rejected, undetected
def main():
words = 10_000
print(f"{words} words of 7 data bits + 1 parity bit; each bit flips with")
print("probability p. Simulated counts, then the exact expected counts:")
print()
print(f"{'p':>5} {'':9}{'intact':>9}{'rejected':>10}{'undetected':>12}")
for k, p in enumerate((0.01, 0.05, 0.2)):
sim = simulate(p, words, seed=100 + k)
exp = [words * q for q in exact_probabilities(p)]
print(f"{p:>5} {'simulated':9}{sim[0]:>9}{sim[1]:>10}{sim[2]:>12}")
print(f"{'':>5} {'exact':9}{exp[0]:>9.1f}{exp[1]:>10.1f}{exp[2]:>12.1f}")
print()
print("With p = 0.01 almost every damaged word is caught: two flips in one")
print("word are rare. With p = 0.2 about 4 in 10 damaged words slip through,")
print("because an even number of flips is invisible to a parity bit.")
print()
print("Epistemic status: the simulated counts are statistical evidence from")
print("one seeded run and wobble around the exact values; the exact columns")
print("are binomial probabilities that follow from the theorem 'a parity bit")
print("detects an odd number of flips and no even number', with the extra")
print("assumption that bits flip independently.")
if __name__ == "__main__":
main()This is statistical evidence: the simulated counts wobble around the exact values from one run to another. The exact columns come from Theorem 5 together with an extra assumption — that each bit flips independently — which real channels do not always satisfy (noise often comes in bursts that damage several neighbouring bits).
Explore: good weights and parity
A weight catches every single-digit error modulo exactly when the row of in the multiplication table modulo is a shuffle (no repeated values). Open the Multiply tab and set : every non-zero row is a shuffle, so any of the weights works. Now set : only the rows of are shuffles. That is why ISBN-13 uses the weights and — and why no weighted scheme modulo 10 can use ten different good weights.
The clock laboratory
On a clock with k hours, counting wraps around. Explore adding and multiplying.
9 + 5 = 14 ≡ 2 (mod 12)
14 hours forward on a 12-hour clock lands on 2: the remainder when 14 is divided by 12.
Below, , , are three data bits and is their parity bit ( is exclusive or: true when exactly one input is true). The receiver adds up the received bits modulo 2 — that is the formula. The first formula flips bit in transit; it is true (odd: rejected) in every row. The second flips and ; it is false (even: accepted) in every row.
One flipped bit versus two
Type a formula of propositional logic and see its value in every possible case.
Read as: ((¬a ⊕ b) ⊕ c) ⊕ ((a ⊕ b) ⊕ c)
Read as: ((¬a ⊕ ¬b) ⊕ c) ⊕ ((a ⊕ b) ⊕ c)
Use the symbols ¬ ∧ ∨ → ↔, the words not, and, or, implies, iff, or ASCII ~ & | -> <->. Variables are single lowercase letters. ¬ binds tightest, then ∧, ∨, →, ↔; p → q → r means p → (q → r).
Tautology — true in all 8 rows.
Not equivalent — they differ in 8 of 8 rows (marked ≠).
| a | b | c | ((¬a ⊕ b) ⊕ c) ⊕ ((a ⊕ b) ⊕ c) | ((¬a ⊕ ¬b) ⊕ c) ⊕ ((a ⊕ b) ⊕ c) | Rows where they differ |
|---|---|---|---|---|---|
| T | T | T | T | F | ≠ |
| T | T | F | T | F | ≠ |
| T | F | T | T | F | ≠ |
| T | F | F | T | F | ≠ |
| F | T | T | T | F | ≠ |
| F | T | F | T | F | ≠ |
| F | F | T | T | F | ≠ |
| F | F | F | T | F | ≠ |
8 rows: one for every way of making the 3 variables true or false.
Exercises
1. Check digits and error detection
Warm-upHumanThe first nine digits of an ISBN-10 are . What is the check digit? (If it is X, answer .)
2. Check digits and error detection
Warm-upHumanExactly one of these is a valid ISBN-13. Which one?
3. Check digits and error detection
CoreHumanFind the check digit of the ISBN-13 that begins .
4. Check digits and error detection
Warm-upHumanWhat parity bit should be added to the message so that the total number of 1s is even? (Answer or .)
5. Check digits and error detection
CoreHumanWhich swap of two neighbouring digits can go undetected in an ISBN-13?
6. Check digits and error detection
CoreHumanIn the proof that ISBN-10 catches every swap of neighbours, is in position and in position . By how much does the swap change the check sum?
7. Check digits and error detection
StretchHumanOne digit of a valid ISBN-10 is smudged: . The smudged digit is in position . Find it. (Hint: you will need a partner modulo .)
8. Check digits and error detection
CoreHumanA received ISBN-10 fails the check. Which statement is true?
9. Check digits and error detection
CoreFormalIn Lean, a code number is a list of digits and pre ++ x :: post is the list pre, then the digit x, then the list post. Which statement says that ISBN-10 detects every single-digit error?
10. Check digits and error detection
StretchComputationalWrite luhn_valid(number), where number is a string of digits, returning True if it passes the Luhn test: from the right, keep the 1st, 3rd, 5th, … digits as they are; double the 2nd, 4th, … digits, subtracting when the double is more than ; the total must be a multiple of . Then check the blind spot: 1099 and 1909 differ by a swap.
Common misconceptions
Misconception
“A check digit can correct the error.” A single check digit only detects errors. As the example 3-26-148410-X shows, a damaged number can be one digit away from several valid numbers, so there is no way to tell which digit was wrong. Correcting errors needs more redundancy.
Misconception
“Every possible error is detected.” Each scheme catches certain kinds of errors and misses others. ISBN-13 misses neighbour swaps of digits differing by 5; Luhn misses ; even ISBN-10 misses some errors that change two digits at once, such as a damaged number that happens to be another valid ISBN. A valid check digit means “no likely error”, not “certainly correct”.
Misconception
“The X in an ISBN is a misprint.” In ISBN-10 the check digit is a remainder modulo 11, so it can be , which is written X. ISBN-13 works modulo 10 and never needs an X.
Misconception
“The more bits go wrong, the more likely a parity bit is to notice.” Not at all: a second flipped bit undoes the effect of the first on the count, so two flipped bits are never noticed. On a very noisy line a large share of the damaged words slip through, as the simulation above shows.
Other ways of seeing
Algebra— Why 11 — and what Verhoeff did instead
A weighted scheme modulo catches every single error when each weight has a partner modulo , and every neighbour swap when each difference of neighbouring weights has a partner. Modulo 10 that is impossible: the weights with partners are , all odd, so the difference of two of them is even, and an even difference times is a multiple of 10. No weighted scheme modulo 10 can catch all single errors and all neighbour swaps. ISBN-10 escapes by working modulo the prime 11, at the price of the extra symbol X. In 1969 the Dutch mathematician Jacobus Verhoeff found a cleverer escape: he replaced addition modulo 10 by the multiplication table of the dihedral group of order 10 — the ten rigid motions of a regular pentagon (five turns and five flips) — combined with a shuffle of the digits. Because that group is not commutative ( in general), it notices order, and Verhoeff's scheme catches every single error and every neighbour swap using the digits – only. India's Aadhaar identity numbers end in a Verhoeff check digit. See groups and rigid motions.
Combinatorics— Codes as points at a distance
Think of all strings of 10 digits as points, and say two strings are at distance when they differ in positions (the Hamming distance). The valid ISBN-10s are a set of points no two of which are at distance 1: around each valid code is a “ball” of the strings one error away, containing no other valid code. Detecting one error needs minimum distance 2; correcting one error needs minimum distance 3, so that the balls of radius 1 do not overlap. Counting points in balls gives limits on how many valid codes there can be — the start of coding theory.
Probability— How likely is an undetected error?
If a number is damaged in a completely random way, its check sum modulo 11 is essentially a random remainder, so it passes the ISBN-10 test with probability about . But real errors are not random: studies of people copying numbers, such as Verhoeff's, found that single-digit errors are by far the most common, followed by neighbour swaps. A good scheme is designed for the errors people actually make — and for those, ISBN-10 is perfect.
History and global context
- 1948–1950. Claude Shannon's theory of communication (1948) showed that errors can in principle be corrected efficiently; Marcel Golay (1949) and Richard Hamming (1950), both working in the USA, published some of the first error-correcting codes.
- 1954. Hans Peter Luhn of IBM filed a patent for a device that computes his check digit (granted in 1960). His scheme now protects bank cards worldwide and the IMEI numbers of mobile phones.
- 1966–1970. A 9-digit Standard Book Numbering system was devised in the United Kingdom in 1966 and became the international ISBN-10 standard (ISO 2108) in 1970.
- 1969. Jacobus Verhoeff in the Netherlands published his dihedral-group scheme, together with a study of the errors people make when copying numbers.
- 1974. The first product with a Universal Product Code barcode (weights modulo 10) was scanned in a supermarket in Ohio, USA. The European Article Number (EAN-13) followed and spread around the world.
- 2007. Books switched to 13-digit ISBNs, identical to EAN-13 barcodes with the prefix 978 or 979.
- Today. International bank account numbers (IBANs), used in dozens of countries, carry two check digits computed modulo 97; India's Aadhaar numbers use Verhoeff's scheme.
Further reading
- Joseph A. Gallian, Contemporary Abstract Algebra (1986; 10th edition 2021), which uses check digits — including Verhoeff's dihedral scheme — as running examples.
- Joseph A. Gallian, “The mathematics of identification numbers”, The College Mathematics Journal 22 (1991).
- Joseph Kirtland, Identification Numbers and Check Digit Schemes (Mathematical Association of America, 2000), written for school and college classrooms.
- Richard W. Hamming, “Error detecting and error correcting codes”, Bell System Technical Journal 29 (1950).