Approach: exact rules for five block lengths, and a double cycle that repeats forever

The tape is mostly five long blocks of 1s, with short words between them, the "particles", and a 43-cell pattern at the left end that is the same at the start of every trip. Each trip runs right across the first block, sometimes further, until a particle turns the head back; how far it gets follows a 12-trip cycle. Every 12 trips the first block grows by 48 cells and the second shrinks by 8, so the particles around the second block close in. When it is down to 2, 4, 6 or 8 cells they collide, and 135 to 147 trips later the five blocks are back with new lengths.

The key idea: each of these events is an exact rule on the five lengths, one for 12 ordinary trips and one for each of the four kinds of collision. Each rule is proved once for all lengths in a stated range, by running the machine on a tape whose block lengths are symbols.

Why that settles it: two of the collisions, at 4 cells and at 2, alternate forever. Call the tape a checkpoint when the first block has odd length, the third is 38 longer than half the second, the fourth is 35 and the fifth 18. From a checkpoint whose second block is at least 52 and leaves remainder 4 when divided by 8, the rules lead through both collisions to another checkpoint, with the second block 32 longer. The run reaches the first checkpoint at step 153,126,993, and every later step lies inside a rule that avoids the missing transition.

The Rocq proof (checked against busycoq) proves the five rules with busycoq's symbolic executor, replays the 4,097,897-step opening exactly, and chains the rules from there to the first checkpoint and from each checkpoint to the next.