Computer assisted verification of the eigenvalue problem for one-dimensional Schrödinger operator

We propose a rigorous computational method for verifying the isolated eigenvalues of one-dimensional Schrödinger operator containing a periodic potential and a perturbation which decays exponentially at ±∞. We show how the original eigenvalue problem can be reformulated as the problem of finding a connecting orbit in a Lagrangian-Grassmanian. Based on the idea of the Maslov theory for Hamiltonian systems, we set up an integer-valued topological measurement, the rotation number of the orbit in the resulting one-dimensional projective space. Combining the interval arithmetic method for dynamical systems, we demonstrate a computer-assisted proof for the existence of isolated eigenvalues within the first spectral gap.