From estimate to proof: certified ground-state energy bounds for singular Schrödinger operators

Xuefeng Liu

Source-linked AI summary

From estimate to proof: certified ground-state energy bounds for singular Schrödinger operators

Xuefeng Liu

arXiv:2608.25760v1Aug 26, 2026math.NA

TL;DR

Accurate Schrödinger eigenvalue simulations do not by themselves certify the true energy or its side of the estimate. This paper combines explicit whole-space truncation bounds with a two-stage verified eigenvalue method, obtaining a rigorous hydrogen-molecular-ion enclosure of width 4.76 × 10−4 while reproducing the numerical value to eleven significant digits.

Problem
Standard simulations estimate low Schrödinger-operator eigenvalues without guaranteeing how far they are from the true value, although some scientific questions require guaranteed bounds.
Method
The framework combines projection-based lower bounds, an auxiliary coercivity eigenproblem, Lehmann–Goerisch sharpening, and explicit two-sided finite-box truncation bounds in verified interval arithmetic.
Results
4.76 × 10−4 is the certified hydrogen-molecular-ion interval width, and the enclosure contains the accepted reference value −0.551317 while reproducing the uncertified value to eleven significant digits.
Takeaways & Limitations
The framework turns the hydrogen-molecular-ion ground-state computation from an estimate into a proof about the true infinite-domain energy.
Takeaways & Limitations
Verified interval computation is heavier than double precision, and the enclosure width is currently limited by Dirichlet-side domain-truncation error.

Abstract

from arXiv · show

Many predictions in quantum chemistry, materials science, and spectral geometry hinge on the lowest energy levels of a Schrödinger operator, yet standard simulations return approximations with no guarantee of how far they sit from the true value. We present a computational framework that returns mathematically certified bounds---an interval provably containing the exact energy---even for the singular, unbounded, sign-changing potentials of real molecules, where existing certified methods fail. For the hydrogen molecular ion this framework delivers, to our knowledge, the first guaranteed two-sided enclosure of the true infinite-domain ground-state energy: an interval of width below $5\times10^{-4}$ that provably contains the accepted reference value. The key that makes a whole-space guarantee possible is an \emph{explicit}, computable bound on the error of restricting the problem to a finite box---replacing the classical argument that the wavefunction merely decays---which brackets the true energy from both sides. Remarkably, the certified interval reproduces the uncertified numerical value to eleven digits, so mathematical rigor costs almost nothing in accuracy. The result turns eigenvalue computation from an estimate into a proof.

1 Introduction

The paper develops certified eigenvalue bounds for singular molecular Schrödinger operators, addressing the gap between highly accurate estimates and guaranteed enclosures. Its two-stage framework yields a rigorous hydrogen-molecular-ion interval while preserving numerical precision.

Motivation: The approach targets a limitation of certified finite-element methods, which are powerful mainly for Laplace operators on bounded domains.The paper extends certification toward singular, three-dimensional Coulomb problems.
Method: The framework combines a projection-based lower bound with a sharp coercivity constant from an auxiliary eigenvalue problem.This first stage also certifies the spectral separation needed by the sharpening stage.
Method: Lehmann–Goerisch sharpening replaces Temple or Weinstein estimates and requires only H1 trial-function data for singular Coulomb potentials.The method avoids requiring the strong image Hu, which may not be square-integrable for generic H1 trials.
Results: 4.76 × 10−4 is the certified interval width containing the accepted hydrogen molecular-ion energy −0.551317.The interval is a rigorous two-sided enclosure of the reference value.
Results: Eleven significant digits of the uncertified floating-point value are reproduced within the rigorous enclosure.Thus the reported certification retains the accuracy of the numerical computation.

2 What “error” means for a computed energy

The paper distinguishes approximation from proof by defining certification as rigorous control of every downstream computational error for a fixed mathematical model. Its output is an interval guaranteed to contain the exact eigenvalue of that operator.

Motivation: Conventional convergence studies and cross-method agreement can produce sharp estimates but do not prove which side of the true eigenvalue they occupy.The distinction matters for questions requiring guaranteed spectral gaps or stability margins.
Certified computation: A certified computation bounds discretization, truncation, algorithmic, and arithmetic errors rigorously.Interval arithmetic handles rounding, residual verification handles algorithmic error, and explicit constants handle discretization and truncation.
Scope: The certified output is an interval guaranteed to contain the exact eigenvalue of the stated operator.Modeling error is deliberately excluded: the physical model is assumed rather than certified.

3 From the whole space to a bounded box

