5-state busy beaver winner

The 5-state busy beaver winner is the Turing machine whose step count determines BB(5). Up to permutations, that machine is 1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA (bbch), which halts after 47176870 steps with 4098 ones on the tape. It was first reported on by Heiner Marxen and Jürgen Buntrock in February 1990, and the high-level rules were first demonstrated by Michael Buro in November 1990.

	0	1
A	1RB	1LC
B	1RC	1RB
C	1RD	0LE
D	1LA	1LD
E	1RZ	0LA

The transition table of the 5-state busy beaver winner.

Analysis

Let $g(x):=0^{\mathrm{\infty }}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}{1}^x{0}^{\mathrm{\infty }}$. Then, $$\begin{array}{lll}g(3x)& \stackrel{5x^2+19x+15}{\to }& g(5x+6),\\ g(3x+1)& \stackrel{5x^2+25x+27}{\to }& g(5x+9),\\ g(3x+2)& \stackrel{6x+12}{\to }& 0^{\mathrm{\infty }}1\text{<mrow data-mjx-texclass="ORD">Z<mo>></mo></mrow>}01001^{x+1}10^{\mathrm{\infty }}.\end{array}$$

Proof

Consider the configuration $C(m,n):=0^{\mathrm{\infty }}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}{1}^{m}001^{n}10^{\mathrm{\infty }}$. After one step this configuration becomes $0^{\mathrm{\infty }}1\text{<mrow data-mjx-texclass="ORD">B<mo>></mo></mrow>}{1}^{m}001^{n}10^{\mathrm{\infty }}$. We note the following shift rule: $$\begin{array}{c}\text{<mrow data-mjx-texclass="ORD">B<mo>></mo></mrow>}{1}^a\stackrel{a}{\to }{1}^a\text{<mrow data-mjx-texclass="ORD">B<mo>></mo></mrow>}\end{array}$$ Using this shift rule, we get $0^{\mathrm{\infty }}{1}^{m+1}\text{<mrow data-mjx-texclass="ORD">B<mo>></mo></mrow>}001^{n}10^{\mathrm{\infty }}$ after $m$ steps. If $n=0$, then we get $0^{\mathrm{\infty }}{1}^{m+4}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}10^{\mathrm{\infty }}$ four steps later. Another shift rule is needed here: $$\begin{array}{c}{1}^{3a}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}\stackrel{3a}{\to }\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}001^a\end{array}$$ In this instance, $\lfloor \frac{m+4}{3}\rfloor$ is substituted for $a$, which creates three different scenarios depending on the value of $m$ modulo 3. They are as follows:

1. If $m+4\equiv 0(\mathrm{mod}3)$, then in $m+4$ steps we arrive at $0^{\mathrm{\infty }}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}001^{(m+4)/3}10^{\mathrm{\infty }}$, which is the same configuration as $C(0,\frac{m+4}{3})$.
2. If $m+4\equiv 1(\mathrm{mod}3)$, then in $m+3$ steps we arrive at $0^{\mathrm{\infty }}1\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}001^{(m+3)/3}10^{\mathrm{\infty }}$, which in five steps becomes $0^{\mathrm{\infty }}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}111001^{(m+3)/3}10^{\mathrm{\infty }}$, equal to $C(3,\frac{m+3}{3})$.
3. If $m+4\equiv 2(\mathrm{mod}3)$, then in $m+2$ steps we arrive at $0^{\mathrm{\infty }}11\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}001^{(m+2)/3}10^{\mathrm{\infty }}$, which in three steps halts with the configuration $0^{\mathrm{\infty }}1\text{<mrow data-mjx-texclass="ORD">Z<mo>></mo></mrow>}01001^{(m+2)/3}10^{\mathrm{\infty }}$, for a total of $2m+10$ steps from $C(m,0)$.

