Discord draft: kill announcement for 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
Not posted. Paste the block below as one message. It is 1,803 characters before the link, under Discord's 2,000-character limit (a link of up to about 197 characters fits).
Before pasting:
1. Replace <LINK> with the URL of the .v file (1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v in this folder).
2. This is a halting proof: the theorem is Lemma halt: halts tm c0., not nonhalt. The message says so in its first line.
3. Duplicate work: the sheet's Results row had only its class (no status, notes or done-by) when this was packaged, and busycoq's verify/ has no proof of it (only the equivalences below). In the Discord exports it appears only on mxdys's UBRRBA to-do list (2026-08-24), which is a to-do list, not a claim. Search #bb6 for the string before posting, in case someone has claimed it since; a courtesy mention of mxdys may fit.
4. Equivalences: the message names the two partners proved equivalent in the pinned verify/Eqv_v3.v (TM636, TM637). Newer busycoq equivalence files also relate it to 1RB0RF_0RC1RD_0LD---_1LE1RA_1LA0LF_0RD0RC (Eqv_RegularPairs TM101) and 1RB---_1LC1RE_1LA0LD_0RE1LC_1LC1RF_1RB0RD (Eqv_WordPairs TM98). Add them if you like; none of the four is on the 740 list.
5. No 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.
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 write-up.
`1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---` (Shift-overflow bouncer counter, 740 line 700) halts. Coq proof: <LINK>
Same table as SOBCv6's TM3 (ours A B C D E F = TM3 B C A E D F, no mirror), started in TM3's B. Left: TM3's binary counter in words 001/111; right: a register `1 (011)^n 01` that grows by one per increment. When the counter is full, the overflow re-reads it shifted by one word and the register becomes (c-1)/2 new zero digits, so c goes roughly 2^c per cycle. From blank it runs 194 cycles; in the 195th overflow an increment inside the re-read carries off the far end, and 1,368 steps later F reads a 1. Step count: informally estimated at a tower of height ~195 (neither computed nor proved).
TM3's rules replay unchanged after renaming the head notations. New: blocks with a lower bound on their length (`W10 l` = (W1 W0)^(1+l+n)), an LInc case that stops inside a W10 block, a "peel" case in LOv_rec that splits the far pair off a W11 block on demand, and a saturating count bound in N. 38,573-step init, then `final_check 192 = true` by vm_compute (192 abstract cycles, the last Incs, and a check on the final counter). The halt is a far-end predicate `Doomed x` (overflow run from `Lmp x` halts for all r), pushed through the prefix by two walk lemmas from a 13-token far tail (1,368 steps).
Top-level `Lemma halt: halts tm c0.`, Coq 8.20.1, busycoq 0940bb9, 838 lines, ~26 s compile (native), `Print Assumptions`: functional_extensionality_dep only, coqchk passes (~43 s). Via Eqv_v3 TM636/TM637 this also settles `1RB0RE_0LB1RC_1LD1RA_1LA0LE_0RC0RF_0LC---` and `1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LB---`.
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).