/machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/submission/README.md · raw

`1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF` never halts

Machine: 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF, a BB(6) holdout. It is on every holdout list since June 2024 (line 240 of the 778-machine list, line 224 of the 740-machine list). busycoq's verify/ has no proof of it (Eqv_v3.v, TM493 only relates its mirror to another machine).
Class: "Bell eats counter" (spreadsheet Results row 1015, no notes or claims). It is BECv5's TM1/TM2 with a different F1 (1LF instead of 0RB / 1LB).
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 65.8 s with -native-compiler yes, and coqchk re-checks it in 29.6 s (check_kill.txt).

Mechanism

Bounce counter. The tape is 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf, BECv5's w <| R n m. Each bounce applies one map phi to the left word w (read as two interleaved binary numbers, even and odd cells) and moves one 10 from the n-block to the m-block.
Two encodings. At n = 0 the right side eats the low end of w and refills n. The left word is mostly a binary counter that alternates between a standard encoding (BECv5's LC0) and a packed one, where the top two bits share one digit pair.
Where halting is. Because F1 = 1LF skips 1s, an overflow can leave the word dirty for a while. The machine halts only if an overflow finds the lowest 1 of phi(w) on an odd cell with 01 or 11 above it, which can only happen in a dirty word.

How the proof works

Exact rules: the left step phi (as an inductive relation on the pair (e, o), proved against the machine by mutual induction), the right step, and the overflow cases.
One sweep lemma for phi on E/O words gives the increments of both counters and the dirty orbits. From it come eleven macro rules (S0–S3 from a standard state, P0–P4 from a packed one), each running from one clean overflow state (typ, N, m) to the next.
The invariant I: 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 and none meets a halting overflow (coverage), and every rule maps I into itself (closure). The run reaches (std, 1, 1) after 32 steps, and progress_nonhalt_cond with P := I gives nonhalt.

Template and what changed

Adapted from busycoq's verify/BECv5.v, Module TM1 / Module TM2, which differ from this machine only in F1. Kept: the right side R n m and its right step, the standard counter, and the architecture (big-step lemma per rule, start by esx, progress_nonhalt_cond). New: E/O words with phi as the relations PA/PF, the lemma Sweep, the packed counter, eleven macro rules in place of TM1's one and TM2's two, and the invariant I with its coverage and closure arithmetic. The file has 1,217 lines, every lemma top level.

Files

1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.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).