Kinetic coefficients: $\dot x=-\lambda x=-\gamma X$

Proved

OnsagerReciprocal.kinetic_coefficients_relation

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

mathematical-physicsonsagerthermodynamics

Let $\beta$ be a positive definite real symmetric $n\times n$ matrix and $\lambda$ any real $n\times n$ matrix. Put $X=\beta x$ and $\gamma=\lambda\beta^{-1}$ . Then for every $x\in\mathbb R^n$ ,

-\lambda x=-\gamma X .

That is, the quasi-stationary relaxation law $\dot x_i=-\lambda_{ik}x_k$ can be rewritten in terms of the conjugate quantities as $\dot x_i=-\gamma_{ik}X_k$ , which is how the kinetic coefficients $\gamma_{ik}$ are introduced.

Preamble

import Mathlib
import Definitions.Def_OnsagerReciprocal_basic

open Matrix

Formal statement

namespace OnsagerReciprocal
theorem kinetic_coefficients_relation {n : ℕ} (β lam : Matrix (Fin n) (Fin n) ℝ)
    (hβ : β.PosDef) (x : Fin n → ℝ) :
    -(lam *ᵥ x) = -(kineticCoeff β lam *ᵥ conjugate β x) := 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\in\mathbb N$ , every real $n\times n$ matrix $\beta$ that is positive definite (in Mathlib's sense for real matrices: $\beta$ is symmetric and $v^{\mathsf T}\beta v>0$ for every nonzero $v\in\mathbb R^n$ ), every real $n\times n$ matrix $\lambda$ and every $x\in\mathbb R^n$ :

-(\lambda x)=-\big((\lambda\beta^{-1})(\beta x)\big),

where $\beta^{-1}$ is the matrix inverse (genuine inverse here, since positive definite matrices are invertible). The statement is a single vector identity; no time variable or derivative appears in it. For $n=0$ both sides are the empty vector.

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

Kinetic coefficients: x˙=−λx=−γX\dot x=-\lambda x=-\gamma Xx˙=−λx=−γX

Kinetic coefficients: $\dot x=-\lambda x=-\gamma X$