Golf a number bigger than TREE(3) The function TREE(k) gives the length of the longest sequence of trees T1, T2, ... where each vertex is labelled with one of k colours, the tree Ti has at most i vertices, and no tree is a minor of any tree following it in the sequence.

TREE(1) = 1, with e.g. T1 = (1).

TREE(2) = 3: e.g. T1 = (1); T2 = (2)--(2); T3 = (2).

TREE(3) is a big big number. Even bigger than Graham's number. Your job is to output a number even bigger than it!

This is a code-golf so the goal is to write the shortest program in any language that deterministically outputs a number bigger than or equal to TREE(3) (to the stdout).


You aren't allowed to take input. 
Your program must eventually terminate but you can assume the machine has infinite memory.
You might assume your language's number type can hold any finite value but need to explain how this exactly works in your language (ex: does a float have infinite precision?)   


Infinities are not allowed as output.
Underflow of a number type throws an exception. It does not wrap around.

Because TREE(3) is such a complex number you can use the fast growing hierarchy approximation fϑ(Ωω ω)+1(3) as the number to beat. 
You need to provide an explanation of why your number is so big and an ungolfed version of your code to check if your solution is valid (since there is no computer with enough memory to store TREE(3))


Note: None of the answers currently found here work.

Why is TREE(3) so big?
New Ruby, 135 bytes, >> Hψ(φ3(Ω+1))(9)

where H is the Hardy hierarchy, ψ is an extended version of Madore's OCF (will explain below) and φ is the Veblen function.

Try it online!

f=-&gt;a,n,b=a{c,d,e=a;a==c ?a-1:e ?a==a-[0]?[[c,d,f[e,n,b]],d-1,c]:c:[n&lt;1||c==0?n:[f[c||b,n-1]],n,n]};h=[],k=9,k;h=f[h,p(k*=k)]while h!=0


Ungolfed: (using functions, not lambdas)

def f(a,n,b)
  c,d,e = a
  if a == c
    return a-1
  elsif e
    if a == a-[0]
      return [[c,d,f(e,n,b)],d-1,c]
    else
      return c
    end
  else
    x = c || b
    if n &lt; 1 || c == 0
      return [n,n,n]
    else
      return [f(x,n-1,x),n,n]
    end
  end
end

k = 9
h = [[],k,k]
while (h != 0) do
  k *= k
  p k
  h = f(h,k,h)
end


Madore's extended OCF:



And (crudely) Veblen's phi function:



Explanation without ordinals: 

f(a,n,b) reduces an array recursively. (if no third argument given, it takes the first argument twice.)
f(k,n,b) = k-1, k is a positive int.
f([c,d,0],n,b) = f([c,0,e],n,b) = c
f([c,d,e],n,b) = [[c,d,f(e,n,b)],d-1,c], d ≠ -1 and c ≠ 0

f([a],0,b) = [0,0,0]
f([0],n,b) = [n,n,n]
f([],n,b) = f([b],n,b)
f([a],n,b) = [f[a,n-1,a],n,n]


My program initiates k = 9, h = [[],9,9]. It then applies k = k*k and h = f(h,k) until h == 0 and outputs k.

Explanation with ordinals:

Ordinals follow the following representation: n, [], [a], [a,b,c], where n,d is a natural number and a,c are all ordinals.
x = Ord(y) if y is the syntactic version of x.
a[n,b] = Ord(f(a,n))
ω = Ord([0]) = Ord(f([a],-1,b))
n = Ord(n)
Ω = Ord([])
ψ'(a) = Ord([a])
ψ'(a)[n] = Ord(f([a],n))
φ(b,c) ≈ Ord([[0],b,c])
a(↓b)c = Ord([a,b,c]) (down-arrows/backwards associative hyper operators I designed just for ordinals)

We follow the following FS for our ordinals:
k[n,b] = k-1, k &lt; ω
ω[n,b] = n(↓n)n
(a(↓b)0)[n,b] = (a(↓0)c)[n,b] = a
(a(↓b)c)[n,b] = (a(↓b)(c[n,b]))(↓b[n,b])a, b ≥ 0 and c &gt; 0.
ψ'(a)[0,b] = 0(↓0)0
ψ'(a)[n,b] = (ψ'(a[n-1,a]))(↓n)ω, a &gt; 0 and n ≥ 0. (also note that we've changed from [n,b] to [n,a].)
Ω[n,b] = ψ'(b)[n,b]


ψ'(ω∙α) ≈ ψ(α), the ordinal collapsing function described in the image above.

My program more or less initiates k = 9 and h = Ω(↑9)9, then applies k ← k² and h ← h[k,h] until h = 1 and returns k.

And so if I did this right, [[],9,9] is way bigger than the Bachmann-Howard ordinal ψ(ΩΩΩ...), which is way bigger than ϑ(Ωωω)+1.

ψ(Ω(↓9)9) > ψ(Ω(↓4)3) > ψ(ΩΩΩ)+1 > ψ(ΩΩωω)+1 > ϑ(Ωωω)+1

And if my analysis is correct, then we should have ψ'(ΩΩ∙x) ~= ψ*(ΩΩ∙x), where ψ* is the normal Madore's psi function. If this holds, then my ordinal is approximately ψ*(φ3(Ω+ω)).



Old Ruby, 309 bytes, Hψ'0(Ω9)(9) (see revision history, besides the new one is way better)