Pavel has found a 3state 4symbol TM which can compute an “Ackermannlevel” function and halts with exactly
[(2 uparrow^{15} 5) + 14]nonzero symbols on the tape. With a number this large, Knuth uparrow format is becoming a bit awkward, so we can approximate this bound as:
[BB(3, 4) > Ack(14)]where (Ack(14)) is the 14th Ackermann number defined as:
[Ack(n) = n uparrow^n n]As far as I know, this is the first TM found “in the wild” that is able to simulate an Ackermannlevel function.
The Machine
1RB3LB1RZ2RA_2LC3RB1LC2RA_3RB1LB3LC2RC
0  1  2  3  

A  1RB  3LB  1RZ  2RA 
B  2LC  3RB  1LC  2RA 
C  3RB  1LB  3LC  2RC 
It halts with final configuration
[0^infty ;; 3^{2 g_{15}^{3}(0) + 1} ;; 2^{16} ;; 1 ;; text{ Z> } ;; 0^infty]which leaves exactly
[sigma = 2 g_{15}^{3}(0) + 18 = (2 uparrow^{15} 5) + 14]nonzero symbols on the tape. (The function (g_k(m)) will be defined below).
Attribution
This TM was discovered by Pavel Kropitz (@uni) and shared on Discord on 25 Apr 2024. His code was not able to specify a humanreadable bound on the TM score and it was simply specified as Halt(SuperPowers(13))
indicating 13 layers of inductive rules needed to prove it. He began a validation of this result using my new “Inductive Proof Validator” (see discussion at end of article).
I completed this validation and was able to extract the precise definition of (g_k^n(m)) on 20 May 2024 (Discord link) and used that to get a bound of (sigma > 2 uparrow^{15} 3).
Matthew House (@LegionMammal978) discovered on 22 May 2024 (Discord link) the remarkably simple closed form evaluation:
[g_k^n(0) = frac{ 2 uparrow^k (n+2) }{2} – 2]which led me to rewrite this article with exact values for (sigma)!
Analysis
Let
[B(k, n, m) = 0^infty ;; 3^{2m+1} ;; 2^k ;; text{ A> } ;; 1^n]then we can prove that
[begin{array}{lcl}0^infty ;; text{A>} ;; 0^infty & xrightarrow{241} & B(16, 3, 0) ;; 2 ;; 0^infty \
B(k, n, m) & to & B(k, 0, g_{k1}^n(m)) & text{if } k ge 1 \
B(k, 0, m) ;; 2 & xrightarrow{1} & 0^infty ;; 3^{2m+1} ;; 2^k ;; 1 ;; text{Z>} \
end{array}]
where
[begin{array}{l}g_0(m) & = & m + 1 \
g_{k+1}(m) & = & g_k^{2m+2}(0) \
end{array}]
Proof by Double Induction
This TM is remarkably simple in the sense that its behavior can be almost completely described by one single rule:
[B(k, n, m) to B(k, 0, g_{k1}^n(m))]but that rule is a whopper requiring double induction to prove!
Lemma 1: For all (k ge 1):
[3 ;; 2^k ;; text{Corollary 2: For all (k ge 1, m ge 0):
[3^m ;; 2^k ;; text{Proofs left as an exercise to the reader.
Theorem 3: For all (k ge 1, n ge 0, m ge 0):
[B(k, n, m) to B(k, 0, g_{k1}^n(m))]Proof by Induction on (k):
 Base Case ((k = 1))
 Goal: (forall n,m ge 0: B(1, n+1, m) to B(1, 0, g_0^{n+1}(m)))
 Proof by induction on (n). Left as an exercise to the reader.
 Induction Case
 Assume (H_k: forall n,m ge 0: B(k, n, m) to B(k, 0, g_k^n(m)))
 Goal: (forall n,m ge 0: B(k+1, n, m) to B(k+1, 0, g_{k+1}^n(m)))

Proof by induction on (n):
 Base Case ((n = 0))
 Trivially true because (g_{k1}^0(m) = m), so (B(k, n, m) = B(k, 0, g_{k1}^n(m)))
 Induction Case
 Assume (H_n: forall m ge 0: B(k+1, n, m) to B(k+1, 0, g_{k+1}^n(m)))
 Goal: (forall m ge 0: B(k+1, n+1, m) to B(k+1, 0, g_{k+1}^{n+1}(m)))
 Base Case ((n = 0))
B(k+1, n+1, m) & = &
0^infty ;; 3^{2m+1} ;; 2^{k+1} ;; text{A>} ;; 1^{n+1} \
& xrightarrow{1} &
0^infty ;; 3^{2m+1} ;; 2^{k+1} ;; text{} ;; 1^{2m+2} ;; 3 ;; 1^n \
& = & B(k, 2m+2, 0) ;; 3 ;; 1^n \
& to & B(k, 0, g_k^{2m+2}(0)) ;; 3 ;; 1^n
& text{by Ind. Hyp. } H_k \
& = &
0^infty ;; 3^{g_k^{2m+2}(0)} ;; 2^k ;; text{A>} ;; 3 ;; 1^n \
& xrightarrow{1} &
0^infty ;; 3^{g_k^{2m+2}(0)} ;; 2^{k+1} ;; text{A>} ;; 1^n \
& = & B(k+1, n, g_k^{2m+2}(0)) = B(k+1, n, g_{k+1}(m)) \
& to & B(k+1, 0, g_{k+1}^n(g_{k+1}(m)))
& text{by Ind. Hyp. } H_n \
& = & B(k+1, 0, g_{k+1}^{n+1}(m)) \
end{array}]
QED
Exact Values
Through what appears to be a remarkable series of coincidences, there is a relatively simple closed form evaluation of (g_k) using only Knuth uparrows and arithmetic:
Theorem: For all (k ge 0, m ge 0):
[2 g_{k+1}(m) + 4 = 2 uparrow^k (2m+4)](where we define (a uparrow^0 b = ab))
Proof by Induction on (k):
 Base case ((k = 0)):
g_1(m) & = & g_0^{2m+2}(0) & = & 2m+2 \
2 g_1(m) + 4 & = & 2 (2m+2) + 4 & = & 4m + 8 & = & 2 uparrow^0 (2m+4) \
end{array}]
 Inductive case: Assume (forall m ge 0: 2 g_{k+1}(m) + 4 = 2 uparrow^k (2m+4)):
2 g_{k+1}(m) + 4 & = & 2 uparrow^k (2m+4) \
2 g_{k+1}^n(m) + 4 & = & (2 uparrow^k)^n (2m+4) \
2 g_{k+2}(m) + 4 & = & g_{k+1}^{2m+2}(0) = (2 uparrow^k)^{2m+2} 4 = (2 uparrow^k)^{2m+2} (2 uparrow^k 2) \
& = & 2 uparrow^{k+1} (2m+4) \
end{array}]
QED
Note: This depends upon the coincidence that (2 uparrow^k 2 = 4) for all (k). If the parameters had been slightly different and we’d ended up with ((2 uparrow^k)^{2m+2} 5) above, I don’t think it would have been possible to get a closed form expression.
Corollary: For all (k ge 0, n ge 0):
[2 g_k^n(0) + 4 = 2 uparrow^k (n+2)]From which it follows directly that:
[sigma = 2 g_{15}^{3}(0) + 18 = (2 uparrow^{15} 5) + 14]Permutations
[begin{array}{lcl}0^infty ;; text{B>} ;; 0^infty & xrightarrow{86} & B(7, 3, 0) ;; 2 ;; 0^infty \
0^infty ;; text{C>} ;; 0^infty & xrightarrow{20} & B(1, 3, 0) ;; 2 ;; 0^infty \
end{array}]
Therefore, we can see that if we switch to:
 Starting in state
B
, the TM halts with a score of (sigma_B = 2 g_6^3(0) + 9 = (2 uparrow^6 5) + 5)  Starting in state
C
, the TM halts with a score of (sigma_C = 2 g_0^3(0) + 3 = (2 uparrow^0 5) – 1 = 9) (which it does at step 72).
This first permutation (start state B
) is another top BB(3, 4) TM. Converted into TNF it is:
1RB3RB1LC2LA_2LA2RB1LB3RA_3LA1RZ1LC2RA
0  1  2  3  

A  1RB  3RB  1LC  2LA 
B  2LA  2RB  1LB  3RA 
C  3LA  1RZ  1LC  2RA 
Not Collatz
One interesting thing about this TM is how surprisingly simple it is. For example, the fact that it does not have any Collatzlike rules (rules which act differently depending on the remainder of some value). Is this the end of the domination of Collatzlike TMs? It is far too early to know, but my guess is that there are Collatzlike Ackermannlevel TMs waiting for us, but we are not seeing them right away because of selection bias. Perhaps this was the first Ackermannlevel TM found because it is simple enough to be proven halting without having to implement modular arithmetic on Ackermannlevel functions.
Inductive Proof Validator
This TM was the perfect test case for an “inductive proof” validator I am currently developing. The goal of this project is to develop a standardized certificate format for “inductive proofs” (an umbrella term for all the sort of forwardreasoning, rulebased analyses that are ubiquitous on this blog). The idea is that anyone with an “inductive decider” could write out their rules in this format and then this validator can check these proofs. The system is still very clunky and not ready for prime time, but I have been able (with a little elbow grease) to use it to prove the behavior of many TMs including this one.