On his blog post, Wythagoras describes a bound for S(7), derived from Pavel Kropitz's current (as of 2010) 6 states and 2 symbols recold holder. On Pascal Michel's Behavior of busy beavers page, Michel notes that the machine with the initial configuration ...0(A0)110... runs at least 10^10^10^10^10^7 steps. This blog post gives a proof for the claim.
We begin by filling the gaps from the transition table shown in Pascal Michel's page.
Let C(n) = ...0(A0)1n0...
Then we have:
| Before | Steps | After |
|---|---|---|
| ...0(A0)0... | 29 | C(9) |
| C(3k+1) | 3k+3 | ...0111(011)k(H0)0... |
| C(9k+6) | (125*16k+2-575*4k+2+228k-2226)/27 | C((50*4k+1-59)/3) |
| C(9k+9) | (125*16k+2+325*4k+2+228k-2289)/27 | C((50*4k+1-11)/3) |
| C(9k+12) | (125*16k+2+325*4k+2+228k-912)/27 | C((50*4k+1+1)/3) |
| C(9k+11) | (2401*16k+2-5635*4k+2+1140k-11226)/135 | C((98*4k+1-59)/3) |
| C(9k+14) | (2401*16k+2+3185*4k+2+1140k-11541)/135 | C((98*4k+1-11)/3) |
| C(9k+17) | (2401*16k+2+3185*4k+2+1140k-4656)/135 | C((98*4k+1+1)/3) |
We start at C(2), which becomes C(11) after 36 steps.
C(11) becomes C(111) after 3802 steps.
Since 111 = 9*11+12, C(111) becomes \(C((50 \times 4^{12}+1)/3) = C(279620267)\) after 20849999082655348 steps.
Since 279620267 = 9*31068917 + 14, C(279620267) becomes \(C((98 \times 4^{31068918}-11)/3)\) after a large number of steps.
Before we continue further, let's show the following lemma:
Euler's theorem gives \(2^{\phi(3^n)} = 2^{2 \times 3^{n-1}} \equiv 1 \pmod{3^n}\). Therefore \(4^{3^{n-1}} \equiv 1 \pmod{3^n}\).
Combining with the above formulas yields the result that the modulo is divided by 9 for each "layer". Since we are showing that \(S(7) > 10^{10^{10^{10^{10^7}}}}\), and \((98 \times 4^{31068918}-11)/3 \approx 10^{10^7}\), we have 3 more "layers" to go. Therefore starting from modulo \(3^8 = 6561\) would be an acceptable choice.
We continue from where we left off, using modulo 6561:
\(31068918 \equiv 2583 \pmod{6561}\)
\(4^{31068918} \equiv 4^{2583} \equiv 16093 \pmod{19683}\)
\((98 \times 4^{31068918}-11)/3 \equiv 525701 \equiv 821 = 9 \times 90 + 11 \pmod{6561}\)
So the next case is C(9k+11) -> C((98*4k+1-59)/3). Letting \(A = ((98 \times 4^{31068918}-11)/3-11)/9\) we have:
\(A+1 \equiv 91 \pmod{729}\)
\(4^{A+1} \equiv 4^{91} \equiv 1246 \pmod{2187}\)
\((98 \times 4^{A+1}-59)/3 \equiv 40683 \equiv 588 = 9 \times 64 + 12 \pmod{729}\)
The next case is C(9k+12) -> C((50*4k+1+1)/3). Again, letting \(B = ((98 \times 4^{A+1}-59)/3-12)/9\) we have:
\(B+1 \equiv 65 \pmod{81}\)
\(4^{B+1} \equiv 4^{65} \equiv 43 \pmod{243}\)
\((50 \times 4^{B+1}+1)/3 \equiv 717 \equiv 69 = 9 \times 7 + 6 \pmod{81}\)
Next case is C(9k+6) -> C((50*4k+1-59)/3). Letting \(C = ((50 \times 4^{B+1}+1)/3-6)/9\):
\(C+1 \equiv 8 \pmod{9}\)
\(4^{C+1} \equiv 4^{8} \equiv 7 \pmod{27}\)
\((50 \times 4^{C+1}-59)/3 \equiv 97 \equiv 7 = 3 \times 2 + 1 \pmod{9}\)
The next case is C(3k+1) -> ...0111(011)k(H0)0... where the machine finally halts. Letting \(D = ((50 \times 4^{C+1}-59)/3-1)/3\), the machine halts after 3D+3 steps, leaving 2D+3 1's on the tape.
In summary:
| Tape | Steps from previous row |
|---|---|
| C(2) | |
| C(11) | 36 |
| C(111) | 3802 |
| C(279620267) | 20849999082655348 |
| \(C((98 \times 4^{31068918}-11)/3)\) = C(9A+11) | \((2401 \times 16^{k+2}+3185 \times 4^{k+2}+1140k-11541)/135\) where k = 31068917 |
| \(C((98 \times 4^{A+1}-59)/3)\) = C(9B+12) | \((2401 \times 16^{A+2}-5635 \times 4^{A+2}+1140A-11226)/135\) |
| \(C((50 \times 4^{B+1}+1)/3)\) = C(9C+6) | \((125 \times 16^{B+2}+325 \times 4^{B+2}+228B-912)/27\) |
| \(C((50 \times 4^{C+1}-59)/3)\) = C(3D+1) | \((125 \times 16^{C+2}-575 \times 4^{C+2}+228C-2226)/27\) |
| ...0111(011)D(H0)0... (total 2D+3 1's) | 3D+3 |
The resulting lower bounds are:
\[\Sigma(7) \geq 2D+3 > 10^{10^{10^{10^{18705352}}}}\]
\[S(7) > (125 \times 16^{C+2}-575 \times 4^{C+2}+228C-2226)/27 > 10^{10^{10^{10^{18705352}}}}\]
In addition, \(10^{10^{10^{10^{18705352}}}} > 10^{10^{10^{10^{10000000}}}} = 10^{10^{10^{10^{10^7}}}}\). The proof is finally complete.
Edit: Slightly corrected bounds with help from somebody I believe is Pascal Michel