Matrix diagonalization and eigenvector computation constructively

Without polishing up on linear algebra, the not very subtle topological answer is yes. Different eigenvalues $\lambda_i$ mean unique solutions (the eigenvectors) on the unit hemisphere, of the kernel equations $(A-\lambda_i I)v=0$.

These solutions can be found by approximation using compactness and uniform continuity.

With the $n$ different eigenvectors at hand, diagonalization should give no trouble at all.

The following works constructively over an arbitrary local ring $R$ (constructively, $\mathbb{R}$ is a local ring).

Assume that you matrix $M$ is canceled by a polynomial $Q$, of degree $m$ (with leading coefficent $1$), that $Q$ can be factored into

$$Q= \prod^m_{i=1}(X-q_i)$$

and that for each $i \neq j$, $(q_i - q_j)$ is invertible (in the case of $\mathbb{R}$ it just means that $q_i$ and $q_j$ are appart).

Then one can diagonalize $M$. In particular it can be applied when you have some multiplicites in your eigenvalue as long as the minimal polynomial has simple roots.

Let $$P_i = \frac{\displaystyle \prod_{j \neq i} (X-q_j)}{ \displaystyle \prod_{j \neq i} (q_i-q_j)} $$

i.e. $P_i(q_i)=1$ and if $i \neq j$ , $P_i(q_j)=0$

It is constructive that a polynomial is divisibe by $Q$ if and only if it vanishes at all the $q_i$ (basically because polynomial division by a polynomial with unit leading coefficient works well). Hence you can easily check that:

$(P_i)^2 - P_i$

$P_i P_j$

$1-\sum_i P_i$

$X-\sum_i q_i P_i$

are all divisible by $Q$ and hence cancel $M$. So the $P_i(M)$ form a complete family of projection, and $M = \sum q_i P_i(M)$ and you get the spectral decomposition of $M$.

At this point, if you already know how to find eigen vectors for projections then you are done: the range of each $P_i$ are in direct sum so you just find a basis of each of these subspaces and you get your diagonal basis.

I have not read the paper by Coquand & Lombardi you are quoting so I'm not sure what is their method for the last step. I know of a process for this that work for local ring of 'zero residual characteristic' (i.e. in which integer are invertible sot ) I'm not sure what happen in the fully general case, but it is already enough for the case of $\mathbb{R}$.