Technically Exists

Theorem ω\omega-0

This theorem establishes a simple lower bound on the Wainer hierarchy up to ω\omega in terms of hyper operators.

fα(n)+12[α+1]n for α<ωfω(n)+12[n+1]n\begin{align*} f_\alpha(n) + 1 &\ge 2 [\alpha + 1] n \text{ for } \alpha < \omega \\ f_\omega(n) + 1 &\ge 2 [n + 1] n \\ \end{align*}

Proposition ω\omega-0

fα(n)2[α+1]nf_\alpha(n) \ge 2 [\alpha + 1] n for n,αN+n, \alpha \in \N_+.

Proof

Base case:

f1(n)=2n=2[1+1]n\begin{align*} f_1(n) &= 2 \cdot n \\ &= 2 [1 + 1] n \\ \end{align*}

Induction step for α\alpha:

fα+1(n)=fαn(n)(2[α+1])nnby the induction hypothesis(2[α+1])n1=(2[α+1])n1(2[α+1]1)=(2[α+1])n12=2[α+2]n\begin{align*} f_{\alpha + 1}(n) &= f_\alpha^n(n) \\ &\ge (2 [\alpha + 1])^n n &&\text{by the induction hypothesis} \\ &\ge (2 [\alpha + 1])^n 1 \\ &= (2 [\alpha + 1])^{n - 1} (2 [\alpha + 1] 1) \\ &= (2 [\alpha + 1])^{n - 1} 2 \\ &= 2 [\alpha + 2] n \\ \end{align*}

Proof of Theorem ω\omega-0

Cases where α=0\alpha = 0:

f0(n)+1=(n+1)+1=2+n=2[0+1]n\begin{align*} f_0(n) + 1 &= (n + 1) + 1 \\ &= 2 + n \\ &= 2 [0 + 1] n \\ \end{align*}

Cases where n=0n = 0 and 1α<ω1 \le \alpha < \omega:

fα(0)+1=fα10(0)+1=0+1=12[α+1]0\begin{align*} f_\alpha(0) + 1 &= f_{\alpha - 1}^0(0) + 1 \\ &= 0 + 1 \\ &= 1 \\ &\ge 2 [\alpha + 1] 0 \\ \end{align*}

Cases where n1n \ge 1 and 1α<ω1 \le \alpha < \omega:

fα(n)+1>fα(n)2[α+1]nby Proposition ω-0\begin{align*} f_\alpha(n) + 1 &> f_\alpha(n) \\ &\ge 2 [\alpha + 1] n &&\text{by Proposition } \omega\text{-0} \\ \end{align*}

Cases where α=ω\alpha = \omega:

fω(n)+1=fω[n](n)+1=fn(n)+12[n+1]nby the previous cases\begin{align*} f_\omega(n) + 1 &= f_{\omega[n]}(n) + 1 \\ &= f_n(n) + 1 \\ &\ge 2 [n + 1] n &&\text{by the previous cases} \\ \end{align*}