1RB1RA_1RC1RZ_1LD0RF_1RA0LE_0LD1RC_1RA0RE

1RB1RA_1RC1RZ_1LD0RF_1RA0LE_0LD1RC_1RA0RE (bbch)

Current BB(6) champion. Discovered by mxdys on 25 June 2025.

It's in a family of 4 machines with the halting time and sigma score between 2↑↑2↑↑2↑↑10 and 2↑↑2↑↑2↑↑11:

1RB1RA_1RC---_1LD0RF_1RA0LE_0LD1RC_1RA0RE (hereafter referred to as TM1)
1RB---_1LC0RF_1RE0LD_0LC1RB_1RA1RE_1RE0RD (TM2)
1RB0LE_1RC1RB_1RD---_1LA0RF_0LA1RD_1RB0RE (TM3)
1RB0RF_1RC1RB_1RD---_1LE0RA_1RB0LF_0LE1RD (TM4)

Coq proof: https://github.com/ccz181078/busycoq/blob/3f302b87f5fb933c46e97672ffbb6907f373fb6e/verify/SOBCv5.v#L10210-L11283

Analysis by mxdys

Inc2:
S1(len0,a0+1,2,a    ,b    ) -->
S1(len0,a0  ,1,a+b+2,2^b-1)

Inc1:
S1(len0,a0+1,1,a    ,b    ) -->
S1(len0,a0  ,0,a+b+2,2^b-1)

Inc0:
S1(len0,a0+1,0,a    ,b    ) -->
S1(len0,a0  ,2,a+b+1,2^b-1)

Rst0:
S1(a0,0,0,a,b) -->
halt

Rst1:
S1(a0,0,1,a,b) -->
S1(a0+a+2,(2^(a0+2)-1)*2^a-1,2,b,2^b-1)

start: S1(3,7,2,6,63)

the rules are used in the following order:
Inc2,Inc1,Inc0, Inc2,Inc1,Inc0, Inc2, Rst1,
Inc2,Inc1,Inc0, ..., Inc2,Inc1,Inc0, Inc2, Rst1,
Inc2,Inc1,Inc0, ..., Inc2,Inc1,Inc0, Inc2,Inc1, Rst0.

where
S1(len0,a0,m,a,b) = 0^inf LH LC(len0,a0) d0 10 1^m LC(a,0) <X 0 11100 111^(1+b) 0^inf
d0 = 100
d1 = 111
LC(0,0) = ""
LC(n+1,2x) = LC(n,x) d1
LC(n+1,2x+1) = LC(n,x) d0
for TM2, X=D, LH=111011
for TM3, X=E, LH=11

TM1 is equivalent to TM2 after several steps
TM4 is equivalent to TM3 after several steps
TM1 has the highest halting time among this family
TM1,TM2 have the highest sigma score among this family

estimation of time/score:

Inc2,Inc1,Inc0, ..., Inc2,Inc1,Inc0, Inc2
n mod 3 = 1:
S1(len0,n,2,b,2^b-1) -->
S1(len0,0,1,st2(n,b)+floor(n/3)*5+2,t2(n+1,b))

Inc2,Inc1,Inc0, ..., Inc2,Inc1,Inc0, Inc2,Inc1, Rst0
n mod 3 = 2:
S1(len0,n,2,b,2^b-1) -->
S1(len0,0,0,st2(n,b)+floor(n/3)*5+4,t2(n+1,b)) -->
halt

Rst1:
S1(len0,0,1,a,b) -->
S1(len0+a+2,2^(len0+a+2)-2^a-1,2,b,2^b-1)

where
t2(0,b) = b, t2(a+1,b) = 2^t2(a,b)-1
st2(a,b) = t2(0,b) + t2(1,b) + ... + t2(a,b)

S1(3,7,2,6,63) -->
S1(3,0,1,st2(7,6)+12,t2(8,6)) -->
S1(≈t2(7,6),≈t2(8,6),2,_,_) -->
S1(≈t2(7,6),0,1,≈2^^t2(8,6),_) -->
S1(≈2^^t2(8,6),≈2^^t2(8,6),2,_,_) -->
S1(≈2^^t2(8,6),0,1,≈2^^2^^t2(8,6),≈2^^2^^t2(8,6)) -->
halt with time/score ≈2^^2^^((2^)^8 6)
2^^^5 < 2^^2^^2^^10 < 2^^2^^((2^)^8 6) < 2^^2^^2^^11 < 2^^^6