/machines/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF/submission/discord.md · raw

Discord draft: kill announcement for 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF

Not posted. Paste the block below as one message. It is 1,634 characters without the link, so a link of up to 366 characters keeps it under Discord's 2,000-character limit.

Before pasting:

  1. Link. Replace <LINK> with the URL of the .v file (1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v in this folder).

  2. Search. Search #bb6 for the string first, in case someone has claimed it since. In the Discord exports on file it appears only on mxdys's UBRRBA to-do list (2026-08-24), a list of holdouts that are easy to accelerate, not a claim; a courtesy mention of mxdys may fit. Its spreadsheet row gives only the class, and busycoq's verify/ has no proof of it or of its two siblings.

  3. Siblings. The last paragraph names the two other entries of the 740 list with the same table (lines 418 and 636). Their own openings and the renaming (and mirror, for 418) are not formalized, so the message says so. If they are killed before you post, change that sentence.

  4. No notes on file. No notes from you on the card or the informal proof were on file when this was packaged. If you add any, fold them into proof.md first.

  5. check_kill.txt. It is the verifier's output from a fresh run, with local paths replaced by placeholders.

  6. Disclosure. The last line uses the same wording as the README and the other drafts.

`1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF` (Bouncer + Chaotic Edge, 740 line 214) never halts. Coq proof: <LINK>

Bouncer: every trip starts at a fixed 43-cell gadget G on the left; right of it are five 1-blocks n,a,b,c,d with four particles between them. Shift rules `C> 11 -> 10 C>` (right) and `0 10 B> 000 -> 0 B> 000 11` (left). The edge isn't chaotic: every 12 trips K(n,a,b,c,d) -> K(n+48,a-8,b+4,c,d+4), and when a gets down to 2/4/6/8 a collision of 135-147 trips rebuilds the pattern. On Even(n,x) = K(n,x,(x+76)/2,35,18) two of the collisions alternate: 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, which is preserved, so no invariant is needed. From blank: 4,097,897 direct steps + 20 macro steps to Even(12863,212) at step 153,126,993.

Each macro rule (S and four collisions, up to ~600k concrete steps) is one `es'` on half-length params, S iterated by induction, the double cycle by follow, then progress_nonhalt_simple on (N,X). Architecture of TranslatedBellv5's TM1 (es' block rules + ind/follow); the opening is 6 cconfig_step vm_compute chunks cut at left records so coqchk can recheck each. Top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9, Individual62 + ES_v3, 361 lines, ~7 s compile (native), Print Assumptions closed, coqchk passes (~45 s).

Same table from C (mirrored) and from E = 740 lines 418 and 636; they reach Even(12857,212) and Even(13299,220), so the same cycle covers them after their own openings (not formalized yet).

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