Approach: a countdown in which only safe blocks run out

It counts a binary number down, like an odometer running backward. The tape is a list of pairs, each like 1010…10 0101…01 0010: a block of 10s, a block of 01s, and one digit (0010 is a 0, 0001 a 1). On each trip the head goes from the left end to the first 1 digit and back, subtracting 1; every pair it reaches flips its digit and trades one 01 for one 10. About every second time the count reaches zero, the blocks are regrouped into new pairs, so growing and shrinking blocks swap roles, and a pair is added.

The danger is a block of 01s shrinking to nothing. At the first 1 digit that is a normal move: the pair fuses with the next one. Anywhere else the tape leaves the pattern, and some of those tapes halt. Parity decides which: a block whose length plus its digit is even can only run out at the first 1 digit.

The key idea: every block is one of two kinds for life. One kind shrinks in one countdown and grows in the next, and never runs out; every block with the wrong parity is of this kind. The other kind wears down and does run out, but always with the right parity, so it only fuses.

The proof turns this into a checklist of simple inequalities, checked at every second regrouping. If it holds at one, every move up to the next is one of nine known moves, none of which halts, and it holds again there. It holds after 78,710 steps, so the machine never halts.

The Rocq proof (checked against busycoq) proves the nine moves for all block lengths, replays the first 78,710 steps, and shows that a move-by-move version of the checklist holds there and survives every move.