Let $s$ be any complex number, $t = e^s$ and $z = t^{1/t}$. Define the sequence $(a_n)_{n\in\mathbb{N}}$ by $a_0 = z $ and $a_{n+1} = z^{a_n} $ for $n \geq 0$, that is to say $a_n$ is the sequence $z$, $z^z$, $z^{z^z}$, $z^{z^{z^{z}}}$ and so on.
I want to show that the sequence $(a_n)_{n\in\mathbb{N}}$ converges to $t$ if and only if $s$ lies in the unit disk. I know that when the sequence converges the limit is $\frac{W(-\ln(z))}{-\ln(z)}$ where $W$ is the Lambert W function.
I have verified the above statements numerically for several thousand values of $z$ but I have no idea how to actually prove it.
I graphed the natural logs of the limits on my computer. I got what appeared to be the unit disk.
If we take the log of the limit we get $\ln\left(\frac{W(−\ln(z)}{−\ln(z)}\right)=-\ln(−\ln(z))−W(−\ln(z))+\ln(−\ln(z))=−W(−\ln(z))$
So what I want to prove is equivalent to showing the sequence $a_n$ is convergent if and only if $|W(−\ln(z))| \leq 1$
I was reading the Wikipedia article on the Lambert W Function and I found this proof that the limit $c$, when it exists, is $c= \frac{W(-\ln(z))}{-\ln(z)}$
$z^c = c\implies z = c^{1/c} \implies z^{-1} = c^{-1/c} \implies 1/z = (1/c)^{1/c} \implies -\ln(z) = \frac{\ln(1/c)}{c} \implies -\ln(z) = e^{\ln(1/c)}\ln(1/c) \implies \ln(1/c) = W(-\ln(z)) \implies 1/c = e^{W(-\ln(z))} \implies \frac{1}{c} = \frac{-\ln(z)}{W(-\ln(z)} \implies c = \frac{W(-\ln(z)}{-\ln(z)}$
I can only assume that at least 1 step is not justified when $|W(-\ln(z)| > 1$ though I am not sure which one. I think that part of the problem is the equation $z^c=c$ has a solution for every non-zero complex number $c$ while the sequence $a_n$ only converges for certain special values of z. In other words the convergence of the $a_n$ is a sufficient but not necessary condition for the existence of a solution to the equation.