Discord draft: kill announcement for 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC
Not posted. Paste the block below as one message. It is 1,663 characters before the link, under Discord's 2,000-character limit (a link of up to about 337 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v in this folder).
2. Duplicate work: sheet Results row 1013 had only its class (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. Search Discord #bb6 for the string before posting, in case someone has claimed it since.
3. Upstream: the earlier PRs are still open. This one can wait in the same queue; the draft does not mention a PR.
4. No Checkpoint notes from you on the card or the informal proof were on file when this was packaged. If you add any, fold them into both proof.md copies first.
5. 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.
6. The disclosure line uses the same wording as the README and the write-up.
`1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC` (Bell eats counter, sheet row 1013) never halts. Coq proof: <LINK>
Tape is a `(10)^p` budget word with a one-cell defect, then a binary counter `BinInc [1;1] N` on the right. Each count is a round trip into the word: N+1, and every second count moves the defect 2 pairs away from the counter. Once the defect leaves the word, the trip hits the blank edge and a C/F sweep shifts the whole word one cell, eating low digits: N odd -> (N+1)/2, 0 mod 4 -> N/4, 2 mod 8 -> (N+6)/8. For N = 6 mod 8 the eat leaves a misaligned fixed-width counter `D_k(x) 0 C(y)` that counts up, gets eaten once more, and overflows into a second defect that walks back and cancels the first. Five macro rules (one per residue class) take E(p,N) to a later eat, and `1 <= N <= 2p` is closed under all of them; it also gives the one precondition (2^t <= p+7 for N = (2m+1)2^(t+3)-2). The residue sequence looks pseudo-random, but every branch keeps the invariant and none reaches F0, so nothing has to be predicted: not cryptid-like.
Architecture of BECv5's TM1 (BinInc counter, defect budget, eat, progress_nonhalt_cond with a linear invariant), but with the counter on the right (RBinInc_spec), the defect walking away from it and the eat at the far blank edge. One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9, imports Individual62 + BinaryCounter_v2. 530 lines, compiles in ~3 s (native), `Print Assumptions` closed, coqchk passes (~1 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).