Technically Exists
Theorem ω-0
This theorem establishes a simple lower bound on the Wainer hierarchy up to ω in terms of hyper operators.
fα(n)+1fω(n)+1≥2[α+1]n for α<ω≥2[n+1]n
Proposition ω-0
fα(n)≥2[α+1]n for n,α∈N+.
Proof
Base case:
f1(n)=2⋅n=2[1+1]n
Induction step for α:
fα+1(n)=fαn(n)≥(2[α+1])nn≥(2[α+1])n1=(2[α+1])n−1(2[α+1]1)=(2[α+1])n−12=2[α+2]nby the induction hypothesis
Proof of Theorem ω-0
Cases where α=0:
f0(n)+1=(n+1)+1=2+n=2[0+1]n
Cases where n=0 and 1≤α<ω:
fα(0)+1=fα−10(0)+1=0+1=1≥2[α+1]0
Cases where n≥1 and 1≤α<ω:
fα(n)+1>fα(n)≥2[α+1]nby Proposition ω-0
Cases where α=ω:
fω(n)+1=fω[n](n)+1=fn(n)+1≥2[n+1]nby the previous cases