1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- never halts #

• Machine: 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (the 778-machine list).
• Class: "Bell eats counter" (spreadsheet Results row 1035, no prior notes or claims).
• Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9c). Print Assumptions nonhalt is closed (no axioms). Compile time is 3.6 s with -native-compiler yes; coqchk re-checks it in 1.1 s (check_kill.txt).

Mechanism #

• At each sweep boundary the tape is S(r) = 0^inf 11 D> <r> 0^inf, where r is a word over three 3-cell digits: L = 110, 0 = 000, 1 = 100. In practice r is a long L-run followed by a short binary counter.
• Each sweep has an eater that turns digits into L until it reads a 1. It then runs k drain passes (k = digits eaten), which rebuild the counter at the right end in bijective binary. A drain pass that reaches an L restarts the eater. The wall ends one cell further left.
• Whenever a sweep enters an L digit (eater or drain pass), it first runs one extra pass over everything to the right. That pass adds +1 to the 0/1 digits, read as a little-endian binary number with L digits skipped.

How the proof works #

The sweep is the inductive relation RIncs hx 0 r r'. RIncs_spec proves each clause is an exact pass-level run, and BigStep gives S(r) -->+ S(r'). The invariant is P r := exists r', RIncs hx 0 r r', starting at S(L1) (step 16). domain shows P is closed under the sweep. nonhalt follows from multistep_nonhalt and progress_nonhalt_cond, as in the template.

Template and what changed #

This extends SOMDCv6.v Module TM7 (1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---), which differs only in A1 (0RC there, 0RF here).

1. New Inc relation (one pass = +1, L skipped), proved as sideRLs tm h.
2. Inc premise on the two L clauses of RIncs (eater enters L, drain pass enters L). Their segment facts become [h; h'; h] (seg_hx_ld, seg_h1_ld).
3. Two zero-pass end clauses, Z1 RIncs h1 0 [D1] [LD] and Z0 RIncs h1 0 [D0] [D1]. They add no machine behaviour (1 100 0^inf = 110 0^inf, 1 000 0^inf = 100 0^inf), but without them the sweep's domain is not closed.
4. Domain lemma redone as key, with j pending +1 passes and a condition Inv that reduces to TM7's when j = 0. It uses the helper lemmas RIncs_Inc, End_1 and End_x.

The file is 599 lines, about 2.4 times TM7. The informal proof is proof.md.

Files #

1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v (the proof), proof.md (informal proof), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).

AI assistance: the informal proof and the Coq formalization were produced with Claude Code (Anthropic) under Dennis's direction, and checked by our checker, check_kill (compile against pinned busycoq, theorem statement, forbidden tokens, Print Assumptions, coqchk).