Prove2Me

Four-divergence of the four-current: ∂μJμ=c ∂ρ∂(ct)+∇⋅j\partial_\mu J^\mu=c\,\frac{\partial\rho}{\partial(ct)}+\nabla\cdot\mathbf j

Proved
ContinuityEqWiki.fourDiv_fourCurrent

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

continuity-equationmathematical-physics

Let c>0c>0 be the speed of light, 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 a density and its current, both C1C^1 jointly in (t,x)(t,x). Form the four-current J=(cρ,jx,jy,jz)J=(c\rho,j_x,j_y,j_z) as a field on spacetime with coordinates (x0,x)(x^0,x), x0=ctx^0=ct. Then at every spacetime point (ct,x)(ct,x),

∂μJμ=c∂ρ∂(ct)+∇⋅j=∂ρ∂t+∇⋅j.\partial_\mu J^\mu=c\frac{\partial\rho}{\partial(ct)}+\nabla\cdot\mathbf j=\frac{\partial\rho}{\partial t}+\nabla\cdot\mathbf j .

This identifies the four-divergence of the four-current with the left-hand side of the continuity equation.

Preamble
import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs
Formal statement
namespace ContinuityEqWiki

theorem fourDiv_fourCurrent (c : ℝ) (hc : 0 < c) (ρ : ℝ → Space → ℝ) (j : ℝ → Space → Space)
    (hρ : ContDiff ℝ 1 (Function.uncurry ρ)) (hj : ContDiff ℝ 1 (Function.uncurry j))
    (t : ℝ) (x : Space) :
    fourDiv (fourCurrent c ρ j) (spacetimePoint c t x) = timeDeriv ρ t x + div (j t) x := 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" (4-current and its 4-divergence)
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. Let J:R4→R4J:\mathbb R^4\to\mathbb R^4 be 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). Then for every t∈Rt\in\mathbb R and x∈R3x\in\mathbb R^3,

∑μ=03∂μ(Jμ)(ct,x)=∂tρ(t,x)+∇⋅j(t,⋅)(x),\sum_{\mu=0}^{3}\partial_\mu(J^\mu)(ct,x)=\partial_t\rho(t,x)+\nabla\cdot\mathbf j(t,\cdot)(x),

where ∂μ\partial_\mu is the partial derivative in the μ\mu-th spacetime coordinate, ∂tρ(t,x)\partial_t\rho(t,x) the derivative of s↦ρ(s,x)s\mapsto\rho(s,x) at tt, and ∇⋅\nabla\cdot the spatial divergence.

View graph