Discord draft: kill announcement for 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---
Not posted. Paste the block below as one message. It is 1,641 characters before the link, under Discord's 2,000-character limit (a link of up to about 359 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---.v in this folder).
2. This message builds on kill #3 (row 1278, 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---), whose draft (discord.md in #3's package) is also unposted. Post #3 first, or post #3, #25 and this one together. #3's draft has a look-alikes paragraph that says this machine and #25 are not covered; both are now killed, so point that paragraph at their messages instead. #25's draft (discord.md in #25's package, before-pasting item 2) says #24 is still not formalized; that note is out of date.
3. Message 2 of our Discord drafts (duplicate-work question, not posted) has group 1 = #3, this machine and #25. All three are now killed. 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 1289 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. If you add any, fold them into proof.md (the working copy and this folder's copy) first.
`1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---` (Skelet 1-like Class 2, sheet row 1289) never halts. Coq proof: <LINK>
It's our row-1278 machine `1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---` mirrored (L<->R), with states renamed A->D, B->A, C->B, D->C (E, F fixed): the only one of the 720 x 2 maps that fits. It starts in A, so it runs 1278's table from `0^inf D> 0^inf`: a different orbit of the same binary down-counter on pairs `(10)^p (01)^q s(d)` with re-pairing overflow. It enters 1278's family at step 1,021 and reaches the E-start `K(2; (95,68,0),(34,33,1),(10,15,1),(1,25,1); -)` at step 78,911. That's 1278's base with 25 for 24, and 1278's per-step invariant J holds there with the same constants. In Coq, 1278's file is kept verbatim as `tm3` (sweeps, 9 macro rules, J, `Jstep`, `J_base`), with a new `init` from `D;; tape0` (busycoq's `solve_init` started in D, since `esx` from a non-c0 start falls back to symbolic `es`), giving `~ halts tm3 (D;; tape0)`. The mirror and renaming are busycoq's own `flip_halts` (Flip.v) and `perm_halts` (Permute.v), with `Perm (flip tm) tm3 phi` checked entry by entry, so no new induction. Same family as `1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---` (row 1280, renamed with no mirror, posted separately).
One file, top-level `Lemma nonhalt : ~ halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~40 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.