Finite dimensional real division algebras

Question

A celebrated theorem of Milnor and Kervaire asserts that any finite dimensional (not necessarily associative, unital) division algebra over the real numbers has dimension 1,2,4 or 8. This result is established using methods from algebraic topology, such as K-Theory.

Now for any given natural number $n$ the existence of such an algebra of dimension $n$ is expressible as an assertion $\phi_n$ in the first-order language of field theory. Since the theory $RCF$ of real closed fields is complete, it follows from the theorem above that $RCF \vdash \neg \phi_n$ for all $n\not\in$ {1,2,4,8}. Here the universal quantifier on $n$ is in the meta-theory: we might say that for each $n$ there is an elementary proof of $\phi_n$.

Given such a theorem scheme, one might wonder whether there might be a uniform elementary proof. Informally this could mean a proof by induction on the relevant complexity parameter: for example, $$RCF \vdash \mbox{ any degree } d \mbox{ polynomial has at most } d \mbox{ roots}.$$ I would like to imagine that there is some first order-theory which suitably contains both RCF and Peano Arithmetic (in particular, so as to enable discussion of finite sequences of field elements) in which the assertion $$\forall n \;\phi_n\leftrightarrow(n=1 \vee n=2 \vee n=4 \vee n=8)$$ can be legfitimately formalized. Are there standard constructions for supporting finite sequences? If so, it should follow from completeness of RCF that this assertion is equivalent (within such a larger theory) to a sentence $\Phi$ in the language of arithmetic. As noted above, via difficult results from topology, $\Phi$ is true in the standard model of Peano Arithmetic. Consequently, it makes sense to ask whether $\Phi$ is provable within Peano Arithmetic.

Some questions:

(1) Can such a recipe be formalized, and does it reasonably capture the notion of "uniform elementary proof" or "purely algebraic" proof for such theorem schemes? Here I am not necessarily claiming that these conjectural notions are the same.

(2) In the given example of the 1,2,4,8 theorem, do we expect $\Phi$ to be provable in Peano Arithmetic?

Perhaps I have been looking in the wrong places, but all I have managed to find are a few comments by Kreisel about "unwinding", on pages 67-68 of this note: http://elib.mi.sanu.ac.rs/files/journals/zr/10/n010p063.pdf

The situation could be compared with what is known in the special cases of commutative division algebras (dimensions 1,2) and associative division algebras (dimensions 1,2,4). Hopf's proof of the (1,2) theorem also uses some topology, namely that the $n$-dimensional sphere and $n$-dimensional projective space are not homeomorphic when $n>1$; in fact it suffices to show that a specific map between these spaces is not a homeomorphism. Perhaps there is an elementary way to formulate this consideration? On the other hand, there is a different and "purely algebraic" proof, via Bezout's Theorem. I don't have the reference at hand, but it there is a citation (froom the 1950s, as I recall) in the Springer-Verlag book Numbers (Ebbinghaus et. al.). I've seen this proof dismissed as unreadable or unenlightening, but when I examined it years ago it seemed like it might qualify. The Frobenius proof of the (1,2,4) theorem is quite evidently purely algebraic, as is the later extension (1,2,4,8) to alternative division algebras.

Answer 1

If you ask for a purely algebraic proof, algebraic K-theory is (almost) OK. Indeed for a compact Hausdorff space $X$, it's topological K-theory $K(X)$ is the same as algebraic K-theory $K_0(C(X;\mathbb{C}))$. So rewrite the proof of Bott-Milnor-Kervaire we will get a (almost) purely algebraic proof.

EDIT(More detail):

The method topologists solve this problem (according to my knowledge) is constructing an complex line bundle $\xi$ over real projective space $\mathbb{R}\mathbb{P}^{n-1}$, and claim that $n(\xi-\varepsilon)=0$ in $K(\mathbb{R}\mathbb{P}^{n-1})$, where $\varepsilon$ is the (complexification of) trivial line bundle over $\mathbb{R}\mathbb{P}^{n-1}$. Since we can compute $K(\mathbb{R}\mathbb{P}^{n-1})=\mathbb{Z}/2^{[\frac{n-1}{2}]}\mathbb{Z}$ with a generator $\xi-\varepsilon$, we must have $2^{[\frac{n-1}{2}]}|n$, and thus $n=1,2,4,8$.

Now let $A=C(\mathbb{R}\mathbb{P}^{n-1};\mathbb{C})$, the ring of continuous functions from $\mathbb{R}\mathbb{P}^{n-1}$ to $\mathbb{C}$. As above we can construct a finite generated projective module $\Gamma(\xi)$ over $A$ and so on. The idea of topological proof now becomes purely algebraic except that the concept of continuous.