Approach: #3's proof in a mirror, 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 seen in a mirror, with left and right swapped and the state letters renamed, started in the state that is #3's D. Watching it is like watching #3 in a mirror: the same countdown, with the head working at the right end of the tape.

What is new is the opening. After 78,911 steps the run reaches the mirror image of the checkpoint #3's argument starts from (#3 gets there after 78,710 steps), except that the last pair has 25 copies of 01 instead of 24, which the checklist allows. From there #3's argument (the nine moves and the checklist, none of which depends on the start) applies unchanged, so it never halts. As far as the two runs have been simulated side by side, they then make the same move every time, with the one extra copy moving around among the blocks at the far end; the proof does not need this.

The Rocq file contains #3's whole proof for #3's own table and adds the 78,911-step opening from state D. It then checks that this table, mirrored and renamed, is exactly #3's, and uses two busycoq theorems (mirroring a machine or renaming its states does not change whether it halts) to carry the result over.