Approach: a timing window that every route returns to

Right of the head is a binary counter with spread-out digits: a seven-cell mark (0110001 for a 1, 0010001 for a 0) followed by a gap of repeated 100s. Left of it is padding, and at the far right a tail: a fixed gadget holding 15 bits, plus a slowly growing end. Each bounce off the left end adds 1 to the counter and lengthens the padding.

At an overflow the tail answers in one of two ways. Either the counter just wraps to zero, or the left part of the tape freezes into a "wall", which the machine eats two counts at a time in a long pause that rebuilds the gaps. The key idea: the proof never predicts the tail's 15 bits, only its front two. At each overflow those two step through a short cycle, 10, 01, 11, 00 and back to 10, and the quiet wrap can happen only at 11, where the proof simply allows either answer.

Why that settles it: the one moment no rule covers is a pause whose wall runs out exactly as the counter overflows. At each overflow outside a pause, the proof measures how far the padding's length is from a length set by the counter. While that surplus stays in a window set by the counter's size and the two front bits, only four sequences of events can follow. Each shifts or flips the surplus by an exact amount, avoids the uncovered moment, and lands back in the window. The run enters the window at step 92,299, so the missing instruction is never used.

The Rocq proof (checked against busycoq) replays the first 92,299 steps, then checks the tape moves by running them, the counting by induction, the tail's answers through a verified model of the head's return trip, and the window by arithmetic.