/machines/1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---/submission/README.md · raw

`1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---` never halts

Machine: 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, a BB(6) holdout. It is on every holdout list from 14 June 2024 through 7 October 2026 (line 34 of the 778-machine list).
Class: "Skelet 1-like Class 2" (spreadsheet Results row 1277, note "Machine with the most common transitions"; no status, links or claims).
It runs the table of our kill #11 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (row 1284), mirrored (L<->R) and renamed (A,B,C,D,E,F -> B,C,D,A,E,F), started in #11's state D.
Two more holdouts share that table: hipparcos's Level 1 machine 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- and 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---. This file proves only our string.
Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9c). Print Assumptions nonhalt is closed (no axioms). It compiles in 10.1 s with -native-compiler yes, and coqchk re-checks it in 2.1 s (check_kill.txt).

Mechanism

The head works at the left edge. At each visit the tape is K = 0^inf <C (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf. Each digit is (10)^v 00 (01)^u (bit 0) or (10)^v (01)^u (bit 1), and d_m, next to the block, is the least significant bit.
Each carry M adds 1 to this binary counter. Every digit it touches pays one 10, and a digit flipped 0->1 also gains a 01. A flipped digit with no 10 left merges into the next one, so the counter loses a digit.
On overflow (all bits 1), O re-pairs the halves of every digit, and the counter restarts at 1 with one more digit. The only way the rules could fail is a carry reaching a bit-0 digit with no 10 left.

How the proof works

Rules. 20 window lemmas, S1-S6 (one block by es, then shift_rule_L/R or induction) and T1-T14 (es), compose into the digit lemmas Lb/Lf/Rb/Ro and, by list induction, into M_spec, Mdrop_spec (carry with a merge) and O_spec.
Invariant. #11's three-phase INV = Common /\ (A \/ B \/ C) (no merges / top digit about to merge / merged): parities, v >= R + 1 and ubar >= 2^j bounds, with R, the carries a digit still has to take, computed structurally. It rules out the failure case.
nonhalt. multistep_nonhalt with init (c0 reaches K [d1 1 3] 4 1 in 215 steps, solve_init, class A), then progress_nonhalt_cond with P := INV and the closure lemma macro_step.

Template and what changed

It extends our kill #11's .v, verify/Skelet1LikeC2_1RB0LE_1RC0RC.v (694 lines), which follows the architecture of SBCv6.v Module TM21 (carries plus a re-pairing overflow). TCv3.v is only a loose relative. - Machine part, mirrored by hand. The dictionary is l {{q}}> r -> r <{{pi q}} l, l <* xs -> xs *> l, shift_rule_R <-> _L, with list literals unchanged. #11's rule-spec statements are kept word for word. Beyond the dictionary, the only edits were dl->dr, L0->R0, one unfold R0 and one explicit S6 instance. The rw/ro_out accumulators change side. - Abstract part (INV, F1-F3, closure, about 390 lines): #11's text byte for byte, except that step is renamed macro_step so it does not shadow the framework's step. - New: init (215 steps to K [d1 1 3] 4 1, against #11's 483 to K [d1 1 2] 8 5) and the base of nonhalt. Everything compiled on the first try.

The file is 671 lines, imports only Individual62 from busycoq, and has one TM_from_str. proof.md is the informal proof; its §6 maps sections to lemma names.

Files

1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---.v (the proof; upstream verify/Skelet1LikeC2_1RB0RE_1LC0RE.v), proof.md (informal proof), check_kill.txt (our verifier's full output, 2026-10-13T00:39:13Z), discord.md (draft announcement, not posted).