The Line That Gives Way · Book XII

Counting, order, grouping and place value all behave. Then one line does not, and nobody is warned about it.

1 · Every number is zero, or one more than another

That sentence is the whole of counting, and Lean's Nat is defined by it: zero, and succ. zero_or_succ says there is nothing else a natural number can be. The payload: counting never stops, and you can say why in one line — whatever number you name, that number plus one is bigger.

2 · Order does not matter, and neither does grouping

Two facts a child discovers with blocks and is then never told are theorems. Because both hold, a sum of any list of numbers has one value, no matter the order you add them or where the brackets go — sum_of_four states it for four numbers at once.

3 · Multiplying is adding, and that is why the ten-times table is free

split_at_ten : a * (10*t + u) = 10*(a*t) + a*u

Any two-digit multiplication splits into a ten-times table and a small one. This is not a trick; it is the distributive law, used once. 7 * 12 = 7 * 10 + 7 * 2.

4 · Place value, said exactly once

“37 means three tens and seven” is taught by example and never stated. Here it is stated for every number at once, and in any base:

place_value_base : b * (n / b) + n % b = n

Notice what is missing from that statement There is no condition on b. It holds for b = 0, 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.

5 · The first thing that goes wrong

Everything above worked. This is where the floor gives way, and it gives way at a place nobody is warned about: subtraction is not the opposite of addition. It is the opposite of addition only when you are allowed to take the smaller from the larger, and on the counting numbers that is a condition, not a rule.

sub_add_cancel_iff : a - b + b = a ↔ b ≤ a

On the side where it works, 9 - 4 + 4 = 9. On the side where it does not, 3 - 5 is not negative here. It is zero, and the machine says so without complaining — so 3 - 5 + 5 = 5.

The payload, and the reason the next rung exists subtraction_is_not_inverse : ∃ a b, a - b + b ≠ a

Five taken from three, then put back, leaves you at five, not at three. Nothing is broken and nothing is hidden — the counting numbers simply do not contain an answer to “three take away five”, so the machine returns the nearest one they do contain.

The integers are not a harder subject. They are the repair for this one line, and you have now seen exactly what needed repairing.

6 · How to check this yourself

lean Counting.lean

No library, no download, about a second. Eleven lines, and tools/axiom_gate.py reads them.