Cryptids: when "does it halt?" is a math problem

1Antihydra's tape is two numbers

Antihydra 1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA keeps coming back to the same shape: a block of b ones, one 0, a block of a ones, and the head in E just past the right end. The brackets name the two blocks.

We write this tape E(a,b), as busycoq's AntiHydra.v does: 0^inf 1^b 0 1^a E> 0^inf. The four rows are E(4,0), E(8,2), E(14,4) and E(23,6). The whole machine is these two numbers.

Antihydra's records in the explorer (10⁹ steps)

2One move, step by step: a grows by half

Here is the real run from the blank tape: 11 steps to E(4,0), then one full move to E(8,2) at step 58. At step 13, F writes a 0 inside a's block. That 0 is a hole, and it walks left.

Go to step 20: the hole is on cell −1, with 3 ones on its right, and B stands just left of it. Go to step 38: the hole is on cell −3, with 6 ones on its right. Each trip, the hole moves two cells left and the block on its right gains three 1s.

Two 1s in, three 1s out: that is the ×3/2. The same move on a bigger tape, E(14,4) to E(23,6), shows it plainly. There is one row each time B steps onto the cell just left of the hole: the hole is on cell 7 with 3 ones on its right, then cell 5 with 6, and so on down to cell −5 with 21. Seven rows, six trips.

One trip is busycoq's lemma B_once (in AntiHydra.v): 1 1 <B 0 1^m becomes <B 0 1^(m+3), as in the rows above. Our check counts 2m + 12 steps per trip, for m = 0 … 15 (C-M7-3). In the last row, B reads the 0 that separates a from b: the move ends there, and what happens next depends on a's parity (next section).

3Even or odd, and the door to halting

If a is even, the 1s pair up exactly, and the end of the move adds two 1s to b (you saw b go 0 → 2 above). If a is odd, one 1 is left over, and the machine takes one 1 from b. If b is already empty, F reads a 0, and F0 is ---, Antihydra's only undefined transition: the machine halts.

The real run has not come back near b = 0 (in its first 100,000 moves b never drops below 2; section 4). So here is a tape we wrote by hand, E(5,1). Play it: a = 5 is odd, so b drops to 0 at step 41, giving E(9,0). Then a = 9 is odd again, b is empty, and the machine halts at step 125.

Go to step 124: F stands on the blank cell −8 and reads a 0. Step 125 is the halt. (Our simulator draws the halting step as "write 1, move right", so the last frame shows cell −8 as a 1 and the head on cell −7.)

So one move is this rule. busycoq proves each line in Coq (AntiHydra.v: lemmas R0, R1 and Rhalt), and this page's check ran every start E(a,b) with a = 2 … 41 and b = 0 … 6 on the real machine: all 280 go where the table says (C-M7-4).

4The long run: b is a lopsided walk

Forget a's size and watch only b. It starts at 0 and goes up 2 for each even a and down 1 for each odd a. So after k moves, b = 2 × (number of even a so far) − (number of odd a so far). The machine halts the first time an odd a arrives while that count is 0.

The walk drifts up: b is 4,862 after 10,000 moves and 50,477 after 100,000. In the first 100,000 moves it never drops below 2. Of those 100,000 values of a, 50,159 are even and 49,841 odd: it looks like fair coin flips (C-M7-5).

Pretend the parities really were coin flips. To halt from b + 1, the walk must first come down to b, and the chance that it ever comes down one step is 0.618. So each extra 1 in b multiplies the halting chance by 0.618: b = 0 gives 62%, b = 10 gives 0.5%, b = 4,862 gives 10⁻¹⁰¹⁶.

In a formula: the chance of ever halting from b would be 0.618^b+1, where 0.618 = (√5 − 1)/2. Here is the same thing with coin flips, done in your browser:

The community calls such a machine "probviously" non-halting: almost surely it never halts, but nobody has proved it.

