Approach: #12's proof with a smaller budget and zero slack

12 works like a recursive call stack written in runs of 1s. Each round starts at the left end with a bottom call that can pay for three calls, the machine halts only if a round needs a fourth, and an exact law shows that every round costs exactly 2. #12b, once its states are renamed, is #12's table with one transition changed, started in the state that is #12's B instead of A; no renaming or mirror makes it exactly #12.

The changed transition is used only at the start of a round, when the bottom call is created at the left end. There it takes a 6-step detour to the same tape that #12 reaches in 2 steps. So the call-stack picture, the replay of rounds one level down and the cost law all carry over unchanged.

What is new is the budget. After a 48-step opening, every round starts with the left end reading 11 00 instead of 111 00, so the bottom call is three 1s long and can pay for only two calls. A single round needing three would halt the machine. But #12's law counts the calls exactly, not just as a bound: every round needs exactly 2, the budget is always just enough, and the missing transition never fires.

The Rocq proof is #12's file with the start-of-round move re-proved by running it, detour included, plus the new 48-step opening and one added lemma for a round that starts with the smaller bottom call.