Discord draft: kill announcement for 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB
Not posted. Paste the block below as one message. It is 1,510 characters before the link, under Discord's 2,000-character limit (a link of up to about 490 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v in this folder).
2. Duplicate work: this string is on mxdys's UBRRBA_TODO list (Aug 2026). Sheet row 918 had no status, notes, links or claims when this was packaged, 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. If mxdys is working through that list, consider replying in that thread.
3. No notes from you on the informal proof were on file when this was packaged. If you add any, fold them into both copies of proof.md first.
4. The disclosure line uses the same wording as the README and the other drafts ("produced with the help of Claude (Anthropic)").
`1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB` (Sync bouncer counter, sheet row 918) never halts. Coq proof: <LINK>
It's a spread binary counter inside a bouncer. Right of the lead `(001)^a 00` the tape is digits `b 100 01 (100)^g` at unary gaps, LSB first, and each bounce adds 1 to the counter and to a. On overflow the carry runs through a block of gap-1 digits into a finite tail that answers N or S. On S the counter just wraps. On N the left part freezes into a wall of zones that a long pause eats two +1s at a time, rebuilding every gap and inserting new digits (the 28, 68, 260, 1028, 4097, 7 gaps in the run). The tail is itself a small mixed-radix counter: its front unit cycles 10 -> 01 -> 11 -> 00 -> 10, and S can only happen at 11. In Coq the leftward overflow return is a 4-rule token transducer proved sound once, so the tail's answer depends only on where its first 0 bit is (14 cases by computation + an induction for the growing end unit), with no 2^14-entry table. Between normal-mode overflows only 4 paths occur, and an interval invariant on (2^N, a - c, front unit) is closed under all of them, whichever way the tail goes at 11. Init is 92,299 steps.
One file, top-level `Lemma nonhalt : ~ halts tm c0.`, Coq 8.20.1, busycoq 0940bb9c, imports only Individual62. Compiles in ~10 s (native), `Print Assumptions` closed, coqchk passes. Architecture adapted from CounterClass3v2 TM1.
AI disclosure: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).