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

Discord draft: kill announcement for 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF

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

Before pasting:

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

  2. Order. The message builds on the kill of the parent 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (740 line 214), whose own draft (discord.md in its package) is also unposted. Post that one first; this one fits as a reply under it. The parent's last paragraph says lines 418 and 636 are not formalized: change it to say that 418 is (and 636 is not) before posting it.

  3. 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, next to the parent), a list of holdouts that are easy to accelerate, not a claim. Its spreadsheet row gives only the class, and busycoq's verify/ has no proof of it or of any renaming or mirror of its table.

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

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

`1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF` (Bouncer + Chaotic Edge, 740 line 418) never halts. Coq proof: <LINK>

It's `1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF` (line 214, posted above) mirrored and renamed (A->B, B->C, C->A, D/E/F fixed), so it runs that table from its C. From C the table hits K(1953,34,68,45,18) after 4,098,826 direct steps; then the same 20 macro steps as the 214 run apply with the same a,b,c,d and n smaller by 6 (each rule adds a constant to n, and its a,b,c,d updates don't depend on n), ending at Even(12857,212) at step 153,013,640. That's inside the double cycle's domain (n odd, x = 4 mod 8, x >= 52), so 214's proof finishes it, no new invariant. In Coq it's 214's file with its table as `tmP` (es' rules, S_iter, DC untouched), a new opening from `C;; tape0` (6 cconfig_step vm_compute chunks cut at left records), the 20 follows with N 3 smaller, then `Perm (flip tm) tmP phi` + `flip_halts` + `perm_halts` as in Skelet15. Top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9, Individual62 + ES_v3, 407 lines, ~7 s compile (native), Print Assumptions closed, coqchk passes (~44 s). Line 636 (same table from E, unmirrored) reaches Even(13299,220) at step 163,638,058, so it should go the same way; not formalized yet.

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