Invariants: why a long run is not a proof

1A billion steps tells you nothing

Press the button: on a laptop, your browser simulates C2-552 at about a hundred million steps a second, and it does not halt. We proved that it halts; the halting step, about 1.765·10⁴⁴, is computed (it is not part of the proof). The same goes for W5-5's 1.8·10¹⁸.

Simulating is only this: one table lookup per step. No finite stretch of steps can tell you that the next one is not the halt. You need an argument that covers every step at once.

2An invariant is a fence the rules cannot cross

Module 4's W5-3 moves from one eat configuration E(p,N) to the next. Five proved rules, M1 to M5, say where E(p,N) goes next. They cover almost every (p,N), and beat 3 shows the gaps. So the whole run is a walk of points (p,N).

Each dot is an eat configuration of the real run, up to step 3,000,000. From E(2,4) at step 165 on, all 62 lie on or under the line N = 2p. That region is the fence J: 1 ≤ N ≤ 2p. Tap any point in it: the page applies the rule, draws the arrow, and runs the real machine from that tape to check. The arrow lands inside again, every time. That is what closed means.

Now the proof is three lines. The run is inside J at step 165 (its first eat configuration, E(0,1) at step 31, is just outside, so the proof replays those 165 steps exactly). J is closed. And none of the five rules ever uses F0, the machine's only undefined transition. So the run never leaves J, and never halts.

Why the deciders miss fences like this: the automatic deciders describe tapes with a fixed pattern-matcher, which can count a block only up to a fixed size or modulo a fixed number. J compares two numbers that both keep growing, so they cannot express it. (Module 1: what the deciders catch)

3Failure 1: a fence too wide to close

Try a simpler fence: drop "N ≤ 2p" and keep only N ≥ 1 (the hatched area). Now E(0,62) is inside, and no rule covers it. Its N is rule M5's case: N + 2 = 64 = 2³⁺³, so t = 3.

M5 walks a defect left through the 10 pairs, two pairs per walk, 2^t−1 − 1 times, so it needs enough pairs on the left: p + 7 ≥ 2^t. From E(0,62) that is three walks, and the third finds only 1 of the 2 pairs it needs. Each red cross is such a point, and one point with no rule is enough: closure cannot be shown.

The machine itself does not care. From E(0,62) it reaches E(12,7) at step 688, back under the line, and every red cross does the same at its next eat (tap one). A fence only has to be one you can prove closed. It may leave out tapes that never halt.

4Failure 2: the shape alone is not enough

Press run both. A is the real run and keeps going (we ran it 2·10⁹ more steps). B halts at step 203,453. Below are B's last 40 steps: at the end E reads 0, which is ---.

So a fence that only says which pieces a tape has, in which order, contains tape B, and B halts. No such fence can be closed. What keeps the real run safe is a balance of sizes, between its counter value and its widths, and we found no size fence that closes. W4-7 is parked.

Where B comes from: we took 237 tapes of the real run, changed sizes (one at a time, or redrawn at random) and kept the pieces. Our digit-level simulator flagged 69 distinct tapes (34 have no rule under any reading of the digits), and 3 of them halt in the real machine, 61,670, 307,823 and 376,776 steps later. B is tape A, one of the 237, with its widths redrawn. B's run reaches, at step 141,783, the flagged tape that halts 61,670 steps later.

tape B's whole run in the explorerthe real run to 2·10⁷ in the explorer

5Success: #11's fuel invariant

#11 is a binary counter whose digits carry fuel (module 3, beat 3): v is the number of 01s in a digit. R is the number of carries still coming to that digit before the next overflow. Between overflows, each carry takes one 01 from v and one from R, so the spare fuel v − R never shrinks.

The rules break only if a carry reaches a 0-digit with no 01 left. Phase A of the invariant rules that out by asking every digit for spare fuel: v ≥ R + 1. Steps 283 and 383 fail it, because their low digit has v = R.

Step 142 fails on the end block, the 10s right of the digits. Its counter is all 1s, so an overflow comes next, and the end block becomes the fuel of a new low digit. S is the spare that digit will get: here S = 0, which is the low digit with v = R at step 283.

Phases B and C cover the cycles in which the top digit runs out and falls (at step 752 its v = 1 is used by the next carry, and it merges into the digit below). There the invariant uses parity instead: every 1-digit has an even number of 01s, so a carry that turns it into a 0-digit leaves it at least one. From step 483 on every row is inside, so the proof replays the first 483 steps exactly and the invariant takes over from there.