/machines/1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA/submission/README.md · raw

`1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA` never halts

Machine: 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA, a BB(6) holdout (line 636 of the 740-machine list). Viewer: https://bbchallenge.org/1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA
Class: "Bouncer + Chaotic Edge" on the spreadsheet. It is the table of 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (740 line 214, the parent) with its states renamed by A->E, B->C, C->D, D->F, E->A, F->B (no mirror), started in the parent's state E.
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 7.8 s with -native-compiler yes, and coqchk re-checks it, the computed parts included, in 64.9 s (check_kill.txt).

Mechanism (in the parent's coordinates)

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. The renaming maps the parent's table run from E onto this machine's run, step for step and halt for halt, on the same tape.
Opening. From E the parent's table reaches K(2583,70,76,43,18) after 6,950,830 steps. Then 18 macro steps by the parent's rules, in a chain of their own (S^8 T6 S^7 TE ... S^17 T6), reach Even(13299, 220) at step 163,638,058.
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 E;; tape0 (ten cconfig_step pieces cut at left records), opening with its own 18 follows, and the renaming bridge of verify/Skelet15.v: perm : Perm tm tmP phi with busycoq's perm_halts (no flip, since there is no mirror). The file has 458 lines, every lemma top level.

Files

1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.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).