Book XI · rung 11 · opened 2026-09-19 · the bottom of the ladder
What a Numeral Names
The bottom rung. For someone meeting written numbers as an adult, and for anyone teaching them. Nothing before this is assumed — not that you can read a numeral, not that you know what 7 means, not that you have ever done a sum.
Being a beginner is the hardest place to stand, because the subject is presented as a mountain. It is not one. You are handed the top of each slope and you come down it — that is what the sections below do, and it is why the general statement comes first and the things you can check by hand come after.
The Lean file is the certificate, not the lesson
An adult meeting written numbers for the first time does not read Lean, and no amount of gentle wording changes that. So the two jobs are kept apart. The learner works with marks, stones, rows and the numerals themselves. The teacher needs to know the rules being taught are the true ones, with no exception waiting further along to embarrass them. The .lean file is for the second reader, and every statement in it that survived has a line saying how to do it on a table with stones.
1 · What is in it
| § | the slope | what you do on the way down |
|---|
| 1 | Same size, decided without counting | pair a row of stones against a row of cups; whoever is left standing is the difference |
| 2 | A numeral is a name for how many | lay down one more stone, say the next word; and notice that the empty space in front of you is a number |
| 3 | Where a digit sits is part of its name | two heaps, one of ten-bundles and one of loose stones; swap which is which and count again |
2 · The payload, and the break that explains it
Two different two-digit numerals never name the same number — no_two_numerals_collide. Reading is never ambiguous. That is not free and it is not obvious: it holds because every digit is smaller than ten, and the file proves the failure directly rather than warning about it.
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 who has been shown the break understands place value; one who has only been shown examples has memorised a habit.
And the machine found something the draft had wrong
no_two_numerals_collide was written with all four digits bounded below ten. The proof closed without two of them. Only the ones digits have to be small: a digit needs to be below the base only at the place where it competes with the next bundle up. “27 tens and 3” is a perfectly unambiguous name for 273.
Where this sits on the ladder
The rung number is the volume number.
docs/floor-ladder.tsv holds the map and
tools/ladder_check.py refuses a rung whose volume disagrees in any of the three places it is written — the ladder, the directory, and the Lean file's own header.
11 what a numeral names ·
12 counting ·
14 the repairs ·
16 order, powers, roots ·
17 statistics ·
18 the chain rule ·
19 AXLE and the manual ·
20 polynomials and the circle ·
21 planar linear systems ·
28 index theory ·
33 noncommutative geometry
3 · Chapters
| ch | title | state |
|---|
| 1 | A Name for How Many — the three slopes, with the theorem that closes each | live |
| 2 | Bundling — why ten, and what changes if it is not ten | planned |
| 3 | Zero — the name most systems did not have, and what it cost them | planned |
4 · What this volume does not claim
- That reading the Lean file teaches anyone to count. It does not. It certifies what is taught.
- That these facts are new. They are not. What is new here is that they are checked, and that the check runs where the library cannot be downloaded.
- Any count of theorems without a tier. Nine theorems, all on the permitted three axioms, report beside the file.