Is it possible to constructively prove that every quaternion has a square root?

Reduction to LLPO (Lesser Limited Principle of Omniscience).

The statement LLPO is the following (from Wikipedia): For any sequence a₀, a₁, ... such that each a_i is either 0 or 1, and such that at most one a_i is nonzero, the following holds: either a_2i = 0 for all i, or a_2i+1 = 0 for all i, where a_2i and a_2i+1 are entries with even and odd index respectively.

This is considered a quintessentially non-constructive claim.

The claim that every quaternion has a square root implies LLPO.

Consider a sequence $(p_n)_{n \geq 1} \in \{0,1\}$, with the property that at most one element of the sequence is equal to $1$. Consider the following infinite quaternionic series $q = -1 + i\left(1 - \sum_{n=1}^\infty\frac{1 - p_{2n}}{2^n}\right) + j\left(1 - \sum_{n=1}^\infty\frac{1 - p_{2n+1}}{2^n}\right)$. The series clearly converges. Now we assume that we can get an $r$ such that $r^2 = q$. Consider the angle $\theta$ between $r$ and $i$ (considered as 4d vectors with the standard inner product), and likewise consider the angle $\phi$ between $r$ and $j$. Either $\theta > \arctan(1/2)$ or $\phi > \arctan(1/2)$, as these two open regions cover all the non-zero quaternions. If $\theta > \arctan(1/2)$ then we conclude that all $p_{2n}=0$. If $\phi > \arctan(1/2)$ then we conclude that all $p_{2n+1}=0$. This is exactly LLPO.

([edit] The discussion between me and Andrej refers to an earlier version of the argument, which was more confusing than this one)

The operation is not Type 2 computable. The argument is similar to how the set $\mathbb R$ is not computably equivalent to its decimal representation. This latter statement is called the tablemaker's dilemma. Constructivists and Type 2 computability theorists make use of a redundant "nega-binary" representation of real numbers instead.

Let $q=-1 + 0i + 0j + 0k$. Assume the T2TM (Type 2 Turing Machine) outputs a quaternion $r$. This $r$ is a vector. Now observe that the machine must have read only finitely many digits of the nega-binary representation of $q$. Displace $q$ by some vector $v$ which is not parallel to $r$, where the vector $v$ has magnitude smaller than $2^{-n}$, where $n$ is the number of nega-binary digits the machine has read. The machine must give the same output because the prefix of the new input is the same, but this output is wrong.

To demonstrate that two quaternions very close to $-1$ may have very different square roots: Consider $-1 + \epsilon i$: Its square roots are $\pm (i + \frac{\epsilon}2)+ o(\epsilon)$. Now consider $-1 + \delta j$: Its square roots are $\pm (j + \frac{\delta}2)+ o(\delta)$. Now the distance between each of each of these sets is at least $\sqrt{2}$, which is much greater than zero. If after reading $n$ digits of $q = -1.0 + 0i + 0j + 0k$, the machine decides to output the first digits of $0 + 1i + 0j + 0k$, then one can play a trick on it by changing $q$ to $q' = -1 + 0i + 10^{-2n}j + 0k$. Those first digits of the output will then be completely wrong.

This T2TM argument is probably a valid Type 1 argument. In which case, it provides a convincing proof that quaternion square-root is uncomputable, and therefore can not be proved constructively.

It would be nice to see a "purer" proof that reduces to LPO or some other such principle, but I can't think of one. [edit] See below.