Approach: a counter whose digits burn fuel but never run dry the wrong way

It counts up in binary, like an odometer. Each digit is a run of 10s then a run of 01s, with two blank cells between them for a 0 (1010…10 00 0101…01) and none for a 1. To add 1, the head walks left from the right end to the nearest 0 digit, makes it a 1, turns the 1s it passed into 0s, and walks back; each digit it changes burns one 01 as fuel. When all digits are 1, an overflow swaps the two halves of every digit and adds a digit.

Trouble needs a carry to reach a digit with no fuel. A digit that runs dry while becoming a 1 just merges into the next digit, which is harmless. The danger is a 1 digit with one unit of fuel being turned into a 0.

The key idea: call the stretch between two overflows a cycle. In a quiet cycle every digit has more fuel than touches still to come. In the lossy cycle after it, digits run dry at irregular times, but each digit's fuel plus its value stays odd, since a touch burns one unit and flips the digit. So a digit on its last unit of fuel is always a 0, and runs dry harmlessly as it becomes a 1.

Why that settles it: each overflow sets up the next cycle. A quiet cycle leaves lengths that give the lossy one its odd sums, and a lossy cycle leaves runs long enough to fuel a quiet one. The run reaches this pattern at step 483 and every move keeps it, so the machine never halts.

The Rocq proof (checked against busycoq) builds both moves from 20 small tape lemmas, replays the first 483 steps, and proves that every move keeps the invariant.