Prove2Me

Onsager's principle: symmetry of kinetic coefficients γik=γki\gamma_{ik}=\gamma_{ki}

Proved
OnsagerReciprocal.onsager_reciprocal_relations

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsonsagerthermodynamics

Onsager's principle (principle of symmetry of kinetic coefficients).

Let x=(x1,…,xn)x=(x_1,\dots,x_n) be fluctuations of nn thermodynamic quantities from equilibrium, distributed according to the Gaussian law

w(x)=A~ e−12βikxixk,w(x)=\tilde A\,e^{-\frac12\beta_{ik}x_ix_k},

where β\beta is a positive definite symmetric real matrix (in the source, βik=−1k∂2S/∂xi∂xk\beta_{ik}=-\frac1k\partial^2S/\partial x_i\partial x_k). In the quasi-stationary regime x˙i=−λikxk\dot x_i=-\lambda_{ik}x_k for a real matrix λ\lambda, so the mean value at time tt of the fluctuation that equals xx at t=0t=0 is ξ(t)=e−tλx\xi(t)=e^{-t\lambda}x. The thermodynamic conjugate quantities are Xi=βikxkX_i=\beta_{ik}x_k, and the kinetic coefficients are

γik=λil (β−1)lk,so thatx˙i=−γikXk.\gamma_{ik}=\lambda_{il}\,(\beta^{-1})_{lk},\qquad\text{so that}\qquad \dot x_i=-\gamma_{ik}X_k .

Assume the symmetry of fluctuations under time reversal: for every t≥0t\ge0 and all i,ki,k,

⟨xi(t) xk(0)⟩=⟨xi(0) xk(t)⟩,i.e.⟨ξi(t) xk⟩=⟨xi ξk(t)⟩,\langle x_i(t)\,x_k(0)\rangle=\langle x_i(0)\,x_k(t)\rangle,\qquad\text{i.e.}\qquad \langle\xi_i(t)\,x_k\rangle=\langle x_i\,\xi_k(t)\rangle,

where ⟨⋅⟩\langle\cdot\rangle is the average with respect to ww. Then the matrix of kinetic coefficients is symmetric:

γik=γkifor all i,k.\gamma_{ik}=\gamma_{ki}\qquad\text{for all }i,k .

This is the abstract form of the Onsager reciprocal relations, which express the equality of cross-coefficients between thermodynamic flows and forces (e.g. Peltier/Seebeck, thermodiffusion/Dufour) near equilibrium.

Formalization Note The Gaussian average is the ratio ∫f w dx/∫w dx\int f\,w\,dx/\int w\,dx over Lebesgue measure on Rn\mathbb R^n (so the normalizing constant A~\tilde A cancels). The time-reversal hypothesis is imposed only for t≥0t\ge0, where the quasi-stationary relaxation ξ(t)=e−tλx\xi(t)=e^{-t\lambda}x is meant to apply.

Preamble
import Mathlib
import Definitions.Def_OnsagerReciprocal_basic

open Matrix
Formal statement
namespace OnsagerReciprocal
theorem onsager_reciprocal_relations {n : ℕ} (β lam : Matrix (Fin n) (Fin n) ℝ)
    (hβ : β.PosDef)
    (hrev : ∀ t : ℝ, 0 ≤ t → ∀ i k : Fin n,
      timeCorrelation β lam t i k = timeCorrelation β lam t k i) :
    ∀ i k : Fin n, kineticCoeff β lam i k = kineticCoeff β lam k i := by sorry
end OnsagerReciprocal
Source
Wikipedia, "Onsager reciprocal relations", https://en.wikipedia.org/w/index.php?title=Onsager_reciprocal_relations&oldid=1355014688, section "Abstract formulation" and its "Proof" subsection (pp. 5-6 of the PDF export), following L. D. Landau, E. M. Lifshitz, Statistical Physics, Part 1 (1975)
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so reviewers must not treat it as independent testimony; compare the Lean code against the source yourself.

For every n∈Nn\in\mathbb N, every real n×nn\times n matrix β\beta that is positive definite (symmetric and vTβv>0v^{\mathsf T}\beta v>0 for every nonzero v∈Rnv\in\mathbb R^n) and every real n×nn\times n matrix λ\lambda, assuming that for every real t≥0t\ge0 and all indices i,k∈{1,…,n}i,k\in\{1,\dots,n\}

∫Rn(e−tλx)i xk e−12xTβx dx∫Rne−12xTβx dx=∫Rn(e−tλx)k xi e−12xTβx dx∫Rne−12xTβx dx\frac{\int_{\mathbb R^n}\big(e^{-t\lambda}x\big)_i\,x_k\,e^{-\frac12x^{\mathsf T}\beta x}\,dx}{\int_{\mathbb R^n}e^{-\frac12x^{\mathsf T}\beta x}\,dx}=\frac{\int_{\mathbb R^n}\big(e^{-t\lambda}x\big)_k\,x_i\,e^{-\frac12x^{\mathsf T}\beta x}\,dx}{\int_{\mathbb R^n}e^{-\frac12x^{\mathsf T}\beta x}\,dx}

(Lebesgue integrals, e−tλe^{-t\lambda} the matrix exponential), it follows that the matrix γ=λβ−1\gamma=\lambda\beta^{-1} is symmetric: γik=γki\gamma_{ik}=\gamma_{ki} for all indices i,ki,k. The hypothesis is satisfiable (for example λ=β\lambda=\beta, giving γ=I\gamma=I; more generally any λ\lambda for which e−tλβ−1e^{-t\lambda}\beta^{-1} is symmetric for t≥0t\ge0). For n=0n=0 the conclusion is empty. Note that the conclusion is about λβ−1\lambda\beta^{-1} only; λ\lambda itself is not asserted to be symmetric.

Human review

  • Endorsed by Shuze Chen · Oct 10, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 10, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph