Rush a system between two equilibrium conditions as violently as you like, and the average of a particular exponential of the work you did still returns the equilibrium free energy difference exactly. Irreversible experiments measure a reversible quantity.
jarzynskiFree energy is the price of moving a system from one equilibrium condition to another at fixed temperature: the least work that has to be paid, and it is paid in full only if the change is made infinitely slowly. Real changes are made in finite time. A stretched molecule, a compressed gas, a switched field: each is driven faster than it can keep up, the work done in a run exceeds the free energy difference, and it exceeds it by a different amount every time, because the microscopic starting configuration differs from run to run. The second law of thermodynamics says only that the average excess is never negative. It does not say what the average is.
Jarzynski found that a different average is fixed exactly. Instead of averaging the work, average the exponential of minus the work divided by the thermal energy. That quantity, averaged over many repetitions of the same fast protocol, equals the exponential of minus the free energy difference divided by the same thermal energy, whatever the protocol and however fast. The rare runs in which the work came out small, or even negative, dominate this average, which is why it can see past the irreversibility of the typical run.
The consequence is practical as well as conceptual. Single molecules can be pulled apart with laser tweezers thousands of times, quickly and irreversibly, and the equilibrium free energy of the unfolding transition read off from the record of work values. The result was tested that way on RNA hairpins within five years of its publication. The ordinary second law, that the average work is at least the free energy difference, follows from the equality in one line, because an average of an exponential is at least the exponential of the average.
Thermodynamics in this programme is not a separate subject with its own postulates. The state a system settles into at a given temperature, the Gibbs state, is derived from a variational principle, and the weight it gives to each energy level is the Born weight of an energy reading made on the equilibrium preparation. The Jarzynski equality is the first result in the corpus that ties those equilibrium weights to a process: the system is read, driven by a unitary change of its dynamics, and read again, and the work is the difference of the two readings.
What the equality establishes is that the exponential average of that difference depends only on the two equilibrium conditions, not on the driving. The proof rests on two facts the programme already owns. The equilibrium weight of the first reading contains the exponential of minus the starting energy, which cancels exactly against the matching factor inside the exponential of minus the work. And the table of transition probabilities between the two sets of energy readings, being built from a unitary, has every row and every column summing to one, so the remaining sum over starting readings collapses. What is left is the ratio of the two partition functions, which is the free energy difference in disguise. The second law for the driven process, that the mean work is at least the free energy difference, then follows from the convexity of the exponential function.
The corpus proves the theorem twice, once for matrices and once on the constraint surface itself, where the two readings are records of a single trajectory. The system starts in the Gibbs state as a mixed preparation on the measurement arena, an apparatus reads the energy levels of the starting Hamiltonian and records what it finds, the driving then moves the system's point on the surface along the unitary change of dynamics, which is the Hamiltonian flow of the energy expectation on the sector, and a second apparatus reads the energy levels of the final Hamiltonian. The record dynamics assigns each pair of readings exactly the probability the matrix theorem uses, so the equality, its free energy form and the second law all hold for the recorded statistics without any further argument. That's what it means to say the thermodynamics of a driven process lives on the record layer here, and you can read either version depending on whether you want the bookkeeping or the picture.
Let H_0 and H_1 be Hermitian matrices on a finite-dimensional space, U a unitary, and beta an inverse temperature. The two point measurement protocol reads the energy in the Gibbs state of H_0 (outcome i, the i-th eigenvalue E_0(i), with probability exp(-beta E_0(i)) / Z_0, which the corpus proves equals the Born weight of the i-th eigenvector in the Gibbs state), applies U, and reads the energy of H_1 (outcome j, eigenvalue E_1(j), with probability the squared modulus of the matrix element of U between the i-th eigenvector of H_0 and the j-th eigenvector of H_1). The work on the pair (i, j) is W = E_1(j) - E_0(i). The theorem is that the sum over all pairs of the joint probability times exp(-beta W) equals Z_1 / Z_0, the ratio of the partition functions, which by the corpus's TH3 free energy F = -log Z / beta is exp(-beta (F_1 - F_0)).
The proof is the cancellation described above made exact. The factor exp(-beta E_0(i)) in the Gibbs weight cancels exp(+beta E_0(i)) in exp(-beta W); the transition matrix is the matrix of squared moduli of V_1^* U V_0, with V_k the eigenvector unitary of H_k, and both its row sums and its column sums are one because V_1^* U V_0 is again unitary (the diagonal entries of M^* M = 1 and of M M^* = 1). Summing over i first leaves the sum over j of exp(-beta E_1(j)) / Z_0. Jensen's inequality for the convex exponential, applied to the joint law as a finite probability measure, gives the mean work bound: F_1 - F_0 is at most the expected work.
Scope: finite dimension, projective energy readings in the eigenbases chosen by the spectral theorem (degenerate spectra are allowed; the sum runs over eigenvectors, not over distinct eigenvalues), a closed driven system with no bath, so the work is the whole energy change, and the same beta at both ends. The free energy difference is that of the Gibbs states of H_1 and H_0 at that temperature.
The record-layer form in RecordLayer/JarzynskiRecord.lean runs the same protocol on the two-stage measurement arena. The Gibbs state enters as the spectral mixture of its eigenrays, the first bank is calibrated to the eigenrays of H_0 and the first context reads that eigenbasis, U moves the base point between the readouts while the pointer fibre stays put, and the second context reads the eigenbasis of H_1. The theorem sigma_tpm_law shows the joint record sector has exactly the joint law above as its measure, and it needs no positivity hypothesis as Gibbs weights are strictly positive, so sigma_jarzynski, sigma_jarzynski_freeEnergy and sigma_mean_work_ge_freeEnergy_sub follow by substituting it in. The engine underneath is a two-time law with a drive between the readouts, in RecordLayer/DrivenTwoTime.lean, and it works because driving the system by a flow before the second readout gives the same record sectors as reading the second context pulled back along that flow, which lets the composed two-stage law apply unchanged. A corollary writes the drive as the manifold Hamiltonian flow of the Schrodinger Hamiltonian on complex projective space, using the corpus's proof that this flow is the unitary exp(-i tau H). The identity uses only the form of that flow and not its volume preservation.
Christopher Jarzynski is an American physicist. He took his doctorate at the University of California, Berkeley, in 1994, moved to Los Alamos National Laboratory, and has been at the University of Maryland, College Park, since 2006, where he is a Distinguished University Professor.
The equality appeared in Physical Review Letters in 1997, under the title Nonequilibrium equality for free energy differences, written at Los Alamos. It was received with some disbelief, since it appeared to extract an equilibrium quantity from arbitrarily irreversible processes, and the classical derivation was scrutinised closely before the result was accepted. Gavin Crooks sharpened it in 1998 and 1999 into a relation between the forward and reverse work distributions, of which the equality is a corollary. Jan Liphardt, Carlos Bustamante and their collaborators confirmed it experimentally in 2002 by pulling single RNA molecules with optical tweezers. The quantum version used here, in which the work is defined by two energy readings, was formulated by Jorge Kurchan and by Hal Tasaki in 2000; Peter Talkner, Eric Lutz and Peter Hanggi made the point in 2007 that quantum work is a two time quantity and not an observable.
CsdLean4/Thermo/Jarzynski.leanSource links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.
Part of Constraint-Surface Dynamics · Formalised in csd-lean4.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.