Discord draft: kill announcement for 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---
Not posted. Paste the block below as one message. It is 1,740 characters before the link, under Discord's 2,000-character limit (a link of up to about 260 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---.v in this folder).
2. This message builds on kill #11 (row 1284, 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---), whose draft (discord.md in #11's package) is also unposted. Post #11 first, or both together. #11's draft says its table has two other holdouts; it has three (#11's notes missed this one, which is #11's table started in its state D). Change that paragraph to name all three and point at this message.
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. The question drafted in observe.json (discord_check) was never sent; this message replaces it. Message 2 of our Discord drafts (not posted) does not list this machine. If it is still unsent, update its group 2: #11 and this machine are killed, and hipparcos's machine and 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- are open. hipparcos's Oct 2025 thread (https://discord.com/channels/960643023006490684/1432566675533992019) is the natural place for this message and #11's.
4. The other two starts of the table (hipparcos's 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- and 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---) are not formalized. The message says so.
5. 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.
`1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---` (Skelet 1-like Class 2, sheet row 1277) never halts. Coq proof: <LINK>
It's the table of our row-1284 machine `1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---` mirrored (L<->R), with states renamed A->B, B->C, C->D, D->A (E, F fixed). It starts in A, so it runs 1284's table from `0^inf D> 0^inf`. Same binary counter, now at the left edge: `0^inf <C (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. Each macro step is one carry (every touched digit pays one `10`, a digit flipped to 1 gains a `01`, and a flipped digit with no `10` left merges into the next one). On overflow the digits are re-paired and the counter restarts with one more digit. From blank it reaches `K((1,1,3); 4, 1)` at step 215, which is in 1284's three-phase invariant. In Coq, 1284's tape lemmas are mirrored by hand (20 window lemmas composing into carry, carry with merge and overflow, with the rule statements kept word for word), and 1284's invariant and closure proof (~390 lines) is pasted verbatim. Only the 215-step init and the base case are new. One `TM_from_str`, no Flip/Permute bridge.
Four holdouts share this table. The other two starts, hipparcos's Level 1 machine `1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` and `1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---`, are not formalized.
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.