View source for 1RB3LA4RB0RB2LA 1LB2LA3LA1RA1RZ

{{machine|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ}}
{{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ}}

This is the current [[BB(2,5)]] champion. It is a halting [[shift overflow counter]] with sigma score (and runtime) over <math>10^{10^{10^{3\,314\,360}}}</math>. It was discovered by Daniel Yuan and shared [https://discord.com/channels/960643023006490684/1084047886494470185/1254826217375273112 on Discord] on 24 Jun 2024 and shared on the busy-beaver-discuss email list [https://groups.google.com/g/busy-beaver-discuss/c/PGOBAz46K6I/m/af5sjd6MBAAJ the next day]. It was verified to halt in [[Coq]] by mxdys on 4 Jun 2025 ([https://discord.com/channels/960643023006490684/1259770421046411285/1379877629288644722 Discord]).

== Analyses ==

=== dyuan01 ===
dyuan01 [https://discord.com/channels/960643023006490684/1084047886494470185/1254826217375273112 24 Jun 2024 11:51am EDT]:<pre>
the TM appears to halt at

[11] [01]^(a+b+c+31) [11]^(d+1) 4 <B 1

Where

a = (2^25-2^19-9)/3 = 11010045
b = [2^(a+27)-2^(a+2)-11]/3
c = [2^(a+b+29)-2^(b+2)-9]/3
d = [2^(a+b+c+31)-2^(c+2)-8]/3
</pre>dyuan01 [https://discord.com/channels/960643023006490684/1084047886494470185/1254842225980997793 24 Jun 2024 12:55pm EDT]:<pre>
Alright, so first things first, I should establish some rules, (all variables are natural numbers unless otherwise specified)

Basic rules (all can be simulated in a fixed number of steps):
1) [01] <A -> [11] A>
2) [11] <A -> <A [33]
3) A> [33] -> [01] A>
4) [01] <A3 -> [11] 0B>
5) [11] <A3 -> <A3 [33]
6) 0B> [33] -> [01] 0B>
7) A> [21] -> <A [22]
8) A> [22] -> <A [23]
9) A> [23] -> [41] A>
10) A> 0^inf -> <A [21] 0^inf
11) 0B> [21] -> <A3 [33]
12) 0B> [22] 0^inf -> Halt at [11] 4 <B 1 0^inf
13) 0B> [23] -> [11] 0B>
14) [41] <A -> <A [23]
15) 0^inf [11] <A -> 0^inf [11] 0B>

Counter rule helper:
A) [01] [11]^x <A -> [11] [01]^x A> (Basic rules 2*, 1, 3*)

Counter rules:
1) [01] [11]^x <A [23]^y 0^inf -> [11] [01]^x <A [23]^y [21] 0^inf (Counter rule A, Basic rules 9*, 10, 14*)
2) [01] [11]^x <A [23]^y [21] -> [11] [01]^x <A [23]^y [22] (Counter rule A, Basic rules 9*, 7, 14*)
3) [01] [11]^x <A [23]^y [22] -> [11] [01]^x <A [23]^(y+1) (Counter rule A, Basic rules 9*, 8, 14*)
4) 0^inf [11]^(x+1) <A -> 0^inf [11] [01]^x 0B> (Basic rules 2*, 15, 6*)
5) [01] [11]^x <A3 -> [11] [01]^x 0B> (Split <A3 into <A 3, then use Counter rule A, then simulate a step and merge 0 B> into 0B>)

Advanced rules:
1) [01]^3 0B> 0^inf -> [11] [01]^3 <A [21] 0^inf (simulatable in finite steps)
2) [01] [11]^(x+2) 0B> 0^inf -> [11] [01]^x [11]^2 [01] <A [21] 0^inf (Uses Basic rules 2* and 3*, but otherwise can be simulated in finite and bounded steps)

Now, I will simulate some tapes when they are overflowing from certain starting positions (assume 0^inf on both ends and x,y>=2):

