Approach: a size bound tying the counter to the length of the last round

The head sits between a binary counter on its left and, on its right, 1 10 10 … 10 0 10 10 … 10: a single 1, a run of fuel pairs, a gap, and a run of spent pairs. Each bounce moves one pair from fuel to spent and adds 1 to the counter. When the fuel is gone, the right side bites off the counter's low end and refills the fuel for a longer round. The counter is normally tidy, its number written on every other cell (or packed, with the top two bits sharing a pair), but a bite can leave it messy for a while.

The machine can halt only at a bite on a messy counter whose low end has one particular bad shape. The key is a size bound: at every bite on a tidy counter, the counter's value is at least the length of the round just finished and at most about 2.5 times it, the exact cap depending on parities and layout.

Why that settles it: the proof sorts tidy bites into eleven cases and follows each to the next tidy bite. In every case the bound keeps any messy bite on the way away from the bad shape and makes the round after it long enough to tidy the counter, and the bound holds again at the end. The run reaches a tidy bite inside the bound at step 32, so it never halts.

The Rocq proof builds on busycoq's BECv5, whose two machines differ from this one in one table entry. It proves each low-level move as an exact run, derives the eleven cases, checks the bound's closure by arithmetic, and runs the 32-step opening directly.