Recurrence relation $a_{n+1}=a_n^2-2$ Sequence $a_n$ is defined $a_{n+1}=a_n^2-2, a_0=\alpha$. 
I know that a closed form for $a_n$ is $a_n=\beta^{2^n}+\frac{1}{\beta^{2^n}}$, where $\beta$ satisfies $\beta+\frac{1}{\beta}=\alpha$ and I can prove it by induction. 
But this way, we have to know answer. Is there any other solution that leads us to this form?

Since this is very close to a rival relation $a_{n+1}=a_n^2$ with easy solution $a_n=\alpha^{2^n}$, it's natural to try $a_n=\beta^{2^n}+\epsilon_n$ for some $\beta$ and sequence $\epsilon_n$ of small error terms. So$$\beta^{2^{n+1}}+\epsilon_{n+1}=(\beta^{2^n}+\epsilon_n)^2-2\implies\epsilon_{n+1}=2\beta^{2^n}\epsilon_n+\epsilon_n^2-2.$$This would be easy to solve if we only kept one of the last three terms, so let's try to cancel two of them. There are only so many combinations to try. You quickly realize cancelling the first and third gives the consistent conditions $\epsilon_n=\beta^{-2^n}$ and $\epsilon_{n+1}=\epsilon_n^2$. Then$$a_n=\beta^{2^n}+\beta^{-2^n}\implies\alpha=\beta+\beta^{-1}.$$
