Approach: both cycle formulas keep the block counts in a safe region

The tape is a binary counter at the left end, four cells per digit, followed by a row of five-cell blocks: "A" blocks 00111 and "B" blocks 10111. The head bounces between the counter and the right end, adding 1 to the counter on every visit and, along the way, new B blocks at the right end.

When the counter rolls over, it gains a digit, and a three-cell marker 111 appears just to its right. The marker walks right through the A blocks, two blocks for every three counts, and on reaching the B blocks turns them all into A blocks. Then the cycle repeats, one digit longer.

The key idea: at each cycle start, count the A blocks ahead of the new marker and the B blocks beyond them (a rollover in mid-conversion needs a small correction). One cycle changes this pair of counts by one of two exact formulas, chosen by whether the A count is even or odd, a choice that looks random.

Why that settles it: the machine stays on these rails only if the timing works out, for example the marker finishing its walk before the next rollover. Scale both counts by the counter's size and each cycle start becomes a point in the plane. The proof finds a six-sided region where every timing condition holds and which both formulas map into itself, so the even/odd choices never matter. The run is inside it at step 17,215, so it never leaves the rails and never uses the missing transition.

The Rocq proof (checked against busycoq) checks the 21 basic tape moves by running them, the longer moves by induction, the region by linear arithmetic, and the first 17,215 steps by exact replay.