Discord draft: kill announcement for 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA

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

Before pasting:

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

2. Order. The message builds on the kills of the parent 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (740 line 214) and its mirrored sibling 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF (740 line 418), whose own drafts (discord.md in their packages) are also unposted. Post those two first; this one fits as a reply under them.

3. Fix the two earlier drafts. The parent's last paragraph says lines 418 and 636 are not formalized, and the 418 draft ends with "Line 636 ... should go the same way; not formalized yet." Change both to say that 636 is formalized too, or drop those sentences, before posting them.

4. 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 (posted 24 August 2026, next to the parent and the 418 sibling), 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.

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

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

`1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA` (Bouncer + Chaotic Edge, 740 line 636) never halts. Coq proof: <LINK>

It's `1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF` (line 214, posted above) with its states renamed (A->E, B->C, C->D, D->F, E->A, F->B, no mirror), so it runs that table from its E. From E the table hits K(2583,70,76,43,18) after 6,950,830 direct steps; then 18 macro steps by 214's rules, in an order of their own (S^8 T6 S^7 TE S^6 T6 S^13 T8 S^10 TO S^18 T8 S^14 T6 S^23 TE S^17 T6, no new rule), end at Even(13299,220) at step 163,638,058. 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 `E;; tape0` (10 cconfig_step vm_compute chunks cut at left records), the 18 follows, then `Perm tm tmP phi` + `perm_halts` as in Skelet15 (no flip needed). Top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9, Individual62 + ES_v3, 458 lines, ~8 s compile (native), Print Assumptions closed, coqchk passes (~65 s). With 418 (also posted above) that covers all three 740 entries of this table.

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