OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/VerticalSpectralInput.lean

The published oscillator gap, specialized to the one-dimensional form.

Gerald Teschl, Mathematical Methods in Quantum Mechanics, second edition, AMS Graduate Studies in Mathematics 157 (2014), Section 8.3, equations (8.39)--(8.43) and Theorem 8.5; form-domain max-min in Theorem 4.12. https://www.mat.univie.ac.at/~gerald/ftp/book-schroe/schroe2.pdf

The one-dimensional Hermite calculation gives eigenvalues (2n+1)freq for -∂²+freq²z² and the Gaussian (8.41). Dividing by two gives bottom freq/2 and gap freq. We assume just the resulting projection-form inequality on compact C¹ tests. The Gaussian and its normalization and attained energy are actual definitions and proved facts, not extra premises.