TH5b: the Crooks fluctuation theorem, 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–TH5a (specs/thermo-plan.md TH5; specs/BACKLOG.md ▶ OPEN QUEUE #2).

Glossary: https://glossary.constraintsurfacedynamics.com/crooks-fluctuation-theorem/

The Jarzynski equality (TH5a, Thermo/Jarzynski.lean) averages the two-point-measurement work of the forward protocol — Gibbs state of H₀, read, drive by U, read in the eigenbasis of H₁. The reverse protocol starts in the Gibbs state of H₁ at the same temperature, drives by U⁻¹ = Uᴴ, and reads in the eigenbasis of H₀. Crooks' theorem (1999) is the pointwise relation between the two work distributions,

P_F(W) = P_R(−W) · e^{β(W − ΔF)},

so the forward and reverse histograms cross exactly at W = ΔF, which is how single-molecule experiments read a free energy off two irreversible data sets. Jarzynski is its corollary (multiply by e^{−βW} and sum: the reverse law sums to one).

The whole content is one symmetry and one cancellation. The reverse protocol's transition matrix is the transpose of the forward one — V₀ᴴ Uᴴ V₁ = (V₁ᴴ U V₀)ᴴ, so ‖⟨e₀ i, Uᴴ e₁ j⟩‖² = ‖⟨e₁ j, U e₀ i⟩‖² (tpmTransition_star, microscopic reversibility) — and the two Gibbs weights differ by exactly e^{βW} times Z₁/Z₀.

Main results

• tpmUnitary_star, tpmTransition_star — the reverse protocol's transition matrix is the transpose of the forward one (Uᴴ between the swapped eigenbases); tpmWork_symm — its work is minus the forward work;
• ★★ crooks_pairwise (TH5b, the pairwise form): on every outcome pair, P_F(i, j) · Z₀ = P_R(j, i) · Z₁ · e^{βW(i, j)}; crooks_pairwise_freeEnergy — the same as P_F(i, j) = P_R(j, i) · e^{β(W − ΔF)} in the TH3 free energies; crooks_ratio — the ratio form on pairs of positive transition probability;
• workDist hH₀ hH₁ U β w — the work distribution, P(W = w) = ∑_{W(i,j) = w} P(i, j); workDist_nonneg, sum_workDist (a probability law on the finite set of work values);
• ★★ crooks (TH5b, the histogram form): P_F(w) = P_R(−w) · e^{β(w − ΔF)} for every real w, by reindexing the reverse pairs along Prod.swap;
• jarzynski_workDist — Jarzynski read on the histogram: ∑_w P_F(w) e^{−βw} = e^{−βΔF}.

CSD reading

The forward and reverse protocols are two runs of the same de-isolation with the flow reversed; on the sector the reverse protocol is the time-reversed Schrödinger flow, which is again a Hamiltonian flow (of −⟨H⟩), so both protocols live under Liouville. The theorem says the two records' work statistics are related pointwise, not only on average: the irreversibility of a single run is priced by e^{β(W − ΔF)}. The sector-level instantiation is TH5d (specs/BACKLOG.md ▶ OPEN QUEUE #4).

Honest scope

As TH5a: finite dimension, projective readouts in the spectral-theorem eigenbases, a closed driven system, the same β at both ends; the reverse protocol is defined with the same eigenbases (its transition matrix is the transpose, tpmTransition_star, so no choice is hidden). The ratio form P_F/P_R = e^{β(W − ΔF)} needs P_R(j, i) ≠ 0, i.e. a positive transition probability; the product form crooks_pairwise_freeEnergy needs nothing and is the theorem. Requires [Nonempty n] (TH3's hypothesis).

Provenance

Foundational-triple only (propext, Classical.choice, Quot.sound); no sorry, no new axioms. Consumes TH5a and TH3; nothing is re-proved.

The reverse protocol

theorem CSD.Thermo.tpmUnitary_star {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) : tpmUnitary hH₁ hH₀ (star U) = star (tpmUnitary hH₀ hH₁ U)

The reverse protocol's unitary between the swapped eigenbases is the adjoint of the forward one: V₀ᴴ Uᴴ V₁ = (V₁ᴴ U V₀)ᴴ.

theorem CSD.Thermo.tpmTransition_star {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) (i j : n) : tpmTransition hH₁ hH₀ (star U) j i = tpmTransition hH₀ hH₁ U i j

Microscopic reversibility: the reverse protocol's transition matrix is the transpose of the forward one, ‖⟨e₀ i, Uᴴ e₁ j⟩‖² = ‖⟨e₁ j, U e₀ i⟩‖².

theorem CSD.Thermo.tpmWork_symm {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (i j : n) : tpmWork hH₁ hH₀ j i = -tpmWork hH₀ hH₁ i j

The reverse protocol's work on the pair (j, i) is minus the forward work on (i, j).

The pairwise Crooks relation

theorem CSD.Thermo.crooks_pairwise {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} [Nonempty n] (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) (β : ℝ) (i j : n) : tpmLaw hH₀ hH₁ U β i j * partitionFn H₀ hH₀ β = tpmLaw hH₁ hH₀ (star U) β j i * partitionFn H₁ hH₁ β * Real.exp (β * tpmWork hH₀ hH₁ i j)

TH5b — the Crooks relation on outcome pairs, partition-function form: the forward probability of the pair (i, j) and the reverse probability of the pair (j, i) satisfy P_F(i, j) · Z₀ = P_R(j, i) · Z₁ · e^{βW(i, j)}. The transition probabilities agree (tpmTransition_star); the Gibbs weights differ by e^{βW} up to the normalisations.

theorem CSD.Thermo.crooks_pairwise_freeEnergy {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} [Nonempty n] (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) {β : ℝ} (hβ : 0 < β) (i j : n) : tpmLaw hH₀ hH₁ U β i j = tpmLaw hH₁ hH₀ (star U) β j i * Real.exp (β * (tpmWork hH₀ hH₁ i j - (freeEnergy H₁ β⁻¹ ⋯ - freeEnergy H₀ β⁻¹ ⋯)))

The Crooks relation in free-energy form: P_F(i, j) = P_R(j, i) · e^{β(W − ΔF)} with ΔF = F₁ − F₀ the TH3 free energies of the two Gibbs states (gibbs_free_energy_eq).

theorem CSD.Thermo.crooks_ratio {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} [Nonempty n] (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) {β : ℝ} (hβ : 0 < β) {i j : n} (hT : 0 < tpmTransition hH₀ hH₁ U i j) : tpmLaw hH₀ hH₁ U β i j / tpmLaw hH₁ hH₀ (star U) β j i = Real.exp (β * (tpmWork hH₀ hH₁ i j - (freeEnergy H₁ β⁻¹ ⋯ - freeEnergy H₀ β⁻¹ ⋯)))

The Crooks ratio: on a pair of positive transition probability, P_F(i, j) / P_R(j, i) = e^{β(W − ΔF)}.

The work distribution and the histogram form

noncomputable def CSD.Thermo.workDist {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) (β w : ℝ) : ℝ

The work distribution of the protocol: the probability that the two-point-measurement work equals w, P(W = w) = ∑_{W(i, j) = w} P(i, j).

Equations

• CSD.Thermo.workDist hH₀ hH₁ U β w = ∑ q : n × n, if CSD.Thermo.tpmWork hH₀ hH₁ q.1 q.2 = w then CSD.Thermo.tpmLaw hH₀ hH₁ U β q.1 q.2 else 0

theorem CSD.Thermo.workDist_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} [Nonempty n] (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) (β w : ℝ) : 0 ≤ workDist hH₀ hH₁ U β w

noncomputable def CSD.Thermo.workValues {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) : Finset ℝ

The set of work values of the protocol: the finite set {E₁ j − E₀ i}.

Equations

• CSD.Thermo.workValues hH₀ hH₁ = Finset.image (fun (q : n × n) => CSD.Thermo.tpmWork hH₀ hH₁ q.1 q.2) Finset.univ

theorem CSD.Thermo.sum_workValues_workDist_mul {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) (β : ℝ) (g : ℝ → ℝ) : ∑ w ∈ workValues hH₀ hH₁, workDist hH₀ hH₁ U β w * g w = ∑ q : n × n, tpmLaw hH₀ hH₁ U β q.1 q.2 * g (tpmWork hH₀ hH₁ q.1 q.2)

Summing a function of the work against the work distribution over the work values is summing it against the joint law over the outcome pairs.

theorem CSD.Thermo.sum_workDist {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} [Nonempty n] (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) (β : ℝ) : ∑ w ∈ workValues hH₀ hH₁, workDist hH₀ hH₁ U β w = 1

The work distribution is a probability law on the work values.

theorem CSD.Thermo.crooks {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} [Nonempty n] (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) {β : ℝ} (hβ : 0 < β) (w : ℝ) : workDist hH₀ hH₁ U β w = workDist hH₁ hH₀ (star U) β (-w) * Real.exp (β * (w - (freeEnergy H₁ β⁻¹ ⋯ - freeEnergy H₀ β⁻¹ ⋯)))

TH5b — the Crooks fluctuation theorem, histogram form: for every real w, P_F(w) = P_R(−w) · e^{β(w − ΔF)}, where P_R is the work distribution of the reverse protocol (Gibbs state of H₁, drive by Uᴴ, read in the eigenbasis of H₀). The forward pairs (i, j) of work w are the reverse pairs (j, i) of work −w, and on each the pairwise relation holds.

theorem CSD.Thermo.jarzynski_workDist {n : Type u_1} [Fintype n] [DecidableEq n] {H₀ H₁ : Matrix n n ℂ} [Nonempty n] (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup n ℂ)) {β : ℝ} (hβ : 0 < β) : ∑ w ∈ workValues hH₀ hH₁, workDist hH₀ hH₁ U β w * Real.exp (-β * w) = Real.exp (-β * (freeEnergy H₁ β⁻¹ ⋯ - freeEnergy H₀ β⁻¹ ⋯))

Jarzynski on the histogram: ∑_w P_F(w) e^{−βw} = e^{−βΔF}, TH5a read on the work distribution.