Discord draft: kill announcement for 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---

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

Before pasting: 1. Replace <LINK> with the URL of the .v file (1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v in this folder). 2. Post it with or right after the announcement for row 1015 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF, since this message leans on that proof. That draft's third paragraph says row 1038 is "Not formalized yet": cut that paragraph, or change its last sentence to "Formalized too, see the next message." 3. Duplicate work: sheet Results row 1038 had only its class (no status, notes, sources or done-by) when this was packaged, the string is not in our Discord exports, and busycoq's verify/ has no proof of it (Eqv_v3.v TM518 only relates it to another machine). Search Discord #bb6 for the string before posting, in case someone has claimed it since. 4. Upstream: the earlier PRs are still open. This one can wait in the same queue as row 1015's; the draft does not mention a PR. 5. 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 both proof.md copies first. 6. check_kill.txt is the verifier's verbatim output, so it contains absolute local paths (the home directory and the framework checkout), like the other packages' copies. Leave it out if the folder is shared publicly. 7. The disclosure line uses the same wording as the README and the other drafts ("produced with the help of Claude (Anthropic)").

`1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---` (Bell eats counter, sheet row 1038) never halts. Coq proof: <LINK>

Mirrored and renamed (A->F, B->A, C->B, D->C, E->D, F->E) it's `1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC` started in F: BECv5's TM1/TM2 with F1 = 1RC, or row 1015 `1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF` with one cell changed. F is only entered by A1, which leaves a 1 on F's right, so F1 = 1RC is always followed by C1 A1, and the three steps do exactly what F1 = 1LF does in one. So it runs row 1015's counter: tape `0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf`, each bounce applies phi to w (two interleaved binary numbers, even/odd cells) and moves one 10 from n to m, overflows eat the low end of w, and the counter alternates between a standard and a packed encoding. Row 1015's 11 macro rules and its parity-split linear invariant I carry over unchanged; only the left-step lemmas get an explicit 1 on the right, plus a 73-step start from F to (std,2,2). Halting is ruled out by inequalities, not residues, so nothing cryptid-like.

One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. The mirror step is `flip_halts` + `perm_halts` with `Perm (flip tm) tmP f349`, so it's a direct proof that doesn't go through Eqv_v3 TM518. Compiles in ~64 s (native), `Print Assumptions` closed, coqchk passes (~27 s).

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