Discord draft: kill announcement for 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA

Not posted. Paste the block below as one message. It is 1,629 characters before the link, under Discord's 2,000-character limit (a link of up to about 370 characters fits).

Before pasting: 1. Replace <LINK> with the URL of the .v file (1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v in this folder). 2. This message builds on kill #4 (row 921, 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---), whose draft (discord.md in #4's package) is also unposted. Post #4 first, or post the two as a pair. #4's draft says nothing about twins, so it needs no edit. 3. Both machines are on dyuan01's Oct 1 longitudinal list (this one is line 7) and mxdys's UBRRBA_TODO (line 45). The longitudinal list is a technique filter, not a claim, but re-read that thread and check nobody has said they are working on either machine since. Our Discord exports mention this string only in those two lists; Discord #bb6 was never searched for it. Search before posting. 4. The last sentence of the second paragraph relies on busycoq's Eqv_v2.v TM7 (halts tm c0 <-> halts tm' c0, with tm' = this machine and tm = 1LB0RC_1RC0LB_0RD1RA_0LA1RE_0RA1RF_1RD---, whose mirror is the eqv-class member). The equivalence is busycoq's own Coq lemma; that its tm is the member's mirror was checked by script (check_proof.py §S), not in Coq. Drop the sentence if you would rather not claim the member. 5. The AI line matches the other unposted drafts. Your posted #2 message worded it as "produced with Claude Code (Opus 5.5)" and added your own review note; adjust it to match if you like. 6. No Checkpoint B notes from you were on file when this was packaged. If you add any, fold them into proof.md (the working copy and this folder's copy) first.

`1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA` (Sync bouncer counter, sheet row 915) never halts. Coq proof: <LINK>

It's our row-921 machine `1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---` with states renamed A->E, B->D, C->B, D->C, E->F, F->A, no mirror (the only one of the 720 x 2 maps that fits). So it runs that table from `0^inf F> 0^inf`: a different orbit of the same macro map, not a trajectory twin. Same binary counter (digits 1010/0010, head `<E 001` / `001 F>`), same A/B blocks 00111/10111 and moving front `111`, same rules R1-R5o, and the same two-branch cycle map with the hexagon `8Y>=N, 8Y<=3N, 3Z<=N, 8Z>=-N, 4Y+2Z>=N, 20Y+16Z<=9N`. The cycle lemma never mentions the start, so only the base changes: the run enters the hexagon at `Q(7,65,1,14,4)` after 16,590 steps (921: `Q(7,65,1,16,0)` after 17,215), again on the facet 4Y+2Z = N. In Coq it's 921's file with the state names renamed (every `es` re-closes unchanged), the new string, and a new `init` (one `esx`) and start index; the conversion gadget, `Inv` and `cycle_step` are verbatim. Direct proof on the holdout string. With busycoq's Eqv_v2.v TM7 (which relates it to the mirror of `1RB0LC_1LC0RB_0LD1LA_0RA1LE_0LA1LF_1LD---`) this also settles that eqv-class member.

One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~7 s (native), `Print Assumptions` closed, coqchk passes.

AI disclosure: the informal proof and the Coq formalization were produced with Claude Code (AI-assisted) under my direction, and checked by compiling against unmodified busycoq, with Print Assumptions and coqchk.