Approach: a known sweep recipe plus one extra +1, shown never to get stuck

Right of a short wall, 11, the tape is cut into three-cell blocks: filler 110, and binary digits 100 (a 1) and 000 (a 0). A typical moment is 11 110 110 … 110 100 000 100: the wall, mostly filler, and a few digits near the right end forming a small binary counter, lowest digit first. Over and over the head sweeps right from the wall and back, and each sweep leaves the wall one cell further left and the filler longer.

The key idea: every sweep follows a fixed recipe, almost the one busycoq already proved for a close relative, its TM7, whose table differs in one entry. Going right, the head turns blocks into filler and runs up a debt of extra passes (trips over the blocks ahead); from the first 1 digit on it pays the debt off, and any leftover is written past the right end in binary. The one difference: whenever the head steps into a filler block, this machine first runs a quick +1 over everything to its right.

Why that settles it: the proof writes the recipe as twelve exact rules and shows two things. Each rule is a real run of the machine that never uses the missing entry (state F reading a 1), because F always arrives on the last cell of a block, which is 0 in all three kinds. And the recipe never gets stuck: it applies to the first sweep and to every tape a sweep produces, which needed two extra end cases and a count of pending +1s on top of TM7's version.

The Rocq proof checks every rule by induction, the never-stuck lemma and the 16-step opening; eight rules reuse TM7's proof unchanged. busycoq has merged it as BellEatsCounter_1RB0RF.v.