Show this recursively defined integer sequence $a_{n+1} = (2b_1 - a_1)a_n + (a_1b_1 - b_1^2 - 2a_1^2)a_{n-1}$ is never $0$. Let $a_1, b_1 \in \mathbb{Z}$ be arbitary integers with $a_1 \neq 0$, and define sequences $\{a_n \}_{n \geq 1}$ and $\{b_n \}_{n \geq 1}$ to be solutions to the following linear system of recursions:
\begin{cases} 
      a_{n+1} = (b_1 - a_1)a_n + (a_1)b_n \\
      b_{n+1} = (-2a_1)a_n + (b_1)b_n
\end{cases}
I have done the following manipulations which give a recursive formula for $a_n$.
First, observe the first equation gives us $b_{n} = \dfrac{a_{n+1} - (b_1 - a_1)a_n}{a_1}$.
Substituting this into the second equation, we see $$b_{n+1} = (-2a_1)a_n + b_1 \Big(\dfrac{a_{n+1} - (b_1 - a_1)a_n}{a_1}\Big).$$
Reindexing $n + 1 \rightarrow n$, we achieve $$b_n = (-2a_1)a_{n-1} + b_1 \Big(\dfrac{a_{n} - (b_1 - a_1)a_{n-1}}{a_1}\Big).$$
Finally, substituting this back into the first equation, we get:
$$ a_{n+1} = (b_1 - a_1)a_n + a_1 \Big[(-2a_1)a_{n-1} + b_1 \Big(\dfrac{a_{n} - (b_1 - a_1)a_{n-1}}{a_1}\Big) \Big].$$
Simplifying, we find $$a_{n+1} = (2b_1 - a_1)a_n + (a_1b_1 - b_1^2 -  2a_1^2)a_{n-1}.$$
I suspect, and would like to prove, that $a_n \neq 0$ for all $n \geq 1$ and for all choices $a_1, b_1 \in \mathbb{Z}$ where $a_1 \neq 0$.
As corrected in the comments, $\lim\limits_{n \rightarrow \infty} \frac{a_{n+1}}{a_n}$ does not appear to be $-3$, so my claim of well-behavedness asymptotically isn't even true. Any suggestions/hints for forward movement are appreciated.

Set $a_0=0$ and $b_0=1$. Then the original recurrence works for $n\ge0$. Write it in matrix form:
$$
\begin{pmatrix}
      a_{n+1} \\ b_{n+1} 
\end{pmatrix}
=
\begin{pmatrix}
      b_1 - a_1 & a_1 \\ -2a_1 & b_1 
\end{pmatrix}
\begin{pmatrix}
      a_{n} \\ b_{n} 
\end{pmatrix}
=
A
\begin{pmatrix}
      a_{n} \\ b_{n} 
\end{pmatrix}
$$
Then
$$
v_{n}=
\begin{pmatrix}
      a_{n} \\ b_{n} 
\end{pmatrix}
=
A^n
\begin{pmatrix}
      a_{0} \\ b_{0} 
\end{pmatrix}
=
A^n
\begin{pmatrix}
      0 \\ 1 
\end{pmatrix}
= A^n v_0
$$
Therefore
$$
A^n
=
\begin{pmatrix}
      * & a_n \\ * & b_n 
\end{pmatrix}
$$
If $a_n=0$, then $v_0$ is an eigenvector of $A^n$ with eigenvalue $b_n$. The eigenvectors of $A^n$ are the same as the eigenvectors of $A$, and these have nonzero first coordinates, unlike $v_0$.
The calculations were made with WA.