The paper makes finite-box reduction rigorous by replacing qualitative decay arguments with explicit two-sided truncation bounds. Neumann and Dirichlet problems then provide lower and upper bounds for the whole-space energy, with domain size controlling the remaining bias.

Truncation analysis: Agmon decay proves convergence qualitatively but does not provide a computable error for a box of specified size.The framework instead uses the analytic confinement constant σ(Ω).
Neumann lower bound: The Neumann eigenvalue supplies a rigorous lower bound when the exterior potential floor satisfies σ(Ω) > λk(R3).For the ground state, this is the lower side of the whole-space enclosure.
Dirichlet upper bound: The Dirichlet eigenvalue supplies a rigorous upper bound, but its boundary-vanishing constraint creates an overshoot that grid refinement cannot remove.Only enlarging the box reduces this truncation bias.
Truncation analysis: An explicit two-sided truncation estimate converts a bounded-box computation into a rigorous enclosure of the whole-space eigenvalue.This is the basis for certifying the reduction from R3 to a bounded box.
Error separation: Two nested boxes separate truncation error from discretization error by revealing which part of the enclosure changes with box size versus basis order.Larger boxes reduce truncation error but can crowd the spectral gap, requiring stronger separation certification.

4 The two-stage framework

The two-stage framework first converts Rayleigh–Ritz data into certified lower bounds and a spectral separator, then uses Lehmann–Goerisch sharpening to obtain a tighter ground-state bound. Verified forms, matrices, definiteness tests, and eigenvalue steps preserve rigor while approximate trial choices affect sharpness בלבד.

Stage A: projection bound: Stage A computes a coercivity shift from an auxiliary lowest eigenvalue and converts Rayleigh–Ritz upper values into certified lower bounds.The shift directly handles negative or singular potential contributions without assuming V is nonnegative.
Stage A: separation certificate: Stage A returns L1 and L2; when L2 exceeds the λ1 upper bound, it creates a certified separator ρ with λ1 < ρ ≤ λ2.The k = 2 whole-space enclosure carries this separator beyond the box problem.
Discrete setting: The method is posed through a shifted energy form and L2 inner product on a cosine trial space, with generalized eigenvalues supplying the discrete bounds.The first omitted Laplacian eigenvalue and projection constant control conversion from upper to lower estimates.
Stage B: Lehmann–Goerisch sharpening: Lehmann–Goerisch uses the certified ρ to produce a Rayleigh–Ritz-quality lower bound for λ1 while requiring only H1 trial-function information.Goerisch’s device represents the needed operator information without forming H2 quantities.
Implementation: The Lehmann–Goerisch implementation uses explicit auxiliary spaces and a symmetric positive-definite linear solve for each trial vector.Zero-padding embeds the lower-order cosine space into the auxiliary space without requiring a mixed flux space.
Verification contract: Only exact or rigorously enclosed quantities affecting the proof must be verified; trial vectors and the splitting parameter may remain approximate and affect only sharpness.The contract includes matrix entries, coercivity, the seed ρ, positive definiteness, and final eigenvalue transformations.

5 Realization: rigor vs. approximation

The computation combines anisotropic-box cosine discretization with verified treatment of Coulomb moments and interval eigenvalue routines. A two-regime enclosure evaluates the required moments without relying on unverified special functions.

Discretization: The anisotropic tensor cosine basis diagonalizes the kinetic term and separates ground and first-excited states into parity sectors.Matrix entries reduce to one-dimensional shifted-Coulomb moments assembled over a Gauss–Legendre grid.
Moment enclosure: The large-t regime uses an elementary infinite-domain integral plus an explicit Gaussian tail bound for truncation.This avoids requiring verified implementation of the complex scaled complementary error function.
Moment enclosure: The small-t regime encloses the broad analytic integrand with verified Gauss–Legendre quadrature and an explicit Bernstein-ellipse remainder.At practical orders, the truncation term is far below the floating-point rounding floor.
Certification: Verified interval eigenvalue routines enclose µ1, µ2, the auxiliary η, and the Lehmann–Goerisch quantities.The approximate Goerisch constraint is handled by enclosing its floating-point residual exactly in interval arithmetic.

6 Results: the hydrogen molecular ion

The framework certifies the hydrogen molecular ion ground-state energy on nested boxes using Neumann lower and Dirichlet upper bounds. Enlarging the box and certifying the spectral separator produces a whole-space enclosure of width 4.76 × 10−4 containing the reference −0.551317, while globally supported Gaussians offer a narrower but not-yet-interval-verified route.

