1RB3RB1LB---2RB 2LA1RA4LB2LA2RA

1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (bbch) is a BB(2,5) machine whose behavior is similar to Skelet 17. A proof was given by Daniel Yuan (@dyuan01) of the machine's nonhalting on July 30th 2024. 1RB3RA2LB1LB1RB_2LA2RA4LA1LA--- (bbch) is equivalent to this machine.

Analysis shared by Daniel Yuan (@dyuan01) on Discord, on June 14th 2024:

I just checked whenever the beaver reaches the 1 on the left side, and calculated the tape for when it next reaches the left side. It would be nice if someone can verify these rules.

[x, y, z] := 1 <B 4^x 12 4^y 12 4^z

[0, a, b, …] -> [a+3, b, …]
[2n+1, 2a, 2b, …, 0] -> Halt 
[2n+1, 2a, 2b, …, 2m+2] -> [2n, 2a, 2b, …, 2m+2, 0]
[2n+1, 2a, 2b, …, 2m+1] -> [2n, 2a, 2b, …, 2m+1, 1]
[2n+1, 2a, 2b, …, 2m+1, x, …] -> [2n, 2a, 2b, …, 2m+1, x+1, …]
[2n+2, a, b, …] -> [2n+1, a+1, b, …]

And you should start at [1, 1].

Review

Matthew House (@LegionMammal978) reviewed the above analysis on June 14th 2024 and agrees with it.

Opus 4.7 Review

  Bug 1: "2a, 2b, …" includes 0 but rules only hold for positive even digits

  The notation 2a, 2b, … in rules 2–5 denotes "even digits" but reads naturally as allowing 0. The rules are 
  false when any middle digit is 0.                                                                          

  Counterexample: [1, 0, 2]. Rule 5 would predict [0, 0, 2, 0] (odd-increment applied to leftmost inner odd —
   but there's no inner odd, so actually rule 3 fires with middle [0], predicting [0, 0, 2, 0]). The actual  
  TM simulation instead collapses over the zero and produces [3, 2] in 9 steps (rule-1-like).                

  Root cause: a digit y encodes 4^y on the tape (so y = 0 means NO 4s). Without the 4-run to sweep over, the 
  separator interaction is different, and the sweep dynamics used to derive rules 3–5 don't fire.

  Bug 2: rule 1 can produce length-1 lists

  [0, a] → [a+3] has length 1 — subsequent rules require length ≥ 2. So rule 1 needs an explicit precondition
   that the input list has length ≥ 3 (i.e., there IS a b after a).

  Corrected rules 

  [x, y, z] := 1 <B 4^x 12 4^y 12 4^z    (encoding; B is state, 1<B means state B on symbol 1)               
  Start: [1, 1]

  (R1) [0, a, b, …]                                → [a+3, b, …]                                             
       where the input has length ≥ 3 (the "…" allows empty tail, but `b` must exist).                       

  (R2) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 0]           → Halt                                                    
       middle digits are strictly positive even (each 2aᵢ+2 ≥ 2); j ≥ 0.                                     

  (R3) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+2]        → [2n, 2a₁+2, …, 2aⱼ+2, 2m+2, 0]                          
       middle positive even, last digit positive even; j ≥ 0.                                                

  (R4) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1]        → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, 1]
       middle positive even, last digit odd; j ≥ 0.

  (R5) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1, x, …]  → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, x+1, …]                     
       middle positive even, then an odd 2m+1, then at least one more digit x (plus possibly a tail).

  (R6) [2n+2, a, …]                                → [2n+1, a+1, …]                                          
       leading is positive even (≥ 2); a arbitrary; tail arbitrary (may be empty). 

  Consequences for the non-halt argument

  - R2 (halt) is still the "bad" pattern, but defined over positive even middles only — configurations with a
   0 in the middle don't trigger R2; they just aren't reached.
  - The claim "the machine never halts" is now: no shape of the form [2n+1, positive-even…, 0] is ever       
  reached from [1, 1]. This is an invariant to be proved, not a property to be checked.                      
  - Rules R3, R4, R5 each require the middle digits to be strictly positive (≥ 2).

  The structural proof in §3 of the paper (the 3 "secure types") is not affected by this fix — it already    
  treats the middle digits as an abstract even-valued block. But the rule derivation (§2, currently a
  placeholder) must use the stricter positivity hypothesis, and the base case "[1, 1] is secure" must be     
  shown without passing through any all-positive-even-middle configuration with a zero slipped in.

This version of the rules was proven in Lean. The nonhalting proof given by @dyuan01 is not yet verified. Opus got stuck and Aristotle couldn't finish from that point either. See the current state, esp. the Aristotle summary in https://github.com/rwst/bbchallenge/tree/main/1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (to be continued..)