Sanity check: does $D_{\omega_9}(9)$ exceed TREE(3)?

Question

TREE(3)

For the Golf a number bigger than TREE(3) challenge I wrote a program but I'm not sure it is 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).

Because of my limited knowledge of TREE(k) and ordinals I decided to post a question here first before submitting my answer.

You can view the code and a limited explanation here but I will define and explain the D function here.

Notation

My program is highly recursive, it produces functions to put inside other functions.

• $\omega_0=0$, $\omega_1=\omega$, $\omega_1=\Omega$,...
• $\alpha_n$ means $cf(\alpha)=\omega_n$ so $\alpha_0$ means $\alpha$ is a natural number
• I will represent ordinals as functions (in lambda calculus) which their fundamental sequence (e.g. $\omega_1\cdot 2=\lambda x_0. \omega_1+x_0$) and call these functions using square brackets e.g. $(\omega_1\cdot 2)[5]=\omega+5$

Definition

1. $\omega_n=\lambda \alpha_k. \alpha_k$ with $k<n$
2. $\alpha_n+1=\lambda \beta_n. \alpha_n$
3. $D_\alpha(\beta)=H'_\alpha(H'_\alpha(\beta))=H'^{2}_\alpha(\beta)$
4. $H'_0(\alpha_n)=\alpha_n+1$
5. $H'_{\alpha_{n+1}}(\beta_k)=D_{H'_{\alpha_{n+1}}(\omega_n)}(\beta_k)$ if $k<n$
6. $H'_{\alpha_{n+1}}(\beta_n)=D_{\alpha_{n+1}[\beta_n]}(\beta_n)$
7. $H'_{\alpha_0+1}(\beta_n)=D_{\alpha_0}(\beta_n)$
8. $H'_{\alpha_{k+1}}(\beta_n)=\lambda \gamma_k. D_{\alpha_{k+1}[\gamma_k]}(\beta_n)$ if $0\le k<n$

My number is $D_{\omega_9}(9)$ but I can easily change it to $D_{\omega_{10^9}}(9)$ if required.

In words

1. $\omega_n$ is the identity function for ordinals of smaller cofanity.
2. The successor of $\alpha$ is the function that returns $\alpha$ for all input (this is to avoid having to handle successor and limit ordinals separately )
3. $D$ is the doubling function it iterates $H'$ once. This is a balance between the hardy hierarchy, which doesn't iterate at all, and the fast-growing hierarchy, which iterates n times.
4. $H'_0$ is the successor function, both for functions and numbers

$H'_\alpha(\beta)$:

5. if the domain of $\alpha$ is so large a size smaller could still fit $\beta$, use $H'$ on $\alpha$ until the domain is just large enough.
   (this is a way to avoid having multiple calls to H' in my code
   e.g. $\alpha_1=H'_{\omega_2}(\omega_1)$ and $H'_{\alpha_1}(9)$
6. if the domain of $\alpha$ is just large enough use $\alpha[\beta]$

if the domain of $\alpha$ is too small:

7. if $\alpha$ is an integer use it's predecessor.
8. else define the result to be the function that uses $\alpha[\gamma]$ as the new subscript when $\gamma$ is put in. The result has the same domain as $\alpha$

note:

• $H'_{\alpha_n}(\beta_m) \in T_m \text{ if } m\le n \text{ or } n=0$
• $H'_{\alpha_n}(\beta_m) \in T_n \text{ if } n<m$

The ordinal interpretation

You don't have to read this is you don't want. The question is if $D_{\omega_9}(9)>TREE(3)$.
But I want to give some more explanation for why I believe my number is bigger than TREE(3).

The functions in program have strong similarities with ordinals This is the definition for the set of tree-ordinals with order type $n$: $$\alpha\in T_n \Leftrightarrow \begin{cases} \alpha=0\\ \alpha=\beta+1 \text{ and } \beta\in T_n\\ \alpha:T_k\mapsto T_n \text{ with } k<n\\ \end{cases}$$

Note

• $T_k \subset T_n \text{ if } k<n$ but except for this it perfectly aligns with the explanation I gave earlier.
• $T_0$ is still the set of natural numbers, since the 3rd rule, which generates all the limit ordinals, can't be used yet.
• My definition of $\omega_n$ is different than usual, usually $\omega_1$ is the first uncountable ordinal ($\Omega$) but for me that's $\omega_2$ I did this to keep $\alpha_n \in T_n$

Notation interpreted as ordinals

• $\alpha_{k}$ is an ordinal with order type k ( $k=\min(n:\alpha\in T_n)$ )
• $\alpha_n[\beta_k]$ is the $\beta$th element of $\alpha$'s fundamental sequence. This is defined when $k<n$.

The ordinal idea behind my number

I believe $\omega_9$ acts as on ordinal about the size of $\tau[9]$ in $H'$.
Since $H'_{\omega*\alpha}(n)>f_\alpha(n)$, My number $D_{\omega_9}(9)=H'^{2}_{\omega_9}(9)\approx H'^{2}_{\tau[9]}(9)>f_{\tau[9]}(9)>f_{ϑ(Ω^ω ω)+1}(9)>TREE(9)$

$H'$ is a modified version of the Hardy Hierarchy. The idea behind $H'$ is that $H'_{\alpha+1}$ = $H'^{2}_{\alpha}$ $\Rightarrow$ $H'_{\alpha_n+\omega_n} \text{ iterates } H'_{\alpha_n}$ $\Rightarrow$ $H'_{\omega*\alpha}(n)>f_\alpha(n)$. You can find a proof here.

Than the idea of an ordinal hierarchy was expended from a using a countable ordinal to generate huge integers, to use huge $\alpha_{n+1}$ to generate huge $\beta_n$.

The 5th definition was than added to iterate $H'$ on the ordinal slot. If I did this correctly this should mean that $H'_{\omega_{n+k}}(n)>f_\tau(n)$ for some reasonably small k.

Examples

These early expansions created a lot of insight into my function for me, so I'll post them here too.

Some very early expansions

The 5th definition makes $D_{\omega_9}(9)$ expand to $H'_{\omega_9}(H'_{\alpha_8}(H'_{\alpha_7}(H'_{\alpha_6}(H'_{\alpha_5}(H'_{\alpha_4}(H'_{\alpha_3}(H'_{\alpha_2}(D_{\alpha_1}(9)))))))))$
$= H'_{\omega_9}(H'_{\alpha_8}(H'_{\alpha_7}(H'_{\alpha_6}(H'_{\alpha_5}(H'_{\alpha_4}(H'_{\alpha_3}(H'_{\alpha_2}(H_{\alpha_1}(D_{\alpha_1[9]}(9))))))))))$

