A Name for How Many · Book XI — Principia Orthogona

You are not being asked to climb anything. The general statement is the hill; the examples under it are what you do on the way down.

1 · Same size, decided without counting

You do not have to be able to count to know two rows are the same size. Put them side by side and match them one to one. If nobody is left standing on either side, the rows are the same size. This is older than counting and it is what counting is for.

same_size : n = m ↔ (n ≤ m ∧ m ≤ n)

Neither row is longer than the other — that is all “the same size” says. And if one row is longer, something is left standing on its side, and the number left standing is the difference:

left_over : m < n → 0 < n − m

The payload of this section one_of_three — pairing off and counting never disagree. Whatever two rows you have, exactly one of three things is true: the first is longer, the second is longer, or they match. There is no fourth case and no undecided case.

On the table. A row of stones and a row of cups, one stone to a cup. Then count only what is left over.

2 · A numeral is a name for how many

The marks III and the numeral 3 name the same row. One is shorter to write. Adding one mark makes the name go up by one, every time, forever — one_more. That is the whole of counting.

And there is a name for having none none_is_a_number. Most number systems in history did not have one, and everything after this rung needs it. On the table: the empty space in front of you is a number of stones.

3 · Where a digit sits is part of its name

12 and 21 are written with the same two marks and are not the same number. Nothing in the marks says so. The place says so. Reading a two-digit numeral is so many tens and so many ones.

no_two_numerals_collide : b < 10 → d < 10 → 10*a + b = 10*c + d → a = c ∧ b = d

Two different two-digit numerals never name the same number. Reading is never ambiguous. This is not obvious and it is not free: it holds because the digits are smaller than ten.

The break, as a theorem rather than a warning the_break : 10 * 1 + 10 = 10 * 2 + 0

Allow a digit to reach ten and “one ten and ten ones” and “two tens and none” both name twenty. That is why you bundle at ten and not at eleven. A learner shown the break understands place value; one shown only examples has memorised a habit.

And it is not about ten. no_collision_in_any_base holds for any bundling size, so long as no digit reaches the size you bundle at. Ten is a fact about hands; this is the fact underneath it.

What the machine corrected in the draft no_two_numerals_collide was first written with all four digits bounded. The proof closed without two of them, and the two it did not need were the tens digits. A digit has to be small enough only at the place where it competes with the next bundle up — “27 tens and 3” is an unambiguous name for 273.

4 · How to check this yourself

The file imports nothing. On a machine with only the Lean toolchain and no library at all:

lean Numerals.lean

About a second. The nine lines it prints are the report kept beside it, and tools/axiom_gate.py is what reads them.