1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB never halts

• Machine: 1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB, a BB(6) holdout (line 301 of the 740-machine list, line 322 of the 778 list). Viewer: https://bbchallenge.org/1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB
• Class: "Structural counter + counter" on the spreadsheet. In mechanism terms: a 3/2 wall conveyor feeding a binary counter.
• Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9), importing only Individual62 and the Coq standard library. Print Assumptions nonhalt is closed (no axioms).
• Check time: it compiles in 315.6 s (about 5 minutes) with -native-compiler yes, and coqchk re-checks it, the computed parts included, in 299.9 s (check_kill.txt).

Mechanism

• Carries. Read the tape as a word of units D0 = 0000, D1 = 1000, P = 11000, S1 = 01000, SP = 011000, W = 111000. Each walk of B to the right and C back from the left edge is one carry, and it acts on the unit word as a recursive increment (Theorem U).
• Walls. SP and W are rotors: a W fires on every second carry, sends three carries up and moves one unit right. The left end runs an exact cycle of 8 left records that adds 8 walls per cycle, and the walls ride a conveyor of P units in birth order.
• Zone. At the right end the walls are absorbed one by one into a binary counter. A flux identity shows that the counter receives D + p(j mod 8) carries per absorption, with p = (47, 48, 48, 47, 48, 47, 48, 47): a closed 2-adic system with no 3/2 arithmetic left. Halting needs a wall's shift to land on another wall, which never happens.

How the proof works

• Units. Unit lemmas by execution, with the arrival on the rest of the tape as a hypothesis, then Theorem U (inc_arr) by induction on the carry relation Inc. A hit has no unit word, so it cannot occur inside any carry that exists.
• Nursery. 8 window runs (window) touch the rest of the tape only through the wall rule. init reaches the first record in 203,465 steps, and nonhalt_of_abs reduces non-halting to the existence of each record step's pops (busycoq's progress_nonhalt_cond).
• Zone. Theorem B (thmB): from each canonical state C(b) the closed system reaches a later one. Small classes, the endgame and the nested range are verified runs of affine families of states (frun_sound, vm_compute); the descent is a symbolic one-step lemma (vs_gen); two short lemmas are by hand; the class recursion EK is well-founded. So the orbit runs forever (zone_forever).
• Conveyor. The word above a position is a relation over the walls (WdR). One carry through it (cascade) turns an SP into a W, fires a W and moves it up, or absorbs the top wall exactly at the closed system's least fixed point. The record invariant RInv is closed under all 8 record steps.

Template

None in busycoq applies: the nearest, verify/CounterCmp_v1.v Module TM1, differs in 11 of 12 transitions. The .v (4,422 lines) follows only the counter pattern of verify/Example.v (unit lemmas with the arrival on the rest as an argument); everything else is new.

Files

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

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).