The Exercise

Let a closed quantum system have Hamiltonian $H$ , and let $\hbar$ denote the reduced Planck constant. Its state at a time $t_2$ is obtained from its state at a time $t_1$ as $|\psi(t_2)\rangle = U(t_1,t_2)\,|\psi(t_1)\rangle$ , where $U(t_1,t_2) = \exp\left[\frac{-iH(t_2-t_1)}{\hbar}\right]$ (1) and the exponential of an operator is the sum of its power series. The exercise is to show that $U(t_1,t_2)$ is unitary.

A Quantum System

A quantum system $S$ is a physical object whose state space is a finite dimensional complex Hilbert space.^✦ An observable $A$ of $S$ is a self adjoint operator on the state space of $S$ , $A^\dagger = A$ ; its spectrum is real and is the set of values a measurement of $A$ can give.^✦

The Claim

The Hamiltonian $H$ of a quantum system $S$ is the observable of the energy of $S$ .

Theorem 1. Let $H$ be an observable of a quantum system $S$ , and let $\hbar$ , $t_1$ and $t_2$ be real numbers. Then the operator $U(t_1,t_2)$ of (1) on the state space of $S$ is unitary, that is, with $I$ the identity operator on that space: $U(t_1,t_2)^\dagger\, U(t_1,t_2) = U(t_1,t_2)\, U(t_1,t_2)^\dagger = I.$ (2)^✦

What Is Checked

The claim is stated over a quantum system $S$ , an observable $H$ of it and three real numbers $\hbar$ , $t_1$ and $t_2$ . The library proves (2) for every such choice, the case of $t_2$ before $t_1$ included.