Let's define the sequence $\{s_n\}$ recursively as
$$s_1=\sqrt2,\ \ \ s_{n+1}=\sqrt2^{\,s_n}.$$
Or, in other words,
$$s_n=\underbrace{\sqrt2^{\sqrt2^{\ .^{\ .^{\ .^{\sqrt2}}}}}}_{n\ \text{levels}}.$$
The sequence is monotonically growing, and rapidly converges to a limit $$\lim\limits_{n\to\infty}s_n=2.$$
I'm interested in estimating its convergence speed.
Based on numerical data, I conjectured that
$$\ln\left(2-s_n\right)=n\ln\ln2+c_{\sqrt2}+O\big(\left(\ln2\right)^n\big)$$
for some constant $c_{\sqrt2}\approx-0.458709787761420587059021…$
Could you suggest possible approaches to prove (or refute) this conjecture?
I am also interested in a possible closed form of the constant $c_{\sqrt2}$.
Update: We can try to generalize this problem to other bases beyond $\sqrt2$. Let's use a usual notation for tetration
$${^n}a=\underbrace{a^{a^{\ .^{\ .^{\ .^a}}}}}_{n\ \text{levels}}.$$
It's known that for all $1/e^e<a<e^{1/e}$ there exists a limit$${^\infty}a=\lim\limits_{n\to\infty}{^n}a=e^{-W\left(-\ln a\right)},$$
where $W(z)$ is the Lambert $W$ function, the inverse of the function $x\mapsto x\,e^x$.
I conjecture that for all $1<a<e^{1/e}$
$$\ln\left({^\infty}a-{^n}a\right)=n \ln\ln\left({^\infty}a\right)+c_a+O\left(e^{n\ln\ln\left({^\infty}a\right)}\right),$$
where $c_a$ is some constant that depends on $a$ but not on $n$ (also note that $\ln\ln\left({^\infty}a\right)<0$, so the last term is exponentially small).
Best Answer
Here's proof of a weaker result. Let $r_n = 2 - s_n$. $$ r_{n+1} = 2 - s_{n+1}= 2 - \sqrt{2}^{s_n}= 2\left(1 - \sqrt{2}^{s_n-2}\right)= 2\left(1 - \sqrt{2}^{\,-r_n}\right) $$ Now, let $\alpha = \ln 2$. $$ \sqrt{2}^{\,-r_n}= \left(e^{\ln \sqrt{2}}\right)^{-r_n}= e^{-\frac{1}{2}\alpha r_n}= 1-\frac{1}{2}\alpha r_n + O\left(r_n^2\right) $$ and so $$ r_{n+1}=\alpha\,r_n + \phi\left(r_n\right),\quad \phi\left(s\right) = O\left(s^2\right) $$ Hence, $$ \ln r_{n+1}= \ln\left(\alpha\,r_n + O\left(r^2_n\right)\right)= \ln\alpha + \ln r_n + \ln\left(1+O\left(r_n\right)\right)= $$ $$ =\ln\alpha + \ln r_n + \psi\left(r_n\right),\quad \psi(s)=O\left(s\right) $$ and $$ \ln r_n = \ln r_1 + \left(n-1\right) \ln \alpha + \sum_{k=2}^n\psi\left(r_k\right) $$ This last sum is convergent (proof below), so the rate of convergence is determined by behaviour of $\psi\left(r_n\right)$. Since $\psi\left(s\right)=O(s)$, it's in fact determined by behaviour of $r_n$.
Using this, we can easily bound the tail of the sum by $O\left(\left(\alpha + \varepsilon\right)^n\right)$, and so, to conclude $$ \ln\left(2 - s_n\right) = n\ln\ln 2 + c + O\left(\left(\ln 2 + \varepsilon\right)^n\right) $$ for every $\varepsilon > 0$, where $c=\ln\left(2 - \sqrt{2}\right) - \ln\ln 2 + S$, where $S$ is sum of the series discussed above.
Of course, that's strictly weaker than the conjuecture from question. Still, I believe it's close enough to be at least relevant.