How can I make this kind of proof rigorous? I have transformed a Diophantine equation into the form
$$
\frac{a-b-3}{a-b-1} = \frac{2(b-1)(a+1)}{a^2+b^2},  \tag{$\star$}
$$
where $a > b \ge 1$ are integers. I want to prove that $a-b=3$ [thus forcing $b=1$]. It’s easy to show that $1 ≤ a-b ≤ 3$ has only the one desired solution. Now assuming $a-b ≥ 4$, I can say
\begin{align}
  \frac{a-b-3}{a-b-1} \simeq 1,
\end{align}
and thus
\begin{align}
  1 &\simeq \frac{2(b-1)(a+1)}{a^2+b^2}  \\
  a^2+b^2 &\simeq 2(b-1)(a+1) \\
       &= 2ab+2(b-a-1)  \\
  \therefore\quad (a-b)^2 &\simeq 2(b-a-1) ≤ 2(-4-1)=-10.
\end{align}
With a strict equality, this would clearly be impossible; QED. The proof might also be valid if I can qualify precisely what is meant by “$\simeq$”, such that the contradiction holds.

QUESTION: How can I make this method of proof rigorous?

EDIT: In case it helps, I have proven that
$$ab = 4(256n^3-640n^2+533n-148) \qquad\text{and}\qquad a-b=16n-13$$
for some $n \ge 1$, and need to prove that $n=1$ is the only solution. Combining those two equations yields
$$a^2+b^2=(8n-7)(256n^2-384n+145),$$
which has certain implications I might be able to leverage…
 A: Claim: For $C > 2$, and arbitrary constants $D, E, F$, then the inequality
$$ a^2 + b^ 2 - Cab - Da - Eb - F \leq 0. $$
always has integer solutions.
Proof: We want to find
$$ (a-b)^2 \leq (C - 2 ) ab + Da + Eb + F. $$
Since $ C - 2 > 0$, we can take $ b = a+1, a  \rightarrow \infty$.
Then, the RHS is dominated by $a^2$ hence tends to $ + \infty$, so is $ \geq 1$ for some large enough $a$. So, (integer) solutions exist.
Corollary: With the restriction of $ a - b \geq N$, since $\frac{a-b-3}{a-b-1 } \geq \frac{N-3}{N-1}$, in OP's solution, we have
$$a^2 + b^2 - \frac{2(N-1)}{N-3} (b-1)(a+1) \leq 0.$$
This has integer roots, hence we cannot just use this approach to reach a contradiction.
Since this proof approach doesn't work, we cannot make it rigorous (in it's current form).
For the more general case, to show that $ (a-b)^2 < 0$

*

*If $ C = 2$, then it greatly depends on the constants (and should be pretty obvious.).

*If $ |C| < 2 $, then the RHS is eventually negative, so we can restrict to considering "small" cases.


To solve the problem, cross multiply and factor to get
$$ (a-b)^3 - (a+b)^2 - 2 = 0. $$
The problem is then equivalent to showing that $ x^3 - y^2 = 2 $ only has one solution, namely $ (3, 5)$.
See solution here, which uses ideas of $\mathbb{Z} [ \sqrt{-2} ] $.
It suggests that you need much more advanced tools than what you just listed out.
