Discord draft: kill announcement for 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB
Not posted. Paste the block below as one message. It is 1,375 characters before the link, under Discord's 2,000-character limit (a link of up to about 625 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v in this folder).
2. Order: the message builds on the row-1053 kill (1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC), whose own draft (discord.md in its package) is also unposted. Post 1053 first, or the family together.
3. Family: all three holdouts with this table are now killed: row 1053 (the parent), this machine (the parent renamed, started in its B) and row 1022 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA (the parent mirrored and renamed, started in its E; its draft is also unposted, and its before-pasting note 3 still calls this machine not killed yet; its message does not mention this machine). Posting the three as one family reads best. If you post them together, this sentence fits at the end of the message's second paragraph: "With row 1022 (1053 mirrored, posted alongside) that's all three holdouts with this table."
4. Duplicate work: sheet row 1046 had no status, notes, sources or done-by when this was packaged, the string is not in our Discord exports, and busycoq's verify/ has no proof of it, byte-exact, renamed or mirrored. Search Discord #bb6 for the string before posting, in case someone has claimed it since.
5. Upstream: PR #15 is still open, and the other claimed kills wait behind it. This one can wait in the same queue; the draft does not mention a PR.
6. No notes from you on the card or the informal proof (Checkpoints A and B) were on file when this was packaged. If you add any, fold them into proof.md (both copies) first. Checkpoint B question 2 asked whether to mention the orbit merge at epoch 795; the message and the public write-up mention it as a remark (the proof does not use it). Cut it if you prefer.
7. Numbers: the parent write-up's own threshold is N* = 14,796 (this orbit reaches it at epoch 591); the .v uses the parent .v's invariant (threshold 17,705) and runs 691 epochs. The message quotes the .v's numbers.
8. check_kill.txt is the verifier's verbatim output, so it contains absolute local paths (the home directory and the framework checkout), like the other packages' copies. Leave it out if the folder is shared publicly.
9. The disclosure line uses the same wording as the README and the other drafts ("produced with the help of Claude (Anthropic)").
`1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB` (Bell eats counter, sheet row 1046) never halts. Coq proof: <LINK>
It's our row-1053 machine `1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC` with states renamed A->E, B->A, C->B, D->C, E->D (no mirror). It starts in A, so it runs 1053's table from `0^inf B> 0^inf`: a different orbit of the same epoch map (hub `(110)^a 0 (011)^b B> X`, a counter eaten one digit at a time, residues digested recursively, one bounce can run a whole sub-epoch). The blank tape reaches the hub K(1,3,t1) at step 55. Everything in 1053's proof is about the table, one epoch or the induction step, so it carries over unchanged. Only the finite part is new, because this orbit first meets 1053's at epoch 795 (N = 20,922): 691 epochs of the fuel model by vm_compute, from K(1,3,t1) to N = 17,712, where 1053's epoch invariant (Inv 11) holds, and inv_step does the rest. In Coq it's 1053's file with the renaming applied to the 59 state names in statements (no proof script touched), a 55-step solve_init and the new finite part: one TM literal, no Perm bridge.
One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~14 s (native), `Print Assumptions` closed, coqchk passes (~64 s).
AI disclosure: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).