Projection Probability Flow

Abstract

Finite-dimensional Hamiltonian evolution differentiates projection probabilities by the commutator trace and conserves them for commuting projections.

Theorem 1.1 (Projection probabilities follow the commutator trace).

$$\begin{array}{c}\forall n,H,P,\rho ,\\ \mathrm{Finite}\left(n\right),H,P\in M_n(\mathbb{C}),\mathrm{DensityState}\left(\rho ,n\right),\mathrm{Hermitian}\left(H\right),\mathrm{StarProjection}\left(P\right),\\ U_t=\exp (-itH),{\rho }_t=U_t\rho U_t^{\ast },p_P(t)=\Re \mathrm{Tr}({\rho }_{t}P)\in \mathbb{R},\\ (\forall t\in \mathbb{R},\mathrm{ofReal}\left(p_P(t)\right)=\mathrm{Tr}({\rho }_{t}P))\wedge \\ (\forall t\in \mathbb{R},\frac{d}{dt}{p}_P(t)=\Re i\mathrm{Tr}({\rho }_t[H,P]))\wedge \\ (\forall t\in \mathbb{R},\mathrm{ofReal}\left(\Re i\mathrm{Tr}({\rho }_t[H,P])\right)=i\mathrm{Tr}({\rho }_t[H,P]))\wedge \\ ([H,P]=0\Rightarrow \forall t\in \mathbb{R},p_P(t)=p_P(0)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow.projection_probability_flow (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let rho be a positive trace-one state on a finite complex matrix algebra, let H be Hermitian, and let P be a star projection. The propagator is the matrix exponential of -i t H, the evolved state is U_t rho U_t^*, and p_P is the real Born probability.

The first displayed conjunct identifies the complex cast of that real probability with the source Born trace. The next two conjuncts give its real derivative and certify that the complex commutator-trace flow is real, so the derivative equals the source formula exactly.

The final conjunct is independent of the derivative clauses: if the Hamiltonian and projection commute, the probability is constant for every real time.

References

• Truth anchor: D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow.projection_probability_flow
• Dependency: D5/S3/Quantum/Decoherence/ProjectedUnistochasticDynamics
• Dependency: D5/S3/Quantum/Divergence/QuantumRelativeEntropyDefectComposition
• Dependency: D5/S3/Quantum/FiniteDimensional