TH3: temperature, free energy, and the Gibbs variational principle

Category: conceptually 1-Mathlib (CSD-free general quantum statistical mechanics) with a CSD reading; kept in the CSD.Thermo tree alongside TH1/TH2.

At fixed inverse temperature β > 0 (temperature T = 1/β), the Gibbs state ρ_β = exp(-βH)/Z, Z = Tr(exp(-βH)), minimises the free energy F(ρ) = E(ρ) − T·S(ρ) (energy E(ρ) = Re Tr(ρH), entropy S) over all density operators, with minimum value the standard F(ρ_β) = −T log Z. This is the variational characterisation of thermal equilibrium: at temperature T, nature minimises free energy, and the minimiser is the Boltzmann/Gibbs state. In the CSD reading it is the equilibrium of the typicality ensemble; the second law (TH2) and canonical typicality (TH1) are its entropy- and volume-facing shadows.

Main results

• gibbsState H hH β : the Gibbs density exp(-βH)/Z, built through the Hermitian functional calculus hH.cfc (x ↦ exp(-βx)/Z); gibbsState_posDef, gibbsState_trace (a genuine density), and the crux cfc_log_gibbsState : log(ρ_β) = −β·H − (log Z)·1.
• freeEnergy H hH T ρ hρ := Re Tr(ρH) − T·S(ρ).
• gibbs_free_energy_eq : F(ρ_β) = −T·log Z (the equilibrium free energy).
• gibbs_free_energy_min (TH3, the variational principle): for β > 0, F(ρ_β) ≤ F(ρ) for every density ρ. Proof: β(F(ρ) − F(ρ_β)) = D(ρ ‖ ρ_β) ≥ 0 by Klein's inequality (relEntropy_nonneg), using the log-linear form of log ρ_β.

Honest scope

F uses vonNeumannEntropy (K1) and the energy Re Tr(ρH); temperature enters as the parameter T = 1/β. Equality F(ρ) = F(ρ_β) iff ρ = ρ_β (the strict Klein case) is not separately extracted here — only the inequality. As with the rest of the thermo track this is a QM-statistical-mechanics theorem with a CSD reading; the deterministic-microdynamics interpretation rests on the shared SO-1/D1 residue. Requires [Nonempty n] (a Gibbs state needs at least one level; otherwise Z = 0).

Provenance

Foundational-triple only (propext, Classical.choice, Quot.sound); no sorry, no new axioms. Reuses K1 (vonNeumannEntropy) and the Klein / relative-entropy layer (relEntropy_nonneg, cfc_eq_conj_diagonal, re_trace_self_log); nothing is re-proved.

The partition function and Gibbs weights

noncomputable def CSD.Thermo.partitionFn {n : Type u_1} [Fintype n] [DecidableEq n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) : ℝ

The partition function Z = Tr(exp(-βH)) = ∑ᵢ exp(-β λᵢ).

Equations

• CSD.Thermo.partitionFn H hH β = ∑ i : n, Real.exp (-β * hH.eigenvalues i)

theorem CSD.Thermo.partitionFn_pos {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) : 0 < partitionFn H hH β

noncomputable def CSD.Thermo.gibbsWeight {n : Type u_1} [Fintype n] [DecidableEq n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β x : ℝ) : ℝ

The Gibbs weight x ↦ exp(-βx)/Z, the function applied to the spectrum of H to build the Gibbs state.

Equations

• CSD.Thermo.gibbsWeight H hH β x = Real.exp (-β * x) / CSD.Thermo.partitionFn H hH β

theorem CSD.Thermo.gibbsWeight_pos {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β x : ℝ) : 0 < gibbsWeight H hH β x

theorem CSD.Thermo.log_gibbsWeight {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β x : ℝ) : Real.log (gibbsWeight H hH β x) = -β * x - Real.log (partitionFn H hH β)

log of the Gibbs weight is affine in the energy: log(exp(-βx)/Z) = −βx − log Z. This is what makes the relative entropy against the Gibbs state collapse to the free-energy difference.

The Gibbs state

noncomputable def CSD.Thermo.gibbsState {n : Type u_1} [Fintype n] [DecidableEq n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) : Matrix n n ℂ

The Gibbs state ρ_β = exp(-βH)/Z, built through the Hermitian functional calculus: hH.cfc (gibbsWeight …). Its eigenvalues are the Gibbs weights exp(-β λᵢ)/Z.

Equations

• CSD.Thermo.gibbsState H hH β = hH.cfc (CSD.Thermo.gibbsWeight H hH β)

theorem CSD.Thermo.gibbsState_isHermitian {n : Type u_1} [Fintype n] [DecidableEq n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) : (gibbsState H hH β).IsHermitian

theorem CSD.Thermo.gibbsState_eq_conj {n : Type u_1} [Fintype n] [DecidableEq n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) : gibbsState H hH β = (↑hH.eigenvectorUnitary * Matrix.diagonal fun (i : n) => ↑(gibbsWeight H hH β (hH.eigenvalues i))) * star ↑hH.eigenvectorUnitary

