Approach: a recursive call stack whose every round costs exactly 2

The tape is runs of 1s separated by 0s, and it behaves like a recursive program's call stack. Left of the head are the pending calls; right of it is input still to come. A new call moves the next run of 1s onto the stack and costs its caller one 1. A call that is down to a single 1 ends: it and its caller leave the stack, and the caller's run goes back to the right, one 1 longer.

Every so often the stack is empty and the head is back at the left end, which reads 111 00. That 111 grows into the next round's bottom call, four 1s long, so it can pay for three calls; the number it pays for is the round's cost. The machine halts exactly when a bottom call has to pay for a fourth.

The key idea is self-similarity. A call behaves the same whatever its length, as long as it can pay. So inside a long round, a big call replays the machine's own rounds one level down, on a tape that also holds markers (lone 1s separated by even-length gaps of 0s). A replayed round costs 2, or 3 when it swallows a marker, and an exact law, proved by induction, says which from the gap lengths alone.

Why that settles it: the real run's top level has no markers (those further right only affect replayed rounds). So every top-level round costs exactly 2, the next one again starts from 111 00, and the fourth payment, the only route to the missing transition, never comes.

The Rocq proof (checked against busycoq) checks the tape moves by running them, the replay and the cost law by induction, and the 50-step opening by exact replay.