$$\alpha_8=H'_{\omega_9}(\omega_8)=D_{\omega_8}(\omega_8)=H'_{\omega_8}(H'_{\omega_8}(\omega_8))$$ \begin{align} \ \alpha_7 & = H'_{\alpha_8}(\omega_7) \\ & = D_{\alpha_8[\omega_7]}(\omega_7) \\ & = D_{H'_{\omega_8}(H'_{\omega_8}(\omega_8))[\omega_7]}(\omega_7) \\ & = D_{D_{\omega_8[\omega_7]}(H'_{\omega_8}(\omega_8))}(\omega_7) \\ & = D_{D_{\omega_7}(H'_{\omega_8}(\omega_8))}(\omega_7) \\ & = H'_{H'_{\omega_7}(H'_{\omega_7}(H'_{\omega_8}(\omega_8)))}(H'_{H'_{\omega_7}(H'_{\omega_7}(H'_{\omega_8}(\omega_8)))}(\omega_7))\\ \end{align}

\begin{align} \ \alpha_6 & =H'_{\alpha_7}(\omega_6) \\ \ & = D_{\alpha_7[\omega_6]}(\omega_6) \\ \ & = D_{H'_{H'_{\omega_7}(H'_{\omega_7}(H'_{\omega_8}(\omega_8)))}(H'_{H'_{\omega_7}(H'_{\omega_7}(H'_{\omega_8}(\omega_8)))}(\omega_7))[\omega_6]}(\omega_6) \\ \ & = \ ... \end{align}
$$\alpha_5=H'_{\alpha_6}(\omega_5)$$ $$\alpha_4=H'_{\alpha_5}(\omega_4)$$ $$\alpha_3=H'_{\alpha_4}(\omega_3)$$ $$\alpha_2=H'_{\alpha_3}(\omega_2)$$ $$\alpha_1=H'_{\alpha_2}(\omega_1)$$

If you want too truly experience the madness I recommend trying to work out $\alpha_1[3]$ but I didn't get very far.

Some very approximate expansions

\begin{align} D_{\omega_9}(9) & = H'^{2}_{\omega_9}(9) \\ & > H'_{\omega_9}(9) \\ & = D_{H'_{\omega_9}(\omega_8)}(9) \\ & > D_{\omega_{8}*2}(9) \\ & > H'_{\omega_{8}*2}(9) \\ & > H'_{\omega_{7}^2}(9)\\ & > H'_{2 ↑^{\omega_{6}} \omega_{6}}(9)\\ & > ... \end{align}

Conclusion

I couldn't get past $\omega_6$ and I ignored all the iteration of D so once $H'_{\alpha_1}(9)$ is finally reached the computer will have to work back up trough all of those extra iterations too.

But that wouldn't even be necessary because $f_{ϑ(Ω^ω ω)}(9)>TREE(3)$ so if $\alpha_1>ϑ(Ω^ω ω)$ my number should be big enough.

So is $\alpha_1>ϑ(Ω^ω ω)$?
I think it should be, but it's quite possible I made a mistake somewhere. Did I?