Constructive Mathematics – Is Hurwitz’s Theorem True?

Question

Hurwitz's theorem says that the only division composition algebras over the real numbers $\mathbb{R}$ are the real numbers themselves $\mathbb{R}$, the complex numbers $\mathbb{C}$, the quaternions $\mathbb{H}$, and the octonions $\mathbb{O}$. However, in pure constructive mathematics without any weak axiom of choice, the notion of the set of real numbers bifurcates into multiple incompatible notions, such as the Cauchy real numbers $\mathbb{R}_C$, the Dedekind real numbers $\mathbb{R}_D$, the Escardó-Simpson real numbers $\mathbb{R}_E$, and the MacNeille real numbers $\mathbb{R}_M$, and I'd imagine the same for $\mathbb{C}$, $\mathbb{H}$, and $\mathbb{O}$ (i.e. Cauchy complex numbers, Dedekind quaternions, etc). For which of these sets of real numbers, complex numbers, quaternions, and octanions, if any at all, does Hurwitz's theorem still hold true?

---

Edit: Swapped out "normed division algebra" for "division composition algebra" for the following reason:

Classically, Hurwitz's theorem is also expressed in terms of finite-dimensional normed division algebras over that set of real numbers. However, finite-dimensional normed divison algebras and division composition algebras over the real numbers do not coincide in constructive mathematics because there are multiple different types of real numbers in constructive mathematics.

In a division composition algebra, the norm $\lvert a \rvert := \langle a, a\rangle$ has a codomain of the ground field.

However, that is not necessarily true of finite-dimensional normed division algebras over some field of real numbers $\mathbb{R}_X$ in constructive mathematics, because the notion of "multiplicative norm" bifurcates into multiple definitions based upon which set of real numbers $\mathbb{R}_Y$ is used as the codomain of the norm. It is perhaps more appropriate to call them finite-dimensional $\mathbb{R}_Y$-normed division $\mathbb{R}_X$-algebras. One can have a finite-dimensional normed division $\mathbb{R}_C$-algebra with a norm valued in $\mathbb{R}_D$, where $\mathbb{R}_C$ are the Cauchy real numbers and $\mathbb{R}_D$ are the Dedekind real numbers, but such a finite-dimensional normed division algebra is not a composition algebra, and is not covered under Hurwitz's theorem.

Thus, for sets of real numbers $\mathbb{R}_X$ and $\mathbb{R}_Y$, every division composition $\mathbb{R}_X$-algebra for some set of real numbers $\mathbb{R}_X$ is a finite-dimensional $\mathbb{R}_X$-normed division $\mathbb{R}_X$-algebra, but a finite-dimensional $\mathbb{R}_Y$-normed division $\mathbb{R}_X$-algebra is only a division composition $\mathbb{R}_X$-algebra if $\mathbb{R}_Y$ is isomorphic to $\mathbb{R}_X$.

Answer 1

There is a weakening of Hurwitz's theorem that is true constructively, with essentially the same proof:

Let $A$ be a division composition algebra. Then any chain of proper subalgebras $\mathbb{R} = A_0 \subsetneq A_1 \subsetneq \cdots \subsetneq A_n = A$ has length $n \leq 3$ (where "proper" means "contains an element with positive distance from the previous algebra).

We can also show that in general, any inclusion of subalgebras generated by adding one element must come from (a quotient of) the General Cayley-Dickson construction with parameter $\cdot \gamma$, $\gamma \leq 0$.