Discord draft: kill announcement for 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---
Not posted. Paste the block below as one message. It is 1,529 characters before the link, under Discord's 2,000-character limit (a link of up to about 470 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---.v in this folder).
2. This message builds on kill #3 (row 1278, 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---), and it mentions the row-1280 twin (#25). Their drafts, and #24's (row 1289), are also unposted. Post #3 first, then the twins, or post all four as one group. #3's look-alikes paragraph and #25's "#24 not formalized" note are stale. Neither names this machine, and the family sweep found it after they were written.
3. Message 2 of our Discord drafts (the duplicate-work question, not posted): every machine in its group 1 is now killed, and so is this fourth start. If it is still unsent, drop group 1.
4. Our targeting notes' §5 Q3 is still open: does the numbered Skelet 1-like list behind Sk1Machines.v (ccz181078 = mxdys) also cover Class 2? Sheet row 1288 has no notes or claims, and nothing in our Discord exports mentions this string, but Discord #bb6 was never searched for it. Search for it before posting.
5. No Checkpoint B notes from you were on file when this was packaged. proof.md §7 asks two reviewer questions: is the delta form acceptable, and is the 3-pair base at the invariant's lower edge (L* = 3) fine as it is? If you add notes, fold them into proof.md (the working copy and this folder's copy) first.
6. The disclosure line uses the reworded form from the README ("with the help of Claude (Anthropic)"). The other unposted drafts still say "with Claude Code (AI-assisted) under my direction", and your posted #2 message said "produced with Claude Code (Opus 5.5)". Pick one wording and use it for the whole batch.
`1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---` (Skelet 1-like Class 2, sheet row 1288) never halts. Coq proof: <LINK>
It's our row-1278 machine `1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---` with states renamed A->D, B->A, C->B, D->C, no mirror (the only one of the 720 x 2 maps that fits). So it runs 1278's table from `0^inf B> 0^inf`: the same binary down-counter on pairs `(10)^p (01)^q s(d)` with re-pairing overflow, the same 9 macro rules (head `<D` for `<A`) and the same per-step invariant J. Unlike the row-1280 twin, this orbit isn't a shifted copy of 1278's: its base has 3 pairs where 1278's has 4, and the first 120 E-starts of the two orbits share none. In Coq it's 1278's file with the state names in the 14 sweep lemmas renamed (every `es` re-closes unchanged), the new string, and a new `init`: 38,732 steps (`esx`) to the E-start `K(2; (47,32,0),(40,33,1),(13,34,1); -)`. That base sits at the invariant's lower edge (L* = 3, one tight clause 48 >= 48), and J, `Jstep` and `J_base` are verbatim. Direct proof on the holdout string, no equivalence lemma. This is the last of the four holdouts with that table (rows 1278, 1280, 1288, 1289).
One file, top-level `Lemma nonhalt : ~ halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~55 s (native), `Print Assumptions` closed, coqchk passes.
AI disclosure: the informal proof and the Coq formalization were produced with the help of Claude (Anthropic), and checked by compiling against unmodified busycoq, with Print Assumptions and coqchk.