The Gibbs state as a unitary conjugation of the diagonal weight matrix: ρ_β = U · diag(exp(-βλ)/Z) · Uᴴ with U = hH.eigenvectorUnitary. This is the definitional unfolding of hH.cfc.

theorem CSD.Thermo.eigenvectorUnitary_isUnit {n : Type u_1} [Fintype n] [DecidableEq n] (H : Matrix n n ℂ) (hH : H.IsHermitian) : IsUnit ↑hH.eigenvectorUnitary

The eigenvector unitary is a unit (invertible), so its vecMul is injective — the input to the positive-definiteness argument.

theorem CSD.Thermo.gibbsState_posDef {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) : (gibbsState H hH β).PosDef

The Gibbs state is positive-definite: a unitary conjugate of the diagonal of strictly-positive Gibbs weights.

theorem CSD.Thermo.gibbsState_trace {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) : (gibbsState H hH β).trace = 1

The Gibbs state has trace one (a genuine density): the conjugation drops out cyclically and the diagonal weights sum to Z/Z = 1.

theorem CSD.Thermo.smul_conj {n : Type u_1} [Fintype n] [DecidableEq n] (a : ℂ) (V : Matrix n n ℂ) (D : n → ℂ) : a • (V * Matrix.diagonal D * star V) = V * Matrix.diagonal (a • D) * star V

Pulling a scalar into a unitary-conjugated diagonal: a • (V · diag D · Vᴴ) = V · diag (a • D) · Vᴴ.

The crux: log(ρ_β) = −βH − (log Z)·1

theorem CSD.Thermo.cfc_log_gibbsState {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) : ⋯.cfc Real.log = -↑β • H - ↑(Real.log (partitionFn H hH β)) • 1

The Gibbs log identity. The functional-calculus logarithm of the Gibbs state is affine in the Hamiltonian:

`log(ρ_β) = −β·H − (log Z)·1`.

Both sides are U · diagonal(…) · Uᴴ on the eigenbasis of H; the diagonal of the LHS is log(exp(-βλ)/Z) = −βλ − log Z (log_gibbsWeight), matching the RHS entrywise. This is the identity that turns D(ρ ‖ ρ_β) into the free-energy difference.

Free energy and the variational principle

noncomputable def CSD.Thermo.energy {n : Type u_1} [Fintype n] (H ρ : Matrix n n ℂ) : ℝ

The energy E(ρ) = Re Tr(ρH) (mean value of the Hamiltonian).

Equations

• CSD.Thermo.energy H ρ = RCLike.re (ρ * H).trace

noncomputable def CSD.Thermo.freeEnergy {n : Type u_1} [Fintype n] [DecidableEq n] (H : Matrix n n ℂ) (T : ℝ) {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : ℝ

The free energy F(ρ) = E(ρ) − T·S(ρ) at temperature T.

Equations

• CSD.Thermo.freeEnergy H T hρ = CSD.Thermo.energy H ρ - T * QuantumInfo.vonNeumannEntropy hρ

theorem CSD.Thermo.re_trace_mul_log_gibbs {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) (β : ℝ) {ρ : Matrix n n ℂ} (htr : ρ.trace = 1) : RCLike.re (ρ * ⋯.cfc Real.log).trace = -β * energy H ρ - Real.log (partitionFn H hH β)

The cross term of the relative entropy against the Gibbs state: Re Tr(ρ · log ρ_β) = −β·E(ρ) − log Z for a trace-one ρ. Immediate from the Gibbs log identity plus trace linearity.

theorem CSD.Thermo.gibbs_free_energy_eq {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) {β : ℝ} (hβ : 0 < β) : freeEnergy H β⁻¹ ⋯ = -β⁻¹ * Real.log (partitionFn H hH β)

The Gibbs free energy equals −T log Z (the standard equilibrium free energy). Obtained by evaluating the relative-entropy identity at ρ = ρ_β, where D(ρ_β ‖ ρ_β) = 0.

theorem CSD.Thermo.gibbs_free_energy_min {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (H : Matrix n n ℂ) (hH : H.IsHermitian) {β : ℝ} (hβ : 0 < β) {ρ : Matrix n n ℂ} (hpsd : ρ.PosSemidef) (htr : ρ.trace = 1) : freeEnergy H β⁻¹ ⋯ ≤ freeEnergy H β⁻¹ ⋯

TH3 — the Gibbs variational principle (the free-energy minimum). At inverse temperature β > 0, the Gibbs state minimises the free energy among all density operators:

`F(ρ_β) ≤ F(ρ)`   for every density `ρ`,

with F(ρ_β) = −T log Z (gibbs_free_energy_eq). Proof: Klein's inequality D(ρ ‖ ρ_β) ≥ 0 unfolds, via the Gibbs log identity, to β(F(ρ) − F(ρ_β)) ≥ 0.

Non-vacuity: the trivial Hamiltonian

theorem CSD.Thermo.gibbsState_zero_trace {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (β : ℝ) : (gibbsState 0 ⋯ β).trace = 1

Non-vacuity: for H = 0 on a nonempty system the Gibbs state is the maximally-mixed state I/d (every temperature is the same), a genuine density, and the variational principle fires. Confirms the hypotheses are satisfiable.