[proofplan]
The proof is a careful version of the usual Heisenberg-picture computation. The invariant-domain hypothesis ensures that $U(t)\psi$ remains in the common domain where $H_0A$, $AH_0$, and the commutator are defined. Differentiating the expectation gives a quadratic form involving $[H_0,A]$; vanishing of the commutator makes the derivative zero. Conversely, constancy of all diagonal expectations gives vanishing of the diagonal quadratic form, and the complex polarization identity upgrades this to vanishing of the full sesquilinear form, hence of the commutator on $D$ by density.
[/proofplan]
[step:Differentiate the expectation on the invariant domain]
Fix $\psi\in D$. Define
\begin{align*}
\psi_t:\mathbb{R}\to D,\qquad t\mapsto U(t)\psi.
\end{align*}
By the invariance hypothesis, $\psi_t\in D\subset D(H_0A)\cap D(AH_0)$ for every $t\in\mathbb{R}$. Define
\begin{align*}
f_\psi:\mathbb{R}\to\mathbb{R},\qquad t\mapsto (\psi_t,A\psi_t)_H.
\end{align*}
The core hypothesis says that $f_\psi$ is differentiable and that differentiating on $D$ is legitimate. Since $U(t)=e^{-itH_0}$, the Schrödinger equation on this domain gives
\begin{align*}
\frac{d}{dt}\psi_t=-iH_0\psi_t.
\end{align*}
Using the product rule for the Hilbert-space [inner product](/page/Inner%20Product), linearity in the first argument, conjugate-linearity in the second argument, and self-adjointness of $H_0$, we obtain
\begin{align*}
f_\psi'(t)=(-iH_0\psi_t,A\psi_t)_H+(\psi_t,A(-iH_0\psi_t))_H.
\end{align*}
Because the inner product is conjugate-linear in the second argument,
\begin{align*}
(\psi_t,A(-iH_0\psi_t))_H=i(\psi_t,AH_0\psi_t)_H.
\end{align*}
Because $\psi_t\in D(H_0A)$ and $H_0$ is self-adjoint,
\begin{align*}
(-iH_0\psi_t,A\psi_t)_H=-i(H_0\psi_t,A\psi_t)_H=-i(\psi_t,H_0A\psi_t)_H.
\end{align*}
Therefore
\begin{align*}
f_\psi'(t)=i(\psi_t,AH_0\psi_t-H_0A\psi_t)_H.
\end{align*}
With the commutator convention $[H_0,A]\psi=H_0A\psi-AH_0\psi$, this is
\begin{align*}
f_\psi'(t)=-i(\psi_t,[H_0,A]\psi_t)_H.
\end{align*}
[guided]
Fix $\psi\in D$ and track its time evolution by defining
\begin{align*}
\psi_t:\mathbb{R}\to D,\qquad t\mapsto U(t)\psi.
\end{align*}
The point of the invariant-domain hypothesis is precisely that this expression remains inside $D$ for every time $t$. Hence $\psi_t$ lies in $D(H_0A)\cap D(AH_0)$, so both $H_0A\psi_t$ and $AH_0\psi_t$ are meaningful.
Now define the expectation function
\begin{align*}
f_\psi:\mathbb{R}\to\mathbb{R},\qquad t\mapsto (\psi_t,A\psi_t)_H.
\end{align*}
Because $A$ may be unbounded, this expression would not even be defined without $\psi_t\in D(A)$. This is why the domain assumptions are part of the theorem rather than a technical afterthought.
The core hypothesis says that the formal differentiation below is valid on $D$. Since $U(t)=e^{-itH_0}$, the time derivative of $\psi_t$ is
\begin{align*}
\frac{d}{dt}\psi_t=-iH_0\psi_t.
\end{align*}
Applying the product rule to the inner product gives
\begin{align*}
f_\psi'(t)=(-iH_0\psi_t,A\psi_t)_H+(\psi_t,A(-iH_0\psi_t))_H.
\end{align*}
We now rewrite each term so that the commutator appears. The inner product is linear in the first argument and conjugate-linear in the second argument, so
\begin{align*}
(\psi_t,A(-iH_0\psi_t))_H=i(\psi_t,AH_0\psi_t)_H.
\end{align*}
For the other term, self-adjointness of $H_0$ allows us to move $H_0$ from the first slot to the second slot. This is legitimate because $\psi_t\in D(H_0)$ and $A\psi_t\in D(H_0)$:
\begin{align*}
(-iH_0\psi_t,A\psi_t)_H=-i(H_0\psi_t,A\psi_t)_H=-i(\psi_t,H_0A\psi_t)_H.
\end{align*}
Combining the two identities gives
\begin{align*}
f_\psi'(t)=i(\psi_t,AH_0\psi_t-H_0A\psi_t)_H.
\end{align*}
By the definition
\begin{align*}
[H_0,A]\eta=H_0A\eta-AH_0\eta,\qquad \eta\in D,
\end{align*}
we obtain the derivative formula
\begin{align*}
f_\psi'(t)=-i(\psi_t,[H_0,A]\psi_t)_H.
\end{align*}
This is the rigorous form of the heuristic statement that the time derivative of an observable expectation is governed by its commutator with the Hamiltonian.
[/guided]
[/step]
[step:Use commutator vanishing to prove conservation of the expectation]
Assume that $[H_0,A]\eta=0$ for every $\eta\in D$. Since $\psi_t\in D$ for every $t\in\mathbb{R}$, the derivative formula gives
\begin{align*}
f_\psi'(t)=-i(\psi_t,[H_0,A]\psi_t)_H=0.
\end{align*}
Thus $f_\psi$ has zero derivative on $\mathbb{R}$. Therefore $f_\psi$ is constant on $\mathbb{R}$:
\begin{align*}
(U(t)\psi,AU(t)\psi)_H=(\psi,A\psi)_H
\end{align*}
for every $t\in\mathbb{R}$ and every $\psi\in D$. This proves that $A$ is a constant of motion on $D$. The extension to the closure determined by the core is exactly the extension property included in the form-core hypothesis.
[/step]
[step:Recover the commutator from constant expectations by polarization]
Assume conversely that for every $\psi\in D$, the function
\begin{align*}
t\mapsto (U(t)\psi,AU(t)\psi)_H
\end{align*}
is constant on $\mathbb{R}$. Then $f_\psi'(0)=0$ for every $\psi\in D$. Applying the derivative formula at $t=0$ gives
\begin{align*}
0=-i(\psi,[H_0,A]\psi)_H.
\end{align*}
Hence
\begin{align*}
(\psi,[H_0,A]\psi)_H=0
\end{align*}
for every $\psi\in D$.
Define the sesquilinear form
\begin{align*}
B:D\times D\to\mathbb{C},\qquad (\phi,\psi)\mapsto (\phi,[H_0,A]\psi)_H.
\end{align*}
The domain $D$ is a complex linear subspace, so $\phi+i^k\psi\in D$ for all $\phi,\psi\in D$ and $k\in\{0,1,2,3\}$. The complex polarization identity for a form linear in the first variable gives
\begin{align*}
B(\phi,\psi)=\frac{1}{4}\sum_{k=0}^{3}i^k B(\phi+i^k\psi,\phi+i^k\psi).
\end{align*}
Each diagonal term on the right-hand side is zero, because the diagonal quadratic form vanishes on all of $D$. Therefore
\begin{align*}
(\phi,[H_0,A]\psi)_H=B(\phi,\psi)=0
\end{align*}
for every $\phi,\psi\in D$.
[guided]
We now prove the converse. The assumption is that every expectation function
\begin{align*}
f_\psi:\mathbb{R}\to\mathbb{R},\qquad t\mapsto (U(t)\psi,AU(t)\psi)_H
\end{align*}
is constant whenever $\psi\in D$. A constant differentiable function has derivative zero, so in particular $f_\psi'(0)=0$. The derivative formula from the first step gives
\begin{align*}
0=f_\psi'(0)=-i(\psi,[H_0,A]\psi)_H.
\end{align*}
Multiplying by $i$ yields
\begin{align*}
(\psi,[H_0,A]\psi)_H=0
\end{align*}
for every $\psi\in D$.
This is only a diagonal identity. To prove that the operator itself vanishes on $D$, we need all mixed pairings against arbitrary test vectors in $D$. Define
\begin{align*}
B:D\times D\to\mathbb{C},\qquad (\phi,\psi)\mapsto (\phi,[H_0,A]\psi)_H.
\end{align*}
This is linear in $\phi$ and conjugate-linear in $\psi$ because the Hilbert-space inner product is linear in the first argument and conjugate-linear in the second argument.
The diagonal identity says $B(\eta,\eta)=0$ for every $\eta\in D$. Since $D$ is a complex linear space, the vectors $\phi+i^k\psi$ also lie in $D$ for $k=0,1,2,3$. Applying the complex polarization identity to the sesquilinear form $B$ gives
\begin{align*}
B(\phi,\psi)=\frac{1}{4}\sum_{k=0}^{3}i^k B(\phi+i^k\psi,\phi+i^k\psi).
\end{align*}
Every term on the right is zero because each $\phi+i^k\psi$ lies in $D$ and the diagonal quadratic form vanishes on all of $D$. Hence
\begin{align*}
B(\phi,\psi)=0.
\end{align*}
By the definition of $B$, this means
\begin{align*}
(\phi,[H_0,A]\psi)_H=0
\end{align*}
for every $\phi,\psi\in D$.
[/guided]
[/step]
[step:Use density of the core to conclude pointwise vanishing of the commutator]
Fix $\psi\in D$ and define
\begin{align*}
\eta_\psi:=[H_0,A]\psi\in H.
\end{align*}
The previous step proves that
\begin{align*}
(\phi,\eta_\psi)_H=0
\end{align*}
for every $\phi\in D$. Since $D$ is dense in $H$, it follows that $\eta_\psi=0$. Therefore
\begin{align*}
[H_0,A]\psi=0
\end{align*}
for every $\psi\in D$. This proves the converse and completes the proof of the commutator criterion.
[/step]
