Book XII · rung 12 · opened 2026-09-19
Counting, and the First Thing That Goes Wrong
Rung 11 comes first: what a numeral names. This rung assumes that much and no more, and it ends at the place where the counting numbers give way — the place nobody is warned about.
Everything on this rung works, until one line does not. Subtraction is not the opposite of addition. It is the opposite of addition only when you may take the smaller from the larger, and on the counting numbers that is a condition, not a rule.
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 | the payload at the bottom |
|---|
| 1 | Every number is zero, or one more than another | counting never stops, and you can say why in one line |
| 2 | Order does not matter, and neither does grouping | a sum has one value however you add it |
| 3 | Multiplying is adding | any two-digit multiplication splits into a ten-times table and a small one |
| 4 | Place value, said exactly once | the same sentence holds in any base — which makes place value an idea, not a habit about ten |
| 5 | The first thing that goes wrong | there are pairs you cannot get back from |
2 · The line that gives way
sub_add_cancel_iff : a - b + b = a ↔ b ≤ a
Take five from three and put it back, and you are at five, not three. Nothing is broken and nothing is hidden: the counting numbers do not contain an answer to “three take away five”, so the machine returns the nearest one they do contain.
Why the next rung exists
subtraction_is_not_inverse exhibits the pair. The integers are not a harder subject. They are the repair for that one line, and a reader arriving at them has already seen exactly what needed repairing.
3 · One more thing the file does not hide
place_value_base carries no condition on the base at all. It holds for base zero, because n / 0 = 0 and n % 0 = n, so the equation reads 0 + n = n. Division by zero is not forbidden here; it is given a value, and the value was chosen so that sentences like this one stay true without an exception clause bolted on. Volume XVII takes that up as its own subject.
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
4 · Chapters
| ch | title | state |
|---|
| 1 | The Line That Gives Way — five slopes, and the pair you cannot get back from | live |
| 2 | Carrying — what the little one above the column actually is | planned |
| 3 | Division — the remainder as a first-class answer | planned |