/machines/1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB/submission/README.md · raw

`1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB` never halts

Machine: 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB, a BB(6) holdout on every holdout list since June 2024 (line 525 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/1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB
Class: "Bell eats counter" (spreadsheet Results row 1044, 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 the Coq standard library. Print Assumptions nonhalt is closed (no axioms). It compiles in 34.7 s with -native-compiler yes, and coqchk re-checks it in 4.6 s (check_kill.txt).

Mechanism

Counter and bell. A bell (10)^q with a wall 00, then a zone holding a binary counter whose bits sit 3 cells apart (a set bit is a 0). Each round trip from the wall moves the wall 2 pairs right and decrements the counter. At 0 an overflow resets the counter according to the zone width modulo 3 (rules O0–O2 of the write-up).
Bites. With q ≤ 2 pairs left, the wall bites the counter's low end. Usually the head sweeps back and the passed part becomes the new bell. A bite on k ≥ 1 low set bits opens k nested levels: the same cycle run on the rest of the zone, shifted right.
Why it never halts. The only halt is a bite at q = 2 on an all-set zone. On cycle starts (n, w, v), d = n - 2^(cap(w)+1) >= 2 and M = n + 2v - 2^(cap+2) != 0 (mod 3) (n + v for w ≡ 1) hold forever: d ≥ 2 is kept, and every cycle negates M.

How the proof works

Rules. Each low-level rule is one es lemma (the round W, PS^(q-3), ZA in three cases by the first zero mod 3). Counter forms on zone r L v give one lemma per round (R1, R2, O0, O1, O2) and per bite (PUSH, B1, B0, B0c).
Levels as frames. The left side is a stack of frames 00 (10)^p 1. A nested bite pushes frames and every ending bite pops one, so the shift law holds by construction.
Bounded induction. No termination of levels is known, so U_all proves by strong induction on the number of steps: a level from J or K' does not halt within N steps if each possible pop satisfying (U1)–(U5) is safe for N - 1. Lemmas K, A1, Z' and P are phase invariants (KI, ZI, Saf) that every round keeps; STK and compose handle the stack.
Start. init runs 327 steps to (6,5,0) by solve_init, and cycles gives nonhalt.

Template and what changed

Adapted from busycoq's verify/BECv5.v, Module TM1: one es lemma per low-level rule and one counter-form lemma per macro rule. Changes: a decrementing counter on a 3-cell lattice whose overflow rule depends on the zone width modulo 3; nested bites, so the left side is a stack of frames; and a bounded induction on steps with phase invariants instead of progress_nonhalt_cond. The file has 1,039 lines, every lemma top level.

Files

1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v (the proof), proof.md (the informal proof; its header maps each section to the .v, and §9 describes the formal proof), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).