Approach: an exploding counter whose carry finally runs off its end

Left of the head is a binary counter, lowest digit next to the head, each digit six cells long: 111111 for a 1, 001111 for a 0, with lone 001s as spacers here and there. Right of the head is a tally, a row of 011 blocks. Every bounce of the head adds 1 to the counter, like an odometer clicking, and one block to the tally.

The key idea is what happens when the counter is all 1s. The head walks to its far end and rewrites it on the way back, shifted by three cells, while the tally turns into new low digits: a block of 0s, about one per two tally blocks, plus a single 1. Filling n zeros back up takes at least 2^n − 1 bounces, each adding a tally block, so every new block of zeros is roughly 2 to the power of the previous one: the first three overflows add 2, 25 and 654,311,423 zeros.

Why it halts: after the first 38,573 steps, simulated directly, the proof records each block only as "at least so many digits" (the rules work the same on any longer block) and pushes that through 192 more cycles. In the 195th overflow, the rewrite near the far end must add 1 to a stretch of all-1 digits with nothing beyond them, so the carry falls off the end. The machine then reads a 1 in state F, the one case its table leaves undefined, 1,368 steps after the head reached the last 63 cells of the counter. The step count is unknown; a rough estimate is a tower of 2s about 195 levels high.

The table is busycoq's TM3 with the states renamed, so TM3's rules are re-proved with its own scripts. Rocq also checks the new lower-bound rules, the 192 cycles and the final 1,368 steps; it proves halting, not the step count.