Discord draft: kill announcement for 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC

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

Before pasting: 1. Replace <LINK> with the URL of the .v file (1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v in this folder). 2. Duplicate work: sheet row 1053 had no status, notes, links or claims when this was packaged, the string is not in our Discord exports, and busycoq's verify/ at 0940bb9c has no proof of it under any renaming or mirror. Search Discord #bb6 for the string before posting, in case someone has claimed it since. 3. Upstream: PR #15 (the #3 family) is still open with no response, and the other claimed kills wait for it. This one can wait in the same queue; the draft does not mention a PR. 4. Sibling, not mentioned in the message: 1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC (C1 = 1RA, our pool #10) has the same hub and is still open (740 list line 611; our status CRYPTID_CANDIDATE). With tm10 (C1 = 1RB, proved in FractalBEC.v), these are three tables that differ only in C1. Add a line about it only if you want to point people at it. 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 copies of proof.md first. 6. Numbers: the informal proof's own threshold is N* = 14,796 with a 591-epoch finite part; the .v uses a simpler invariant with threshold 17,705 and runs 691 epochs. The public proof.md keeps the write-up's mathematics and explains the .v's variant in its header and §8.3. The message quotes the .v's numbers. 7. 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. 8. The disclosure line uses the same wording as the README and the other drafts ("produced with the help of Claude (Anthropic)").

`1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC` (Bell eats counter, sheet row 1053) never halts. Coq proof: <LINK>

Its table is FractalBEC's tm10 mirrored except C1 (0RE here, 1RB there). The bounce is tm10's RInc: hub `(110)^a 0 (011)^b C> X`, each bounce moves the marker one block and adds 1 to a counter X of 3-cell blocks `d01 (001)^e` with `000` separators and a 4-stage tail. The eat is different: at b = 1 only the low digit goes. An a-block gives new budget, a b-block sweeps (110)^a into a left record, and the next epoch restarts with budget N = k+1 and a residue that isn't a clean counter. Digesting that residue is recursive. At a b-block one bounce builds a sub-hub behind a 1 and runs a whole sub-epoch on the rest of the word (it never reads its context until its own left record), and the next digestion level runs nested inside the block it leaves. Halting needs an eat before digestion ends; digestion costs ~2^(k/2) bounces against N >~ 2^(k+3). In Coq: `LP`/`Phi` mutually inductive (D6 is an LP constructor with a Phi premise), potentials over counter positions that bound the created positions, the cost and the merged exponents, and an epoch invariant (two weighted exponent masses) closed for N >= 17,705. The first 691 epochs (to N = 17,713) run by vm_compute on a fuel model proved sound.

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

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