Approach: each epoch's cleanup costs only about the square root of its budget

Left of the head the tape reads 110 110 … 110 0 011 011 … 011: used blocks, a 0 marker, and budget blocks. Right of the head is a binary counter. On each bounce the head runs into the counter to add 1, comes back, and moves the marker one block right, usually turning a budget block into a used one. When one budget block is left, the machine eats the counter's lowest digit; sometimes that buys more budget, otherwise the head sweeps left and a new epoch starts with a larger budget, set by the length of the used run.

The eat leaves the counter messy, and the first bounces of the next epoch tidy it up. The tidying is recursive: at some digits a single bounce runs a whole mini-epoch on the rest of the counter, leaving its own mess one level deeper. The missing table entry (state D reading 0) can only come up if the budget runs out while the counter is still messy.

The key estimate: tidying a counter of k digit blocks costs about 2^(k/2) bounces, while the budget is at least about 2^(k+3), so the cleanup needs only about the square root of the budget. The proof bounds the cost with a weighted score over the counter's digits and carries an invariant from epoch to epoch, which works once the budget reaches 17,705. The 691 epochs before that (epochs 3 to 694, ending at budget 17,713) are computed exactly.

The Rocq proof checks every rule as an exact machine run, the cost bounds and the invariant from budget 17,705 up, and the opening by verified simulation. A verified model of the rules computes the 691 epochs, and a soundness proof turns that computation into a real machine run.