Approach: #30's proof in a mirror, 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 seen in a mirror, with the state letters renamed. So its tape is #30's reversed: the counter is left of the head, and right of it come budget blocks 110 110 … 110, the 0 marker and used blocks 011 011 … 011.

What differs is the start. From the blank tape this machine acts like #30's table started in its fifth state, so it takes a different opening. Its first four epochs fall outside #30's proof, and in two of them the machine eats an untidy counter that simply happens not to halt. The fifth begins cleanly: at step 1,114 it is a tidy epoch start with budget 17.

From there 687 epochs are computed exactly, until the budget reaches 17,724 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 own, seen in the mirror) is never reached.

The Rocq proof keeps #30's development word for word, as a proof about #30's table. New are the 1,114-step opening from #30's fifth state, by verified simulation, the 687-epoch computation, and the check of #30's condition at its end. busycoq's mirror and renaming theorems then carry the result over to this machine.