The Digit That Guards the Rest

The check — every number on this page, verified

Each scheme here is recomputed live in your browser and proven independently in research/check-digits/verify.mjs — each claim twice, by an algebraic argument over the weights and by exhaustive or large-sample enumeration. 91/91 checks green. The last block hands the guarantees to the Lean kernel, for every length.

• Luhn — all single errors, all swaps but 0↔9. The doubling map is a bijection of the digits (so single errors can't hide); the swap blind spot is proven to be exactly {0,9} both algebraically and by testing every valid 6-digit Luhn number.
• ISBN-10 — the prime 11 catches every transposition. Proven for all positions and all digit pairs, and confirmed on 60,000 real-length ISBNs with zero misses. The X count — 90,909,090 of 1,000,000,000 — is computed exactly by a dynamic program over residues mod 11 (residue 1 is the single class one short of a perfect eleventh).
• EAN-13 — blind to the five ±5 swaps. The blind pairs {0,5}, {1,6}, {2,7}, {3,8}, {4,9} are derived algebraically and independently recovered by sweeping 60,000 valid barcodes.
• Verhoeff — all single and all adjacent, incl. 0↔9. Verified by exhaustively testing every valid number of length 2–7 (over a million of them) plus 40,000 random 16-digit numbers — zero single-error or adjacent-swap misses. The group D₅ is checked to be a genuine non-commutative group. Its imperfection on twin errors is demonstrated too, not hidden.
• Damm: the same guarantee, one table. Verified by exhaustively testing every valid number of length 2–7 plus 40,000 random 16-digit numbers, with zero single-error or adjacent-swap misses, and no blind pair at all. The table is checked to be a Latin square with an all-zero diagonal, totally anti-symmetric, and (unlike D₅) not associative. The zero-diagonal bonus (check digit = running total) is confirmed over 20,000 numbers.
• Named, not invented. Error-frequency figures are from J. Verhoeff, Error Detecting Decimal Codes (Mathematical Centre Tract 29, 1969): single-digit errors 79.05%, transpositions 10.21% of 12,112 recorded errors. The example card, ISBN and barcode numbers are published test values or computed here; no real personal account number is used or implied.

Machine-checked: the guarantees, for every length

Everything above is checked two ways, but for the for all lengths claims the tests can only sample: exhaustive over short numbers, a 60,000 sweep at real length, a named theorem for the rest. A sample, however large, settles only finitely many lengths. So the claims are also handed to a proof assistant that settles all lengths at once: research/check-digits/lean/CheckDigits.lean (Lean 4, zero imports, so the only trusted component is the kernel).

One idea does most of the work. Three of the schemes are a sum of per-position contributions, so editing one digit changes the total by exactly that position's local delta. Whether an error is caught therefore reduces to a finite fact about the ten-digit alphabet, which the kernel settles with zero axioms. Because the reduction is proved for an arbitrary number, the guarantee holds for every length and every position. The last two schemes fold a non-commutative product instead of a sum, and each needs its own reduction:

• Luhn. luhn_single_detects (every single error caught), luhn_swap_detects (every adjacent swap but the 0/9 pair caught), and luhn_swap_blind: the swap of an adjacent 0 and 9 is proved invisible, at every position. The one blind spot, exactly.
• ISBN-10. isbn_transposition_detects: a transposition of two distinct digits at any distance is caught. This is the prime 11 doing what mod 10 cannot, proved for the ten positions rather than sampled, and the whole reason some ISBNs end in X.
• EAN-13. ean_swap_detects / ean_swap_blind: every adjacent swap caught except the five |a−b|=5 pairs, each proved invisible.
• Verhoeff folds a non-commutative group product over the dihedral group D₅, not a sum, so it needs a second reduction (vfold_append splits the fold at a hole; vfold_factor lets the prefix cancel on the left, the suffix on the right). verhoeff_single_detects catches every single error; verhoeff_transposition_detects catches every adjacent transposition, with no blind pair, 0↔9 included. That last theorem is the one no commutative sum scheme above can prove; its whole content is the finite fact vtrans_core, that D₅'s product refuses to commute in exactly the way Verhoeff hand-designed across all eight positions.
• Damm folds a quasigroup that is not associative, so Verhoeff's factor-out-the-accumulator move cannot apply. The reduction is instead that the fold over any fixed suffix is a bijection of the running total (dfold_inj, because each step is a Latin-square column). damm_single_detects catches every single error; damm_transposition_detects catches every adjacent transposition with no blind pair, its whole content one finite fact, dm_antisym: the table is totally anti-symmetric. And damm_check_digit proves the zero-diagonal bonus: appending the payload's own running total always validates. Verhoeff's guarantee, from a single 10×10 table.

Every theorem's axiom footprint is [propext, Quot.sound] or tighter (the eight Damm theorems are just [propext]): no sorry, no Classical.choice, no native_decide. And the Lean model is cross-checked in JS against the schemes above over a sweep of numbers (valid and corrupted alike), so the predicate proved is the same one you just operated. Reproduce from a fresh checkout: bash research/check-digits/lean/install-lean-nix.sh && bash research/check-digits/lean/verify.sh.