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

`1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---` never halts

Machine: 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---, a BB(6) holdout. It is on every holdout list from 14 June 2024 through 7 October 2026 (line 388 of the 778-machine list).
Class: "Skelet 1-like Class 2" (spreadsheet Results row 1282 and the Classifications tab, class only, with no notes or claims; nothing in our Discord exports).
It is the table of our kill #33 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA--- (row 1277) with the states renamed by σ = A->B, B->C, C->D, D->A (E, F fixed), with no mirror, started in #33's state D.
Equivalently, it is our kill #11's table 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (row 1284) mirrored and started in #11's state C.
Four holdouts share this table, the fourth being hipparcos's Level 1 machine 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---. All four are formalized, each in its own file.
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 13.2 s with -native-compiler yes, and coqchk re-checks it in 2.5 s (check_kill.txt).

Mechanism

Same counter as #33. The head works at the left edge. At each visit the tape is K = 0^inf <D (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.
Carry and overflow. Each carry M adds 1. Every digit it touches pays one 10, a digit flipped 0->1 gains a 01, and a flipped digit with no 10 left merges into the next one. On overflow (all bits 1), O re-pairs the halves of every digit, and the counter restarts with one more digit.
Different orbit, same macro map. The rules are #33's with head state D instead of C. Only the start differs: from blank the machine reaches K((1,1,9); 8, 1) at step 687 (class A of the invariant), where #33 reaches K((1,1,3); 4, 1) at step 215.

How the proof works

Rules. 20 window lemmas S1-S6, T1-T14 (es, then shift_rule_L/R or induction) compose into the digit lemmas Lb/Lf/Rb/Ro, the sweeps LbS/RbS/RoS and the rule specs 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), with parities and lower bounds, rules out the one failure case (a carry reaching a bit-0 digit with no 10 left). macro_step shows that every INV state takes M or O to an INV state.
nonhalt. multistep_nonhalt with init (c0 reaches K [d1 1 9] 8 1 in 687 steps, solve_init), then progress_nonhalt_cond with P := INV.

Template and what changed

It extends our kill #33's .v, verify/Skelet1LikeC2_1RB0RE_1LC0RE.v (671 lines). That file ports #11's .v, verify/Skelet1LikeC2_1RB0LE_1RC0RC.v, which follows the architecture of busycoq SBCv6.v Module TM21 (carries plus a re-pairing overflow). A script applied proof.md §5, with no hand edits to the code: - the TM string; - σ on every state name: {{A}}->{{B}} (5), {{C}}->{{D}} (22), {{D}}->{{A}} (18), with {{E}} (18) unchanged; - init (687 steps to K [d1 1 9] 8 1, against #33's 215 to K [d1 1 3] 4 1) and the base in nonhalt, closed by #33's own tactic line; - the header and the comments.

Every proof script, the three rule specs and the invariant part are #33's text. It compiled on the first try, and no tactic was changed. The file is 673 lines, imports only Individual62 from busycoq, and has one TM_from_str. It is a direct proof on the holdout string, with no Flip/Permute bridge.

Files

1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---.v (the proof; upstream verify/Skelet1LikeC2_1RB0LD_1RC0RE.v), proof.md (informal delta proof), parent-proof.md (#33's informal proof, cited as P§n), check_kill.txt (our verifier's full output, 2026-10-13T00:40:21Z), discord.md (draft announcement, not posted).