Approach: walls that never collide, and a counter on a fixed schedule

Each time the head walks in from the left edge and back, it delivers one carry into a long row of short blocks, like the input wheel of an odometer. Digit blocks count in binary (0000 is a 0, 1000 a 1), and wire blocks 11000 pass carries straight through. Walls (111000 or 011000) swallow every second carry; on the others a wall sends three carries onward and creeps one block to the right.

A small gadget at the left end repeats exactly, adding 8 new walls every 8 times the head reaches fresh tape there. The walls ride the wire in single file and are swallowed one by one by a binary counter at the far right. The machine can halt only after a hit: a creeping wall pushing into a block that is not wire or a plain digit, such as another wall.

The key idea: on the wire a hit is impossible, since three carries always turn the block ahead of a creeping wall into wire. At the far counter, a bookkeeping identity shows that the carries arriving between two swallowed walls depend only on the wall's place in the cycle of 8 and on how far the counter's edge has moved. So the counter runs on a fixed schedule, which the proof shows never produces a hit.

Why that settles it: at each visit to a fresh cell on the left, two counts (visits so far, walls swallowed) fix the whole tape, and that description carries over to the next visit with no hit on the way. The first such visit comes at step 203,465, so the machine never halts.

The Rocq proof checks each block's rule by running the machine on that block alone, the rest of the tape a black box. Computation covers the gadget, the opening and thousands of representative counter runs; the visit-to-visit step is proved for all 8 kinds of visit.