Discord draft: kill announcement for 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---
Not posted. Paste the block below as one message. It is 1,472 characters before the link, under Discord's 2,000-character limit (a link of up to about 520 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v in this folder).
2. This message builds on the row-1284 proof (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---), whose draft is also unposted. Post row 1284 first, or the whole family together (row 1284, row 1277 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, row 1282 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---, then this one). The drafts for rows 1277 and 1282 still say this machine is not formalized, and the row-1284 draft says only that it reaches the same invariant in simulation; update those lines before posting them. The sentence "all four holdouts with this table have Coq proofs" is true only once all four are posted.
3. Where: hipparcos's thread (https://discord.com/channels/960643023006490684/1432566675533992019) is the natural place; consider @-mentioning him. The thread's opening posts are about this string, 1RB0RB_..., not row 1277's 1RB0RE_.... They are an analysis (block rules, stride acceleration, hypotheses, "I don't have enough analysis to prove that yet"), not a proof. Only those opening posts were available; read the rest of the thread first, and if he finished a proof there, reword the existing-work sentence to credit it.
4. No notes of yours on this machine's informal proof were on file when this was packaged. If you add any, fold them into proof.md first.
`1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` (Skelet 1-like Class 2, sheet row 1276) never halts. Coq proof: <LINK>
It's the row-1284 machine `1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---` with states renamed A->E, B->A, C->B, D->C, E->D (F fixed), no mirror, so it runs 1284's table from `0^inf B> 0^inf`. Same binary counter at the right edge, `0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf` with digits `(10)^u 00 (01)^v` = 0 and `(10)^u (01)^v` = 1, same carry and re-pairing overflow rules (head `A>` for `B>`), same three-phase invariant. Only the orbit differs: from blank it reaches `K((1,1,10); 8, 1)` at step 732, which is in the invariant (class A). In Coq it's 1284's file with the state names renamed (every `es`/`follow` proof re-closes unchanged), the new string, and a new 732-step init and base case. Direct proof on the holdout string, no equivalence lemma.
There may be existing work on this machine by hipparcos (marked done on the community sheet, not yet in busycoq): his Oct 2025 thread has block rules, a stride acceleration and conjectures for it. This proof comes from 1284's proof, not from that thread. With this, all four holdouts with this table have Coq proofs.
One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~9 s, `Print Assumptions` closed, coqchk passes.
AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).