+
+
Technically Exists
+
Theorem ω-1
+
+
This theorem establishes a simple upper bound on the Wainer hierarchy up to ω in terms of hyper operators.
+
+
2⋅fα(n)2⋅fω(n)≤2[α+1](2⋅n) for α<ω≤2[n+1](2⋅n)
+
+
The correctness of this bound was originally proven by Deedlit for 1≤α<ω and n≥1. This proof follows the same approach as Deedlit’s proof. It is worth noting that Deedlit has also proven the correctness of a more complicated but tighter upper bound.
+
+
Lemma ω-0
+
+
In order for 2⋅fm(n)≤gm(2⋅n) to hold for all m,n∈N0, it is sufficient for the following conditions to be met.
+
+
+ - f is a function f:N0→N0
+ - g is a non-decreasing function g:N0→N0
+ - 2⋅f(n)≤g(2⋅n) for all n∈N0
+
+
+
Proof
+
+
Base case:
+
+
2⋅f0(n)=2⋅n=g0(2⋅n)
+
+
Induction step for m:
+
+
2⋅fm(n)g(2⋅fm(n))2⋅f(fm(n))2⋅fm+1(n)≤gm(2⋅n)≤g(gm(2⋅n))≤g(gm(2⋅n))≤gm+1(2⋅n)by the induction hypothesisby conditions 1 and 2by condition 3
+
+
Lemma ω-1
+
+
2⋅n≤2[m]n for all m,n∈N0,m≥2.
+
+
Proof
+
+
Base cases where m=2:
+
+
2⋅n=2[2]n
+
+
Base cases where n=0 and m≥3:
+
+
2⋅0=0<1=2[m]0
+
+
Base cases where n=1:
+
+
2⋅1=2=2[m]1
+
+
Induction step for n≥1, with the assumption that the lemma holds for m:
+
+
2⋅(n+1)=2⋅n+2≤2⋅n+2⋅n=2⋅(2⋅n)≤2⋅(2[m+1]n)≤2[m](2[m+1]n)=2[m+1](n+1)by the induction hypothesisby assumption
+
+
Performing induction over m completes the proof.
+
+
Lemma ω-2
+
+
(2[α+1])m(2[α+2]n)=2[α+2](n+m) for all m,n,α∈N0.
+
+
Proof
+
+
Base case:
+
+
(2[α+1])0(2[α+2]n)=2[α+2]n=2[α+2](n+0)
+
+
Induction step for m:
+
+
(2[α+1])m+1(2[α+2]n)=2[α+1]((2[α+1])m(2[α+2]n))=2[α+1](2[α+2](n+m))=2[α+2](n+m+1)by the induction hypothesis
+
+
Proof of Theorem ω-1
+
+
Base case:
+
+
2⋅f0(n)=2⋅(n+1)=2+(2⋅n)=2[0+1](2⋅n)
+
+
Induction step for α:
+
+
2⋅fα+1(n)=2⋅fαn(n)≤(2[α+1])n(2⋅n)≤(2[α+1])n(2[α+2]n)=2[α+2](2⋅n)by the induction hypothesis and Lemma ω-0by Lemma ω-1by Lemma ω-2
+
+
Case where α=ω:
+
+
2⋅fω(n)=2⋅fω[n](n)=2⋅fn(n)≤2[n+1](2⋅n)by the previous cases
+
+
+
+