Approach: a base-3 odometer made of tape flaws

The tape looks like a zebra stripe, 0101…, with a few dozen flaws: spots where two neighbouring cells match (00 or 11). The head sweeps back and forth, flipping every cell it crosses. Flipping keeps matching neighbours matching, so the pattern of flaws changes only where the head runs into one. Read the right way, the flaws form a base-3 odometer: a chain of digits in the middle counts the head's trips, and a four-digit dial at the left end ticks each time the chain rolls over.

The key idea: the head's behaviour repeats every four cells, so what happens at a flaw depends only on its position counted in fours and on the order of the flaws, not on exact distances, as long as flaws are not crowded together. A million-cell gap acts like a short gap with the same remainder, so one finite computation covers every size.

Why that settles it: a round ends when the dial overflows; then the chain regroups and the right end moves on to the next of six phases. After six rounds the picture repeats with two more digits and its long flawless stretches roughly nine times longer. The missing instruction fires only if the head, moving right, pushes a flaw two cells along while another flaw sits right beside it. No piece of a round does that, and every round ends in the same family of tapes, so the run never stops.

In Rocq (busycoq), a verified simulator that treats gap lengths as symbols replays the first 2.6 trillion steps. It then checks every chain block, dial tick and right-end phase for all sizes, and that each round returns to the same family of tapes.