0RB1RZ0RB_1RC1LB2LB_1LB2RD1LC_1RA2RC0LD

0RB1RZ0RB_1RC1LB2LB_1LB2RD1LC_1RA2RC0LD (bbch) is a halting BB(4,3) machine that appears to run for around

$$2\uparrow \uparrow \uparrow (2^{2^{32}+1}-1)$$

steps. The TM was discovered by Pavel Kropitz in May 2024 as a group of 6 long-running halting BB(4,3) TMs. Racheline analyzed the machine by hand in Feb 2025, validating the result and provided the step estimate listed above.

Pavel listed the halting tape as:

1 2^((80*2^((<(8*2^((8*2^(29) - 2)) - 5); (<(80*2^((b - 10)/5) - 17)/9; (40*2^((8*2^((a - 11)/5) - 2)) - 4); (40*2^(2) - 4)> + 4); (<(80*2^((<(80*2^((8*2^((8*2^(29) - 2)) - 3)) - 13)/9; (40*2^((8*2^((a - 11)/5) - 2)) - 4); (40*2^(2) - 4)> - 6)/5) - 17)/9; (40*2^((8*2^((a - 11)/5) - 2)) - 4); (40*2^(2) - 4)> + 4)> - 10)/5) - 3)) 1 0 1 2 1^2 Z> 1 2^2 1

Analysis by racheline

https://discord.com/channels/960643023006490684/1331570843829932063/1337228898068463718

f(n) = 2^2^(n+1)
g(n) = (5*2^(2^(f^n(0)+1)+2)-8)/9
n0 = (5*2^(2^(2^32+1)+1)-4)/9
n1 = 2^(2^32+1)-4
0RB1RZ0RB_1RC1LB2LB_1LB2RD1LC_1RA2RC0LD halts with 5*2^(2^(f^g^n1(n0)(0)+1)+2)+7 nonzero symbols on the tape, after roughly (that)^2 steps
that's around 2^^^(2^(2^32+1)-1)
the rules necessary for verification:
0^inf 1 <D 0^(5n) 2^4 ->
0^inf 1 <D 0^(5*2^n+2)

0^inf 1 <D 0^(5n+2) 2^5 ->
0^inf 1 <D 0^(5*2^(n+1))

0^inf 1 <D 0^(5n) 221122 ->
0^inf 1 <D 0^(5*2^n+4)

0^inf 1 <D 0^(5n+4) 1 0^5 ->
0^inf 1 <D 0^2 2^23 1 0^(5*2^(n+2)-22) 1011221

0^inf 1 <D 0^(5n) 1 0^10 ->
0^inf 1 <D 0^2 2^(5*2^(n+1)) 11221

0^inf 1 <D 0^(5n+2) 2222112 ->
0^inf 1 <D 0^(5*2^(n+1)+2)

0^inf 1 <D 0^(5n+2) 21 0^10 ->
0^inf 1 <D 0^2 2^(5*2^(n+2)-4) 11221

0^inf 1 <D 0^(5n+2) 2^9 ->
0^inf 1 <D 0^(5*2^(n+1)) 2^4 ->
0^inf 1 <D 0^(5*2^2^(n+1)+2) =
0^inf 1 <D 0^(5f(n)+2)

0^inf 1 <D 0^2 2^(9n) ->
0^inf 1 <D 0^(5f^n(0)+2)

0^inf 1 <D 0^2 2^(9n+4) 11221 0^10 ->
0^inf 1 <D 0^(5f^n(0)+2) 222211221 0^10 ->
0^inf 1 <D 0^(5*2^(f^n(0)+1)+2) 21 ->
0^inf 1 <D 0^2 2^(5*2^(2^(f^n(0)+1)+2)-4) 11221 =
0^inf 1 <D 0^2 2^(9g(n)+4) 11221

0^inf 1 <D 0^2 2^(9n+4) 11221 0^(10m) ->
0^inf 1 <D 0^2 2^(9g^m(n)+4) 11221

0^inf 1 <D 0^2 2^16 11221 0^inf
0^inf 1 <D 0^10 2^11 11221 0^inf
0^inf 1 <D 0^22 2^7 11221 0^inf
0^inf 1 <D 0^160 2211221 0^inf
0^inf 1 <D 0^(5*2^32+4) 1 0^inf
0^inf 1 <D 0^2 2^23 1 0^(5*2^(2^32+2)-22) 1011221 0^inf
0^inf 1 <D 0^10 2^18 1 0^(5*2^(2^32+2)-22) 1011221 0^inf
0^inf 1 <D 0^22 2^14 1 0^(5*2^(2^32+2)-22) 1011221 0^inf
0^inf 1 <D 0^160 2^9 1 0^(5*2^(2^32+2)-22) 1011221 0^inf
0^inf 1 <D 0^(5*2^32+2) 2^5 1 0^(5*2^(2^32+2)-22) 1011221 0^inf
0^inf 1 <D 0^(5*2^(2^32+1)) 1 0^(5*2^(2^32+2)-22) 1011221 0^inf
0^inf 1 <D 0^2 2^(5*2^(2^(2^32+1)+1)) 11221 0^(5*2^(2^32+2)-32) 1011221 0^inf =
0^inf 1 <D 0^2 2^(9n0+4) 11221 0^(10n1+8) 1011221 0^inf
0^inf 1 <D 0^2 2^(9g^n1(n0)+4) 11221 0^8 1011221 0^inf
0^inf 1 <D 0^(5*2^(f^g^n1(n0)(0)+1)+2) 21 0^8 1011221 0^inf
this continues the same way as if the 0^8 was a 0^10 until the last few steps, so the tape differs from 0^inf 1 <D 0^2 2^(5*2^(2^(f^g^n1(n0)(0)+1)+2)-4) 11221 in a small amount of symbols on the left end and the right end, which you can easily count by running a smaller example