On 5-adic representation of square root of -1 Let $\alpha \in \mathbb{Z}_5$ be the solution to $f(x):=x^2+1=0$ such that $\alpha \equiv 2 \, (\text{mod} \,5)$ (that we obtain by Hensel's lemma). Then
$$ \alpha = \sum_{k=0}^{\infty} a_k \, 5^k$$
where $a_0=2$ and $0\leq a_{n+1}<5$  is the only integer such that  $a_{n+1}\equiv f(S_n)/5^{n+1}  \, (\text{mod} \,5)$ where $S_n=\sum_{k=0}^{n} a_k \, 5^k$. Similarly if $b_0=3$ and $0\leq b_{n+1}<5$  is the only integer such that  $b_{n+1}\equiv -f(T_n)/5^{n+1}  \, (\text{mod} \,5)$ where $T_n=\sum_{k=0}^{n} b_k \, 5^k$, then 
$$ \beta = \sum_{k=0}^{\infty} b_k \, 5^k$$
would give us the other root (i.e. $\beta=-\alpha$).
I have some numerical evidence that suggest the following inequalities should be true for all $l \geq 2$
$$ 5^{2(l-4)}\leq  \sum_{k=l+1}^{2l-1} a_k \, 5^k $$
$$ 5^{2(l-4)}\leq  \sum_{k=l+1}^{2l-1} b_k \, 5^k  $$
Here I plot $2(l-4)/\log_5 \left( \sum_{k=l+1}^{2l-1} a_k \, 5^k \right)$ for $2\leq l \leq5000$ note that it's always bounded by 1 , and here I do the same for  $2(l-4)/\log_5 \left( \sum_{k=l+1}^{2l-1} b_k \, 5^k \right)$.
(sorry for the quality I'm not allow to embed images yet, just links)
The reason I'm interested in this inequalities is that they would give a way to prove that the only solutions for $n^2 + 1 = 2 \times 5^m$ with $n\geq 0$ are $(n,m) = (1,0),(3,1), (7, 2)$. 
Indeed, let $(m,n)$ be a solution then $(n-\alpha)(n-\beta)=2 \times 5^m$, also $(n-\alpha)-(n-\beta)=-2\alpha$, thus either $n-\alpha$ or $n-\beta$ have $5$-adic valuation equal to $m$ and the other valuation $0$, let's say $n-\alpha$ have valuation $m$, then since 
$0\leq n =\sqrt{2 \times 5^m -1}<5^m$ (at least for $m \geq 1$), and $n$ is an integer we must have
$$n=\sum_{k=0}^{m-1} a_k \, 5^k$$
Now write $m=2l+r$ for $r\in\{0,1\}$, diving by $5^l$ we have that
$$a_{0}5^{-l}+\ldots +a_{l}+ a_{l+1}5+\ldots+ a_{m-1}5^{l+r-1}=\frac{n}{5^l}\leq \sqrt{2 \times 5^r -5^{-2l}}<\sqrt{10}<5 $$ but that would imply
$a_{l+1}=0,a_{l+2}=0, \ldots,a_{m-1}=a_{2l+r-1}=0$ that would clearly contradic the first inequality, we could do the same if the valuation of $n-\beta$ is the one that is $m$ leading us to contradiction again, thus $l\in \{0,1 \}$ and the given solutions are the only ones.
My questions are:
1.  Is my reasoning ok?
2. Are this inequalities true?
2.  Can we prove this inequalities?
3.  Can we at least prove the RHS's are nonzero?

Update: Thank to the answer of @Gerry Myerson I realized that the real question I should be asking it's whether or not the $a_k$'s are evenly distributed in $\{0,1,2,3,4\}$, if that the case acording to this we should expect to be a run of $\geq r$ zeros in the first $n$ of the $a_k$'s if $n \approx (1/4)5^{r+1}$. With this in mind I've found  a run of 6 zeros from $k=12412$ to $k=12417$, with a little more efford we could find a run of 8 zeros that would prove the inequality wrong (that would require $k$ to be roughly $500000$ but I don't see the point in doing it).
However theses are still good news because if they're indeed evenly distributed, then $ \sum_{k=l+1}^{2l-1} a_k \, 5^k \neq 0$ because otherwise almost half of the $a_k$'s would be zero not $1/5$, and that's all we need for the diophantine equation.
So, Are there any result on "normality" of  p-adic square roots ?. At
 least one powerfull enough to prove $ \sum_{k=l+1}^{2l-1} a_k \, 5^k \neq 0$ for all $l$ bigger than some effective bound ?.
 A: The result you hinted at is true, and follows from some facts about gaussian integers and recurrent sequences. Indeed we have:
Lemma: For any $C>0$, it is true for sufficiently large $m$ (deppending on $C$) that if $5^m$ divides $n^2+1$, then $n^2+1 > C 5^m$.
This lemma for say $C = 16 \cdot 5$ implies your result for the expansion having a non-zero digit between $l+1$ and $2l-1$ (without any non-zero digit, the truncation up to $2l-1$ would give $n < 4 \cdot 5^l$ (so $n^2+1 \le 16 \cdot 5 \cdot 5^{2l-1}$) for which $5^{2l-1}$ divides $n^2+1$, contradictng the lemma. In fact it is easy to see the lemma is equivalent to showing that for any $c$ the expansion has a non-zero digit between $n$ and $2n-c$ for large $n$.
Proof of lemma: if $5^m$ has prime factorization $(2+i)^m(2-i)^m$ in gaussian integers, and if it divides $n^2+1=(n+i)(n-i)$, then $(2+i)^m$ must divide one factor and $(2-i)^m$ the other (notice that $gcd(n+i,n-i)$ divides $2i$). 
So say $\tau \cdot (2+i)^m = n+i$ where $\tau$ is a gaussian integer. Then $n^2+1 = N(\tau) \cdot 5^m$ (taking norms). Because there are only finitely many gaussian integers $\tau$ with $N(\tau) \le C$, it is enough to show that for each $\tau$, $\tau (2+i)^m = n+i$ has finitely many integer solutions. But if for some $m$ that is a solution, taking imaginary parts of both sides we get then $\tau (2+i)^m -\overline{\tau} (2-i)^m = 2i$.
But $a_m = \tau (2+i)^m -\overline{\tau} (2-i)^m - 2i$ is a linear recurrent sequence of degree 3, and these have finitely many zeroes from something such as Skolem–Mahler–Lech Theorem. So we are done with proving the lemma. Maybe there is something more specific that can be done for this case that give better bounds, since all of this is very ineffective. 