Returning to $0^{\mathrm{\infty }}{1}^{m+1}\text{<mrow data-mjx-texclass="ORD">B<mo>></mo></mrow>}001^{n}10^{\mathrm{\infty }}$, if $n\ge 1$, then in three steps it changes into $0^{\mathrm{\infty }}{1}^{m+3}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>D</mrow>}1001^{n-1}10^{\mathrm{\infty }}$. Here we can make use of one more shift rule: $$\begin{array}{c}{1}^a\text{<mrow data-mjx-texclass="ORD"><mo><</mo>D</mrow>}\stackrel{a}{\to }\text{<mrow data-mjx-texclass="ORD"><mo><</mo>D</mrow>}{1}^a\end{array}$$ Doing so takes us to $0^{\mathrm{\infty }}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>D</mrow>}{1}^{m+4}001^{n-1}10^{\mathrm{\infty }}$ in $m+3$ steps, which after one step becomes the configuration $0^{\mathrm{\infty }}\text{<mrow data-mjx-texclass="ORD"><mo><</mo>A</mrow>}{1}^{m+5}001^{n-1}10^{\mathrm{\infty }}$, equal to $C(m+5,n-1)$. To summarize: $$\begin{array}{c}C(m,n)\stackrel{2m+8}{\to }C(m+5,n-1)\text{ if }n\ge 1.\end{array}$$ We have $g(x)=C(x-1,0)$. As a result, if $x\equiv 0(\mathrm{mod}3)$, we then get $C(0,\frac{1}{3}x+1)$ and the above rule is applied until we reach $C(\frac{5}{3}x+5,0)$, equal to $g(\frac{5}{3}x+6)$, in $\sum _{i=0}^{x/3}(2\times 5i+8)=\frac{5}{9}{x}^2+\frac{13}{3}x+8$ steps for a total of $\frac{5}{9}{x}^2+\frac{19}{3}x+15$ steps from $g(x)$ (with $g(0)$ we see the impossible configuration $C(-1,0)$, but it reaches $g(6)$ in 15 steps regardless). However, if $x\equiv 1(\mathrm{mod}3)$, we then get $C(3,\frac{x+2}{3})$ which reaches $C(3+\frac{5(x+2)}{3},0)$, equal to $g\left(\frac{5x+22}{3}\right)$, in $\frac{5}{9}{x}^2+\frac{47}{9}x+\frac{74}{9}$ steps ($\frac{5}{9}{x}^2+\frac{65}{9}x+\frac{173}{9}$ steps total).

The information above can be summarized as $$g(x)\to \{\begin{array}{ll}g(\frac{5}{3}x+6)& \text{if }x\equiv 0(\mathrm{mod}3),\\ g\left(\frac{5x+22}{3}\right)& \text{if }x\equiv 1(\mathrm{mod}3),\\ 0^{\mathrm{\infty }}1\text{<mrow data-mjx-texclass="ORD">Z<mo>></mo></mrow>}01001^{(x+1)/3}10^{\mathrm{\infty }}& \text{if }x\equiv 2(\mathrm{mod}3).\end{array}$$ Substituting $x\leftarrow 3x$, $x\leftarrow 3x+1$, and $x\leftarrow 3x+2$ to each of these cases respectively gives us our final result.

In effect, the halting problem for the 5-state busy beaver winner is about whether repeatedly applying the function $f(n)=3n+6-4\lfloor \frac{n}{3}\rfloor$ eventually produces a value of $n$ that is congruent to 2 modulo 3.

Trajectory

The initial blank tape represents $g(0)$, and the Collatz-like rules are iterated 15 times before halting: $$\begin{array}{l}\begin{array}{llllllllll}g(0)& \stackrel{15}{\to }& g(6)& \stackrel{73}{\to }& g(16)& \stackrel{277}{\to }& g(34)& \stackrel{907}{\to }& g(64)& \stackrel{2757}{\to }\\ g(114)& \stackrel{7957}{\to }& g(196)& \stackrel{22777}{\to }& g(334)& \stackrel{64407}{\to }& g(564)& \stackrel{180307}{\to }& g(946)& \stackrel{504027}{\to }\\ g(1584)& \stackrel{1403967}{\to }& g(2646)& \stackrel{3906393}{\to }& g(4416)& \stackrel{10861903}{\to }& g(7366)& \stackrel{30196527}{\to }& g(12284)& \stackrel{24576}{\to }\end{array}\\ 0^{\mathrm{\infty }}1\text{<mrow data-mjx-texclass="ORD">Z<mo>></mo></mrow>}01001^{4095}10^{\mathrm{\infty }}\end{array}$$