/machines/1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC/submission/README.md · raw

`1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC` never halts

Machine: 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC, a BB(6) holdout on every holdout list since June 2024 (line 134 of the 740-machine list). busycoq's verify/ has no proof of it, and no other holdout has the same table up to renaming and mirror. Viewer: https://bbchallenge.org/1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC
Class: "Bell eats counter" (spreadsheet Results row 1013, class only, no notes or claims).
Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9), importing Individual62 and BinaryCounter_v2. Print Assumptions nonhalt is closed (no axioms). It compiles in 3.4 s with -native-compiler yes, and coqchk re-checks it in 1.0 s (check_kill.txt).

Mechanism

Counter and budget word. The tape is a word (10)^p with one defect cell, then the counter BinInc [1;1] N on the right. Each count is a round trip into the word and back: it adds 1 to N, and every second count moves the defect two pairs further from the counter.
The eat. Once the defect has left the word, the next trip reaches the blank left edge. A C/F sweep shifts the whole word one cell into the counter, which eats the low digits: N odd → (N+1)/2, N ≡ 0 (mod 4) → N/4, N ≡ 2 (mod 8) → (N+6)/8. A new defect then walks the word again.
The N ≡ 6 (mod 8) case. The eat leaves a misaligned fixed-width counter Q_k(x, y) = D_k(x) 0 C(y). It counts up, is eaten once more, and overflows into a second defect, which walks left and cancels the first.

How the proof works

16 exact low-level runs give the count rules (INC1, INC0, INC011, OVF) and the eat rules (EAT, Y1–Y4). Each count is a left lemma plus an Inc right lemma (RBinInc_spec on C, IncQ on Q).
Walk lemmas (Wk, W2, W2Q, Bk, W0k) give five macro rules BS1–BS5, one per residue class of N, each EC p N -->+ EC p' N'.
The invariant J(p, N): 1 ≤ N ≤ 2p is closed under all five, and it implies the one precondition, 2^t ≤ p+7 for N = (2m+1)·2^(t+3) − 2 (step_J, split by lowbitS_cases).
The start is 171 steps to EC 2 4 (solve_init). Then multistep_nonhalt and progress_nonhalt_cond with P := J give nonhalt.

Template and what changed

Adapted from busycoq's verify/BECv5.v, Module TM1, architecture only: a BinInc counter, a budget word with a one-cell defect, one budget pair per count, an eat of low digits, BigStep lemmas and progress_nonhalt_cond with a linear invariant. Changes: the counter is on the right (RBinInc_spec); the defect walks away from it; the eat is at the far blank edge after a sweep over the whole word; it removes 1–3 digits by N mod 8; and N ≡ 6 (mod 8) adds the misaligned counter Q and a two-defect transient. The file has 530 lines, every lemma top level.

Files

1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.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).