The parities are not coins: the rule fixes every one of them. The machine halts exactly when the odd a's get ahead of twice the even a's. Proving that repeated ×3/2 never lets that happen is a question of the same kind as the Collatz problem, and nobody knows how to do it. That is what makes Antihydra a cryptid (the wiki relates it to Mahler's 3/2 problem; atlas/curriculum.md §6.1).

5Ours: #32, one transition away from a kill

#11 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- is one of our proved kills: a counter whose digits carry fuel (module 3). #32 1RB0LC_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- is the same table with one cell changed: what A does on reading 1 (outlined).

#11 is proved. #32 is not. Its tape is a counter too: a wall on the left, then digits, each made of a block of 10s, sometimes 00, and a block of 01s. Here is a real #32 tape. The orange bracket is the top digit's 01 block: its length is the fuel N.

Each cycle of the top digit takes 5 from N (and adds 1 to M). In the real run, N is 136 at step 276,564,068, 131 at step 943,819,758, and 126 at step 7,099,688,084 (C-M7-13). So N's remainder when divided by 5 never changes, and only remainder 2 leads to the halting path.

We took the tape above, changed only N to each value 0 … 44, and ran each copy:

Exactly N = 2, 7, 12, 17, 22 halt: the values with remainder 2, after 0, 1, 2, 3 or 4 cycles. From N = 23 on, the next digit's fuel (48, which loses 12 per cycle) runs out in the 5th cycle, before N does, and even the remainder-2 values stop halting. Cutting that digit's fuel too switches the outcome again, irregularly.

So halting depends on remainders at every level of the counter, and no invariant we know of can capture that (#32's status.json and notes.md).

R4 1RB0RE_1LC0RD_1LD0LD_1RA0LC_1RA1RF_1RA--- is #32's table, mirrored and with the states permuted, started in #32's state D (C-M7-6). Its top fuel was N = 32 at step 475,465, and N = 27 one cycle later, at step 14,968,044,039. And 27 = 5 × 5 + 2: the halting remainder.

If the top keeps losing 5 per cycle, R4 halts when N reaches 2. But a deeper digit (fuel 1,083) has to run out first, and neither machine halts by 10⁸⁰ steps. Unlike Antihydra, the coin-flip guess here leans to a halt, astronomically late (R4's status.json). That is how a cryptid could hold one of the longest runs of all (section 7).

6Ours: a chaotic edge, and the bits of a number

frozen leftovers the edge ↘ block of 1s →

#5 is a race. Each bounce, the head runs right through the block of 1s, adds one cell at its right end, runs back, and dives into the edge. So the block gains 1 cell per bounce on its right, while the edge eats about 0.04 cells per bounce on its left (C-M7-14).

By step 10⁹ there have been 32,262 bounces: the block's right end is at cell 32,261, its left end (the edge) only at cell 1,861. A Coq file of ours proves #5 never halts exactly when the edge never eats the block down to two cells. We found no bound on how fast the edge can eat in a burst. No halt in 10⁸ bounces, about 9.6·10¹⁵ steps (#5's status.json).

#26 1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB is #5's table, mirrored and permuted, started in #5's state C (C-M7-6).

W5-2 1RB0RF_1RC1LB_1LD1RE_1LB0LD_1RF0RC_1RA--- repeats one cycle, and each cycle turns a number x into a much bigger one. Count x's bit positions from the lowest bit, which is position 0. The cycle repeats as long as x has a 1-bit at an even position (green below). Only a cycle whose 1-bits all sit at odd positions lets the machine leave the cycle, and then it can halt.

If the bits were coin flips, a cycle whose x has k one-bits would leave with chance about 2^−k: every one of them must land on an odd position. x has 25 one-bits at cycle 4 and 14,392 at cycle 20,000, and none of the first 20,000 cycles leaves (W5-2's status.json and notes.md). Again "probviously" non-halting, and again a question about the digits of a fast-growing number.

#5's edge in the explorer (zoom in on it)one bounce off the edge, every step

7Why BB(6) waits for cryptids, and why we stop

BB(6) = the longest run among all halting 6-state machines.

R4 makes this concrete. Its coin-flip guess leans towards a halt, after more than 10⁸⁰ steps, at a step count nobody can compute (section 5). Until someone settles it, nobody can say whether that number beats every other halting machine.

Every machine on the holdout list has to land in the first or second box before BB(6) has an exact value. A cryptid cannot be moved without solving its number problem, and simulation cannot do it: a run that has not halted yet proves nothing (module 5). So our rule for a cryptid is short (CLAUDE.md):

1. Formalise the rules. Prove the rules in Coq, so the machine provably reduces to its number problem. AntiHydra.v does this with R0, R1 and Rhalt; our reduction.v for #5 proves "never halts ⇔ the edge never eats the block".
2. Flag it. Status CRYPTID_CANDIDATE in the machine's status.json: all five above.
3. Stop. No more compute. Dennis stopped #32 and R4 on 2026-10-12; the effort goes to holdouts that can be proved.