(Overflow rule 1)
[11]^x <A [23]^y [21]
[11] [01]^(x-1) 0B> [23]^y [21] (Counter rule 4)
[11] [01]^(x-1) [11]^y 0B> [21] (Basic rule 13*)
[11] [01]^(x-1) [11]^y <A3 [33] (Basic rule 11)
[11] [01]^(x-2) [11] [01]^y 0B> [33] (Counter rule 5)
[11] [01]^(x-2) [11] [01]^(y+1) 0B> (Basic rule 6)
[11] [01]^(x-2) [11] [01]^(y-2) [11] [01]^3 <A [21] (Advanced rule 1)

(Overflow rule 2)
[11]^x <A [23]^y
[11] [01]^(x-1) 0B> [23]^y (Counter rule 4)
[11] [01]^(x-1) [11]^y 0B> (Basic rule 13*)
[11] [01]^(x-2) [11] [01]^(y-2) [11]^2 [01] <A [21] (Advanced rule 2)

(Overflow rule 3)
[11]^x <A [23]^y [22]
[11] [01]^(x-1) 0B> [23]^y [22] (Counter rule 4)
[11] [01]^(x-1) [11]^y 0B> [22] (Basic rule 13*)
Halt at [11] [01]^(x-1) [11]^(y+1) 4 <B 1 (Basic rule 12)

The only steps missing now are the steps to get from (11|01)* <A (21) to (11)* <A (23)* (|21|22), which takes advantage of binary representations and division mod 3.
Now we start to simulate the tape

At some point, the tape reaches [11]^7 <A [23]^17 [21]. By overflow rule 1, we reach
[11] [01]^5 [11] [01]^15 [11] [01]^3 <A [21]

If we treat [11] as 0 and [01] as 1 in binary, then [11] [01]^5 [11] [01]^15 [11] [01]^3 has a binary representation of (2^25-2^19-9). This is divisible by 3, so let a = (2^25-2^19-9)/3 = 11010045 (an odd number). Then we get
[11] [01]^5 [11] [01]^15 [11] [01]^3 <A [21]
[11] [11]^5 [11] [11]^15 [11] [11]^3 <A [23]^a [21]
[11]^26 <A [23]^a [21]

We apply overflow rule 1 again to get 
[11] [01]^24 [11] [01]^(a-2) [11] [01]^3 <A [21]

This has a binary representation of 2^(a+27)-2^(a+2)-9, which is 2 mod 3. Let b = (2^(a+27)-2^(a+2)-11)/3, which is an odd number, then we get
[11] [01]^24 [11] [01]^(a-2) [11] [01]^3 <A [21]
[11]^(a+28) <A [23]^(b+1)

Apply overflow rule 2 to get 
[11] [01]^(a+26) [11] [01]^(b-1) [11]^2 [01] <A [21]

This has a binary representation of 2^(a+b+29)-2^(b+2)-7, which is also 2 mod 3. Let c = (2^(a+b+29)-2^(b+2)-9)/3, another odd number, then we get
[11]^(a+b+30) <A [23]^(c+1)

We apply overflow rule 2 again to get
[11] [01]^(a+b+28) [11] [01]^(c-1) [11]^2 [01] <A [21]

This has a binary representation of 2^(a+b+c+31)-2^(c+2)-7, which is 1 mod 3. Let d = (2^(a+b+c+31)-2^(c+2)-8)/3. We get
[11]^(a+b+c+32) <A [23]^d [22]

After applying overflow rule 3 we get that this halts at
[11] [01]^(a+b+c+31) [11]^(d+1) 4 <B 1
</pre>Btw, d > 2^c > 2^2^b > 2^2^2^a > 2^2^2^2^23 > 2^2^2^2^2^4 = 2^2^2^2^2^2^2 = 2^^7, so that's probably the lower bound that should be used in steps and sigma for this TM.

