How we proved our kills never halt

All 18 kills are proved the same way at heart. Each one is a Rocq file, checked against the unmodified busycoq framework, that ends in the statement "this machine, started on a blank tape, never halts".

This page gives the common recipe, a table of the 18 kills, what is special about each kind of proof, and a few sentences you can use to describe a proof in chat.

1. The common recipe

Two words first.

• A macro rule is a proved shortcut: "from any tape of this shape, with any block sizes a, b, c, the machine reaches that other shape after finitely many exact steps". It is proved once for all sizes, usually by induction, so it covers rounds no simulation could ever reach.
• An invariant is a property of the tape that, if it holds before a round, still holds after it. Example: "every digit of the counter still has at least one unit of fuel".

The recipe has five steps.

1. Find the repeating structure. Simulate, and look at the tape each time the head comes back to the same spot. In every kill it is a counter of some kind: a binary counter whose digits are blocks, a bouncer that piles up blocks, or a stack of blocks that call each other.

2. Write one round as a macro rule. Usually a handful of rules, one per kind of round (an ordinary count, an overflow, a merge).

3. Find an invariant that excludes halting. The halting transition can only fire from a few tape shapes that no rule covers. The invariant is chosen so that, while it holds, some rule always applies, and every rule keeps it.

4. Show the run starts inside it. Simulate the opening exactly (from a few steps to about 92,000) until the tape has the round shape, and check the invariant there.

5. Let Rocq check every step. busycoq's multistep_nonhalt handles the opening: if the start reaches tape c in exact steps and c never halts, the start never halts. Its progress_nonhalt_cond handles the rest: if every tape with the property moves, by at least one real step, to another tape with the property, and the first tape has it, the machine never halts.

Every macro rule is an exact run of the real transition table, so no halting step can hide inside a round.

Two tricks come back again and again.

• Do not predict the unpredictable. Many runs depend on bits that look random: a parity, which digit runs dry first, which answer a tail gives. The invariant is chosen to survive every branch, so the proof never needs to know which one happens.
• Compute the small cases. When the invariant only works for large sizes, Rocq simply computes the early rounds. For #30's table that is about 700 rounds.

2. The 18 kills

Status: accepted means our busycoq pull request is merged; submitted means it is in an open pull request; claimed means the Rocq proof passes all our checks but is not submitted yet. Currently that is 1 accepted, 4 submitted and 13 claimed.

Each label links to the machine's card. #11b, #25, #24 and #12b have no card of their own, so they link to their kill page. Rows are grouped by family, and within a family by transition table; the first row of each table is its parent proof.

