Discord draft: kill announcement for 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---
Not posted. Paste the block below as one message. It is 1,596 characters before the link, under Discord's 2,000-character limit (a link of up to about 404 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---.v in this folder).
2. This message builds on kill #33 (row 1277, 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---) and kill #11 (row 1284, 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---), whose drafts (discord.md in their packages) are also unposted. Post #11, then #33, then this one, or all three together. Both earlier drafts say this machine is not formalized. Before posting them, cut that from their twins paragraphs (#33's names this machine and hipparcos's; #11's names this machine as "the mirror, C-start" and misses #33) and point at this message. hipparcos's machine is still open.
3. Duplicate work: the sheet has no claim on this string and it is not on the lists in our Discord exports, but Discord #bb6 was never searched for it, so search first. Message 2 of our Discord drafts (not posted) names this machine in group 2. If it is still unsent, drop this machine, #11 and #33 from group 2, leaving only hipparcos's machine, or drop group 2. hipparcos's Oct 2025 thread (https://discord.com/channels/960643023006490684/1432566675533992019) is the natural place for this message, #11's and #33's.
4. No Checkpoint A or 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.
`1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---` (Skelet 1-like Class 2, sheet row 1282) never halts. Coq proof: <LINK>
It's our row-1277 machine `1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---` with states renamed A->B, B->C, C->D, D->A (E, F fixed), no mirror (the only one of the 720 x 2 maps that fits). So it runs 1277's table from `0^inf D> 0^inf`; equivalently, row 1284's table mirrored, started in C. Same binary counter at the left edge, `0^inf <D (01)^b 000 (01)^a d_m .. d_1 1001 0^inf` with digits `(10)^v 00 (01)^u` = 0 and `(10)^v (01)^u` = 1, same carry and re-pairing overflow rules (head `<D` for `<C`), same three-phase invariant. Only the orbit differs: from blank it reaches `K((1,1,9); 8, 1)` at step 687, which is in the invariant (class A). In Coq it's 1277's file with the state names renamed (every `es`/`follow` proof re-closes unchanged), the new string, and a new 687-step init and base case. Every proof script is verbatim. Direct proof on the holdout string, no equivalence lemma.
That's three of the four holdouts with this table. The fourth, hipparcos's Level 1 machine `1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---`, is not formalized (in simulation it reaches the same invariant at step 732).
One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~10 s, `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.