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

3 counts a binary number down on a list of pairs of blocks, like an odometer running backward, and its proof is a checklist of inequalities showing that a block only ever runs out where that is harmless. This machine is #3's table with four state letters renamed, started in the state that is #3's B instead of A. Watching it, you see the same countdown on a run of its own: the blocks have other lengths, and it is not a copy of #3's run.

Everything in #3's proof that does not depend on the start carries over unchanged: the nine moves, the checklist, and the argument that once the checklist holds at a checkpoint (every second regrouping of the list), it holds again at the next one. What is new is the opening. After 38,732 steps the run reaches a checkpoint with three pairs, the fewest the checklist allows, and every inequality holds there. From then on #3's argument applies, so this machine never halts either.

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