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

`1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---` never halts

Machine: 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 622 of the 778-machine list).
Class: "Skelet 1-like Class 2" (spreadsheet Results row 1289 and the Classifications tab, class only, with no notes or claims; nothing in our Discord exports). It is the mirrored, state-renamed twin of our kill #3, 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (row 1278).
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 40.0 s with -native-compiler yes, and coqchk re-checks it in 14.6 s (check_kill.txt).

Mechanism

#3's table, mirrored, with a different start. Flip every direction (L↔R) and rename the states by φ: A→D, B→A, C→B, D→C, E→E, F→F, and you get #3's table, all 12 entries. φ is the only one of the 720 × 2 maps that does this. The twin starts in A, and φ(A) = D, so it is #3's machine run from 0^inf D> 0^inf: a different orbit of the same macro map.
#3's counter, mirrored. The twin's tape is the mirror image of #3's 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 (10)^p (01)^q s(d), so it grows to the right where #3's grows to the left. Each macro step decrements a binary number. Merges, an End tail, a re-pairing overflow and the rare X1/X2 detour all occur, under #3's 9 macro rules.
Only the start changes. From (D, tape0) the run reaches K(2; (11,12,0); −) at step 1,021. At step 78,911 it reaches the E-start K(2; (95,68,0),(34,33,1),(10,15,1),(1,25,1); −), which is #3's base except for the far q (25 instead of 24). #3's invariant holds there with the same constants.

How the proof works

#3's whole development, kept as tm3. It has 14 es sweeps, the 9 macro rules K h P T -->+ K h' P' T', the per-step invariant J (a ghost phase of the two-cycle period plus per-pair bounds on p + Rt and q − Rt) and Jstep. This proves nonhalt_D : ~ halts tm3 (D;; tape0), starting from a new init (78,911 steps by solve_initD) and J_base.
The conjugacy uses busycoq's own lemmas. perm_twin : Perm (flip tm) tm3 phi is checked entry by entry. Then Flip.flip_halts (the blank tape is symmetric, so flip_conf c0 = A;; tape0) and Permute.perm_halts (φ(A) = D) turn halts tm c0 into halts tm3 (D;; tape0), which nonhalt_D refutes.

Template and what changed

The file extends kill #3's .v (1,303 lines; in #3's own package). A script generated it, asserting each edit, and no hand edits were made afterwards. The changes: - tm is the twin, and #3's table becomes tm3, with the local -->*/-->+ bound to it; - solve_initD is busycoq's solve_init started in D (esx from a non-c0 start falls back to symbolic es, which did not finish); - init0, and base with far pair (1,25); - #3's nonhalt becomes nonhalt_D; - the conjugacy (phi, perm_twin, nonhalt, about 15 lines).

Every sweep, macro rule, J, Jstep and J_base is #3's text, unchanged, and the file compiled on the first attempt. In all, 22 of #3's lines were replaced and 82 lines added. The file is 1,363 lines and imports only Individual62 from busycoq. It is a direct proof on the holdout string. The second TM_from_str literal (#3's string, as tm3) is the only warning from our checker.

Files

1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---.v: the proof.
proof.md: the informal delta proof.
parent-proof.md: #3's informal proof, which proof.md cites by section.
check_kill.txt: our verifier's full output.
discord.md: the draft announcement, not posted.