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

`1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---` never halts

Machine: 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---, a BB(6) holdout on every holdout list since June 2024 (line 349 of the 740-machine list). busycoq's verify/ has no proof of it; Eqv_v3.v, Module TM518, only relates it to another machine.
Class: "Bell eats counter" (spreadsheet Results row 1038, class only, no notes or claims). Mirrored and renamed (A→F, B→A, C→B, D→C, E→D, F→E) it is TP = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC started in F, and TP is BECv5's TM1/TM2 with F1 = 1RC.
Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c), importing only Individual62. Print Assumptions nonhalt is closed (no axioms). It compiles in 64.1 s with -native-compiler yes, and coqchk re-checks it in 27.2 s (check_kill.txt).

Mechanism

A mirrored Bell-eats-counter. On TP's side the tape is 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf. Each bounce applies one map phi to the left word w (two interleaved binary numbers, even and odd cells) and moves one 10 from the n-block to the m-block. At n = 0 the right side eats the low end of w and refills n.
A three-step detour. TP's F1 = 1RC is always followed by C1 = 1LA and A1 = 1LF, because F is entered only by A1, which leaves a 1 on F's right. The three steps leave the tape exactly as a single F1 = 1LF would, so the left step still computes phi, 2 steps slower per detour.
Where halting is. The counter alternates between a standard and a packed encoding, and an overflow can leave it dirty. The machine halts only if an overflow finds the lowest 1 of phi(w) on an odd cell with 01 or 11 above it. The invariant keeps every overflow off those points.

How the proof works

Exact rules on TP: eight one-digit lemmas, the left step as the inductive relations PA/PF (proved against the machine by mutual induction), the right step and the overflows.
One sweep lemma for phi gives eleven macro rules (S0–S3, P0–P4) between clean overflow states (typ, N, m).
The invariant I is 1 ≤ m ≤ N plus linear bounds on N in terms of m, chosen by the parities of N and m. Under I exactly one macro rule applies, none meets a halting overflow, and each maps I into itself. From F the run reaches (std, 2, 2) after 73 steps, and progress_nonhalt_cond with P := I gives nonhalt_F : ~halts tmP (F;; tape0).
The conjugacy perm_349 : Perm (flip tm) tmP f349 holds by computation, and busycoq's flip_halts and perm_halts turn halts tm c0 into halts tmP (F;; tape0).

Template and what changed

Adapted from busycoq's verify/BECv5.v, Module TM1 / Module TM2, through our proof of 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (the same table with F1 = 1LF, 1,217 lines, in its own package). Changes: tm becomes tmP with F1 = 1RC; TF2, TF3 and the PF clause of phi_spec carry [1] *> r on the right; a 73-step initF from F (solve_initF) replaces the 32-step start; nonhalt becomes nonhalt_F; tm, f349, perm_349 and nonhalt are added. Comments aside, 16 lines were replaced and 43 added. The file has 1,278 lines, every lemma top level.

Files

1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v (the proof), proof.md (informal proof; its §8 maps it to the .v), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).