Only 8 of the 18 needed a new idea (#2, #4, #8, #11, #3, #12, #30, W4-2). The other 10 reuse a parent proof.

3. What is special about each kind of proof

Counters whose digits carry fuel (#11's and #3's tables)

The tape is a binary counter whose digits are pairs of blocks, such as (10)^u (01)^v. Each count step changes the block lengths of every digit it touches.

In #11 (counting up), each increment burns one 01 of "fuel" from every digit it touches. In #3 (counting down), each decrement lengthens one block of a pair and shortens the other.

At an overflow (for #3, every second time the count reaches zero) the blocks re-pair: each block joins a neighbour to form a new digit, so the roles of the two kinds of block swap, and the counter gains a digit.

The danger is a block running dry at the wrong moment. The invariant combines parity (a block that runs dry has the right parity, so it just merges with its neighbour, which a rule covers) with lower bounds (the other blocks never get too short). It never needs to know when the merges happen.

Bell eats counter (#2, #30's table, W4-2)

One side of the tape is a counter. The other side is a budget, or a stretch of filler blocks. When the budget runs out, the machine eats the low end of the counter and refills the budget. Halting needs an eat to meet a tape in a bad shape.

• #2. busycoq already proves a neighbour (TM7 in its SOMDCv6 file) that differs in one transition; ours adds a +1 pass each time a sweep enters a filler block. The invariant is "the sweep recipe applies to this tape". The work is showing that every tape the recipe produces is again one it applies to, counting the pending +1s.
• #30's table (#30, #7, #31). Each round first digests a messy leftover from the last round, recursively: one bounce can run a whole mini-round. The invariant keeps the leftover small, so digesting it costs about the square root of the budget. From budget 17,705 on it always fits; Rocq computes the roughly 700 rounds before that.
• W4-2. The counter switches between two encodings and can be left messy after an eat. Linear bounds tie the counter's size to the last round's length (about 1 to 2.5 times it, the exact cap set by parity). They keep rounds long enough that a bite on a still-messy counter never lands at a bad moment.

Sync bouncer counters: a safe region (#4, #8)

A binary counter sits at one end, a row of blocks grows at the other, and the head bounces between them adding 1 per bounce. The numbers that matter are the block counts at each overflow.

• #4. One cycle changes the counts by one of two linear formulas, picked by a parity that looks random. Scaled by the counter's size, there is a six-sided region that both formulas map into itself. So the parity never matters. The run enters the region at step 17,215.
• #8. The same idea with an interval. A small tail at the right end answers each overflow with "wrap to 0" or "pause and rebuild", leaving four possible routes from one overflow to the next. A window for the left stretch's length, measured against the counter, survives all four.
• #8's tail is tracked only through its two front bits. Where they allow both answers, the proof accepts both.

A call stack with an exact cost (#12)

The tape is a stack of blocks of 1s, and each block acts like a function call that costs its caller one 1. Each round starts at the left edge with 3 calls to spend; halting needs a 4th.

A round replays the machine's own earlier history one level down, with some extra lone 1s added. An induction says exactly which inner rounds cost 3 instead of 2. The real top level has no extra lone 1s, so every top round costs exactly 2. This is exact counting, not an estimate.

Siblings: same table, new start

Nine kills share a transition table with a parent kill. They differ only in the state letters (for #33, #33b, #24 and #7 also by a mirror) and in which state the run starts from.

The same table means the same macro rules and the same invariant. The only new piece is the opening: simulate from the new start until the tape has the round shape, and check the parent's invariant there. For example, #3b reaches a tape with #3's property after 38,732 steps.

Some siblings shadow the parent's run (#25's far block is always 2 longer than #3's). Others take their own path through the same rules (#3b, #4b, #33b, #7, #31). Both are fine, because the invariant is about the shape of the tape, not about one particular run. Most sibling files are the parent's proof with the state names swapped, plus a new opening.

Mirrored siblings

A mirrored machine swaps L and R in every transition, so its run is the parent's run seen in a mirror.

busycoq already proves that mirroring a machine (flip_halts) or renaming its states (perm_halts) does not change whether it halts. So for #24 and #7, the file proves the parent's table never halts from the matching start state. It then checks that the mirrored, renamed table is exactly the parent's, and these two lemmas carry the result over.

33 is done the other way. Its tape rules are rewritten in mirrored form directly, and #11's invariant is used word for word, since it only talks about digit sizes, never about direction. #33b then reuses #33's file with its states renamed.

Neighbours: one transition changed (#12b)

After renaming, #12b differs from #12 in one transition. That transition only fires when a call starts at the left edge, where it takes a 6-step detour to the same tape #12 reaches in 2 steps.

So #12's whole picture carries over. But #12b's edge budget is 2 calls instead of 3, so it needs #12's exact result that every top round costs 2, with zero slack.

Adapted templates

busycoq holds proofs of hundreds of machines. For each new parent proof we started from the closest one and kept its architecture: how a tape shape is written, how one round is proved, and the final non-halting call. The rules, the invariant and the arithmetic are new.

"Adapted" means few lines in common. Counting the non-blank lines of our file that also appear, word for word, somewhere in the template's file, only 10% to 34% match. One changed transition can change the behaviour a lot (#4 is one transition from its template, yet only 18% of its lines match). By the same count, 81% to 95% of a sibling's lines also appear in its parent's file.

4. How to say it in one breath

Examples you can paste or adapt.

• #3: "It's a binary down-counter whose digits are pairs of blocks; each decrement grows one block and shrinks the other in every pair it touches, and every second zero re-pairs the blocks. A parity-plus-size invariant shows no block runs dry at a bad moment; it holds after 78,710 steps, and Rocq checks every rule."
• #4: "Each cycle the block counts follow one of two linear maps, picked by a parity we can't predict, but there's a hexagon (in the counts scaled by the counter size) that both maps send into itself. The run is inside it from step 17,215, so whichever parities come, it never halts."
• #30's table: "Every round has a budget N and first has to digest the last round's leftover. The digestion is recursive but costs about √N, so from N ≈ 17,700 it always fits, and Rocq simply computes the ~700 rounds before that."
• A sibling (#3b): "Same table as #3 with the states renamed, just started in another state. The rules and invariant are #3's word for word; the only new part is the opening, which lands inside #3's invariant after 38,732 steps." For a mirrored twin such as #24, add: "busycoq's flip and permute lemmas carry #3's proof across the mirror."