Discord draft: kill announcement for 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---
Not posted. Paste the block below as one message. It is 1,553 characters before the link, under Discord's 2,000-character limit (a link of up to about 442 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---.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 the two as a pair. #3's draft has a look-alikes paragraph that says this machine and 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC--- (#24) are not covered. Before posting it, change that paragraph to point at this message for this machine. #24 is still not formalized (CHECKPOINT_B).
3. Message 2 of our Discord drafts (duplicate-work question, not posted) lists this machine in group 1. If it is still unsent, drop this machine and #3 from group 1, leaving only #24, or 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 1280 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.
`1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---` (Skelet 1-like Class 2, sheet row 1280) never halts. Coq proof: <LINK>
It's our row-1278 machine `1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---` with states renamed by (A C)(B D), no mirror (the only one of the 720 x 2 maps that fits). So it runs that table from `0^inf C> 0^inf` instead of from A: a different orbit of the same macro map. It's the same binary down-counter on pairs `(10)^p (01)^q s(d)` with re-pairing overflow, with the same 9 macro rules (head `<C` for `<A`) and the same invariant. At every macro step its config is 1278's with the far block 2 longer, under the same rule sequence (checked over 2,209 re-pairings). The +2 enters only additively and never flips a branch, so only the start changes. In Coq it's 1278's file with the state names in the 14 sweep lemmas swapped by the renaming (every `es` re-closes unchanged), the new string, and a new `init`: 79,114 steps (`esx`) to the E-start `K(2; (95,68,0),(34,33,1),(10,15,1),(1,26,1); -)`, which is 1278's base with 26 for 24. The per-step invariant J, `Jstep` and `J_base` are verbatim. Direct proof on the holdout string, no equivalence lemma.
One file, top-level `Lemma nonhalt : ~ halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~70 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.