1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---: never halts

Submission copy of the working proof.md, made 2026-10-10 after the kill. Only the formal-status lines were updated: header, §4, §5, §6, §7. Scripts and scratch files it cites (check_proof.py, check_rules.py, the Rocq scratch file probe_segments_2.v, notes.md) live in the working directory and are not in this folder.

• Machine: 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---, viewer https://bbchallenge.org/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---
• Holdout lists: on every holdout-list snapshot we have, 2024-06-14 (12,091) through 2026-10-07 (778). Sheet: Results row 1035, class "Bell eats counter"; Status, Notes, Sources and Done By are blank. No Discord thread.
• Written for: the string itself. There is no mirror or state permutation.
• Template: verify/SOMDCv6.v, Module TM7 (1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---). Our machine differs from it in one transition: A1 is 0RF here and 0RC in TM7.
• Status: fully formalized, killed. 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v (599 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9c). check_kill (our checker) PASS on 2026-10-10: compile 3.6 s, Print Assumptions nonhalt closed, coqchk pass in 1.1 s (check_kill.txt).
• Where each section lives in the .v: §3.1 Inc_spec, seg_hx_ld, seg_h1_ld, RIncs_spec; §3.2 BigStep; §3.3 Inc_total, Inc_fun, RIncs_Inc (Lemma A), RIncs_nxt_1 (Total_1), End_1, End_x, Inv, key (RIncs_nxt'), domain; §4 and §5 start, nonhalt.

Summary. The configuration at each sweep boundary is S(r) = 0^inf 11 D> <r> 0^inf, where r is a word over three 3-cell digits. TM7's proof carries over with three changes: 1. Where TM7's sweep enters an L digit, ours first runs one extra "+1 pass" over everything to the right. This adds an Inc premise to two clauses of TM7's RIncs. 2. RIncs gets two new end clauses, Z0 and Z1, that use zero passes. They describe no new machine behaviour (each is an identity between two ways of writing the same tape), but without them the sweep map's domain is not closed under the sweep map (§3.3). 3. TM7's domain lemma RIncs_nxt gets an extra parameter j, the number of pending +1 passes. Its condition Inv reduces to TM7's when j = 0.

1. Families and notation

• Digits: L = 110, 0 = 000, 1 = 100 (cells left to right). For a word r over {L,0,1}, <r> is its cells in order. A word followed by 0^inf denotes the same tape with or without trailing 0 digits.
• Counter value: inc(r), also written r+1, adds 1 to the little-endian binary number formed by the 0/1 digits of r. L digits are skipped; a carry out of the last digit appends a 1 digit.
• Family: S(r) := 0^inf 11 D> <r> 0^inf (busycoq S' r), for r in the domain P of §3.3.
• Passes (busycoq sideRLs). A pass runs over a right part X and never reads a cell left of where it exits, so it holds for every left part:
• h: B> X ->+ <C X'. The head exits one cell left of where it entered, and X' starts at the same cell as X.
• h': 1 D> X ->+ <C X'. The 1 belongs to the pass, so X' starts at the cell that held the 1.
• Inc(r, r'): the pass [h] turns <r> into <r'>.
• R(tp, k, r, r') (busycoq RIncs):
• R(hx, k, r, r'): the passes [h', h^k] turn <r> into <r'>.
• R(h1, k, r, r'): the passes [h^k] turn 1 <r> into <r'>, where the extra 1 cell comes first.

So hx is "the eater pass plus k queued passes", and h1 is "k passes draining over a stray 1".

2. Rule table

1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---      (SOMDCv6 TM7 with A1 = 0RF instead of 0RC)

S(r) = 0^inf 11 D> <r> 0^inf          L = 110, 0 = 000, 1 = 100
start: 0^inf A> 0^inf  -(5)->  S(1)
sweep: S(r) -+-> S(r')  if R(hx,0,r,r')            (r' starts one cell further left)
domain P(r) := exists r', R(hx,0,r,r');   P(1);   P(r) /\ R(hx,0,r,r') -> P(r')

Inc (one h pass = +1):
  I1  Inc(1::r, 0::r')  <- Inc(r,r')         I3  Inc(L::r, L::r')  <- Inc(r,r')
  I2  Inc(0::r, 1::r)                        I4  Inc([], [1])

R (k >= 0); NEW = differs from TM7's RIncs:
  X1  R(hx,k,    L::r, L::r')  <- Inc(r,r1), R(hx,k+1,r1,r')   NEW (TM7: R(hx,k+1,r,r'))  RIncs_hx_ld
  X2  R(hx,k,    0::r, L::r')  <- R(hx,k+1,r,r')                                          RIncs_hx_d0
  X3  R(hx,k,    1::r, L::r')  <- R(h1,k,r,r')                                            RIncs_hx_d1
  C1  R(h1,k+1,  L::r, L::r')  <- Inc(r,r1), R(hx,k+1,r1,r')   NEW (TM7: R(hx,k+1,r,r'))  RIncs_h1_ld
  C2  R(h1,k+1,  1::r, L::r')  <- R(h1,k,r,r')                                            RIncs_h1_d1
  C3  R(h1,2k+1, 0::r, 0::r')  <- R(h1,k,r,r')                                            RIncs_h1_d0_0
  C4  R(h1,2k+2, 0::r, 1::r')  <- R(h1,k,r,r')                                            RIncs_h1_d0_1
  R0  R(h1,0,    [],   [1])                                                               RIncs_h1_rh_0
  R1  R(h1,2k+1, [],   0::r')  <- R(h1,k,[],r')                                           RIncs_h1_rh_1
  R2  R(h1,2k+2, [],   1::r')  <- R(h1,k,[],r')                                           RIncs_h1_rh_2
  Z1  R(h1,0,    [1],  [L])     NEW: 0 passes, 1 100 0^inf = 110 0^inf
  Z0  R(h1,0,    [0],  [1])     NEW: 0 passes, 1 000 0^inf = 100 0^inf
  (no clause: hx at the right end; h1 with 0 passes on a word other than [], [1], [0])

machine level (j = number of digits of X before its first 0 digit, or |X| if none):
  B> 100 X  -(3)->  000 B> X            B> 000 X  -(1)->  <C 100 X        B> 0^inf  -(1)->  <C 100 0^inf
  B> 110 X  -(3)->  011 B> X            011 <C  -(3)->  <C 110            000 <C  -(3)->  <C 000
     =>  B> <X> 0^inf  -(6j+1)->  <C <X+1> 0^inf                       (Inc, no A1)
  eater enters L:   1 D> 110 <X>  -(6j+13)->  1 111 D> <X+1>       TM7: -(11)-> 1 111 D> <X>
  drain enters L:   B> 1 110 <X>  -(6j+12)->  1 111 D> <X+1>       TM7: -(10)-> 1 111 D> <X>
  wall:             0^inf 1 <C <r'>  -(3)->  0^inf 11 D> <r'>      (C1, D0, D0)

In words: - Eater (hx). The eater turns every digit it crosses into L. It gains one pass at each L or 0, and at each L the rest of the word gets +1 (X1, NEW). It switches to draining at the first 1 (X3). - Drain (h1, k passes). Each 1 absorbs one pass and becomes L (C2). Each 0 keeps one bit of the count and halves it (C3, C4). At the right end the count is written in bijective binary (R0–R2). An L restarts the eater with the same count and adds +1 to the rest (C1, NEW; this is the "drain-enters-L restart"). With 0 passes left, the drain can only be at the last digit, and it leaves the stray 1 in place (Z0, Z1, NEW).

Worked example. This is the start of the Checkpoint A picture pair, S(L^4 1L1), and it is the extra 1 Dennis noticed there (checked in §7). - First eat. Both machines eat the 4 L's (k = 4) and stop at the 1. Ours added +1 at each L, so its rest is 1L1 + 4 = 1L11, while TM7's is still 1L1. The extra 1 digit on the right is the extra bar after the first eat. - Drain. The first drain pass enters the L. - TM7 restarts the eater on 1. - Ours first runs +1 pass number 5: 11 + 1 = 001. The extra 1 is not ignored: the carry turns both 1s into 0s and appends a new 1. - Second eat. Ours also eats the two new 0s (k = 6). TM7 stops at once (k = 4). - Right end. The count is written in bijective binary: 6 gives 111, 4 gives 101. - Result. Ours reaches S(L^9 111) and TM7 reaches S(L^7 101). Ours has two more L's on the left, and the right end differs.

3. The argument

3.1 Every clause is an exact pass-level transition (RIncs_spec), Rocq-checked

Claim: R(hx,k,r,r') implies sideRLs ([h'] ++ h^k) <r> <r'>, and R(h1,k,r,r') implies sideRLs (h^k) (1 <r>) <r'>. Proof by induction on R, one clause at a time, as in TM7.

This section compiles. check_proof.py --rocq states Inc and all 12 clauses of R for the real machine string, then proves Inc_spec, seg_hx_ld, seg_h1_ld and RIncs_spec. Print Assumptions is closed. The two segment facts were first probed in probe_segments_2.v. - X2, X3, C2, C3, C4, R0, R1, R2. Each clause's run never fires A1, the one transition where the two machines differ (§7 counts A1 firings). So the run is the same as TM7's, and TM7's tactic scripts for these 8 cases (cat3, tr1/tr2, wal, am) are reused verbatim. - X1 (eater enters L). - TM7: the eater reaches A1 at the middle cell of the 110 in 4 steps (D1, B1, E1, A1). TM7's A1 = 0RC writes 0 and steps right onto the last cell of the 110 in state C. C0 = 0LC then turns left. - Ours: A1 = 0RF writes the same 0 and steps onto the same cell in state F. F0 = 0RB then puts B on the first cell of X. That is one h pass over X: B> <X> ->(6j+1) <C <X+1>. It returns with C on the last cell of the 110, which is exactly where TM7 is one step after its A1. From then on the two runs agree. - So TM7's segment fact for the L digit, segRLs [h'] [h', h] 110 110, becomes segRLs [h'] [h, h', h] 110 110, followed by the wall for h^k (Rocq: seg_hx_ld). The passes reaching the rest are [h] ++ ([h'] ++ h^(k+1)). That is Inc(r, r1) (Inc_spec below), followed by R(hx, k+1, r1, r') (induction hypothesis), joined by sideRLs_trans. - C1 (drain enters L). The same argument. The first pass of h^(k+1) meets 1 110 and reaches A1 in 3 steps (B1, E1, A1). TM7's segment fact segRLs [h] [h', h] 1110 110 becomes segRLs [h] [h, h', h] 1110 110 (Rocq: seg_h1_ld). - Inc_spec (Inc(r,r') implies sideRLs [h] <r> <r'>). By induction on Inc, using the six machine-level h-pass rules of §2 for I1–I4. - Z1 and Z0. These use zero passes, so they hold by sideRLseq_O (via applys_eq) and the stream identities 1 100 0^inf = 110 0^inf and 1 000 0^inf = 100 0^inf (const_unfold).

3.2 Sweep (BigStep)

Suppose R(hx,0,r,r'). The left part 0^inf 1 is never read by the pass, so:

S(r) = 0^inf 1 · 1 D> <r> -+-> 0^inf 1 <C <r'> -(3)-> 0^inf 11 D> <r'> = S(r')

The first arrow is the single pass h' (sideRLs_1); the second is the wall rule. This is TM7's BigStep, with the same proof. It compiles (§7).

3.3 The domain is closed (RIncs_nxt')

Let P(r) := exists r', R(hx,0,r,r'). We need R(hx,0,r,r') to imply P(r').

Why the extension is needed. Without Z0/Z1 this is false: - r = LLLL10LL1L1 is in P, and its sweep is LLLLL1LLLLLLL111, which is not in P without Z0/Z1. Its second sweep needs Z1 and gives LLLLLLLLLLLLLL011L, which is also what the real machine produces. - Up to 11 digits, 170 words fail this way.

Z0/Z1 are never used on the run from blank (§7), so they matter only to the domain lemma.

Auxiliary lemmas. All are stated as relations. The only functionality the proof uses is that of Inc.

Lemma A says one extra pass after the k passes is +1 on the result. It is what turns the second sweep's +1 passes into extra count for the first.

Key lemma (RIncs_nxt'). Two sweep processes run over the same digits: - the first has R(tp,k,r,r1); - the second reads the first's output after j pending +1s, R(tp,k+j,r,rK) (by Lemma A this is r1 + j), with count q.

Write K = k+j. The lemma:

R(tp,k,r,r1) /\ R(tp,K,r,rK) /\ Inv(tp,k,j,tq,q)  ->  exists r2, R(tq,q,rK,r2)
  Inv(hx,k,j,hx,q) := k <= q /\ j <= q
  Inv(h1,k,j,hx,q) := k+1 <= q /\ j <= q
  Inv(h1,k,j,h1,q) := (j = 0 /\ 2k+1 <= q) \/ (j >= 1 /\ K <= q /\ 1 <= q)      [both imply K <= q, 1 <= q]
  Inv(hx,_,_,h1,_) := False

With j = 0 these are exactly TM7's conditions (k<=k', k+1<=k', k*2+1<=k'). The domain step is the instance tp = tq = hx, k = j = q = 0.

Proof. Induct on the derivation of R(tp,k,r,r1), generalizing j, rK, tq and q. The induction is on the derivation, not on r, because X1/C1 recurse on inc r. In each case, invert R(tp,K,r,rK); Inc is functional, so both derivations name the same incremented word. The second process reads the first digit of rK, and that leaves one IH obligation. Each obligation's count K' is supplied by Lemma A, since the second's +1 passes land on the first's rest.

Some shorthand for the table: - t+ means Inc(t). - In C3/C4, k1 = floor((k-1)/2) and K1 = floor((K-1)/2). Then j1 = K1 - k1 equals ceil(j/2) when K is odd and floor(j/2) when K is even.

No other case occurs: - hx at the right end has no clause. - h1 with 0 passes occurs only as Z0/Z1. - Inv(hx,_,_,h1,_) is False.

∎

3.4 Progress

R is inductive, so every derivation is finite. Each clause is a finite run: its segment lemma, plus the finitely many passes of its premises (§3.1). So S(r) -+-> S(r') is a finite run of at least 4 steps: h' takes at least 1, and the wall takes 3. Example: S(1) to S(L1) takes 11 steps (steps 5 to 16).

3.5 The halting transition F1

Formally, every rule is a proved exact run, so no step on the way from c0 is the halting transition.

As a sanity check: F is entered only by A1 = 0RF and E0 = 0RF. In the machine-level rules of §2, F is entered on the last cell of a digit, and that cell is 0 for all three digits, so F0 = 0RB fires. In every simulated rule instance F read a 0; the count of F reading 1 is 0 (§7).

4. Initial segment

0^inf A> 0^inf reaches S(1) in 5 steps:

• -A0-> 0^inf 1 B> 0^inf
• -B0-> 0^inf 1 <C 1 0^inf
• -C1-> 0^inf <D 0 1 0^inf
• -D0-> 0^inf 1 D> 0 1 0^inf
• -D0-> 0^inf 11 D> 100 0^inf = S(1)

S(1) is in the domain: R(hx,0,[1],[L,1]) by X3 and R0.

TM7's nonhalt uses the same start, S' [D1], by esx. Here too, init: c0 -[tm]->* S' [D1] compiles by esx (§7).

The .v file starts one sweep later: start : c0 -->* S' [LD;D1] (S(L1), step 16), also by esx. Its initial domain witness is R(hx,0,[L,1],[L,L,L,1,1]): X1 with Inc([1],[0,1]), then X2, X3, and R2 over R0.

5. Conclusion

Use multistep_nonhalt with c' = S(1) (§4), then progress_nonhalt_cond with P(r) := exists r', R(hx,0,r,r'): - §3.2 gives S(r) -+-> S(r'). - §3.3 gives P(r'). - §3.4 shows each sweep is at least one step.

So the machine never halts. In Rocq this is TM7's nonhalt with RIncs replaced by R and with a different call to the domain lemma. TM7 calls RIncs_nxt with (tp':=hx) (k':=O) on one hypothesis. Here the call is RIncs_nxt' at tp = tq = hx and k = j = q = 0. Both R hypotheses are I1 (K = k+j = 0), and Inv(hx,0,0,hx,0) is discharged by lia.

In the .v file c' = S(L1) (see §4), RIncs_nxt' is named key, and the instance above is the lemma domain.

6. Mapping to SOMDCv6 TM7

Formal status: all done. Every row above compiles in 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v, and check_kill (our checker) passes (check_kill.txt). - The X1/C1 segment lists are proved by seg_hx_ld and seg_h1_ld (esx, then TM7's wall tactic wal). - §3.3 is the lemma key, proved by induction on the first derivation. The case table above matched the Coq cases one to one, and no case needed a change. Its two expected risks were handled with plain lia: 1. the floor/ceil arithmetic on j1, via mod2 case splits as in TM7's solve_v1; 2. the C3/C4 inversion of the K-derivation, which depends on K's parity rather than k's (inv_h1_d0, three alternatives).

7. Evidence

The checks are in check_proof.py, in this directory (reuses check_rules.l_entry). The numbers below are from python3 -B check_proof.py --full (36 s). That mode includes the Rocq check, which --rocq runs alone (4 s). The default run (8 s) gives the same verdicts on smaller samples, with the from-blank check to 1e8 steps. "Real machine" means simulation of the actual transition table: a pass stops the first time the head reaches its exit cell, so cells left of it are never read.

Gaps: none. The simulation rows are evidence only. The kill rests on the .v file alone, which passes our checker, check_kill.

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

Review log

Independent skeptic review, 2026-10-10. Verdict: sound; 5 minor gaps, no fatal or major ones. All 5 were accepted and fixed.

Also added, though the review did not ask for it: the worked example in §2, which explains Dennis's Checkpoint A observation (the extra 1 after the first eat is carried away by +1 pass 5), with a check in §7.