Prove2Me

Power-law virial: ∑kFk⋅rk=−n VTOT\sum_k F_k\cdot r_k=-n\,V_{\mathrm{TOT}}

Proved
VirialTheorem.virial_power_law

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 pairwise distinct, n∈Rn\in\mathbb R, and let αjk=αkj\alpha_{jk}=\alpha_{kj} be real coefficients. For the power-law pair potentials Vjk(s)=αjksnV_{jk}(s)=\alpha_{jk}s^n, with FkF_k the net pair force and VTOT=∑k∑j<kVjk(∥xk−xj∥)V_{\mathrm{TOT}}=\sum_k\sum_{j<k}V_{jk}(\|x_k-x_j\|),

∑k=1NFk⋅xk=−n VTOT.\sum_{k=1}^N F_k\cdot x_k=-n\,V_{\mathrm{TOT}} .

Formalization Note The article uses one constant α\alpha; allowing a symmetric pair-dependent αjk\alpha_{jk} contains that case and also covers gravitation (αjk=−Gmjmk\alpha_{jk}=-Gm_jm_k).

Preamble
import Mathlib
import Definitions.Def_virial_theorem_defs

open Filter Topology
Formal statement
namespace VirialTheorem

theorem virial_power_law {N : ℕ} (α : Fin N → Fin N → ℝ) (n : ℝ) (x : Fin N → Space)
    (hα : ∀ j k, α j k = α k j)
    (hx : ∀ j k, j ≠ k → x j ≠ x k) :
    ∑ k, inner ℝ (netPairForce (powerLawPotential α n) x k) (x k) =
      -n * totalPotential (powerLawPotential α n) x := by sorry

end VirialTheorem
Source
Wikipedia, "Virial theorem" (article supplied as Virial_theorem.pdf), https://en.wikipedia.org/wiki/Virial_theorem, section 'Special case of power-law forces'
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, real numbers αjk\alpha_{jk} for all ordered pairs with αjk=αkj\alpha_{jk}=\alpha_{kj}, a real exponent nn, and a configuration x∈(R3)Nx\in(\mathbb R^3)^N with xj≠xkx_j\ne x_k whenever j≠kj\ne k. Using the potentials Vjk(s)=αjksnV_{jk}(s)=\alpha_{jk}s^n (real power), the net pair forces Fk(x)F_k(x) satisfy

∑k⟨Fk(x),xk⟩=−n∑k∑j<kαjk ∥xk−xj∥ n.\sum_k\langle F_k(x),x_k\rangle=-n\sum_k\sum_{j<k}\alpha_{jk}\,\|x_k-x_j\|^{\,n}.

There is no restriction on the sign of nn or of αjk\alpha_{jk}; n=0n=0 is allowed.

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