In my previous question I asked about the numerical instability and convergence of my tetration. It would seem to be the case that it converges, but suffers from catastrophic cancellation. The definition of my tetration is provided as:
$${}^xa=\lim_{n\to\infty}\log_a^{\circ n}({}^\infty a-({}^\infty a-{}^na)[\ln({}^\infty a)]^x)$$
where ${}^na$ for natural $n$ is defined as the usual tetration, with ${}^\infty a$ as the limit of that, and $\log^{\circ n}$ being the $n$ times applied logarithm. We consider the above for $a\in(1,e^{1/e})$ and $x\in(-2,\infty)$. I want to prove that it satisfies the basic tetration properties:
${}^0a=1$
${}^{x+1}a=a^{({}^xa)}$
It is easy enough to verify the first one, as we have:
\begin{align}{}^0a&=\lim_{n\to\infty}\log_a^{\circ n}({}^\infty a-({}^\infty a-{}^na)[\ln({}^\infty a)]^0)\\&=\lim_{n\to\infty}\log_a^{\circ n}({}^\infty a-({}^\infty a-{}^na))\\&=\lim_{n\to\infty}\log_a^{\circ n}({}^na)\\&=\lim_{n\to\infty}1\\&=1\end{align}
I attempted to verify the second property:
\begin{align}a^{({}^xa)}&=\lim_{n\to\infty}\log_a^{\circ(n-1)}({}^\infty a-({}^\infty a-{}^na)[\ln({}^\infty a)]^x)\\&=\lim_{n\to\infty}\log_a^{\circ n}({}^\infty a-({}^\infty a-{}^{n+1}a)[\ln({}^\infty a)]^x)\\&=\lim_{n\to\infty}\log_a^{\circ n}({}^\infty a-({}^\infty a-{}^na)[\ln({}^\infty a)]^{x+1}+\mathcal O(({}^\infty a-{}^na)^2[\ln({}^\infty a)]^x))\\&=\lim_{n\to\infty}\log_a^{\circ n}({}^\infty a-({}^\infty a-{}^na)[\ln({}^\infty a)]^{x+1})\tag{$\star$}\\&={}^{x+1}a\end{align}
How can I justify $(\star)$ though?
Update: Rough outline of possible proof?
For $t\ge1,~a>1$, and sufficiently small $\epsilon>0$, we have
\begin{align}\log_a(t+\epsilon)&=\log_a(t)+\log_a(1+\epsilon/t)\\&\le\log_a(t)+\frac\epsilon{t\ln(a)}\end{align}
In this case, $t\ge{}^xa$ by monotonicity of the logarithm and the limit.
We start with $\epsilon=q^n$ where $q=\ln^2({}^\infty a)$ and apply the above $n$ times to get:
$$\log_a^{\circ n}({}^\infty a-({}^\infty a-{}^na)[\ln({}^\infty a)]^{x+1}+\epsilon)\le\log_a^{\circ n}({}^\infty a-({}^\infty a-{}^na)[\ln({}^\infty a)]^{x+1})+\left(\frac{\ln^2({}^\infty a)}{{}^xa\cdot\ln(a)}\right)^n$$
Seeing as we have
$$\frac{\ln^2({}^\infty a)}{{}^xa\cdot\ln(a)}=\frac{{}^\infty a}{{}^xa}\cdot\ln({}^\infty a)$$
and $\ln({}^\infty a)<1$, this should work for sufficiently large $x$.