Does $2x^2-1=y^5$ have a solution in integers, with $y>1$?

In my solution to this MSE problem, I noted that $2x^2-1=y^5$ is unlikely to have solutions in integers with $y>1$. Recently, I've tried to find a proof, without success.

Following Thomas Andrews's suggestion (see his solution to the same problem), we start by writing $1-2x^2=(-y)^5$. Working in the ring $\mathbb{Z}[\sqrt{2}]$ we can factorize this as $$(1-x\sqrt{2})(1+x\sqrt{2})=\text{ a fifth power }.$$ After showing that $1-x\sqrt{2}$ and $1+x\sqrt{2}$ are relatively prime (always working in $\mathbb{Z}[\sqrt{2}]$), the proposed equation would force $$1+x\sqrt{2}=u(a+b\sqrt{2})^5$$ for some integers $a,b$ and some unit $u$.

The group of units in $\mathbb{Z}[\sqrt{2}]$ is given by $\pm (1+\sqrt{2})^n$ for $n\in \mathbb{Z}$. A minus sign could be absorbed into the fifth power, so we only need to show that $$1+x\sqrt{2}=(1+\sqrt{2})^\delta(a+b\sqrt{2})^5$$ for some integers $a,b$ and $0\leq \delta\leq 4$ forces $|x|\leq 1$. Here I am following the method described by Adrián Barquero in this MSE question for dealing with an infinite group of units.

For $\delta=0$, it is pretty straightforward but for $\delta=1$, I'd need to show that $$1= a^5+20 a^3 b^2+20 a b^4+10 a^4b+40a^2b^3+8b^5$$ is not possible, excepting the trivial solution $a=1$ and $b=0$. I haven't made any progress with this, or the other similar expressions we get when $\delta=2,3,4$. I'm stuck here, and this problem seems to me to be as difficult as the original question.

Question: Can the method outlined here be pushed through to give a full solution, or does this problem require higher level approaches?

I'm clearly out of my depth with algebraic number theory, so any suggestions or references that are suitable for amateurs will be greatly appreciated.

Update (Feb. 20) I have followed Ewan's suggestion and tested all the cases $\delta=0,1,2,3,4$ with Sage and there really are no solutions with $y>1$. I will wait a couple of days before rewarding the bounty in case an elementary solution is given. Otherwise, it will go to Ewan.

The answer to your question is YES, the method can be pushed to a full solution, if you are willing to rely on some standard number theory software (see below). Of course you may still ask for a computer-free proof, that unfortunately may not exist because of the horribly complicated computations involved.

You asked about the equation $Q(a,b)=1$, where $Q(a,b)=a^5 + 10ba^4 + 20b^2a^3 + 40b^3a^2 + 20b^4a + 8b^5$. This is a Thue equation, which can be solved by a one-liner in GP and other software : just type

thue(thueinit(a^5 + 10*a^4 + 20*a^3 + 40*a^2 + 20*a + 8,1),1)

and, lo and behold, GP tells you that the only solution is (a=1,b=0), just as you guessed. You can download and install GP on your computer, or, if you are lazy, just use GP directly online at http://www.sagemath.org/

If $\zeta$ denotes the unique real root of $Q(1,t)=0$, and $\cal O$ denotes the ring of integers of the number field ${\mathbb Q}(\zeta)$, the equation $Q(a,b)=1$ reduces to the problem of finding a unit in $\cal O$ of the form $a+b\zeta$ where $a$ and $b$ are integers.

The equation $1= a^5+20 a^3 b^2+20 a b^4+10 a^4b+40a^2b^3+8b^5$ that you run against is of the form $f(a,b)=1$ where $f$ is a homogeneous form of degree at least $3$.

A theorem of Thue asserts that $$|f(a,b)|\geq C_{\varepsilon} (|a|+|b|)^{n/2-1-\varepsilon},$$ where $n=\deg f$. It is equivalent to the more-familiar version which is about the approximation of algebraic numbers. If $g(x)$ is a polynomial of which an algebraic number $\alpha$ is a root, then $q^n g(p/q)$ is a homogeneous form of degree $n$ in $p$ and $q$. Conversely, if $f(x,y)$ is a homogeneous form, then we can factor $f(x,y)=\prod (x-\alpha_i y)$ for some algebraic numbers $\alpha$. We can assume these $\alpha$ are distinct because we can assume that $f$ is irreducible. So, for any $p,q$ have $f(p,q)=C(|p|+|q|)^{n-1}(p-\alpha q)$, where $\alpha$ is the closest of the roots to $p/q$. Then the result follows from the lower bound on $|p/q-\alpha|$.

Thus, Thue's theorem tells us that the number of solutions to the equation is finite. However, it is no use in finding these solutions since the constant $C_{\varepsilon}$ is non-effective, meaning the proof gives no bound on it (it does give a bound for the constant $C_{\varepsilon}$ for which the inequality holds with at most a single exception). Roth's theorem strengthens Thue's result, giving $|f(a,b)|\geq C_{\varepsilon}(|a|+|b|)^{n-2-\varepsilon}$, but also suffers from non-effectivity.

There are effective lower bounds on homogeneous forms, but they come with fairly large bounds. For example, Fel'dman proved that $$|f(a,b)|\geq C (|a|+|b|)^{c}$$ for some effective positive constants $C$ and $c$ that depend on $f$ (very badly!). This was the first effective power bound. I do not know what the state of the art in the effective improvements on Liouville's theorem is, but as far as I hear the bounds are still astronomical. To check that there are no solutions below the upper bound that one obtains from these results, one often needs a good deal of cleverness even with the aid of modern computers. However, I will expose the true depth of my ignorance if I say any more.