Approach: #30's proof, from a different start

30 keeps a binary counter fed by a marker that bounces through a run of budget blocks. Each epoch begins by tidying a messy leftover in the counter, and #30's proof shows that the tidying costs only about the square root of the budget, so the budget never runs out mid-cleanup. This machine is #30's table with the state letters renamed and no mirror, so its tape looks the same: 110 110 … 110 0 011 011 … 011 (used blocks, a 0 marker, budget blocks), then the head and the counter.

What differs is the start. The renaming makes this machine's first state #30's second one, so from the blank tape it runs #30's rules from a different opening and passes through a different sequence of epochs. After 55 steps it reaches a tidy epoch start with budget 3.

From there 691 epochs are computed exactly, until the budget reaches 17,712 and the condition that #30's proof carries from epoch to epoch holds. After that, #30's argument carries it forever, so the missing table entry (#30's, renamed) is never reached. This run only merges with #30's own at epoch 795, a fact the proof does not need.

The Rocq proof is #30's with the state names changed in its statements, so no transfer step is needed. New are the 55-step opening by verified simulation, the 691-epoch computation and the check that #30's condition holds at its end.