Every complex number has a square root via LLPO without weak countable choice

Question

Is it possible to prove that every complex number has a square root using analytic LLPO, but avoiding Weak Countable Choice or Excluded Middle? Unique Choice is allowed.

(Analytic LLPO is the statement that given any pair of real numbers $x$ and $y$, either $x \leq y$ or $x \geq y$. This statement is non-constructive, but still weaker than other statements like LPO or Excluded Middle.)

It is true in Johnstone's Topological Topos. This is because the Fundamental Theorem of Algebra is true for Cauchy Real numbers, and Cauchy reals are isomorphic to Dedekind reals in the Topological Topos. But this reasoning doesn't seem to work unless Cauchy is iso to Dedekind.

Answer 1

Yes it is but there is no extensional square root function unless we also have LPO.

Note that the squaring function is a bijection from $Q_{+} = \{x + iy \mid x \geq 0, y \geq 0\}$ onto $H_{+} = \{x + iy \mid y \geq 0\}$. Similarly it is a bijection from $Q_{-} = \{x + iy \mid x \geq 0, y \leq 0\}$ onto $H_{-} = \{x + iy \mid y \leq 0\}$. Given LLPO, $H_{+} \cup H_{-} = \mathbb{C}$ and that is enough to prove the existence of square roots. The confusing part is that for a negative real number $x$, we obtain the square root $+ i\sqrt{-x}$ or $-i\sqrt{-x}$ depending on whether LLPO gives $x \in H_{+}$ or $x \in H_{-}$. So this does not give an extensional square root function.

Interestingly, this argument gives the stronger conclusion that every complex number has a square root in $$Q_{+} \cup Q_{-} =\{ x + iy \mid x \geq 0\}. $$ This stronger statement turns out to be equivalent to LLPO. Indeed, given a small enough real number $x$, if the square root of $-1+ix$ in $Q_{+} \cup Q_{-}$ is close to $i$ then $x \geq 0$ and similarly if that square root is close to $-i$ then $x \leq 0$.