/machines/1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB/submission/README.md · raw

`1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB` never halts

Machine: 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 437 of the 778-machine list). busycoq's verify/ has no proof of it, under any renaming or mirror.
Class: "Sync bouncer counter" (spreadsheet Results row 918, no notes or claims).
Result: Lemma nonhalt : ~ halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c). Print Assumptions nonhalt is closed (no axioms). It compiles in 10.3 s with -native-compiler yes, and coqchk re-checks it in 3.2 s (check_kill.txt).

Mechanism

A spread binary counter inside a bouncer. Right of the lead (001)^a 00, the tape is a counter in the tokens 00, 01, Z = 100: each digit is b Z 01 Z^g (bit b, gap g), LSB first. Every bounce off the left end adds 1 to the counter and 1 to a.
Overflow and pause. When all bits are 1, the carry runs through a block of gap-1 digits into a finite tail, which answers N or S. On S the counter wraps to 0. On N the left part freezes into a wall of zones, and a long pause eats it two increments at a time, rebuilding every gap and inserting new digits (the run shows gaps 28, 68, 260, 1028, 4097, 7).
The tail is a small counter too. Its 2-bit front unit cycles 10 → 01 → 11 → 00 → 10, and S can happen only at 11. The rest of the tail only decides which answer comes at an 11, and the proof covers both.

How the proof works

Window lemmas (es) and a carry lemma by induction on the carry depth give the increment and the seven pause rules. The pause rules are three generic lemmas over an arbitrary wall.
The overflow's leftward return is a 4-rule token transducer retf, proved sound once (retf_spec). On the tail its answer depends only on where the first 0 bit is: 14 cases by computation, plus an induction for the tail's growing end unit. No 16,384-entry table is needed.
Between normal-mode overflows only four paths occur (S, P1, P1S, P3). An interval invariant INV on (M = 2^N, s = a − c, front unit) is closed under all four, whatever the tail picks at 11 (step). init is one 92,299-step solve_init, and nonhalt is multistep_nonhalt plus progress_nonhalt_cond with P := INV.

Template and what changed

Adapted from busycoq's verify/CounterClass3v2.v, Module TM1 (1RB0LC_0LC1RE_1LD1LC_1LA1RD_---1RF_0RA0RF), a hand-written multi-level counter proof. The transition tables are unrelated, so the file follows TM1's architecture, not its lemmas. - Kept: es window lemmas and shift rules, a carry lemma by induction on the carry depth (TM1's E_stmt/E_all), macro lemmas chained with follow, and multistep_nonhalt. - Changed: TM1 closes by strong induction over a trajectory family (Traj) with progress_nonhalt_simple. Here the macro state is (a, G, r1, tail), closed by the interval invariant with progress_nonhalt_cond. - New: the token layer, the retf transducer for the overflow and the tail, one IR shape KP for normal and pause mode, and the zone-rebuild induction Zones, whose no-overflow condition is stated on the final value only.

The file has 1,327 lines and imports only Individual62 from busycoq.

Files

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