Let $a_1=5, a_2=25, a_{n+2}=7a_{n+1}-a_n-6$. Prove that $\exists x, y \in \Bbb{Z} $ s.t. $a_{2023}=x^2+y^2.$
Doing some trials and errors, I found that $a_n=(2F_{2n-1})^2+F_{2n}^2$. ($F_n$: Fibonacci number) Then I tried to show this...
\begin{align} n=1; \; & a_1=5=(2 \cdot 1)^2+1^2. \\ n=2; \; & a_2=25 = (2 \cdot 2)^2+3^2. \\ \text{Assume.} \; & a_k=(2F_{2k-1})^2+F_{2k}^2, a_{k-1}=(2F_{2k-3})^2+F_{2k-2}^2. \\ n=k+1; \; & a_{k+1}=7(2F_{2k-1})^2+7F_{2k}^2-(2F_{2k-3})^2-F_{2k-2}^2-6. \end{align}
And I'm stuck...
The Fibonacci Lemmas I know with squares are those below, which I don't know where to use...
\begin{align} & F_{k}^2=F_{k-1}F_{k+1} + (-1)^{k+1}. \\ & \sum_{i=1}^{k} F_i^2=F_kF_{k+1}. \end{align}
Can I use these lemmas to this problem?
Inspired by @CalvinLin's comment.
\begin{align} & F_1=F_2=1, F_{n+2}=F_{n+1}+F_{n}. \\ \ \\ & \text{Lemma 1. } F_n^2=F_{n-1}F_{n+1}+(-1)^{n+1}. (n \geq 2) \\ & \text{(i) } n=2: F_2^2=1^2=1\cdot2+(-1)^3=F_1F_3+(-1)^3. \\ & \ \quad n=3: F_3^2=2^2=1\cdot3+(-1)^4=F_2F_4+(-1)^4. \\ & \text{(ii) Assume that } F_k^2=F_{k-1}F_{k+1}+(-1)^{k+1}, F_{k-1}^2=F_{k-2}F_{k}+(-1)^k. (k\geq 3)\\ & \text{(iii) } F_{k+1}^2=F_k^2+2F_kF_{k-1}+F_{k-1}^2 = F_{k}(F_k+2F_{k-1})+F_kF_{k-2}+(-1)^k \\ & \quad \ = F_k(F_k+2F_{k-1}+F_{k-2})+(-1)^{k+2} = F_kF_{k+2}+(-1)^{k+2}. \\ &\quad \ F_{k+2}^2=F_{k+1}^2+2F_{k+1}F_k+F_k^2 = F_{k+1}(F_{k+1}+2F_{k})+F_{k+1}F_{k-1}+(-1)^{k+1} \\ & \quad \ = F_{k+1}(F_{k+1}+2F_{k}+F_{k-1})+(-1)^{k+3} = F_{k+1}F_{k+3}+(-1)^{k+3}. \ _\blacksquare \\ \ \\ & \text{Lemma 2. } F_{n+4}^2=7F_{n+2}^2-F_n^2+2(-1)^n. \\ & \text{By Lemma 1, } F_{n+1}^2=F_nF_{n+2}+(-1)^{n+2} \\ & \Rightarrow (F_{n+2}-F_n)^2-F_nF_{n+2}=(-1)^n, F_{n+2}^2-3F_nF_{n+2}+F_n^2=(-1)^n. \\ & \Rightarrow 2F_{n+2}^2-6F_nF_{n+2}+2F_n^2=2(-1)^n. \\ & \Rightarrow (9F_{n+2}^2-6F_nF_{n+2}+F_n^2)-(7F_{n+2}^2-F_n^2)=2(-1)^n. \\ & \Rightarrow (3F_{n+2}-F_n)^2=7F_{n+2}^2-F_n^2+2(-1)^n. \\ & \therefore F_{n+4}^2=7F_{n+2}^2-F_n^2+2(-1)^n. \ _\blacksquare \\ \ \\ & \text{Claim. } a_n=(2F_{2n-1})^2+F_{2n}^2. \\ & \text{(i) } n=1: a_1=5=(2\cdot1)^2+1^2=(2F_1)^2+F_2^2. \\ & \ \quad n=2: a_2=25=(2\cdot2)^2+3^2=(2F_3)^2+F_4^2. \\ & \text{(ii) Assume that } a_k=(2F_{2k-1})^2+F_{2k}^2, a_{k-1}=(2F_{2k-3})^2+F_{2k-2}^2. (k\geq 2)\\ & \text{(iii) } \\ & a_{k+1}=7a_k-a_{k-1}-6 \\ & = 28F_{2k-1}^2+7F_{2k}^2-4F_{2k-3}^2-F_{2k-2}^2-6 \\ & = 4\left\{7F_{2k-1}^2-F_{2k-1}^2+2(-1)^{2k-1}\right\}+\left\{7F_{2k}^2-F_{2k-2}^2+2(-1)^{2k-2}\right\} \\ & = 4F_{2k+1}^2+F_{2k+2}^2=(2F_{2k+1})^2+F_{2k+2}^2. \ _\blacksquare \\ \ \\ &\therefore x=2F_{4045}, y=F_{4046}. \ _\blacksquare \end{align}