= Solution
Let $L_n=\operatorname{span}\{e_1,\ldots,e_n\}$ and let $P_n$ be its <orthogonal projection>. For $z\in\mathbb C$, define
$$
\gamma_n(z)^2
=\lambda_{\min}\!\left(
(1+|z|^2)I_n-\bar z\,P_nAP_n-z\,P_nA^*P_n
\right).
$$
Because $A$ is <unitary operator>[unitary],
$$
\gamma_n(z)
=\inf_{\substack{x\in L_n\\\|x\|=1}}\|(A-zI)x\|.
$$
The displayed finite <Hermitian matrix> uses only finitely many matrix entries of $A$, and its least eigenvalue can be approximated by an <arithmetic algorithm in the SCI hierarchy>.
As $L_n$ increases densely,
$$
\gamma_n(z)\downarrow
\inf_{\|x\|=1}\|(A-zI)x\|.
$$
A <unitary operator> is <normal operator>[normal], so the <spectral theorem for normal operators on a separable Hilbert space> identifies the limit as
$$
\operatorname{dist}(z,\operatorname{Sp}(A)).
$$
The functions $\gamma_n$ are continuous and decrease to a continuous function on the compact unit circle. The <Dini theorem> therefore gives uniform convergence there.
Take successively finer rational meshes $G_n$ around $\mathbb T$. From the finitely computed values of $\gamma_n$, retain the mesh minima in the comparison neighborhoods whose radii are $\gamma_n(z)$; equivalently, use the standard local-minimum construction for a decreasing approximation to a distance function. Call the resulting finite set $\Gamma_n(A)$. Uniform convergence and the shrinking mesh imply
$$
\boxed{\Gamma_n(A)\longrightarrow\operatorname{Sp}(A)}
$$
in <Hausdorff distance>. Every operation at stage $n$ is finite and arithmetic, so $(\Gamma_n)$ is the required one-limit sequence.
There is no finite-stage certificate that the whole output has the correct Hausdorff error: the convergence of $\gamma_n$ has no uniform computable rate over all unitary operators, and unseen matrix entries can still reveal a missing spectral component. A small computed residual can certify that an individual output point lies near the spectrum, but it cannot verify that $\Gamma_n(A)$ covers all of $\operatorname{Sp}(A)$. Thus the full finite-stage output is not verifiable without additional information.
Back to article page
