1RB1RA_1RC1RZ_1LD0RF_1RA0LE_0LD1RC_1RA0RE

1RB1RA_1RC1RZ_1LD0RF_1RA0LE_0LD1RC_1RA0RE (bbch) is the current BB(6) champion. It was discovered by mxdys on 25 June 2025 (Discord link).

It's in a family of 4 machines with halting times and sigma scores 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)

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

In October 2025, Peacemaker II calculated a more precise sigma score of $10\uparrow \uparrow 10\uparrow \uparrow 10\uparrow \uparrow 8.10237$^[1] for 1RB1RA_1RC1RZ_1LD0RF_1RA0LE_0LD1RC_1RA0RE (bbch).

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