Approach: the counter never exceeds twice the word's length

The tape holds a binary counter on the right, written 11 for a 1 and 00 for a 0, lowest digit first, and on its left a word of 10 pairs with one flaw, an extra cell called the defect. Each trip of the head into the word and back adds 1 to the counter, and every second trip moves the defect two pairs further from the counter. Once the defect has walked off the far end, the next trip reaches the blank left edge, where a sweep shifts the whole word by one cell, eats the counter's lowest digits and plants a fresh defect. So the word grows with every eat.

The key fact is a size bound at each eat: the counter's value is at most twice the number of pairs in the word. The eats fall into five cases by the counter's last binary digits. In the hardest, the eat misaligns the low digits and briefly creates a second defect, which later cancels the first; that works out only if the word is long enough, and the bound supplies exactly that.

Why that settles it: each case is a chain of exact moves from one eat to a later one, where the bound holds again. The missing table entry (state F reading 0) could only come up if the left-edge sweep met two 0 cells in a row, but that sweep only crosses the word 10 10 … 10 1, which has none. The blank tape reaches an eat inside the bound at step 165, so the machine never halts.

The Rocq proof uses busycoq's binary-counter library, proves every move as an exact run and every case as a chain of them, checks the bound's closure by arithmetic, and runs the opening directly.