Approach: W4-2's proof in a mirror, with a three-step detour

W4-2 keeps a binary counter on one side of the head and two runs of 10 pairs on the other, fuel and spent. Each bounce adds 1 to the counter and moves one pair from fuel to spent; when the fuel is gone, the pairs bite off the counter's low end and a longer round starts. This machine does the same in a mirror: left of the head are the spent pairs, a gap, the fuel pairs and a single 1 (01 01 … 01 0 01 01 … 01 1), and right of it is the counter.

Mirrored and renamed, this table is W4-2's with one entry changed. In one of W4-2's two ways of stepping over a 1 while scanning the counter, this machine takes three steps instead (one back, two forward) and ends in the same place with the same tape and state. The detour needs a 1 behind the head, and one is always there, because the state that makes the detour is only entered by a step that writes that 1.

So W4-2's arithmetic carries over unchanged, including its key size bound: at every bite on a tidy counter, the counter's value is between one and about 2.5 times the length of the round just finished. New is the start: this machine acts like the mirrored table started in another state, and at step 73 it reaches such a bite inside the bound. From there W4-2's induction runs forever and never reaches the missing entry.

The Rocq proof copies W4-2's arithmetic word for word, re-proves the low-level moves on the mirrored table with the detour, and runs the 73-step opening directly; busycoq's mirror and renaming theorems carry the result over to this machine.