Approach: #11's proof in a mirror, 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 seen in a mirror, with left and right swapped and the state letters renamed, started in the state that is #11's D. So the same kind of counter runs with the head at the left end of the tape and a fixed marker, 1001, at the right.

The invariant talks only about the digits' lengths and values, never about direction, so it and its proof carry over word for word. Only the small tape lemmas that the two moves (add 1, and overflow) are built from had to be mirrored.

What is new is a 215-step opening. At step 82 the counter has no digits; an overflow of that empty counter creates the first one, and at step 215 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 re-proves #11's tape lemmas in mirror image and keeps #11's moves, invariant and closure proof word for word. It replays the 215 steps, checks the invariant there, and proves the result for this table directly.