Prove2Me

Virial as a sum over pairs (Newton's third law)

Proved
VirialTheorem.virial_sum_pairs

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

classical-mechanicsvirial-theorem

Let x1,…,xN∈R3x_1,\dots,x_N\in\mathbb R^3 be positions and Fjk∈R3F_{jk}\in\mathbb R^3 (1≤j,k≤N1\le j,k\le N) be the force of particle jj on particle kk, satisfying Newton's third law Fjk=−FkjF_{jk}=-F_{kj} for all j,kj,k (in particular Fjj=0F_{jj}=0). With Fk=∑jFjkF_k=\sum_j F_{jk},

∑k=1NFk⋅xk=∑k=1N∑j<kFjk⋅(xk−xj).\sum_{k=1}^N F_k\cdot x_k=\sum_{k=1}^N\sum_{j<k}F_{jk}\cdot(x_k-x_j).

This rewrites the virial as a sum over unordered pairs.

Preamble
import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology
Formal statement
namespace VirialTheorem

theorem virial_sum_pairs {N : ℕ} (Fp : Fin N → Fin N → Space) (x : Fin N → Space)
    (hanti : ∀ j k, Fp j k = -Fp k j) :
    ∑ k, inner ℝ (∑ j, Fp j k) (x k) =
      ∑ k, ∑ j ∈ Finset.univ.filter (fun j => j < k), inner ℝ (Fp j k) (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' (pair splitting)
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≥0N\ge0, let Fjk∈R3F_{jk}\in\mathbb R^3 be given for every ordered pair of indices (j,k)(j,k), and let x0,…,xN−1∈R3x_0,\dots,x_{N-1}\in\mathbb R^3. Assume Fjk=−FkjF_{jk}=-F_{kj} for all j,kj,k (which in particular forces Fjj=0F_{jj}=0). Then

∑k⟨∑jFjk, xk⟩=∑k∑j<k⟨Fjk, xk−xj⟩,\sum_k\Big\langle\sum_j F_{jk},\,x_k\Big\rangle=\sum_k\sum_{j<k}\langle F_{jk},\,x_k-x_j\rangle,

where j<kj<k refers to the natural order on indices. No other conditions; the statement is purely algebraic at a single configuration.

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