Prove2Me

Time reversal at t=0t=0: γil⟨Xlxk⟩=γkl⟨Xlxi⟩\gamma_{il}\langle X_lx_k\rangle=\gamma_{kl}\langle X_lx_i\rangle

Proved
OnsagerReciprocal.reciprocity_at_time_zero

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

mathematical-physicsonsagerthermodynamics

Let β\beta be a positive definite real symmetric n×nn\times n matrix, λ\lambda a real n×nn\times n matrix and γ=λβ−1\gamma=\lambda\beta^{-1}. Average over the Gaussian fluctuation distribution w(x)∝exp⁡(−12βikxixk)w(x)\propto\exp(-\tfrac12\beta_{ik}x_ix_k), let ξ(t;x)=e−tλx\xi(t;x)=e^{-t\lambda}x and X=βxX=\beta x. Assume the symmetry of fluctuations under time reversal

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

Then for all i,ki,k,

γil ⟨Xl xk⟩=γkl ⟨Xl xi⟩.\gamma_{il}\,\langle X_l\,x_k\rangle=\gamma_{kl}\,\langle X_l\,x_i\rangle .

This is the identity obtained by differentiating the time-reversal relation and putting t=0t=0.

Preamble
import Mathlib
import Definitions.Def_OnsagerReciprocal_basic

open Matrix
Formal statement
namespace OnsagerReciprocal
theorem reciprocity_at_time_zero {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) :
    ∑ l : Fin n, kineticCoeff β lam i l *
        fluctuationAverage β (fun x => conjugate β x l * x k) =
      ∑ l : Fin n, kineticCoeff β lam k l *
        fluctuationAverage β (fun x => conjugate β x l * x 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 positive definite real n×nn\times n matrix β\beta, every real n×nn\times n matrix λ\lambda, assuming that for every real t≥0t\ge 0 and all indices i,ki,k

Cik(t)=Cki(t),Cik(t)=∫(e−tλx)i xk wβ(x) dx∫wβ(x) dx,wβ(x)=e−12xTβx,C_{ik}(t)=C_{ki}(t),\qquad C_{ik}(t)=\frac{\int(e^{-t\lambda}x)_i\,x_k\,w_\beta(x)\,dx}{\int w_\beta(x)\,dx},\quad w_\beta(x)=e^{-\frac12x^{\mathsf T}\beta x},

it follows that for all indices i,ki,k

∑l=1nγil ⟨(βx)l xk⟩=∑l=1nγkl ⟨(βx)l xi⟩,γ=λβ−1,\sum_{l=1}^n\gamma_{il}\,\langle(\beta x)_l\,x_k\rangle=\sum_{l=1}^n\gamma_{kl}\,\langle(\beta x)_l\,x_i\rangle,\qquad\gamma=\lambda\beta^{-1},

where ⟨f⟩=∫f wβ dx/∫wβ dx\langle f\rangle=\int f\,w_\beta\,dx\big/\int w_\beta\,dx (Lebesgue integrals on Rn\mathbb R^n). The symmetry hypothesis is only required for t≥0t\ge0. It is satisfiable, e.g. by λ=β\lambda=\beta (or λ\lambda any matrix for which e−tλβ−1e^{-t\lambda}\beta^{-1} is symmetric for all t≥0t\ge0).

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