Approach: a size bound plus a remainder that never hits zero

Most of the tape is a long row of 10 pairs, the "bell", with one 00 in it, the "wall"; at the right end sits a counter whose bits sit every third cell (a 0 means the bit is set). Each round trip of the head moves the wall two pairs right and counts the counter down by 1. When the bell ahead of the wall is used up, the wall bites the counter's low end, and usually the pairs behind the wall become the new bell. But a bite on set low bits starts smaller nested copies of the whole process on the rest of the counter.

The only way to halt is a bite on a counter with every bit set, exactly when two pairs of bell remain. At each cycle start the proof tracks two facts. The bell is long: at least 2 pairs more than a power of 2 set by the counter's width. And a certain mix of bell length, width and counter value leaves remainder 1 or 2 when divided by 3; each cycle swaps the two, so it is never 0.

Why that settles it: among long-bell starts, the ones headed for the halt all have remainder 0, apart from one small state the proof excludes separately. The nested copies, and the rest of a cycle after them, start with an odd bell when the width is not a multiple of 3, which cannot reach the halt either. Nobody knows whether nested copies always finish, so the proof shows "no halt within N steps" for every N, by induction, from the good start reached at step 327.

The Rocq proof checks every move as an exact run, the arithmetic of rounds and bites, both invariants and that induction, and runs the 327-step opening directly.