Approach: #11's proof, from a different start

11 is a binary counter whose digits burn a unit of fuel each time a carry touches them, and its proof is an invariant showing that a digit only ever runs dry where that is harmless. This machine is #11's table with the state letters renamed, started in the state that is #11's B instead of A. Watching it, you see the same kind of counter at the right end of the tape, on a run of its own.

Everything in #11's proof except the start carries over unchanged: the two moves (add 1, and overflow), the invariant, and the proof that every move keeps it. What is new is a 732-step opening. In it the counter loses its digits to merges until none is left, an overflow builds a new one, and at step 732 the tape is a one-digit counter with fuel to spare, a state the invariant covers. From then on #11's argument applies, so this machine never halts.

The Rocq file is #11's with the states renamed and a new opening. It replays the 732 steps, checks the invariant there, and proves the result for this table directly.