Prove2Me

Relativistic continuity equation: ∂μJμ=0  ⟺  ∂tρ+∇⋅j=0\partial_\mu J^\mu=0\iff\partial_t\rho+\nabla\cdot\mathbf j=0

Proved
ContinuityEqWiki.fourDiv_eq_zero_iff_continuity

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

continuity-equationmathematical-physics

Let c>0c>0, and let ρ:R×R3→R\rho:\mathbb R\times\mathbb R^3\to\mathbb R and j:R×R3→R3\mathbf j:\mathbb R\times\mathbb R^3\to\mathbb R^3 be C1C^1 jointly in (t,x)(t,x), with four-current J=(cρ,jx,jy,jz)J=(c\rho,j_x,j_y,j_z). Then

∂μJμ=0  on all of spacetime⟺∂ρ∂t+∇⋅j=0  for all t,x.\partial_\mu J^\mu=0\ \text{ on all of spacetime}\quad\Longleftrightarrow\quad \frac{\partial\rho}{\partial t}+\nabla\cdot\mathbf j=0\ \text{ for all } t,x .

This is the manifestly covariant form of the source-free continuity equation.

Preamble
import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs
Formal statement
namespace ContinuityEqWiki

theorem fourDiv_eq_zero_iff_continuity (c : ℝ) (hc : 0 < c) (ρ : ℝ → Space → ℝ)
    (j : ℝ → Space → Space)
    (hρ : ContDiff ℝ 1 (Function.uncurry ρ)) (hj : ContDiff ℝ 1 (Function.uncurry j)) :
    (∀ X : Spacetime, fourDiv (fourCurrent c ρ j) X = 0) ↔
      ∀ (t : ℝ) (x : Space), timeDeriv ρ t x + div (j t) x = 0 := by sorry

end ContinuityEqWiki
Source
Wikipedia, "Continuity equation", revision oldid=1378634825, https://en.wikipedia.org/w/index.php?title=Continuity_equation&oldid=1378634825, section "Relativistic version", subsection "Special relativity" ("Then the continuity equation is ∂μJμ=0\partial_\mu J^\mu=0")
Read-back

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

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, at the explicit request of the proposal owner. Its author knew the source text and the intended meaning while writing it, so it must not be mistaken for a blind, independent audit. Reviewers should compare the Lean code against the source themselves.

Let c>0c>0, ρ:R×R3→R\rho:\mathbb R\times\mathbb R^3\to\mathbb R and j:R×R3→R3\mathbf j:\mathbb R\times\mathbb R^3\to\mathbb R^3 with (t,x)↦ρ(t,x)(t,x)\mapsto\rho(t,x) and (t,x)↦j(t,x)(t,x)\mapsto\mathbf j(t,x) both C1C^1, and let J(x0,xˉ)=(c ρ(x0/c,xˉ), j(x0/c,xˉ))J(x^0,\bar x)=\big(c\,\rho(x^0/c,\bar x),\ \mathbf j(x^0/c,\bar x)\big) on R4\mathbb R^4. The statement is the equivalence:

(∀X∈R4: ∑μ=03∂μ(Jμ)(X)=0)  ⟺  (∀t∈R, ∀x∈R3: ∂tρ(t,x)+∇⋅j(t,⋅)(x)=0).\Big(\forall X\in\mathbb R^4:\ \sum_{\mu=0}^{3}\partial_\mu(J^\mu)(X)=0\Big)\iff\Big(\forall t\in\mathbb R,\ \forall x\in\mathbb R^3:\ \partial_t\rho(t,x)+\nabla\cdot\mathbf j(t,\cdot)(x)=0\Big).

View graph