1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF never halts

• Machine: 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF, a BB(6) holdout (line 214 of the 740-machine list). Viewer: https://bbchallenge.org/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF
• Class: "Bouncer + Chaotic Edge" on the spreadsheet. In mechanism terms: a bouncer whose right part is a four-particle system with a closed double-cycle law (the edge is not chaotic).
• Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9), importing Individual62, ES_v3 and the Coq standard library. Print Assumptions nonhalt is closed (no axioms).
• Check time: it compiles in 6.6 s with -native-compiler yes, and coqchk re-checks it, the computed parts included, in 44.9 s (check_kill.txt).

Mechanism

• Bouncer. Every round trip starts at a fixed 43-cell gadget G at the left end. Right of it are five 1-blocks n, a, b, c, d with four short particles between them. The head crosses blocks by C> 11 -> 10 C> going right and 0 10 B> 000 -> 0 B> 000 11 going left, and a particle turns it back; how far it gets depends on the phase (period 12 trips).
• Drift and collisions. Every 12 trips, rule S takes K(n,a,b,c,d) to K(n+48, a-8, b+4, c, d+4). When a is down to 2, 4, 6 or 8, a collision of 135 to 147 trips (TO, TE, T6, T8) rebuilds the pattern.
• Double cycle. On Even(n,x) = K(n, x, (x+76)/2, 35, 18), the chain S^((x-4)/8), TE, S^((x-52)/8), TO gives Even(n+12x+808, x+32) for n odd, x = 4 mod 8, x >= 52, and these conditions are preserved. The blank tape reaches Even(12863, 212) at step 153,126,993.

How the proof works

• Rules. S, TE, TO, T6 and T8 are one es' each, for their whole domains, on half-length parameters Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d). es' finds the shift rules itself; S needs no case split.
• Cycle. S_iter repeats S by induction, and DC : Ev N X -->+ Ev (48*X+716+N) (4+X) is four follows.
• Start and end. init is the 4,097,897-step direct run on busycoq's list configurations, in six vm_compute pieces cut at left records. opening follows 20 macro steps to Ev 6431 20 = Even(12863, 212). nonhalt is multistep_nonhalt plus progress_nonhalt_simple on (N, X), with no invariant.

Template and what changed

Adapted from busycoq's verify/TranslatedBellv5.v, Module TM1: block macro rules by es', repeated by induction and chained with follow. Changes: fixed five-block configurations instead of TM1's lists, and no invariant, so the proof ends with progress_nonhalt_simple as in verify/Bouncer_v2.v Module TM1. The long opening uses nested step counters as in verify/Bouncer_v3.v's multistep_c', cut into six pieces so that coqchk can re-check each computation. The file has 361 lines, every lemma top level.

Siblings

The same table started in C (mirrored) and in E is lines 418 and 636 of the 740 list. By direct simulation they reach Even(12857, 212) and Even(13299, 220), so the double cycle covers them after their own openings. They are not formalized here.

Files

1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.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).