Is it possible to constructively prove that every $q \in \mathbb H$ has some $r$ such that $r^2 = q$? The difficulty here is that $q$ might be a negative scalar, in which case there might be "too many" values of $r$. Namely, $r$ could then equal any vector quaternion of magnitude $\sqrt{|q|}$. The presence of this seemingly severe discontinuity suggests that there can't be a way to constructively prove that every quaternion has a square root.

The variety of constructivism can be as strong as possible. So any Choice principle, or Markov's Principle, or Bar Induction, is allowed.

My thoughts were to do some kind of reduction to $LPO$ or $LLPO$ or $LEM$. But I don't see how.

The way to find a square-root classically is as follows: If $q = w + xi + yj + zk$ is not a scalar quaternion, then it lies on a unique "complex plane". This is due to the fact that a vector quaternion (of the form $xi + yj + zk$) always squares to $-(x^2 + y^2 + z^2)$, which is a negative scalar. The problem then reduces to finding the square root of a complex number. The difficulty is exactly in the case when $x=y=z=0$ and $w < 0$, in which case $q$ and $r$ lie on *all* complex planes.

ispossible to prove that everycomplex numberhas a square root in spite of the fact that there is nocontinuous functionthat gives the square root $\endgroup$ – ogogmad Sep 19 '19 at 18:26