Approach: replaying a binary counter until a digit runs out of fuel

Look at the tape each time the head reaches fresh tape on the right, and it reads as a binary counter, lowest digit on the right. Digits are fenced off by walls, runs of equal cells (usually 11). Inside each digit sit a bit marker (00 for 0, 1111 for 1), sometimes a few spare walls, and a final alternating stretch whose length is the digit's fuel. Each trip adds 1: the carry runs left past every 1 digit to the first 0, and every digit it touches burns fuel.

The key idea: spare walls are spare lives. A digit with a spare wall that runs out of fuel hands that wall to the fence on its right and takes the gap before it as new fuel; the wall later moves into the next digit. So walls drift toward the head, and a digit with no spare wall survives only if walls reach it in time. Between such events everything changes at a steady rate, so long runs of increments can be done in one batch by a formula.

Why it halts: from step 342, a checker replays the run in 107,781 moves, about half of them batches. In increment 11,631,266,794,472,450,654,093 (about 1.16 × 10^22), a carry reaches a digit with no spare wall, bit 0 and no fuel, and the machine hits its one missing instruction. Adding up every move's cost gives a 45-digit step count, about 1.77 × 10^44: exactly 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463.

In Rocq (busycoq), every carry rule and batch formula is a proved lemma, and the checker, proved correct once, runs to the halt, re-checking each proposed batch. The step count is not part of that proof; its per-move costs match direct simulation over the first 10^11 steps.