The problem is: find integer a that satisfies the 5-adic norm inequality $|a^2+6|_{5}<5^{-4}$.
I tried in vain finding it computationaly. Are there any methods from number theory to help me solve it?
An equivalent problem is: find x>5, r, s and $gcm(r,s,5)=1$ s.t. $a=(5^x r/s-6)^{1/2}$ is an integer.
I have a good idea for proving existence using Hensel's lemma but it would be nice to have them explicitly. thanks
Consider the polynomial map $f : \mathbb{Z}_5 \to \mathbb{Z}_5, x \mapsto x^2+6$. Since $f$ is continuous $\{ x \in \mathbb{Z}_p : |f(x)|_5 < 5^{-k} \}$ is an open set, and since $\mathbb{Z}$ lies dense in $\mathbb{Z}_p$ we only have to show that this set is nonempty to proof the existence of an integral solution. Now by Hensel's lemma there exists a 5-adic square root of $-6$ which provides obviously a solution for any $k$.
For explicitly computing an integral solution just use Newton's method to approximate a 5-adic square root of $-6$ by integers. The above proof guarantees that you will reach an integral solution to your inequality after finitely many steps.
Let us for example compute a solution for $k=4$ as asked in the question. We start by approximating a root of $f$ by rational numbers using Newton's method. We first set $a_0 := 2$ since this is a root for $f$ modulo $5$, and then calculate iteratively $a_{n+1} := a_n - \frac{f(a_n)}{f'(a_n)}$. In this way we obtain $a_1 = -\frac{1}{2}$, $a_2 = \frac{23}{4}$, $a_3 = \frac{433}{184}$, and so on. The latter one is a rational solution to the inequality, since $|(a_3)^2 + 6|_5 = |\frac{390625}{33856}|_5 = 5^{-8} < 5^{-4}$. Of course $a_3$ is no ordinary integer but it is a $5$-adic integer, and especially its denominator $184$ is a $5$-adic unit whose inverse can be approximated by integers.
By testing the inverses of $184$ modulo $5^i$ for increasing $i$ we find that its inverse $2089$ modulo $3125 = 5^5$ suffices. Let $a := 433 \cdot 2089 = 904537$ then we have $|a^2+6|_5 = |818187184375|_5 = 5^{-5} < 5^{-4}$. Therefore $a$ is a desired solution.