Virial of potential pair forces: $\sum_k F_k\cdot r_k=-\sum_{j<k}V'_{jk}(r_{jk})\,r_{jk}$

Proved

VirialTheorem.virial_central_potential

by Lucas · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

classical-mechanicsvirial-theorem

Let $x_1,\dots,x_N\in\mathbb R^3$ be pairwise distinct and let $V_{jk}:\mathbb R\to\mathbb R$ be pair potentials with $V_{jk}=V_{kj}$ , each $V_{jk}$ ( $j\ne k$ ) differentiable at $r_{jk}=\|x_k-x_j\|$ . With $F_{jk}=-\nabla_{x_k}V_{jk}(\|x_k-x_j\|)$ and $F_k=\sum_j F_{jk}$ ,

\sum_{k=1}^N F_k\cdot x_k=-\sum_{k=1}^N\sum_{j<k}V_{jk}'(r_{jk})\,r_{jk}.

Preamble

import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology

Formal statement

namespace VirialTheorem

theorem virial_central_potential {N : ℕ} (V : Fin N → Fin N → ℝ → ℝ) (x : Fin N → Space)
    (hsymm : ∀ j k, V j k = V k j)
    (hx : ∀ j k, j ≠ k → x j ≠ x k)
    (hV : ∀ j k, j ≠ k → DifferentiableAt ℝ (V j k) (dist (x k) (x j))) :
    ∑ k, inner ℝ (netPairForce V x k) (x k) =
      -∑ k, ∑ j ∈ Finset.univ.filter (fun j => j < k),
        deriv (V j k) (dist (x k) (x j)) * dist (x k) (x j) := by sorry

end VirialTheorem

Source

Wikipedia, "Virial theorem" (article supplied as Virial_theorem.pdf), https://en.wikipedia.org/wiki/Virial_theorem, section 'Connection with the potential energy between particles' (final formula)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - drafting agent, non-blind

Non-blind read-back. This read-back is not independent testimony. It was written by the same agent that drafted the Lean statements, with full knowledge of the source article and of the intended meaning. Reviewers must not treat it as a blind audit; an independent read-back should still be obtained before relying on it.

Let $N\ge0$ , pair potentials $V_{jk}:\mathbb R\to\mathbb R$ and $x\in(\mathbb R^3)^N$ , with (i) $V_{jk}=V_{kj}$ for all $j,k$ ; (ii) $x_j\ne x_k$ for $j\ne k$ ; (iii) $V_{jk}$ differentiable at $\|x_k-x_j\|$ for all $j\ne k$ . Then, with $F_k(x)=\sum_j F_{jk}(x)$ the net pair force,

\sum_k\langle F_k(x),x_k\rangle=-\sum_k\sum_{j<k}V_{jk}'\big(\|x_k-x_j\|\big)\,\|x_k-x_j\| .

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Virial of potential pair forces: ∑kFk⋅rk=−∑j<kVjk′(rjk) rjk\sum_k F_k\cdot r_k=-\sum_{j<k}V'_{jk}(r_{jk})\,r_{jk}∑k​Fk​⋅rk​=−∑j<k​Vjk′​(rjk​)rjk​

Virial of potential pair forces: $\sum_k F_k\cdot r_k=-\sum_{j<k}V'_{jk}(r_{jk})\,r_{jk}$