/machines/1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB/submission/discord.md · raw

Discord draft: kill announcement for 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB

Not posted. Paste the block below as one message. It is 1,778 characters without the link, so a link of up to 222 characters keeps it under Discord's 2,000-character limit.

Before pasting:

  1. Link. Replace <LINK> with the URL of the .v file (1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v in this folder).

  2. Search. Search #bb6 for the string first, in case someone has claimed it since. When this was packaged, its spreadsheet row (Results row 1044) had only the class, with no status, notes or done-by; the string was not in the Discord exports on file; and busycoq's verify/ had no proof of it.

  3. No siblings. No other holdout has this table up to renaming and mirror, and its starts in B to F halt within 44 steps, so the message names no siblings.

  4. No notes on file. No notes from you on the card or the informal proof were on file when this was packaged. If you add any, fold them into proof.md first.

  5. check_kill.txt. It is the verifier's output from a fresh run, with local paths replaced by placeholders.

  6. Upstream. The draft does not mention a PR; this kill can go into the next batch.

  7. Disclosure. The last line uses the same wording as the README and the write-up.

`1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB` (Bell eats counter, sheet row 1044) never halts. Coq proof: <LINK>

Tape: a bell `(10)^q` with a wall `00`, then a zone holding a binary counter whose bits sit 3 cells apart (set bit = 0, LSB first). Each round trip from the wall moves the wall 2 pairs right and decrements the counter; at 0 it overflows, and the reset depends on the zone width mod 3 (rules O0–O2). With q <= 2 left the wall bites the counter's low end, and usually the head sweeps back and the passed part becomes the new bell. A bite on k >= 1 low set bits opens k nested levels (the same cycle on the rest of the zone, shifted right); that's where the chaotic-looking transients come from. The only halt is a bite at q = 2 on an all-set zone. On cycle starts (n,w,v), d = n - 2^(cap(w)+1) >= 2 and M = n + 2v - 2^(cap+2) != 0 mod 3 hold forever (every cycle negates M), and inner levels start in a parity class that can't reach the halting overflow. Not cryptid-like.

Formal side: one `es` lemma per low-level rule, a counter-form lemma per round/bite, and the left side as a stack of frames (push on a nested bite, pop on an ending bite, so the shift law comes for free). No termination of levels is known, so `nonhalt` is a bounded induction on the number of steps (U_all, CPS style), with the K / Z' / sign bounds as phase invariants that every round keeps. BECv5 TM1's one-lemma-per-rule layout. One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9, Individual62 + stdlib only, 1039 lines, ~35 s compile (native), Print Assumptions closed, coqchk passes (~5 s).

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic); corrections from an independent audit by GPT-6 Astra (OpenAI).