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

`1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---` never halts

Machine: 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 53 of the 778-machine list).
Class: "Skelet 1-like Class 2" (spreadsheet Results row 1278, no notes or claims; no Discord thread found). Two other holdouts, 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC--- and 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---, look like the same mechanism in simulation: at 1e9 steps their tapes are within 4 cells of ours (67,343 / 67,345 / 67,347 cells). They are not formalized; 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 71.1 s with -native-compiler yes (about 30 s of that is the 78,710-step init), and coqchk re-checks it in 24.7 s (check_kill.txt).

Mechanism

The tape is K(h; P; T) = 0^inf <A (10)^h 11001 [p_1,q_1,d_1] .. [p_L,q_L,d_L] T 0^inf, with pairs [p,q,d] = (10)^p (01)^q s(d), s(1) = 0001, s(0) = 0010. The digits form a binary number V, least significant next to the head.
Each macro step (three short bounces, then one sweep to the borrow pair and back) subtracts 1 from V. Every pair it touches gets p+1, q-1 and a flipped digit. A borrow pair whose q runs out fuses with the next pair (DecMerge).
At V = 0 an End sweep adds a tail (10)^t 1. At the next 0, the overflow re-pairs the blocks as (q_j, p_{j+1}), adds a pair and resets h to 2. Rare double run-outs detour through a second tail (101)^2 (01)^k (X1, X2). The machine halts only from shapes no rule covers, for example a pass-through pair with q = 1.

How the proof works

Rules. 14 sweep lemmas (each one plain es) and three list inductions give the 9 macro rules Dec, DecMerge, DecMergeTail, DecMergeEmpty, End, EndLast, X2, Ov and X1. Each rule is a lemma K h P T -->+ K h' P' T'.
Start. init : c0 -->* K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); -) runs 78,710 steps in one esx.
Invariant J. The state is (h, P, T, phase, c4). The ghost phase (8 values) records where the run is in the two-cycle period: an E-cycle containing End, then an L-slot containing EndLast or ending in X1. For every pair, J bounds the projected values p + Rt and q - Rt, where Rt is the number of touches the pair still gets before the next re-pairing. It also fixes parities, and bounds pairs 1 and 2 and h. A touch leaves the projected values unchanged, so only merges and re-pairings need arithmetic. Jstep shows that every J state takes one macro rule into another J state. In particular it never reaches a halting shape.
nonhalt = multistep_nonhalt with init, then progress_nonhalt_cond with P := J.

Template and what changed

It loosely follows SBCv6.v Module TM21 (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE): a pair list with counting sweeps and a re-pairing overflow. - Kept: a Fixpoint over the pair list as the configuration, the overflow as a list re-pairing (ovp/ovpX, as TM21's Ov), and multistep_nonhalt + progress_nonhalt_cond. - Changed: the macro step is one decrement, not TM21's whole-countdown LIncs. Here merges are routine and happen mid-countdown. The digits carry binary tags, and there is the X1/X2 tail detour. TM21's LWF (q >= 2^len, which rules out merges) is replaced by J. proof.md's per-cycle invariant INV+(e) (§3.8) appears inside J in projected form. J has no period lemma, and it does not need proof.md's L6 or L5'.

The file is 1,303 lines, about 4.2 times TM21's 308. proof.md §4 maps the informal proof to lemma names.

Files

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