Big Number Competition: Proof Edition

[Europe2048]

Say a number bigger than the last.

Rules:

• You must provide a proof that your number is bigger than the last.
• No infinities, uncomputable functions, or anything else that make the game boring.
• Very large or small increments are not allowed.
• If you used a function in one entry, nobody can use it anymore.

I'll start:
A googol.
Since this is the first number, no proof is needed.

[PkmnQ]

Define F as:
F(2k+1, n) = n+k
F(2k, n) = F(k, F((2n+1)k, n))

F(16, 16) > 10^100
Will give proof tomorrow but it's still small enough to be calculatable in Python and can be easily seen to be greater than a googol that way

[TonyBrown148]

I'll analyze PkmnQ's function before I make my own.
let g(k, n, x)=f(2^k (2n+1), x)
Then g(0, n, x)=n+x
g(k+1, n, x)=g(k, n, g(k, 2nx+n+x, x))

[Europe2048]

F has already been used before by PkmnQ.

[TonyBrown148]

F has already been used before by PkmnQ.

Did you read the first sentence? That post is NOT my submission.
Anyway, here's my submission:
ß_4(4), where ß_4 is the 4th function of the Eszett Hierarchy
Proof:
It can be verified easily that f(16,16)=246195764991809400615851757409678501609112226596897318241965487623462435376542940541565076088135382696945983127005479150515157329970534633628937426960395539934729289796096<10^1000
Then, 10^1000<16^1024=2^4096=2^2^12<2^2^16=2^2^2^2^2=2^^5<2^^65536=2^^2^^2^^2=2^^^4=ß_4(4)

[PkmnQ]

Let's just quickly get rid of the factorials for no reason

Define supercoolfactorialsequence!!!_n as follows:
supercoolfactorialsequence!!!₀ = 3
supercoolfactorialsequence!!!_n+1 = supercoolfactorialsequence!!!_n!

My submission is supercoolfactorialsequence!!!_M82589933. (yes, I'm also eliminating Mersenne numbers, why not. Hey wait a minute, they're about to announce a new prime?)

First, notice that supercoolfactorialsequence!!!_n > 2↑↑n + 1:

• supercoolfactorialsequence!!!₀ = 3 > 2 = 2↑↑0 + 1
• supercoolfactorialsequence!!!_n+1 = supercoolfactorialsequence!!!_n! > (2↑↑n + 1)! = product of [2, 3, 4, 5, ...] (2↑↑n elements) >= product of [3, 2, 2, 2, ...] (2↑↑n elements) = 3/2 * 2↑↑(n+1) >= 2↑↑(n+1) + 1

Thus, ß_4(4) = 2↑↑65536 < 2↑↑65536 + 1 < supercoolfactorialsequence!!!₆₅₅₃₆ < supercoolfactorialsequence!!!_M82589933.

[PkmnQ]

...did I really have to post that just hours before they revealed M136279841?