Solving the recurrence $S_{n+1} = S_n^2-2$ Note. This question is not solely about solving the recurrence below, I already know the solution. I would like to get a reference, preferably a textbook, which summarizes methods to explicitly solve recurrence relations such that the methods of that textbook are sufficient to solve \eqref{*} below.
The recurrence \begin{equation}\tag{*}\label{*}S_{n+1} = S_n^2-2\end{equation} is the basis for the Lukas-Lehmer primality test and it is a classical result from the literature that for $S_0 = 4$, the solution to \eqref{*} is given by \begin{equation}\label{Sol}\tag{Sol}S_n = (2+\sqrt 3)^{2^n}+(2-\sqrt{3})^{2^n}.\end{equation}
It is easy to  verify that the $S_n$ given in \eqref{Sol} indeed satisfy \eqref{*}. However, I would like to have some reference, preferably a book with comprehensive overview of explicit solutions to recurrence relations, which explains the idea behind \eqref{Sol}.

My thoughts: I will follow the ideas of [1; Chapter 1.4]. It is left as an exercise to verify that for all $z\in\mathbb C$, $$\cos(2z) = Q(\cos(z)),$$
where $$Q\in\mathbb R[z], \\ Q(z)=2z^2-1$$ is the second Tschebyscheff polynomial. Our goal is to know more about the iterates of the map \begin{align}f:\mathbb C&\to\mathbb C, \\z&\mapsto z^2-2.\end{align}
We have $f = \phi\circ Q\circ\phi^{-1}$, where $\phi:\mathbb C\to\mathbb C$ is given by $\phi(z)=2z$. So $f^{\circ n} = \phi\circ Q^{\circ n}\circ\phi^{-1}$. But we can compute, thanks to the cosine identity above, $$Q^{\circ n}(\cos(z)) = \cos(2^n z)$$ for all $n\in\mathbb N$ and $z\in\mathbb C$.
Thus, let $y\in\mathbb C$ and let $z\in\mathbb C$ be any solution to $y=\cos(z)$ (with an  abuse of notation I will write $z=\arccos(y)$). The solution exists by [3].
Then $$S_n = f^{\circ n}(S_0)=2Q^{\circ n}(S_0/2)=2\cos(2^n\arccos(S_0/2)).$$
This is a fairly explicit formula and as noted by podiki below, one can obtain \eqref{Sol} directly from this formula using particular values of the complex exponential.
Literature
[1] Alan F. Beardon: Iteration of Rational Functions. (1991)
[2] Related question: If $x_1=5$, $x_{n+1}=x_n^2-2$, find $\lim x_{n+1}/(x_1\cdots x_n)$.
[3] Prove that $\cos(z)$ and $\sin(z)$ are surjective over the complex numbers.
 A: The recurrence $S_{n+1} = S_n^2-2$ belongs to the class of doubly exponential sequences.

An instructive treatment can be found in section 2.2.3 of Mathematics for the Analysis of Algorithms by D. H. Greene and D. E. Knuth (with the title of this section being the name of this class).
This section treats in detail the more general recurrence relation
\begin{align*}
\color{blue}{x_{n+1}=x_n^2+g_n}\tag{2.72}
\end{align*}
where $g_n$ is a slowly growing function of $n$ possibly depending on the earlier members of the sequence.

The authors consider also two special cases of (2.72), namely

*

*Golomb's nonlinear recurrence:
\begin{align*}
y_{n+1}=y_0y_1\cdots y_n+r,\qquad y_0=1\tag{2.88}
\end{align*}
which can be shown to be equivalent to the finite-history recurrence
\begin{align*}
y_{n+1}=\left(y_n-r\right)y_n+r,\qquad y_0=1,y_1=r+1\tag{2.89}
\end{align*}
Completing the square using the substitution $x_n=y_n-\frac{r}{2}$ we obtain
\begin{align*}
x_{n+1}=x_n^2+\frac{r}{2}-\frac{r^2}{4}\tag{2.91}
\end{align*}
showing it's a special case of (2.72).


*Balanced Trees:
The number of balanced binary trees of height $n$ is given by the recurrence
\begin{align*}
y_{n+1}=y_n^2+2y_ny_{n-1}\tag{2.92}
\end{align*}
Making the transformation $x_n=y_n+y_{n-1}$ we obtain
\begin{align*}
x_{n+1}=x_n^2+2y_{n-1}y_{n-2}\tag{2.93}
\end{align*}
Following the authors we find the term $g_n$ is not constant, but grows slowly enough $\left(2y_{n-1}y_{n-2}\ll y_n < x_n\right)$ to meet the requirements on $g_n$.
Notes:

*

*According to the authors the techniques used in this section 2.2.3 are presented in the paper Some Doubly Exponential Sequences by A. V. Aho and N. J. A. Sloane. They finally cite in this section two recurrence relations from this paper
\begin{align*}
y_{n+1}&=y_n^3-3y_n\\
y_{n+1}&=y_ny_{n-1}+1
\end{align*}
indicating that although they are not precisely of the form (2.72) the techniques can also be used to attack these recurrence relations.


*In the cited paper (section 2.3) we also find closely related to OPs recurrence relation:
\begin{align*}
 x_{n+1}=x_n^2-1\qquad n\geq 0
 \end{align*}
A: I don't think you want $S_0=2$ this leads to the constant sequence $S_n=2$. Your formula has $S_0=4$.
$$\begin{align}2\cos(2^n\arccos(S_0/2))&=e^{i2^n\arccos(2)}+e^{-i2^n\arccos(2)}\\
&=(e^{i\arccos(2)})^{2^n}+(e^{-i\arccos(2)})^{2^n}\\
&=(2+\sqrt{3})^{2^n}+(2-\sqrt{3})^{2^n}\\ \end{align}$$
where I used the fact that the solutions to $\cos(z)=2$, satisfy
$$e^{iz}=2\pm\sqrt{3}$$