Setup: The computation uses nested boxes Ω1 and Ω2 with verified interval enclosures, and the confinement condition makes the Neumann lower bound admissible as a whole-space bound.The boxes are [−10, 10] × [−8, 8]2 and [−20, 20] × [−16, 16]2; σ(Ω1) = −0.2425 and σ(Ω2) = −0.1240 exceed λ1 ≈−0.551.
Certified enclosure: 4.76 × 10−4 is the certified ℝ3 enclosure width on Ω2 at N = 64, and it contains the accepted reference −0.551317.The lower bound is Neumann Lehmann–Goerisch and the upper bound is Dirichlet Rayleigh–Ritz.
Certified separator: 5.8 × 10−4 improvement in the lower bound from a certified µ2 separator reduces the enclosure width from 1.05 × 10−3 to 4.76 × 10−4.The recomputation takes less than a second and requires no re-assembly.
Domain convergence: 1.4 × 10−3 is the Ω1 enclosure width, with a nearly N-independent Dirichlet–Neumann gap of ≈1.1 × 10−3 caused by domain truncation rather than discretization.Doubling to Ω2 collapses the truncation error, while the certified separator and N = 64 reopen the crowded spectral gap.
Accuracy cost: 11 guaranteed digits are retained relative to the identical floating-point formula, with interval and floating-point Ritz values agreeing to 3 × 10−15 at N = 48.The enclosure width is set by domain truncation and discretization, not by interval arithmetic.
Truncation-free route: 3.3×10−5 is the width of a narrower whole-space enclosure from globally supported Gaussian trial functions, 14× narrower than the certified box/FEM interval.These figures use high-precision floating point rather than verified interval arithmetic, and the pure-Gaussian route encounters a cusp floor near 10−5.

7 Discussion

The framework extends certified eigenvalue bounds to broad self-adjoint operators while making whole-space guarantees for singular molecular problems. Its remaining limitations are quantitative, involving verified-computation cost and domain-truncation error, with clear routes for improvement.

Generality: A variational form and a coarse spectral gap support the framework across other molecules, confining potentials, and spectral-geometry operators.Stage A manufactures the separation certificate consumed by Stage B, so no external a-priori second-eigenvalue bound is required.
Limitations: Verified interval computation is heavier than double precision, limiting the spectral order and box size that can currently be certified.The cost is dominated by verified eigenvalue solves, while the sharp coercivity constant keeps certified computation practical.
Truncation error: 9.8×10−5 is the minimum gap placing the Ω1 Dirichlet eigenvalue above the true energy, confirming genuine truncated-domain overestimation.Under refinement, the margin rises, showing the effect is not a grid artefact.
Truncation error: Below 4.8 × 10−4, the Ω2 truncation error collapses sufficiently for the certified enclosure, while the Dirichlet side remains the rougher bound.The enclosure width is therefore set by domain truncation rather than arithmetic.
Outlook: Gaussian product integrals transfer Stages A–B unchanged to non-separable multi-centre ions, unlike two-centre prolate-spheroidal references.Future work targets scaling the verified eigensolver to larger orders.

Materials and Methods

The computation uses a tensor Neumann cosine basis on an anisotropic box, interval-assembled matrices, and certified quadrature and remainder bounds for the Coulomb kernel.

Discretization: A tensor Neumann cosine basis on an anisotropic box uses parity decomposition to isolate the ground and first-excited symmetry sectors.The Coulomb kernel is represented through a Gauss–Legendre grid in an auxiliary variable.
Certified assembly: Each shifted moment is enclosed with a two-regime rule using interval exp, cos, and sqrt, plus Gaussian-tail and Bernstein-ellipse remainders.These explicit bounds control the quadrature-related contributions to the certified computation.
Certified assembly: Interval arithmetic assembles the matrices and supports eigenvalue enclosures for the discretized problem.

Data and code availability

The paper provides open code and machine-readable certified result tables, enabling reproduction of every certified bound.

Reproducibility: All code and data needed to reproduce every certified bound are openly available in the paper’s GitHub repository.The repository includes certified result tables in machine-readable form.
Software: The repository contains Stage-A double-precision and Stage-B verified interval-arithmetic Julia pipelines.The verified eigensolver VEIGS.jl is maintained as a standalone package.

Appendix

The appendix gives a self-contained account of the projection lower bound and proofs underlying the main theorems, while defining the Rayleigh–Ritz quantities used in cosine and sine trial spaces.

Appendix scope: The appendix restates the projection lower bound on which Stage A rests and supplies proofs of Theorems 1–3.It also presents precision-improvement techniques that make the certified spectral order practical.
Appendix scope: The appendix is self-contained, with equations, figures, and tables numbered S1, S2, and onward.
Notation: μk,N denotes the k-th Rayleigh–Ritz value in cosine Neumann or sine Dirichlet trial spaces VN whose dimension grows with spectral order N.

