TH5a: the Jarzynski equality, two-point-measurement form #
Category: 3-Local (conceptually 1-Mathlib; CSD-free finite-dimensional quantum
statistical mechanics) with a CSD reading; kept in the CSD.Thermo tree alongside
TH1–TH4 (specs/thermo-plan.md TH5; specs/BACKLOG.md ▶ OPEN QUEUE #1).
Glossary: https://glossary.constraintsurfacedynamics.com/jarzynski-equality/
A finite quantum system with Hamiltonian H₀ starts in the Gibbs state ρ_β = e^{−βH₀}/Z₀
(TH3, gibbsState). The two-point-measurement protocol: measure the energy — outcome
i, the eigenvalue E₀ i of H₀, with Born probability the Gibbs weight e^{−βE₀ i}/Z₀;
drive the system by a unitary U while its Hamiltonian becomes H₁; measure the energy
again — outcome j, the eigenvalue E₁ j of H₁, with Born probability
‖⟨e₁ j, U e₀ i⟩‖². The work done on the system in that run is W = E₁ j − E₀ i. The
Jarzynski equality (1997) says that the exponential average of the work over the
protocol is a state function of the two endpoints,
⟨e^{−βW}⟩ = Z₁/Z₀ = e^{−βΔF}, ΔF = F₁ − F₀ = −β⁻¹ (log Z₁ − log Z₀),
an equality valid arbitrarily far from equilibrium, whose Jensen consequence ⟨W⟩ ≥ ΔF
is the second law for the process (TH2 is its entropy-facing twin). The proof is bookkeeping
once the transition matrix is seen to be doubly stochastic: the Gibbs factor e^{−βE₀ i}
cancels against the e^{+βE₀ i} inside e^{−βW}, and the sums of ‖⟨e₁ j, U e₀ i⟩‖² over
i are 1 by unitarity, leaving ∑ⱼ e^{−βE₁ j}/Z₀.
Main results #
tpmUnitary hH₀ hH₁ U— the process read between the two eigenbases,V₁ᴴ U V₀(again a unitary);tpmUnitary_apply— its(j, i)entry is the amplitude⟨e₁ j, U e₀ i⟩;tpmTransition hH₀ hH₁ U i j := ‖(V₁ᴴ U V₀) j i‖², the Born transition probability (tpmTransition_eq), doubly stochastic:sum_tpmTransition_left(over the final outcome) andsum_tpmTransition_right(over the initial outcome), both by unitarity;tpmLaw hH₀ hH₁ U β i j := gibbsWeight (E₀ i) · tpmTransition i j— the joint law of the two outcomes, a probability law (tpmLaw_nonneg,sum_tpmLaw);tpmWork hH₀ hH₁ i j := E₁ j − E₀ i;gibbsState_mulVec_eigenvectorBasisandgibbsWeight_eq_re_born— the Gibbs weight IS the Born probability⟨e₀ i, ρ_β e₀ i⟩of the energy outcomeiin the Gibbs state, so the joint law is the statistics of the protocol, not a definition;- ★★
jarzynski(TH5a):∑ᵢⱼ tpmLaw i j · e^{−β W i j} = Z₁/Z₀; - ★★
jarzynski_freeEnergy: the same with right-hand sidee^{−β(F₁ − F₀)}in the TH3 free energies of the two Gibbs states (gibbs_free_energy_eq), forβ > 0; - ★
mean_work_ge_freeEnergy_sub— Jensen (convexOn_exp):ΔF ≤ ⟨W⟩, the second law of the driven process.
CSD reading #
The protocol's two readouts are records; the Gibbs weights are the Born weights of the first
readout in the equilibrium preparation, and the transition probabilities the Born weights of
the second after a unitary de-isolation. On the sector the same statement is the two-time
record law of RecordLayer/TwoTimeLuders.lean under a Gibbs preparation measure and the
Schrödinger flow (the Hamiltonian flow of ⟨H⟩, Q29(e)); that instantiation is the priced
row TH5d (specs/BACKLOG.md ▶ OPEN QUEUE #4). This file is the bare-matrix theorem it
consumes.
Honest scope #
Finite-dimensional, projective energy measurements with the eigenbases chosen by
Matrix.IsHermitian.eigenvectorBasis (degenerate spectra are allowed: the equality sums
over eigenvectors, not over distinct eigenvalues, and the transition weights are those of the
chosen bases). The work is the two-point-measurement work E₁ j − E₀ i, the standard
definition for closed driven systems; ΔF is the difference of the equilibrium free energies
of H₁ and H₀ at the same β. No bath, no heat: the driven system is closed, so
W = ΔE. Requires [Nonempty n] where a Gibbs state is involved (TH3's hypothesis).
Provenance #
Foundational-triple only (propext, Classical.choice, Quot.sound); no sorry, no new
axioms. Consumes TH3 (gibbsState, partitionFn, gibbs_free_energy_eq) and Mathlib's
spectral theorem and convexOn_exp; nothing is re-proved.
Unitaries are doubly stochastic in modulus squared #
Entry (i, i) of Mᴴ M = 1: the squared moduli down a column of a unitary sum to 1.
Entry (j, j) of M Mᴴ = 1: the squared moduli along a row of a unitary sum to 1.
The transition matrix of the protocol #
The process U read between the eigenbases of H₀ and H₁: V₁ᴴ U V₀, with V_k the
eigenvector unitary of H_k. Its (j, i) entry is the amplitude ⟨e₁ j, U e₀ i⟩
(tpmUnitary_apply).
Equations
- CSD.Thermo.tpmUnitary hH₀ hH₁ U = star hH₁.eigenvectorUnitary * U * hH₀.eigenvectorUnitary
Instances For
The (j, i) entry of V₁ᴴ U V₀ is the transition amplitude ⟨e₁ j, U e₀ i⟩ from the
i-th eigenvector of H₀ to the j-th eigenvector of H₁.
The transition probability of the protocol from energy outcome i of H₀ to energy
outcome j of H₁: ‖⟨e₁ j, U e₀ i⟩‖², the Born weight of the second readout in the
post-first-readout state U e₀ i.
Equations
- CSD.Thermo.tpmTransition hH₀ hH₁ U i j = ‖↑(CSD.Thermo.tpmUnitary hH₀ hH₁ U) j i‖ ^ 2
Instances For
Stochastic in the final outcome: for each initial outcome i, the transition
probabilities over j sum to 1.
Doubly stochastic: for each final outcome j, the transition probabilities over the
initial outcome i also sum to 1 — unitarity in the other order. This is the identity
that makes the Jarzynski average a state function.
The Gibbs weights are the Born weights of the first readout #
The Gibbs weights over the spectrum sum to 1.
The eigenvectors of H are eigenvectors of the Gibbs state, with eigenvalue the Gibbs
weight of the energy: ρ_β e_i = (e^{−βE_i}/Z) e_i.
The eigenvectors are unit vectors: entry (i, i) of V₀ᴴ V₀ = 1.
The Gibbs weight is a Born probability: e^{−βE_i}/Z = Re ⟨e_i, ρ_β e_i⟩, the
probability of the energy outcome i when the Gibbs state is measured in the eigenbasis of
H.
The joint law and the work #
The joint law of the two readouts: the Gibbs weight of the first outcome times the transition probability to the second.
Equations
- CSD.Thermo.tpmLaw hH₀ hH₁ U β i j = CSD.Thermo.gibbsWeight H₀ hH₀ β (hH₀.eigenvalues i) * CSD.Thermo.tpmTransition hH₀ hH₁ U i j
Instances For
The joint law is a probability law on the outcome pairs.
The two-point-measurement work on the outcome pair (i, j): E₁ j − E₀ i, the energy
difference between the two readouts (the system is closed, so this is the work done on it).
Equations
- CSD.Thermo.tpmWork hH₀ hH₁ i j = hH₁.eigenvalues j - hH₀.eigenvalues i
Instances For
The Jarzynski equality #
TH5a — the Jarzynski equality. The exponential average of the two-point-measurement
work over the protocol is the ratio of the partition functions of the final and initial
Hamiltonians, ⟨e^{−βW}⟩ = Z₁/Z₀, whatever the driving unitary U. The Gibbs factor of
the first readout cancels the e^{+βE₀ i} in e^{−βW}, and the transition matrix is doubly
stochastic (sum_tpmTransition_right).
The Jarzynski equality in free-energy form: ⟨e^{−βW}⟩ = e^{−β(F₁ − F₀)}, with F_k
the TH3 equilibrium free energy −β⁻¹ log Z_k of the Gibbs state of H_k at temperature
β⁻¹ (gibbs_free_energy_eq).
The second law of the driven process (Jensen on the Jarzynski equality): the mean
two-point-measurement work is at least the free-energy difference, ΔF ≤ ⟨W⟩. Convexity of
exp gives e^{−β⟨W⟩} ≤ ⟨e^{−βW}⟩ = e^{−βΔF}.