/machines/1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB/submission/discord.md · raw

Discord draft: kill announcement for 1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB

Not posted. Paste the block below as one message. It is 1,621 characters without the link, so a link of up to 379 characters keeps it under Discord's 2,000-character limit.

Before pasting:

  1. Link. Replace <LINK> with the URL of the .v file (1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB.v in this folder).

  2. Search. Search #bb6 for the string first, in case someone has claimed it since. No Discord discussion of it is on file, and its spreadsheet row (Results tab, row 842, class "Structural counter + counter") has no status, notes or claim.

  3. No partners. It is a singleton in the equivalence-class listing of 7 October 2026, so the message names no equivalent machines.

  4. Size. The .v is long (4,422 lines, about 5 minutes to compile with the native compiler). coqchk passes in about 5 minutes, so the vm_compute steps are re-checked independently too. The message says both.

  5. Disclosure. The last line uses the same wording as the README and the other drafts.

`1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB` (Structural counter + counter, 740 line 301) never halts. Coq proof: <LINK>

Read the tape as units D0=0000, D1=1000, P=11000, S1=01000, SP=011000, W=111000; each B-right/C-back trip from the left edge is one carry, which acts as a recursive increment on the unit word. SP/W are walls: a W fires on every 2nd carry, sends 3 carries up and moves one unit right (a 3/2 rotor). The left end is an exact 8-record cycle that adds 8 walls per cycle; they ride a P conveyor in birth order and get absorbed one by one into a binary counter at the right end (the zone). A flux identity shows the zone gets D + p(j mod 8) carries per absorption with p = (47,48,48,47,48,47,48,47), so the zone is a closed 2-adic counter system with no 3/2 arithmetic left. Halting needs a wall's shift to land on another wall, which never happens.

Zone: canonical states C(b) at j = 32b+17, and C(b) reaches a later C(b') for every b: verified runs of affine state families (small classes nu2(b+2) <= 40, endgame mod 2^12, nested range), a symbolic one-step descent lemma, two lemmas by hand, and a well-founded recursion on the class. Conveyor: a one-carry cascade lemma over the walls, plus a record invariant over the 8 record types.

Top-level `Lemma nonhalt: ~halts tm c0.`, Coq 8.20.1, busycoq 0940bb9, Individual62 only, 4,422 lines, ~5 min compile (native), Print Assumptions closed, coqchk passes (~5 min). No template applies (nearest is CounterCmp_v1 TM1, 11 of 12 transitions differ).

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