LegionMammal978 [https://discord.com/channels/960643023006490684/1084047886494470185/1254967208291991582 24 Jun 2024 9:11pm EDT]:

Assuming your values are correct, HyperCalc and my own manual calculations agree that σ ≈ 2^2^(2.8138364628466968⋅10^3314361) ≈ 10^10^(8.470491782098934⋅10^3314360). Equivalently, this is (2 ↑)⁷ 1.127778888301767 or (10 ↑)⁴ 6.5203998005419574.

=== Shawn Ligocki ===
Shawn Ligocki [https://groups.google.com/g/busy-beaver-discuss/c/PGOBAz46K6I/m/L8hh3KqOBAAJ 25 Jun 2024 1:35am EDT]:

At a high level, this TM satisfies the following rules:

Counter Rules:

* 01 11^x <A 23^y 00 -> 11 01^x <A 23^y 21
* 01 11^x <A 23^y 21 -> 11 01^x <A 23^y 22
* 01 11^x <A 23^y 22 -> 11 01^x <A 23^y 23

In other words, each iteration, the left counts up 1 in a binary counter (using "01" for 0 and "11" for 1) while the right keeps track of the number of iterations modulo 3 (using the final value of "21", "22" or "23") and grows every 3 iterations.

This continues until the counter "overflows" and depending upon the mod on the right side it has one of 3 possible behaviors.

Overflow Rules:

* 0^inf 11^x+2 <A 23^y+2 0^inf    -> 0^inf 11 01^x 11 01^y 11^2 01 <A 21 0^inf
* 0^inf 11^x+2 <A 23^y+2 21 0^inf -> 0^inf 11 01^x 11 01^y 11 01^3 <A 21 0^inf
* 0^inf 11^x+1 <A 23^y+1 22 0^inf -> 0^inf 11 01^x 11^y+2 1 Z> 1 0^inf

I have [https://github.com/sligocki/busy-beaver/commit/3189833014f1b2442d4ffe91c6e1d7fdb574675a confirmed] all of the above rules in my inductive validator.

At step 2430 it is in config "0^inf 11^7 <A 23^17 21 0^inf" and Daniel reports that it proceeds to overflow 5 times with the last one hitting the halt rule (I have not confirmed this behavior yet myself). The penultimate config reported by Daniel is:<pre>
0^inf [11] [01]^(a+b+c+31) [11]^(d+1) 4 <B 1 0^inf
</pre>Where<pre>
a = (2^25-2^19-9)/3 = 11010045
b = [2^(a+27)-2^(a+2)-11]/3
c = [2^(a+b+29)-2^(b+2)-9]/3
d = [2^(a+b+c+31)-2^(c+2)-8]/3
</pre>and Mathew House on Discord reported that this makes the sigma value for this TM > (10 ↑)^4 6.5

=== Pascal Michel ===
Pascal Michel [https://groups.google.com/g/busy-beaver-discuss/c/PGOBAz46K6I/m/ptLo9T7NCQAJ 15 Jan 2025 2:58am EST]:

Let M be the 2x5 TM found by Daniel Yuan in June 2024, with s(M) > 10^(10^(10^3314360)).

Here, I give a proof that s(M) is approximately 3/2 (sigma(M)^2).

(1) Time for

- Counter rules:

01 (11)^x <A (23)^y 00 --( 4(x + y) + 6 )--> 11 (01)^x <A (23)^y 21

01 (11)^x <A (23)^y 21 --( 4(x + y) + 6 )--> 11 (01)^x <A (23)^y 22

01 (11)^x <A (23)^y 22 --( 4(x + y) = 6 )--> 11 (01)^x <A (23)^y 23

so we have

. . .  <A (23)^y 00 --( . . . + 12y + . . . )-->  . . . <A (23)^(y + 1)

- Overflow rules:

0 (11)^(x + 2) <A (23)^(y + 2) 0^3 --( 4x + 8y + 53 )--> 11 (01)^x 11 (01)^y  01 <A 21

0 (11)^(x + 2) <A (23)^(y + 2) 21 0^3 --( 4x + 8y + 73 )--> 11 (01)^x 11 (01)^y 11 (01)^3 <A 21

0 (11)^(x + 1) <A (23)^(y + 1) 22 0 --( 4(x + y) + 15 )--> 11 (01)^x (11)^(y + 2) 1 Z>1

(2) The time taken on the binary counter  is linear in the number of binary steps, so it is dominated by the time taken on the 23s, which is quadratic.

(3) The total time is dominated by the time taken from the 4th overflow to the last overflow.

Just before the last overflow, the configuration is

. . . <A (23)^d 22 0^inf

So the total time is

T ~= (12x1) + (12x2) + . . . +(12x(d - 1)) = 12(d - 1)d/2 ~= 6 d^2

We have sigma(M) ~= 2d, so s(M) ~= 3/2 (sigma(M)^2).

=== racheline ===
racheline [https://discord.com/channels/960643023006490684/1084047886494470185/1329499932847243424 16 Jan 2025 12:18 PM EST]:<pre>
for i in {1,2,3}, (3(a+2)+i,b) is <A 3^(2b+2) (23)^a 2 i
(3k+1,n) -> ((2^n-1)*2^k-2,n+k)
(3k+2,n) -> halt
(3k+3,n) -> ((2^n-1)*2^k,n+k)
start from (58,6)

(58,6) -> (3a+1,25) -> (3b+3,a+25) -> (3c+3,a+b+25) -> (3d+2,a+b+c+25) -> halt
where
a = 11010047
b = ((2^25-1)*2^a-5)/3
c = ((2^(a+25)-1)*2^b-3)/3
d = ((2^(a+b+25)-1)*2^c-2)/3
it halts with exactly a+b+c+25+2d+2 = a+b+c+2d+27 ones on the tape (and no other nonzero symbols)
</pre>

=== mxdys ===
mxdys  [https://discord.com/channels/960643023006490684/1259770421046411285/1379877629288644722 4 Jun 2025, 1:41 PM EDT]<pre>
halting shift-overflow bouncer counters

1RB2RA3LA4RB---_2LA3RB3RA1LB3LB
1RB3LA4RB0RB2LA_1LB2LA3LA1RA---

are added to Coq.

I can confirm that the current BB(2,5) champion 1RB3LA4RB0RB2LA_1LB2LA3LA1RA--- halts at

S1
  (24 + ((((2 ^ 5 - 1) * 2 + 1) * 2 ^ 15 - 1) * 16 + 1) / 3 + 4 +
   ((((2 ^ 24 - 1) * 2 + 1) *
     2 ^ (((((2 ^ 5 - 1) * 2 + 1) * 2 ^ 15 - 1) * 16 + 1) / 3) - 1) * 16 + 1) /
   3 + 4 +
   ((((2 ^ (24 + ((((2 ^ 5 - 1) * 2 + 1) * 2 ^ 15 - 1) * 16 + 1) / 3 + 4) - 1) *
      2 + 1) *
     2
     ^ (((((2 ^ 24 - 1) * 2 + 1) *
          2 ^ (((((2 ^ 5 - 1) * 2 + 1) * 2 ^ 15 - 1) * 16 + 1) / 3) - 1) * 16 +
         1) / 3) - 1) * 16 + 3) / 3 + 4 + 1)
  (((((2
       ^ (24 + ((((2 ^ 5 - 1) * 2 + 1) * 2 ^ 15 - 1) * 16 + 1) / 3 + 4 +
          ((((2 ^ 24 - 1) * 2 + 1) *
            2 ^ (((((2 ^ 5 - 1) * 2 + 1) * 2 ^ 15 - 1) * 16 + 1) / 3) - 1) *
           16 + 1) / 3 + 4) - 1) * 2 + 1) *
     2
     ^ (((((2
            ^ (24 + ((((2 ^ 5 - 1) * 2 + 1) * 2 ^ 15 - 1) * 16 + 1) / 3 + 4) -
            1) * 2 + 1) *
          2
          ^ (((((2 ^ 24 - 1) * 2 + 1) *
               2 ^ (((((2 ^ 5 - 1) * 2 + 1) * 2 ^ 15 - 1) * 16 + 1) / 3) - 1) *
              16 + 1) / 3) - 1) * 16 + 3) / 3) - 1) * 16 + 3) / 3 + 3)

where S1 a b := 0^inf 1 10^a 11^b 1 B> 41 0^inf
</pre>