The usual story is that zero was a great invention because without it you cannot tell 25 from 205. This chapter checks that story and finds half of it wrong. A numeral system can do perfectly well without a zero digit. What zero really gives you is smaller and more useful: it makes every digit a remainder.
On the table: three loose stones, and an empty plate where the ten-bundles go. Written out, that is 03. Add an empty plate for hundreds and it is 003. Every empty plate adds a zero and changes nothing.
For the teacher: Bundling.lean proves that a zero in the highest place never changes the value (high_zero). So 3 and 03 are two names for one number (two_names). The script counts four names for three at lengths one to four COMPUTED. That is why Chapter 2's uniqueness theorem needs “the same length”, and why we agree never to write a leading zero. Zero causes this ambiguity just as much as it resolves the other one.
Use the digits one to ten, with a single symbol for ten (write it A), and no zero. Ten is A. Twenty is 1A, one ten and ten ones. A hundred is 9A, nine tens and ten ones. 2026 is 1A26. This is called bijective numeration, and it has no ambiguity at all. bijective_unique proves that two zero-free numerals of any lengths name the same number only if they are the same. The script lists all 111,110 zero-free names up to five digits and finds that every number from 1 to 100,000 has exactly one COMPUTED.
So 25 and 205 can be kept apart without a zero: 205 is 1A5. The ambiguity people blame on missing zero comes from a gap left with nothing in it, not from the missing digit.
On the table: share 273 stones into bundles of ten. You get 27 bundles and 3 left over. Share the bundles into tens: 2 and 7 left over. The digits of 273, read from the right, are exactly the leftovers: 3, 7, 2.
For the teacher: low_digit_is_remainder proves that the lowest digit of a standard numeral is its remainder on division by the base. multiple_ends_in_zero proves that a number which shares out evenly ends in zero. That is what zero is for: it is the name of “nothing left over”. Every standard digit is a possible remainder, 0 through 9, and the script confirms that reading remainders back gives every number below 100,000 COMPUTED.
The zero-free system loses exactly this. Twenty's lowest digit there is ten, but twenty shares into tens with nothing left over COMPUTED. Its digits are not remainders, so the checks and short-cuts that use remainders all need adjusting: divisibility tests, carrying, reading off n mod 10. The zero-free system is sometimes shorter (a hundred takes two digits instead of three). It is never simpler to calculate in.