In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple Cauchy complete Archimedean ordered fields, which are not provable to be equivalent to each other: one cannot in general prove that the Dedekind real numbers embeds into the initial Cauchy complete Archimedean ordered field. (By Cauchy complete we mean complete by Cauchy sequences, not Cauchy nets.)
The principal square root function is a function defined on the non-negative elements $[0, \infty)$ of a Cauchy complete Archimedean ordered field $\mathbb{R}$ such that it is a two-sided inverse of the square function $x^2$ when $x^2$ is restricted on the domain and codomain to $[0, \infty)$.
In classical mathematics, one could prove that the principal square root function exists by proving the fundamental theorem of algebra for any Cauchy complete Archimedean ordered field. However, in constructive mathematics, the fundamental theorem of algebra cannot in general be proven for Cauchy complete Archimedean ordered fields.
In classical mathematics, there is an alternative to proving that the principal square root function exists: by first proving that zero has a square root, and that there exists a two-sided inverse function of $x^2$ on the positive elements $(0, \infty)$ of $\mathbb{R}$. The square root of zero is zero in any integral domain, and because in any Cauchy complete Archimedean ordered field the square function $x^2$ is continuously differentiable on the open interval $(0, \infty)$ and its derivative $2x$ is always positive on the open interval $(0, \infty)$, by the inverse function theorem, there exists a two-sided inverse defined on $(0, \infty)$. (In constructive mathematics, the inverse function theorem still holds for $x^2$ because $x^2$ is uniformly differentiable on every closed subinterval of $(0, \infty)$. Then we use excluded middle to show that if the principal square root function is defined at $0$ and defined on the domain $(0, \infty)$, then it is defined on $[0, \infty)$. However, in constructive mathematics, by definition there is no excluded middle, so we cannot prove the last step.
The exponential function is defined by a particular Taylor series, and the logarithm function could be defined by an analytic continuation of a particular Taylor series. Thus, one could try to define the square root as the function
$$e^{\frac{1}{2} \ln(x)}$$
However, because $\ln(x)$ is undefined at $x = 0$, that function is only defined on the open interval $(0, \infty)$. Similarly to the previous attempt, in classical mathematics, one could use excluded middle to extend the function to $[0, \infty)$, but that isn't possible in constructive mathematics.
Is there a way of proving that the principal square root function on the non-negative elements of a Cauchy complete Archimedean ordered field actually exists? I might be missing something very obvious. Or is it not provable in constructive mathematics that such a function exists in all Cauchy complete Archimedean ordered fields?
This is fairly important because it is one of the functions used in defining the Euclidean metric in finite-dimensional vector spaces over Cauchy complete Archimedean ordered fields. If the latter is the case, then one might have to equip Cauchy complete Archimedean ordered fields with the additional structure of a principal square root function in order to do constructive Euclidean geometry.
Best Answer
I think see how this is related to your other questions. These are not resolved last I checked, but the following will answer this question whichever way the other questions end up going.
I believe the following are constructively equivalent for any notion of $\mathbb R$ which is Cauchy complete assuming that unique choice is valid:
The equivalence of 1 and 2 follows from these relations: $$|x| = \max(x,-x), \qquad \max(x,y) = \frac{x + y + |y - x|}{2}, \qquad \min(x,y) = \frac{x + y - |y - x|}{2}.$$ That 3 implies 2 follows from $|x| = \sqrt{x^2}$.
The fun part is that 1 & 2 implies 3. As you have observed, there is a square root function $(0,\infty)\to(0,\infty)$ by the Inverse Function Theorem.
With this apparatus, we can define continuous functions $f_n:[0,\infty)\to[0,\infty)$: $$f_n(x) = \begin{cases} 1/2^n & \text{when $0 \leq x \leq 1/4^n$} \\ \sqrt{x} & \text{when $x \geq 1/4^n$} \\ \end{cases}$$ As stated, that requires knowing whether $x \leq 1/4^n$ or $x \geq 1/4^n$, but we can work around this by patching two functions together:
Since these functions agree on their overlap, and their domains comprise all of $[0,\infty)$ we do get a total function $f_n:[0,\infty)\to[0,\infty)$ as a result. (This is where unique choice is used.)
Now the sequence of functions $(f_n)_{n=0}^\infty$ so defined converges uniformly on any closed bounded interval to a continuous function $f:[0,\infty)\to[0,\infty)$. It is easily seen that this is indeed the square-root function: $(f(x))^2 = x$ for all $x \geq 0$.
In the above, I discreetly used the fact that a uniformly Cauchy sequence $(f_n )^\infty_{n=0}$ of continuous functions on a closed bounded interval converges to a continuous function on that interval. This is a straightforward consequence of Cauchy completeness and unique choice, so nothing to worry about... but it just occurred to me that this is enough to prove the existence of the absolute value function. To do this without circular reasoning, we need to pick a sequence $(f_n)_{n=0}^\infty$ whose definition doesn't involve min/max, absolute values, square root. That takes some thought but I believe $f_n(x) = x\tanh(n x)$ does the trick!
So it looks like all three statements above are equivalent because they are all true!
As mentioned in the comments, there are two common notions of "Cauchy complete" used in constructive mathematics. The "classical" notion, in symbolic form, is: $$\forall \varepsilon > 0\,\exists N\,\forall m, n \geq N\,[-\varepsilon < x_m - x_n < \varepsilon]$$ (I avoided the customary absolute value for good form.) The stricter notion requires a modulus of convergence $\phi : \mathbb N\to\mathbb N$ such that: $$\forall m,n \geq \phi(N)\,\left[\frac{-1}{2^N} < x_m - x_n < \frac{1}{2^N}\right]$$ There's a bunch of equivalent variations but you get the idea... The latter is usually preferred by constructivists because of things like the Specker sequence.
The answer above is agnostic about this distinction since it is straightforward to supply the requisite modulus of convergence wherever Cauchy completeness is used.