Current status of computable spectral theorem and interpretation of quantum mechanics The spectral theorem states if $A$ is a Hermitian operator acting on an $n-$dimensional Hilbert space space $H$, and $\lambda_1, ... \lambda_m$ are $m \leq n$ distinct eigenvalues of $A$, then 
$$ H=\oplus_{i=1}^{m} H_i,$$
where $H_i$ are the corresponding eigenspaces, and in turn
$$ A = \sum_{i=1}^{m}\lambda_i P_i,$$
where $P_i$-s are the corresponding projections. It is known that the spectrum of a Hermitian operator acting on a finite-dimensional Hilbert-space can be computed provided that its cardinality is known beforehand, or, alternatively, that for each pair of eigenvalues $\lambda_i, \lambda_j$, it is known whether $\lambda_i = \lambda_j$ or $\lambda_i \neq \lambda_j$. It is a crucial condition when we try to build a computable foundation of quantum mechanics since deciding which eigenvalue is actually measured essentially defines what eigenspace the system falls into after the measurement. The problem of degeneracy is described in Bridges and Svozil, 2000 in the following example:

Under this link, I came across this book of Ye where he explains the degeneracy problem as follows:

The representation in [when $\forall i,j. \lambda_i \neq \lambda_j \lor \lambda_i = \lambda_j$] above is exactly the same as the classical case. It seems
  that indistinguishable $\lambda_i$-s arise only in artificial constructions. In other words, we
  expect that the operators on finite-dimensional spaces appearing in natural physics
  contexts all satisfy the condition $\forall i,j. \lambda_i \neq \lambda_j \lor \lambda_i = \lambda_j$. Because, in quantum mechanics, the spectrum of an operator A is supposed to consist of the possible values
  of the observable corresponding to A. Any realistic observation can be performed
  only up to a finite precision. So, in a finite dimensional case, we can expect that the
  eigenvalues are all mutually distinguishable.

What is actually behind such a justification and what does it have to do with the fact that each measurement can be done up to a finite precision?
I also have a side question regarding the following theorem of Ziegler and Brattka (2001):

where a matrix is called computable iff the corresponding linear map is computable. How does this fact enable us to reconstruct exactly the classical theorem? I can't see how we'd obtain the cardinality of the spectrum just from the condition that $A$ be computable (normal) matrix.
WARNING: there is no such a corollary in the preprint!
 A: I think the point is this.  It is impossible in general to decide computationally whether two computable real numbers $\alpha$ and $\beta$ are equal.   If in fact they are not equal, by computing sufficiently good approximations you can determine that they are not equal, but no finite computation can determine that they are equal.
For a polynomial $P(\lambda)$ (in particular the characteristic polynomial of a matrix), the roots of $P$ are distinct iff the discriminant of $P$ is nonzero.  This discriminant is a polynomial in the coefficients, so it is computable.  But again, if the discriminant happens to be $0$ we can't determine that by a finite computation.
However, in "real-life" or "natural" situations, we should expect eigenvalues to be distinct unless they have a good reason (typically involving a symmetry) to be equal.
The situation in Corollary 15 is different: there is no requirement here for the $\lambda_j$ to be distinct.
EDIT: In fact, Corollary 15 is false.  Consider the family of $2 \times 2$ matrices
$$ A(p) = \pmatrix{\min(p,0) & \max(p,0)\cr
          \max(p,0) & \max(-p,0)\cr} $$
where $p$ is a computable real number.  Then $A(p)$ is a computable real symmetric matrix.  If $p < 0$ it has orthonormal eigenvectors $$ \pmatrix{1/\sqrt{2}\cr 1/\sqrt{2}\cr}, \ \pmatrix{1/\sqrt{2}\cr -1/\sqrt{2}\cr}$$
while if $p > 0$ it has orthonormal eigenvectors $$ \pmatrix{1\cr 0\cr},\ \pmatrix{0\cr 1\cr}$$
The 
 orthonormal eigenvectors $x_1,\; x_2$ mentioned in Corollary 15 can't be computable functions, because they can't be continuous at $p=0$.
