Composite trapezoidal approximation

The $U_{n,j}$ must enclose entire cells, not just sampled values. They can be obtained from outward-rounded evaluations of the Hermite formula and its derivatives, with subdivision when necessary. The computable bounds in Lemma lem:Gbound remove the need for an unverified sampled operator-norm supremum.

Arbitrary-precision ball-arithmetic integration with rigorous error bounds is an established methodology Johansson. That reference supplies a general numerical method, not an executed certificate for this manuscript. If complex-analytic integration is used for oscillator entries, the holomorphic integrand is ${\varphi }_m(z){\varphi }_n(z)$, whose restriction to the real axis is the required product. Extending a real-axis conjugate expression as $v(z)v(z{)}^{†}$ would not give a holomorphic integrand.