Discord draft: kill announcement for 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA

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

Before pasting: 1. Replace <LINK> with the URL of the .v file (1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA.v in this folder). 2. Order: the message builds on the row-1053 kill (1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC), whose own draft (discord.md in its package) is also unposted. Post 1053 first, or both together. 3. Family: the same table is on the holdout list a third time, 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB (1053's table renamed with no mirror, started in 1053's state B). It is not killed yet and the message does not mention it. If it is killed soon, posting the three starts together as one family reads best. 4. Duplicate work: sheet row 1022 had no status, notes, sources or done-by when this was packaged, and busycoq's verify/ at 0940bb9c has no proof of the string, byte-exact, renamed or mirrored. Search Discord #bb6 for the string before posting, in case someone has claimed it since. 5. Upstream: PR #15 is still open with no response, and the other claimed kills wait behind it. This one can wait in the same queue; the draft does not mention a PR. 6. No notes from you on the card or the informal proof (Checkpoints A and B) were on file when this was packaged. If you add any, fold them into both copies of proof.md first. 7. Numbers: the write-up's own threshold is the parent's N* = 14,796, with a 587-epoch finite part; the .v uses the parent .v's invariant (threshold 17,705) and runs 687 epochs. The message quotes the .v's numbers. 8. 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. 9. The disclosure line uses the same wording as the README and the other drafts ("produced with the help of Claude (Anthropic)").

`1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA` (Bell eats counter, sheet row 1022) never halts. Coq proof: <LINK>

It's our row-1053 machine `1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC` mirrored (L<->R), with states renamed A->E, B->A, C->B, D->F, E->C, F->D: the only one of the 720 x 2 maps that fits. It starts in A, so it runs 1053's table from `0^inf E> 0^inf`, a different orbit of the same epoch map (hub `(110)^a 0 (011)^b C> X`, a counter eaten one digit at a time, residues digested recursively). Its first four left records are outside 1053's invariant family. The fifth, L(16, 0001) at step 1,059, restarts into the hub K(1,17,t1) at step 1,114, which is 1053's base case (kappa = 0, special residue) with t1 for t2. Everything after that is about the table or one epoch, so it carries over, except the finite part: this orbit doesn't meet 1053's below N = 20,000, so it gets its own 687 epochs of the fuel model by vm_compute, to N = 17,724, where 1053's epoch invariant (Inv 10) holds. In Coq, 1053's file is kept verbatim as `tm30` with a new `init7` (busycoq's solve_init started in E) and `fin7`/`inv7`, giving `~ halts tm30 (E;; tape0)`. The mirror and renaming are busycoq's own `flip_halts` (Flip.v) and `perm_halts` (Permute.v), with `Perm (flip tm) tm30 phi` checked by computation, so no new induction.

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

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