Approach: W4-3's proof in a mirror, from a different start

W4-3's tape is a zebra stripe, 0101…, whose few dozen flaws (two matching neighbours) form a base-3 odometer; its proof follows the odometer from one overflow of its left-end dial to the next. W4-3c is W4-3's table seen in a mirror, with its state letters renamed, started in the state that is W4-3's F instead of A. On its tape everything is reversed: the dial sits at the right end and the long flawless stretches lie to its left.

Only the opening differs. At step 2,629,080,059,236 (about 2.6 trillion, some 8.2 million steps sooner than W4-3) it reaches, in mirror image, the snapshot W4-3's formal proof starts from, just after a dial overflow. Its flaws then match W4-3's except for five gaps deep inside the counter, which differ by −4, −12, −16, +8 and −36 cells.

Those differences change nothing. W4-3's argument only needs each deep gap to have the right remainder when divided by 4 and a minimum length, and all five changes are multiples of 4 that leave the gaps long enough. From that snapshot W4-3's proof applies unchanged: each round of the odometer is a finite run that never reaches the missing instruction and ends in the same family of tapes, so the run never stops.

The Rocq proof (busycoq) reuses W4-3's simulator and invariant library word for word, stated for W4-3's table; the opening run (38 checked pieces) and the final theorems are its own. Then busycoq's mirror and renaming lemmas turn any halt of this machine into a halt of W4-3's table started in F.