source.bib
Skelet #17 and the fifth Busy Beaver number
1. Description
1.1. Introduction
The busy beaver function is defined to be the maximum number of moves a halting -state -symbol Turing machine makes before it halts. Although there is no general algorithm to compute in general, researchers have long conjectured that , perhaps most recently by Aaronson [bbfrontier].
A massive undertaking by The Busy Beaver Challenge team [bbchallenge] has narrowed down the determination of to showing non-halting of approximately 30 “holdout” machines [bbchallengeholdouts]. Of those machines, there is significant overlap with a different list of 43 holdouts for which Georgi “Skelet” Georgiev claimed to find in 2003 [skelethomepage]: the machine dubbed Skelet #17 [skelet17] is the focus of our paper.
Although most of the 30 holdouts can be grouped into well-known categories, analysis of Skelet #17 has eluded all known attempts at classification. Members of [bbchallenge] are in general agreement that Skelet #17, along with Skelet #1, comprise the two most difficult holdouts to analyze. In this paper, we show that Skelet #17 does not halt (Theorem 1.3).
1.2. Skelet #17
By [savask], is known that Skelet #17 can be described by the following process: begin with the state . Let be the next state after . is defined by the following rules:
-
•
Overflow: If , transition to .
-
•
Halt: If , halt.
-
•
Zero: If and , transition to .
-
•
Halve: If , transition to .
-
•
Increment: If is not in the form specified by any of the above rules, find the rightmost index of with an odd value. Transition to
Remark 1.1.
Note that the conventions of [savask] are slightly different from ours: the precise correspondence is as follows:
-
•
(E1) and (E2) in [savask] correspond to Zero here.
-
•
(E3) in [savask] corresponds to Halt here.
-
•
(O1) in [savask] corresponds to Zero Overflow here.
-
•
(O2), (O3), (O4) and (O5) in [savask] correspond to Increment here.
-
•
(O6) in [savask] corresponds to Halve Increment here.
Definition 1.2.
Given two states and , say that if for some . In this case, define to be the sequence of transition rules that were applied from to obtain .
The goal of this paper is to show that the above process never terminates. In particular, we will establish the following theorem:
Theorem 1.3.
We have for all . Moreover, during this, we use exactly one Overflow rule. As a result, Skelet #17 never halts.
1.3. Formalization
The author originally wrote up a sketch of this paper in 2023. Recently, “Mxdys” has adapted its contents to a formal proof of Skelet #17’s nonhalting [formalproof17], along with formalizing everything else in the program [formalproof]. As a result, we are able to conclude:
Theorem 1.4.
We have .
2. Basics
2.1. State variables
For , let denote the nearest integer to , where we round up if is a half-integer (e.g ).
Definition 2.1.
For , the Gray code of is defined to be , where each digit equals the mod reduction of .
For a state , introduce the following notation, which is specified in order to capture the most important properties of Skelet #17:
-
•
Let denote the number . Here we let , and note that we are not considering in the formation of .
-
•
Let denote the number one less than the size of , i.e. .
-
•
Let be if is odd, and if is even.
-
•
In addition to the three state variables above, let denote the value of the index of , for
Under the transition rules, we may write down how the first three state variables change for each rule that is applied. In particular, one can verify the following table (where the substitutions in a given rule’s row are performed going left to right):
Rule | |||
---|---|---|---|
Overflow | |||
Empty | |||
Halve | |||
Increment | |||
Halt |
The above table does more than just specify how the state variables change with each rule: it also restricts what can be immediately before a given rule is applied. For instance, if is a state for which we Overflow out of, then we must necessarily have and .
2.2. Increments
Define the function
The next proposition states how a state’s coordinates change under a series of increments:
Proposition 2.2.
Suppose we have states and where , such that consists of rules of the form Increment. Denote , and . Then for each we have
Proof.
For , we have , which is precisely the number of Increment rules in . Since decreases after an Increment rule, the claim follows immediately. For , note that by Definition 2.1, the value quantifies how much increases when incrementing the Gray code of to the Gray code of . ∎
3. The speedup
3.1. Conventions
From this section onwards, fix and let . From now on, every state we will consider will satisfy , but not . For and , denote , which is but with incremented by .
3.2. Empty and embanked states
Definition 3.1.
Call a state empty if and , but the next rule applied is not Halt (so in particular the state immediately after is achieved by applying Zero).
If is empty, then let denote the next state after that is empty. Let denote the sequence of rules if exists, and otherwise let denote the sequence of rules after .
Definition 3.2.
Let be an empty state.
-
(1)
Say that is embanked if the non-Increment rules of consist of exactly one Zero rule at the start and exactly two Halve rules elsewhere.
-
(2)
Say that is weakly embanked if the rules of consist of one Zero rule at the start and at least two Halve rules (in particular, there may be arbitrarily many), such that all other rules before the second Halve rule are Increment rules.
-
(3)
Suppose is weakly embanked. For , define (resp. ) to be the value of for the state immediately after (resp. before) the Halve rule is applied in . Let (resp. ) denote the tuple (resp. ). So in particular we have .
In the course of proving Theorem 1.3, we will in fact see that the vast majority of the empty states we consider are embanked. In the first non-embanked empty state we see, an Overflow rule results, at which point an explicit analysis will yield the desired result. It is in this fact that the reason for the term embanked becomes clear: it signifies that flows extremely well as we repeatedly apply , and in particular well enough for us to apply major speedups to the Skelet #17 process.
Example 3.3.
Let . Then is embanked with . Let us spell out in detail: will start at after the first Empty rule, with corresponding state . Here, we have , so we must immediately apply the first Halve rule, which takes to and to , with ensuing state . A series of Increment rules are applied until , where the state is now . Then the second Halve rule is applied to yield , and after a further series of Increment rules we have , which corresponds to the state . The reader is highly encouraged to graph the values of attained in to gain an intuition behind this paper.
Proposition 3.4.
Empty state is weakly embanked if and only if the following conditions hold:
-
(1)
.
-
(2)
.
Proof.
For to be weakly embanked, the sequence must have two Halve rules before any non-Increment rule. To guarantee that the first Halve rule occurs before any non-Increment rule, the variable must decrement to from before the variable decrements to from . This is the same as the first condition.
Assume condition (1) holds, and let be the state immediately after applying the first Halve rule in . To guarantee that the second Halve rule occurs before any non-Increment rule, the variable must decrement from to before the variable increments from to (after which an Overflow rule would have to be applied). We readily compute
so that the desired condition becomes the inequality
Note that is necessarily even (since is empty), so the above inequality becomes
which further simplifies to This is exactly condition (2), so we win. ∎
3.3. Speedup
Lemma 3.5.
Let be an embanked state with , , and choose such that is weakly embanked. Then we have
Proof.
Note that depends on only the indices and of (this immediately implies for ). In particular, influences while influences . Thus, if , then, before the first Halve rule of , we must apply the Increment rule two additional times compared to before the necessary occurs; it follows that . A similar analysis for the states preceding the second Halve rule of yields ∎
Proposition 3.6.
Suppose is an embanked state such that for some , and suppose is weakly embanked. Let , and . Then is in fact embanked, with
Proof.
If , then by Lemma 3.5, . is just with incremented by , and the index will shift to the index upon another application of . Since the indices and are the same for and , we have , hence is embanked with .
The nontrivial cases are . If , then Lemma 3.5 implies that, compared to , the transition acquires exactly two additional Increment rules between the first and second Halve rules, as well as one additional Increment rule after the second Halve rule. Let us analyze what happens to the index for each . Let denote the transition ; this is but with the first transition removed. By Proposition 2.2, we have
noting that (1) the indices shift every time a Halve rule is applied, and (2) all ’s are in fact defined, since Zero adds two extra indices to the state. Moreover, define
which agrees with if is embanked, but will still make sense if is only weakly embanked. Note that will fail to be embanked if and only if ; in this case, for after the second Halve rule, the quantity decrements to before can decrement to , at which point a third Halve rule has to be applied. From the above expressions, we obtain
where the first equality is justified by the fact that by the definition of , and the third equality is justified by verifying that always holds. We learn , and therefore that is embanked. Moreover, we have exactly one index such that ; this is the index for which . Such is characterized by being a half-integer, and this occurs precisely when . The desired claim follows for the case.
If , a completely analogous analysis occurs: we compute
and define
so that for all , we have
As in the case, the fact that immediately implies that is embanked, and in fact positive if and only if is a half-integer, which occurs precisely when . This completes the proof. ∎
In light of Proposition 3.6, we are induced to speed up the function to a new function :
Definition 3.7.
Define the following terms:
-
(1)
For an embanked state such that , define to be the state
where the second equality holds by Proposition 3.6.
-
(2)
Say that an embanked state is rooted embanked if it is the result of applying to some amount of times, i.e. there exists such that .
-
(3)
For , say that a rooted embanked state is -rooted embanked if . Every rooted embanked state is either -rooted embanked or -rooted embanked.
-
(4)
For a state transition of rooted embanked states, let denote the sequence of ’s that were applied to to achieve .
We have the immediate corollary:
Corollary 3.8.
For , let be an -rooted embanked state with , and assume that is weakly embanked. Then we have
so that is -rooted embanked if , and -rooted embanked if .
4. Proof of nonhalting
Proposition 4.1.
Let be a -rooted embanked state such that there exists of odd -adic valuation such that . Then the following hold:
-
(1)
If in denotes the next number after satisfying , then there exists a unique 1-rooted embanked state satisfying , such that .
-
(2)
In the setting of (2), let . Then for .
Proof.
Suppose and are as in the problem statement. In what follows, the quantities and never breach the bounds given by the conditions in Proposition 3.4; combining this with Corollary 3.8, it follows that all -iterates of we consider will be rooted embanked.
We claim that for each , is -rooted embanked with . This follows by induction on : the base case is given, while for the induction step, if satisfies the induction hypothesis, then since , it must necessarily have even valuation; hence by Corollary 3.8, is -rooted embanked, and moreover by Lemma 3.5 we have . This completes the induction. In addition, we also learn that from to , the quantity increments by
When we apply to , we obtain a state such that . Since is odd, it follows by Corollary 3.8 that is -rooted. We claim that for each , is -rooted embanked with . This, again, follows by induction on : the base case is given, while for the induction step, if satisfies the induction hypothesis, then since , it must necessarily have even valuation; hence by Corollary 3.8, is -rooted embanked, and moreover by Lemma 3.5 we have . This completes the induction. In addition, we also learn that from to , the quantity decrements by
Finally, applying to yields a state such that , and is -rooted embanked, which proves (1). This extra application of also increments by , so in total, has incremented by , while has decremented by ; this proves (2). ∎
Starting with , a brief computation yields and . Thus, applying to five times yields a -rooted embanked state such that . Hence, by inducting on to reach , Proposition 4.1 and Proposition 3.4 imply the following corollary:
Corollary 4.2.
There exists a rooted embanked state such that .
4.1. Counting increments
For rooted embanked states , let denote the number of in such that .
Proposition 4.3.
Suppose we are in the setting of Proposition 4.1, with , , and defined as before. Then, for all , we have .
Proof.
For a statement , define to be if is true, and if is false. Fix a . By Corollary 3.8, we have
where the third equality is using the fact that and have odd -adic valuations, but every number in between has even -adic valuation. ∎
4.2. Endgame
Our setup for the end of the proof is the sequence of state transitions , where , and are all rooted embanked states satisfying , and . In particular, we have since Proposition 4.1(2) guarantees that will satisfy the bounds in Proposition 3.4 so that is weakly embanked, and then Corollary 3.8 implies that is embanked. Also, we have . An explicit computation yields
It follows that
Since moving from to increments by , we obtain
Observe that fails the conditions of Proposition 3.4, and so it will not make sense to apply anymore. We resort to an explicit analysis from here. From the state , applying Zero yields
after which applying Increment rules yields
and now we Halve to obtain
Applying Increment rules yields
after which we are forced to apply an Overflow rule to get
By Proposition 3.4, is weakly embanked, and one may compute that . Further computing the state formed after the second Halve rule of shows that is in fact embanked with . By (1), applying to yields
By Lemma 3.5, we have ; therefore, Proposition 3.6 tells us that . Hence,
which is just .