/machines/1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF/submission/README.md · raw

`1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF` never halts

Machine: 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF, a BB(6) holdout (line 418 of the 740-machine list). Viewer: https://bbchallenge.org/1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF
Class: "Bouncer + Chaotic Edge" on the spreadsheet. It is the table of 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (740 line 214, the parent), mirrored (L <-> R) and renamed by A->B, B->C, C->A (D, E, F fixed), started in the parent's state C.
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.4 s (check_kill.txt).

Mechanism (in the parent's orientation)

Bouncer. Every round trip starts at a fixed 43-cell gadget G. Beyond it are five 1-blocks n, a, b, c, d with four short particles between them, and a particle turns the head back.
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 (TO, TE, T6, T8) rebuilds the pattern.
Double cycle. On Even(n,x) = K(n, x, (x+76)/2, 35, 18), 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.

How the proof works

Relation. Mirror plus renaming maps the parent's table run from C onto this machine's run, step for step and halt for halt.
Opening. From C the parent's table reaches K(1953,34,68,45,18) after 4,098,826 steps. The parent's own 20 macro steps then apply with the same a, b, c, d and n smaller by 6, reaching Even(12857, 212) at step 153,013,640.
End. From there the parent's double cycle runs forever. No new invariant is needed.

Template and what changed

The template is the parent's kill file (adapted from busycoq's verify/TranslatedBellv5.v, Module TM1, ending with progress_nonhalt_simple as in verify/Bouncer_v2.v). Its macro rules, S_iter and DC are kept word for word on the parent's table, renamed tmP. New here: the opening init from C;; tape0 (six cconfig_step pieces cut at left records), opening with new arguments, and the bridge of verify/Skelet15.v: perm : Perm (flip tm) tmP phi with busycoq's flip_halts and perm_halts. The file has 407 lines, every lemma top level.

Files

1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v (the proof), proof.md (the informal proof, as a delta from the parent; its header maps each section to the .v), parent-proof.md (the parent's write-up), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).