Solution (source code)

= Solution

The squared <norm> is obtained by moving the <adjoint operator> to the other side of the <inner product>:
$$
\|a_-\psi\|^2=\langle\psi,a_+a_-\psi\rangle
=2m\left\langle\psi,\left(H-\frac12\hbar\omega\right)\psi\right\rangle.
$$
For an <energy eigenstate>, this is
$$
\boxed{\|a_-\psi\|^2=2m\left(E-\frac12\hbar\omega\right)\|\psi\|^2.}
$$
Since a squared <norm> is nonnegative, every nonzero <energy eigenstate> has $E\geq\hbar\omega/2$. Moreover $a_-\psi=0$ exactly when $E=\hbar\omega/2$.