1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD--- never halts

• Machine: 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 293 of the 778-machine list).
• Class: "Skelet 1-like Class 2" (spreadsheet Results row 1280 and the Classifications tab, class only, with no notes or claims; nothing in our Discord exports). It is the 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 68.1 s with -native-compiler yes (most of it is the 79,114-step init), and coqchk re-checks it in 24.7 s (check_kill.txt).

Mechanism

• Same table as #3, different start. Renaming the states by σ = (A C)(B D), with no mirror, gives #3's table. σ is the only one of the 720 × 2 maps that does. The twin starts in A = σ(C), so it runs #3's machine from 0^inf C> 0^inf: a different orbit of the same macro map.
• #3's counter. The tape is K(h; P; T) = 0^inf <C (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 C.
• Coupled orbits. At every macro step the twin's K is #3's K with the far block 2 longer, under the same rule sequence (checked over 2,209 re-pairings). The +2 enters only additively and never changes a branch. So the start is the only thing that changes: the twin's base E-start has far q = 26 where #3's has 24.

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; (95,68,0),(34,33,1),(10,15,1),(1,26,1); -) is one esx over 79,114 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 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). A script applied proof.md §5, with no hand edits: - the TM string; - a simultaneous σ-swap of the state names in the 14 sweep lemmas and K ({{A}}→{{C}}, {{B}}↔{{D}}); - init0 with (11,13); - base with last pair (1,26), and init (now 79,114 steps); - the header and rule-table comments.

Every es proof, the macro rules, J, Jstep and J_base are #3's text, unchanged. The file compiled on the first attempt. Apart from the state names, 36 lines differ. The file is 1,307 lines and imports only Individual62 from busycoq. It is a direct proof on the holdout string, with no equivalence lemma.

Files

1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---.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).

AI assistance: the informal proof and the Coq formalization were produced with the help of Claude (Anthropic). They were checked by our checker, check_kill: compile against pinned busycoq, theorem statement, forbidden tokens, Print Assumptions, coqchk.