/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/submission/discord.md · raw
Discord draft: kill announcement for 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---
Not posted. Before pasting, replace <LINK> with the URL of the .v file (1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v in this folder). Paste the block below as one message: it is 1,371 characters before the link, under Discord's 2,000-character limit.
`1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---` (Bell eats counter, sheet row 1035) never halts. Coq proof: <LINK>
It is busycoq's SOMDCv6 TM7 (`1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---`) with A1 changed from 0RC to 0RF. The sweep config is the same, `0^inf 11 D> <r> 0^inf` over the digits L=110, 0=000, 1=100. The difference: whenever a sweep enters an L digit (eater or drain pass), A1 now runs one extra h-pass to the right. That pass adds +1 to the 0/1 digits (little-endian binary, L skipped) and comes back to exactly where TM7 is one step after its A1. The proof is TM7's with three changes:
- an `Inc` relation, added as a premise to the two L clauses of `RIncs`;
- two zero-pass end clauses, `RIncs h1 0 [D1] [LD]` and `RIncs h1 0 [D0] [D1]`. They are just `1 100 0^inf = 110 0^inf` and `1 000 0^inf = 100 0^inf`, but without them the domain is not closed;
- the domain lemma, redone with a count j of pending +1 passes. At j = 0 it reduces to TM7's conditions.
It is one file with a top-level `Lemma nonhalt: ~halts tm c0.`, built with Coq 8.20.1 against busycoq 0940bb9c. It compiles in about 4 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.