Approach: W4-3's proof, 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-3b is W4-3's table with its state letters renamed, started in the state that is W4-3's B instead of A. Watching it, you see the same stripe, the same odometer and the same long flawless stretches.

Only the opening differs, and the run soon settles into W4-3's pattern. At step 2,629,088,387,088 (about 2.6 trillion, 159,680 steps later than W4-3) it reaches the snapshot W4-3's formal proof starts from, just after a dial overflow. Its flaws then match W4-3's except for one gap deep inside the counter, which is 17 cells long instead of 13.

The longer gap changes nothing. W4-3's argument only needs each deep gap to have the right remainder when divided by 4 and a minimum length, and 17 passes both tests just as 13 does. 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) keeps W4-3's library word for word, stated for W4-3's table. New are a verified run from this start to the snapshot, in 38 checked pieces, and an entry-by-entry check that this table is W4-3's with the states renamed. So a halt here would be a halt of W4-3's table started in B.