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

`1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---` never halts

Machine: 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 604 of the 778-machine list).
Class: "Skelet 1-like Class 2" (spreadsheet Results row 1288 and the Classifications tab, class only, with no notes or claims; nothing in our Discord exports). It is the fourth holdout with the table of our kill #3, 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (row 1278). The other two, 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD--- (row 1280) and 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC--- (row 1289), are also killed.
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 52.4 s with -native-compiler yes (most of it is the 38,732-step init), and coqchk re-checks it in 17.5 s (check_kill.txt).

Mechanism

Same table as #3, different start. Renaming the states by ρ: A→D, B→A, C→B, D→C (E and F fixed, no mirror) gives #3's table. ρ is the only one of the 720 × 2 maps that does. The machine starts in A = ρ(B), so it runs #3's machine from 0^inf B> 0^inf.
#3's counter. The tape is K(h; P; T) = 0^inf <D (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). Each macro step decrements a binary number, and merges, an End tail, a re-pairing overflow and the rare X1/X2 detour all occur. #3's 9 macro rules hold verbatim, with head state D.
An uncoupled orbit. #25 and #24 run #3's orbit with one far exponent shifted. This orbit is not coupled to #3's: none of its first 120 E-starts (configurations after an even re-pairing) is one of #3's. Its base E-start, K(2; (47,32,0),(40,33,1),(13,34,1); -) at step 38,732, has 3 pairs where #3's has 4. That is L* = 3, the smallest value #3's invariant allows.

How the proof works

14 sweep lemmas (each plain es) and three list inductions give the 9 macro rules, each K h P T -->+ K h' P' T'.
init : c0 -->* K 2 base TN is one esx over 38,732 steps.
3's per-step invariant J is a ghost phase of the two-cycle period plus, for every pair, bounds on the projected values p + Rt and q − Rt. J_base shows it holds at the 3-pair base (one clause is tight, 48 ≥ 48, as at #3's base), and Jstep shows every J state takes a macro rule to another J state.
nonhalt = multistep_nonhalt with init, then progress_nonhalt_cond with P := J.

Template and what changed

It extends kill #3's .v (1,303 lines, in #3's own package; #3 loosely follows busycoq's verify/SBCv6.v, Module TM21). A script applied proof.md §5, with no hand edits to proof scripts: - the TM string; - a simultaneous ρ-rename of the state names in the 14 sweep lemmas and K ({{A}}→{{D}}, {{B}}→{{A}}, {{D}}→{{C}}); - init0 with (7,4) at 402 steps (a cross-check, not used by nonhalt); - a 3-pair base, and init (now 38,732 steps); - the header and rule-table comments.

Every es proof, the macro rules, J, Jstep, J_base and nonhalt are #3's text, unchanged, and the file compiled on the first attempt. After the renaming, 16 of #3's lines differ. The file is 1,309 lines and imports only Individual62 from busycoq. It is a direct proof on the holdout string, with no equivalence lemma.

Files

1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---.v (the proof), proof.md (informal delta proof), parent-proof.md (#3's informal proof, cited as P§n), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).