Discord draft: kill announcement for 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF

Not posted. Paste the block below as one message. It is 1,538 characters before the link, under Discord's 2,000-character limit (a link of up to about 460 characters fits).

Before pasting: 1. Replace <LINK> with the URL of the .v file (1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v in this folder). 2. Duplicate work: sheet Results row 1015 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 (Eqv_v3.v TM493 only relates its mirror to another machine). Search Discord #bb6 for the string before posting, in case someone has claimed it since. 3. The third paragraph is about row 1038 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (also "Bell eats counter", no notes), which this proof covers mathematically but not formally (proof.md §7.3). Its sheet row and our Discord exports had no claim on it either. Cut the paragraph if you would rather not announce it before it is formalized. 4. 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. 5. 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 both proof.md copies first. 6. 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. 7. The disclosure line uses the same wording as the README and the other drafts ("produced with the help of Claude (Anthropic)").

`1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF` (Bell eats counter, sheet row 1015) never halts. Coq proof: <LINK>

It's BECv5's TM1/TM2 with F1 = 1LF. Tape `0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf` (BECv5's `w <| R n m`): each bounce applies a map phi to w (read as two interleaved binary numbers, even/odd cells) and moves one 10 from n to m; at n = 0 the right side eats the low end of w. Because F1 = 1LF skips 1s, the counter alternates between the standard encoding and a packed one (top two bits share a digit pair), and an overflow can leave the word dirty for a while. It halts only if an overflow finds the lowest 1 of phi(w) on an odd cell with 01/11 above it. One sweep lemma for phi gives 11 macro rules between clean overflow states (typ, N, m), and the invariant I (1 <= m <= N plus linear bounds on N vs m, picked by the parities of N and m) keeps every overflow off those points: under I exactly one rule applies, none halts, and each preserves I. Halting is ruled out by inequalities, not residues, so nothing cryptid-like.

The same math covers row 1038 `1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---`: Eqv_v3 TM518's tm is this table mirrored and renamed, started in F, which enters the same rules at (std,2,2). Not formalized yet.

One file, top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~66 s (native), `Print Assumptions` closed, coqchk passes (~30 s).

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).