1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA never halts

• Machine: 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 17 of the 778-machine list). Its equivalence-class member is 1RB0LC_1LC0RB_0LD1LA_0RA1LE_0LA1LF_1LD---.
• Class: "Sync bouncer counter" (spreadsheet Results row 915; no status, notes or claims). It is on mxdys's UBRRBA_TODO and dyuan01's Oct 1 longitudinal list. Neither list is a claim. It is the state-renamed twin of our kill #4, 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC--- (row 921).
• 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 7.0 s with -native-compiler yes, and coqchk re-checks it in 2.1 s (check_kill.txt).

Mechanism

• #4's table, different start. Renaming the states by σ = EDBCFA (A→E, B→D, C→B, D→C, E→F, F→A), with no mirror, turns #4's table into this one. σ is the only one of the 720 × 2 maps that does. This machine starts in A = σ(F), so it runs #4's machine from 0^inf F> 0^inf. That is a different orbit of the same macro map, not #4's own run.
• #4's counter. On the left is a binary counter (digits 1010/0010), and a head <E 001 / 001 F> bounces off the right edge, adding 1 per visit. In the P phase each bounce appends a block B = 10111. On each overflow the counter gains a digit, and a front 111 walks right through the A blocks (00111). When the front reaches the B blocks, they all become A blocks.
• Same invariant. At each cycle start S(k,Y,Z), with N = 2^k, the block counts follow #4's two-branch affine map. Both branches keep the hexagon 8Y>=N, 8Y<=3N, 3Z<=N, 8Z>=-N, 4Y+2Z>=N, 20Y+16Z<=9N, so the parity never matters (not a cryptid). The two orbits differ: the branch sequences are not the same, and this one uses R5o once (m = 31).

How the proof works

• 4's cycle lemma cycle_step : Inv k i y z -> exists ..., CfgF k i y z -->+ CfgF k' i' y' z' /\ Inv k' i' y' z' never mentions the start. So only init and the start index of nonhalt change.

• init : c0 -->* CfgF 5 0 14 4, one esx over 16,590 steps. That is S(6,14,4) = Q(7,65,1,14,4); #4 has S(6,16,0) after 17,215 steps. Inv 5 0 14 4 holds, with 4Y+2Z >= N tight (64 = 64), as at #4's base. The final cbn; lia closes it.
• Every rule is re-proved on this machine's own table by es (22 shift lemmas), so the renaming is an explanation, not a premise. nonhalt = multistep_nonhalt with init, then progress_nonhalt_cond with Inv. It is a direct proof on the holdout string; it does not use busycoq's Eqv_v2.v TM7.

Template and what changed

It extends kill #4's .v (504 lines; in #4's own package), which extends SBCv7.v Module TM4. A script applied proof.md §5, with every substitution count asserted: - the TM string; - σ applied to every state name {{X}}: {{A}}→{{E}} 37 times, {{C}}→{{B}} 6, {{E}}→{{F}} 35; - init0/init (16,590 steps to CfgF 5 0 14 4) and the start index (5,0,14,4); - the header and the rule-table comment.

After the renaming, 4 code lines differ from #4's .v. The counter, the Gad conversion gadget (R4/R5/R5o), Inv and cycle_step are #4's text. It compiled and passed check_kill on the first attempt. 510 lines, imports only Individual62.

Files

1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v (the proof), proof.md (informal delta proof), parent-proof.md (#4'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.