Folkman's_Number
Proving the upper bound of G(1) is actually quite easy. Simply expand G(1):
3^^^^3 = 3^^^(3^^^3)
Folkman's Number of 2^^^(2^901) is less than 3^^^(3^^^3) because 2<3 and 2^901 < 3^^^3.
The latter inequality can be demonstrated as follows:
2^901 < 3^7,625,597,484,987 = 3^3^3^3 = 3^^4 < 3^^7,625,597,484,987 = 3^^3^3^3 = 3^^3^^3 = 3^^^3
Proving the lower bound of a greagol is much more difficult. One reason for expecting greagol to be smaller is that it is approximately 2^^^100 << 2^^^(2^901). The complication is that, in fact, a greagol is larger than 10^^^100 (Jonathan Bowers' gaggol). The reason for this is 10^^^100 = E1#1#100 < E100#100#100. So we know greagol > 2^^^100. The good news is that we have a lot of slack here, so we don't have to be that precise with our overestimate to prove Folkman's Number is still much larger.
We can begin with the following:
E100#100#100 = E100#(E100#100#99) < E10,000,000,000#(E100#100#99) = E10^10#(E100#100#99) = E1#(2+E100#100#99) = E1#(2+E100#(E100#100#98)) < E1#(E102#(E100#100#98)) <
E1#(E10^10#(E100#100#98)) = E1#(E1#(2+E100#100#98) = E1#(E1#(2+E100#(E100#100#97))) <
E1#(E1#(E102#(E100#100#97))) < E1#(E1#(E1#(E102#(E100#100#96)))) < ...
< E1#(E1#( ... (E1#(E1#(E102#(E100#100#1)))) ... )) w/98 E1#s = E1#(E102#(E100#100))#98 <
E1#(E10^10#(E100#100))#98 = E1#(E1#(2+E100#100))#98 = E1#(2+E100#100)#99 <
E1#(E102#100)#99 < E1#(E10^10#100)#99 = E1#(E1#102)#99 = E1#102#100
So greagol < E1#102#100. This still isn't good enough for us to directly compare it to Folkman's Number but it gets a little easier from here. Next we need to turn the second argument to 1. So we observe:
E1#102#100 < E1#10^^10#100
Now observe E1#1#102 = E1#(E1#1#101) = E1#(E1#(E1#1#100)) = E1#(E1#( ... (E1#1#1) ... )) w/102 E1#s = E1#(E1#(E1#1#1))#100 = E1#(E1#(E1))#100 = E1#(E1#10)#100 = E1#10^^10#100.
Thus E1#10^^10#100 = E1#1#102.
So greagol < E1#1#102 = 10^^^102. Not bad. We aren't even anywhere close to Folkman's Number yet. Next we need to convert the base of 10 to 2, so that comparison becomes readily apparent.
To do this we can do the following:
10^^^102 < 16^^^102 = 16^^16^^16^^ ... ^^16^^16 w/102 16s.
16 = 2^4 = 2^2^2 = 2^^3. 16^^2 = (2^4)^(2^4) = 2^(4*2^4) = 2^(2^2*2^4) = 2^2^6 < 2^2^16 = 2^2^2^2^2 = 2^^5.
16^^3 = 16^16^^2 < 16^2^^5 = (2^4)^2^2^^4 = 2^(4*2^2^^4) = 2^2^(2+2^^4) < 2^2^(2^^5) = 2^^7.
(Induction)
Let 16^^k < 2^^(2k+1)
16^^(k+1) = 16^16^^k < 16^2^^(2k+1) = (2^4)^2^2^^(2k) = 2^2^(2+2^^(2k)) < 2^2^2^^(2k+1) = 2^^(2k+3).
Since 2(k+1)+1 = 2k+3, it follows inductively that:
16^^n < 2^^(2n+1)
If n is a positive integer than it also follows that:
2^^(2n+1) < 2^^(4n)
So
16^^n < 2^^(4n) [Lemma 1 or L1 for short]
This is a gross overestimate, but as you'll see shortly, it makes little difference. We'll still fall vastly short of Folkman's Number.
(Note: when working with hyper-operators my default order of operations is to work from right to left regardless of hyper-operator rank.)
16^^16 < 2^^64 [via L1] < 2^^65,536 = 2^^2^^4 = 2^^2^^2^^2 = 2^^^4
16^^^3 = 16^^16^^16 < 16^^2^^64 < 2^^(4*2^^64) [L1] < 2^^2^^65 < 2^^2^^65,536 = 2^^2^^2^^4 = 2^^2^^2^^2^^2 = 2^^^5
16^^^4 = 16^^16^^^3 < 16^^2^^^5 < 2^^(4*2^^^5) [L1] < 2^^2^^^6 < 2^^^7
16^^^5 = 16^^16^^^4 < 16^^2^^^7 < 2^^(4*2^^^7) [L1] < 2^^2^^^8 < 2^^^9
(Induction)
Let 16^^^k < 2^^^(2k-1)
16^^^(k+1) = 16^^16^^^k < 16^^2^^^(2k-1) < 2^^(4*2^^^(2k-1)) < 2^^2^^^(2k) = 2^^^(2k+1)
Since 2(k+1)-1 = 2k+1, it follows inductively that:
16^^^n < 2^^^(2n-1) : n>2 & n=Z+
Notice the condition n>2. We'll make this upper bound even worse so that we can include all positive integers as cases:
2^^^(2n-1) < 2^^^(2n) < 2^^^(4n) : n=Z+
Now observe 16^^^1 = 16 < 2^^^4 since 2^^^4 = 2^^2^^2^^2 = 2^^2^^4 = 2^^65,536 >> 2^65,536 > 2^4 = 16.
16^^^2 = 16^^16 < 2^^^4 < 2^^^8.
So we can now generalize to all cases and say:
16^^^n < 2^^^(4n) : n=Z+ [Lemma 2 or L2 for short]
Thus:
16^^^102 < 2^^^408 [L2]
We thus conclude our lower-bound proof:
greagol = E100#100#100 < E1#102#100 < E1#1#102 = 10^^^102 < 16^^^102 < 2^^^408 <
2^^^65,536 = 2^^^(2^16) << 2^^^(2^901) = Folkman's Number
:: greagol << Folkman's Number