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

`1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---` never halts

Machine: 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, a BB(6) holdout. It is on every holdout list from 14 June 2024 through 7 October 2026 (line 467 of the 778-machine list).
Class: "Skelet 1-like Class 2" (spreadsheet Results row 1284, no notes or claims).
The same transition table, started in B, C and D, gives three more holdouts: 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- (hipparcos, Level 1 tab), and the mirrored 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- and 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---.
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 9.3 s with -native-compiler yes, and coqchk re-checks it in 1.9 s (check_kill.txt).

Mechanism

At the right edge the tape is K = 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b B> 0^inf. Each digit is (10)^u 00 (01)^v (bit 0) or (10)^u (01)^v (bit 1), and d_m is the least significant bit.
Each carry M adds 1 to this binary counter. Every digit it touches loses one 01, and a digit flipped 0→1 also gains a 10. When a flipped digit has used up its last 01, it merges into the digit below it, so the counter loses a digit.
On overflow (all bits 1), O re-pairs the halves of every digit: the (10)^u blocks become the (01) fuel of new bit-0 digits. 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 01 left.

How the proof works

Rules. 20 window lemmas: shifts S1–S6 (one block by es, then shift_rule_L/R or induction) and turns T1–T14 (es). They compose into the digit lemmas Lb/Lf/Rb/Ro and, by list induction over the digits, into M_spec, Mdrop_spec (carry with a merge) and O_spec.
Invariant. INV = Common ∧ (A ∨ B ∨ C), a three-phase cycle: A (no merges), B (the top digit (0,0,1) is about to merge), C (it has merged). Each digit's conditions use R, the number of carries still to come into it before the next overflow (Rof, computed from the digits above it). They are parities, v ≥ R + 1, and bounds ubar ≥ 2^j, and together they rule out the failure case. Which digits merge when is irregular, but the invariant never needs to know, so the machine is not a cryptid.
nonhalt. multistep_nonhalt with init (c0 reaches K((1,1,2); 8, 5) in 483 steps, solve_init), then progress_nonhalt_cond with P := INV. step shows each INV state takes one M, merge or O step into INV, with the closure facts F1 (carry), F2 (merge) and F3 (overflow) proved as list inductions.

Template and what changed

It follows the architecture of SBCv6.v Module TM21 (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE), a binary counter over a list of (n, m) pairs with a re-pairing overflow. Its transitions are not close (10 of 12 differ under the best renaming). - Kept: a Fixpoint over a digit list as the configuration, the overflow as a list re-pairing (Oz/Oout, as TM21's Ov), and multistep_nonhalt + progress_nonhalt_cond with a list invariant. - Changed: every digit carries a bit. The macro step is one carry (M_spec) rather than TM21's whole-cycle LIncs/BigStep, because merges happen at data-dependent times. TM21's LWF (2^len ≤ m) fails here, so it is replaced by the three-phase INV. The window lemmas are direct es runs, not flip/sideRLs.

The file is 694 lines, about 2.2 times TM21's 308. The informal proof is proof.md (§6 maps it to lemma names).

Files

1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v (the proof; upstream verify/Skelet1LikeC2_1RB0LE_1RC0RC.v), proof.md (informal proof), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).