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

4 keeps a binary counter at the left end of the tape and a row of five-cell blocks to its right, "A" blocks 00111 and "B" blocks 10111. Each time the counter rolls over, a marker walks right through the A blocks and then turns all the B blocks into A blocks. #4b is #4's table with its state letters shuffled, started in the state that is #4's F instead of A, so watching it you see the same picture with different numbers.

Renaming states changes nothing the machine does to the tape, so all of #4's proof holds here as it stands. That includes the two formulas that take the block counts from one cycle start to the next (one for an even A count, one for odd), and the six-sided safe region that both formulas map into itself.

What is new is the opening. After 16,590 steps #4b is at a cycle start with 14 A blocks ahead of the marker and 4 B blocks beyond them, where #4 has 16 and 0 after 17,215 steps. That point is also inside the safe region, so from there the region argument keeps the run on the rails forever and the missing transition is never used. The two runs are not copies of each other: their even/odd choices already differ in the second cycle.

The Rocq proof is #4's file with the states renamed and the opening replaced. Every tape move is re-proved on #4b's own table by running it, and the first 16,590 steps are replayed exactly.