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

`1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---` never halts

Machine: 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 681 of the 778-machine list).
Class: "Sync bouncer counter" (spreadsheet Results row 921, no notes or claims; archive: "does not halt in 2e13").
Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9c). Print Assumptions nonhalt is closed (no axioms). Compile time is 6.4 s with -native-compiler yes; coqchk re-checks it in 2.0 s (check_kill.txt).

Mechanism

On the left is a binary counter C_k(n): k digits, MSB first, 1 = 1010, 0 = 0010 (TM4's d1/d0). The head bounces between the counter and the right edge, adding 1 to the counter on each visit. Between them is a row of 5-cell blocks, A = 00111 and B = 10111.
In the P phase, each bounce adds one B block. When the counter overflows, it gains a digit and a 3-cell front 111 appears at its right. In the Q phase the front walks right, 2 A blocks every 3 bounces.
When the front reaches the B blocks, it turns them all into A blocks, and the next cycle runs with one more counter digit. The conversion has an even and an odd case. In the odd case the counter can overflow partway through, and a new front then runs while the old conversion finishes.

How the proof works

Rules. 21 shift rules (each one es) and their repeated forms. A counter ctr k n with an increment lemma CTR. A one-step front lemma QC. On the right-edge configurations P/Q, these give the macro rules R1–R3.
Conversion. Gad is an inductive gadget: each hit reflects the head and adds 0 or 1 A block. One induction over it gives R4, R5 and the overflow case R5o.
Invariant. Over a cycle, the scaled block counts (Y/N, Z/N), with N = 2^k, follow an affine map. It has two branches, picked by the parity of Y, and both map a hexagon into itself. So the parity never matters, and the machine is not a cryptid.
nonhalt. multistep_nonhalt with init (c0 reaches Q(7,65,1,16,0) in 17,215 steps, by esx), then progress_nonhalt_cond. Its index is (k,i,y,z) and its invariant Inv is the hexagon. Each step is one R3, or one conversion plus a P phase. Every side condition is lia.

Template and what changed

This extends SBCv7.v Module TM4 (1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_0RA---), which differs only in F0 (0RA there, 1RC here). TM1, TM2, TM3, TM18 and TM37 in that file also differ only in F0. - Kept: TM4's moving head <A 001 / 001 E> (hL/hR), its digits d0/d1, and the overall shape: init, a big step per cycle, and progress_nonhalt_cond with a linear invariant. - Changed: - F0 = 1RC changes every right-side word. TM4's unary right counter is replaced by the A/B blocks, the front gadget (FL, FR1–FR3) and the conversion gadget. - TM4's Longitudinal counter lemma is replaced by a direct Fixpoint ctr, so the file imports only Individual62, Arith, Lia and String. - TM4's one-inequality invariant is replaced by a 6-facet hexagon that holds on both branches. - New lemmas ConvOV/PostOV cover the overflow during an odd conversion.

The file is 504 lines, about 3 times TM4's 170. The informal proof is proof.md.

Files

1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v (the proof), proof.md (informal proof, §6 maps it to lemma names), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).