1 Proof of Theorem 1 (whole-space enclosure)

The theorem brackets each whole-space eigenvalue between a Dirichlet upper bound and, under exterior confinement, a Neumann lower bound. For the ground state, this recovers a rigorous two-sided enclosure without requiring simplicity or a spectral-gap hypothesis.

Dirichlet restriction provides an upper bound because zero extension preserves the Rayleigh quotient while restricting the trial space.
The Neumann lower bound uses restricted whole-space eigenfunctions as a k-dimensional trial space and requires the exterior potential floor σ(Ω) to exceed λk(R3).
Combining both inequalities encloses λk(R3) between LNeu and UDir, with the ground state recovered by setting k = 1.
The enclosure is factor-free, and its lower bound needs neither simplicity nor a spectral-gap hypothesis.

2 The projection lower bound of the spectral-Galerkin framework

The projection-based framework converts finite-dimensional spectral approximations into rigorous lower bounds through an explicit projection-error constant. For exact Laplacian modes, that constant is explicit and optimal, while the bound remains unconditional with respect to neighboring eigenvalues.

The appendix restates and proves the unpublished framework results needed by the paper, making the dependent argument self-contained.
The projection-based theorem supplies lower bounds for each discrete eigenvalue under Gram, positivity, and projection-error assumptions.
The lower-bound quality is controlled by the dimensionless product C_N^2λk,N, with unconditional validity requiring no lower bound on λk+1 or spectral localization.
For trial spaces of exact Laplacian eigenmodes, C_N equals the inverse square root of the first omitted eigenvalue and is the smallest admissible projection-error constant.
In the cosine trial space, the omitted-mode floor gives C_N = O(N^-1), after a coercivity shift restores positivity for the Coulomb operator.

3 The projection-error constant via the potential form factor

The paper controls the gap between modal and Ritz projections through a potential form factor, then extends the resulting lower-bound machinery to singular Coulomb potentials using a coercivity shift. A tail-refined form factor improves under refinement, unlike the crude bound.

The main technical difficulty is controlling the gap between the modal projection and the Ritz projection in the cosine trial space.
An algebraic gap identity reduces this control to the potential contribution, which is bounded by the potential form factor ηV.
The projection-error estimate and eigenvalue lower bound follow from the form-factor control, the modal-tail estimate, and the Ritz projection.
The tail-refined factor η′V shrinks with refinement because it scales with potential fluctuation relative to the omitted spectral gap, unlike the N-independent crude factor.
For singular, unbounded, sign-changing Coulomb potentials, a localized-Hardy coercivity shift makes the form positive definite and keeps the form factor finite.

4 Localized Hardy inequality and coercivity

The section replaces a conservative coercivity shift with a sharp auxiliary-eigenvalue constant, substantially tightening certified lower bounds while preserving rigor. It also explains why Lehmann–Goerisch is effective for singular Coulomb problems and can match Rayleigh–Ritz precision.

Sharp coercivity constant via the auxiliary eigenvalue: The sharp shift σ = −η(ϵ) is the negative ground eigenvalue of an auxiliary operator and is the smallest admissible shift at fixed ϵ.Its coercivity and positivity follow from localized Hardy control and the attractive Coulomb potential.
Precision-improvement techniques: An optimized auxiliary shift σ ≈ 10.46 is 11.6× smaller than the explicit Hardy shift, reducing the certified gap by factors of 245–308.The separation certificate is first attained at N = 96 rather than approximately N ≈ 360.
Two-stage certification: The first stage certifies a separator while the second Lehmann–Goerisch stage sharpens the ground-state lower bound to Rayleigh–Ritz precision.The method uses a certified lower bound on the second eigenvalue rather than a heuristic separator.
Weinstein, Temple, and Lehmann–Goerisch: Lehmann–Goerisch retains second-order accuracy and can bound an entire eigenvalue cluster, unlike first-order estimates or scalar Temple bounds.For the isolated H+2 ground state, Temple and Lehmann–Goerisch bounds essentially coincide.
Weinstein, Temple, and Lehmann–Goerisch: The Goerisch reformulation requires only H1 trial functions, avoiding the strong residual Hu and H2 regularity unavailable for generic Coulomb trial functions.Its auxiliary defect can be solved approximately while enclosing the residual rigorously.
Sharpness of the certified bound: At the sharp separator ρ = λ2, the lower-bound gap is no larger than the upper-bound gap in the dominant direction, and both vanish for an exact eigenvector.This establishes practical sharpness for simple eigenvalues.