Proposition: Two-pulse switching-work identity

For the prescribed source controls, the total switching work is

where $O_1=Z,O_2=X$, and the expectation is in the chronologically evolved joint state. Both pulses are included. The second expectation contains the correlations created by the first.

Proof. In the Schrödinger description the explicitly time-dependent interaction is

On the common finite-energy form domain,

This follows by the Schrödinger equation; the commutator terms cancel in the total generator.

The identity is legitimate for the present paths: instantaneous compact spatial tests have arbitrarily many high-frequency spectral moments, and the threshold estimates control the required doubled energy moments at zero. Weyl products preserve these form domains. Alternatively one may first insert finite-particle and spectral cutoffs, prove the identity there, and pass to the form limits using these bounds.

The switched interaction vanishes at both endpoints, and the initial generator expectation is zero. Integration gives the first expression in (eq:work). The final generator expectation is the same Wick expansion as the summed two-point change in Theorem thm:energy, with frequency inserted. It is exactly $\delta E_{\mathrm{tot}}$.