Discord draft: kill announcement for 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---
Not posted. Paste the block below as one message. It is 1,752 characters before the link, under Discord's 2,000-character limit (a link of up to about 240 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v in this folder).
2. The duplicate-work question (Message 2 of our Discord drafts) is marked not posted, and no reply is on file. Its group 1 is this machine plus the two look-alikes; its group 2 is #11's table (#11 is killed, its two twins are not). If it is still unsent, cut group 1 down to the two look-alikes, or drop it.
3. Our targeting notes' §5 Q3 is still open: does the numbered Skelet 1-like list behind Sk1Machines.v (ccz181078 = mxdys; Class 1, TM1..TM105) also cover Class 2? Nothing on file says anyone has claimed this machine, but check before posting.
4. The look-alikes 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC--- and 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD--- (pilot targets #24 and #25) are not formalized. The message says only that they look like the same mechanism in simulation: at 1e9 steps their tapes are within 4 cells of ours.
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.
`1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---` (Skelet 1-like Class 2, sheet row 1278) never halts. Coq proof: <LINK>
The tape is a binary down-counter `0^inf <A (10)^h 11001 [p_1,q_1,d_1] .. [p_L,q_L,d_L] T 0^inf` over pairs `[p,q,d] = (10)^p (01)^q s(d)`, `s(1) = 0001`, `s(0) = 0010`, least significant digit next to the head. Each decrement touches the pairs up to the borrow (p+1, q-1, digit flips), and a borrow pair whose q runs out fuses with the next pair. At 0 an End sweep adds a tail `(10)^t 1`; at the next 0 the blocks are re-paired as (q_j, p_{j+1}) with one more pair and h back to 2. Rare double run-outs detour through a tail `(101)^2 (01)^k`. Nine macro rules (each `K -->+ K'`, built from 14 `es` sweeps) and `init` (78,710 steps, `esx`) feed `progress_nonhalt_cond` with a per-step invariant: a ghost phase of the two-cycle period plus, for each pair, bounds on p + Rt and q - Rt (Rt = touches still due before the next re-pairing), parities, and bounds on the two newest pairs and h. Touches leave the projected values fixed, so only merges and re-pairings need arithmetic. Architecture as SBCv6 TM21 (pair list + re-pairing overflow), but one macro step per decrement, since merges are routine here.
`1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---` and `1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---` look like the same mechanism in simulation; this file does not cover them.
One file, top-level `Lemma nonhalt : ~ halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c. 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.