Discord draft: kill announcement for 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---
Not posted. Paste the block below as one message. It is 1,639 characters before the link, under Discord's 2,000-character limit.
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v in this folder).
2. Re-read dyuan01's Oct 1 longitudinal-filter thread (our export of it, 2026-10-01_dyuan01_longitudinal_24.txt). This machine is on that list, which is a technique filter, not a claim, but check nobody has said they are working on it since. It is also on mxdys's UBRRBA_TODO, which counts as fair game. If you want to acknowledge the lists, this optional line fits (131 characters plus a blank line; the message is then 1,772 characters plus the link): (It is on dyuan01's Oct 1 longitudinal list and mxdys's UBRRBA_TODO; this proof is a direct one, without the Longitudinal library.)
3. No Checkpoint B notes from you were on file when this was packaged. If you add any, fold them into proof.md (working copy and this folder) first.
`1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---` (Sync bouncer counter, sheet row 921) never halts. Coq proof: <LINK>
It is SBCv7 TM4 (`1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_0RA---`) with F0 changed from 0RA to 1RC. The left side is TM4's binary counter (digits 1010/0010, same `<A 001` / `001 E>` head), +1 per bounce. The right side is new: a row of blocks A=00111, B=10111. In the P phase each bounce appends a B. When the counter overflows it gains a digit and a front `111` appears, which walks right 2 A blocks every 3 bounces. When it reaches the B blocks they all become A blocks, by one of two gadgets (even or odd number of A blocks left ahead of the front). In the odd one the counter can overflow partway through, so the next front starts early. At the start of each Q phase, with counter range N = 2^k, the block counts (Y ~ A blocks ahead of the front, Z ~ B blocks; exact definitions in the comment block at the end of the .v) follow an affine map from cycle to cycle, with two branches picked by the parity of Y. Both branches map the hexagon `8Y>=N, 8Y<=3N, 3Z<=N, 8Z>=-N, 4Y+2Z>=N, 20Y+16Z<=9N` into itself, so the parity never matters. The run enters it at `Q(7,65,1,16,0)` after 17,215 steps.
It is one file with a top-level `Lemma nonhalt: ~halts tm c0.`, built with Coq 8.20.1 against busycoq 0940bb9c (Individual62 only, no Longitudinal). It compiles in about 7 s, `Print Assumptions` is closed, and coqchk passes.
AI disclosure: the informal proof and the Coq formalization were produced with Claude Code (AI-assisted) under my direction, and checked by compiling against unmodified busycoq, with Print Assumptions and coqchk.