Quantum probability current: $\nabla\cdot\mathbf j+\partial_t|\Psi|^2=0$ from the Schrödinger equation

Proved

ContinuityEqWiki.probability_continuity_of_schrodinger

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

continuity-equationmathematical-physics

Let $\hbar>0$ and $m>0$ , let $U:\mathbb R\times\mathbb R^3\to\mathbb R$ be a real potential, and let $\Psi:\mathbb R\times\mathbb R^3\to\mathbb C$ be a wavefunction of class $C^2$ jointly in $(t,\mathbf r)$ that solves the time-dependent Schrödinger equation

-\frac{\hbar^2}{2m}\nabla^2\Psi+U\Psi=i\hbar\frac{\partial\Psi}{\partial t}.

With the probability density $\rho=\Psi^*\Psi=|\Psi|^2$ and the probability current

\mathbf j=\frac{\hbar}{2mi}\big[\Psi^*(\nabla\Psi)-\Psi(\nabla\Psi^*)\big],

the continuity equation holds everywhere:

\nabla\cdot\mathbf j+\frac{\partial\rho}{\partial t}=0 .

This expresses local conservation of probability in quantum mechanics.

Preamble

import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs

Formal statement

namespace ContinuityEqWiki

theorem probability_continuity_of_schrodinger (hbar m : ℝ) (hhbar : 0 < hbar) (hm : 0 < m)
    (U : ℝ → Space → ℝ) (Ψ : ℝ → Space → ℂ) (hΨ : ContDiff ℝ 2 (Function.uncurry Ψ))
    (hS : SchrodingerEq hbar m U Ψ) :
    ∀ t x, div (probCurrent hbar m Ψ t) x + timeDeriv (probDensity Ψ) 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 "Quantum mechanics", including the box "Consistency with Schrödinger equation"

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 $\hbar,m$ be real numbers with $\hbar>0$ and $m>0$ , let $U:\mathbb R\times\mathbb R^3\to\mathbb R$ be arbitrary (no regularity assumed), and let $\Psi:\mathbb R\times\mathbb R^3\to\mathbb C$ be $C^2$ jointly in $(t,x)$ , where $\mathbb C$ is viewed as a real normed space. Assume that for all $t,x$

-\frac{\hbar^2}{2m}\,\nabla^2\Psi(t,\cdot)(x)+U(t,x)\,\Psi(t,x)=i\hbar\,\partial_t\Psi(t,x),

with $\nabla^2=\sum_{k=0}^2\partial_k\partial_k$ (real-direction partial derivatives of the complex-valued function). Define $\rho(t,x)=|\Psi(t,x)|^2$ and $\mathbf j(t,x)\in\mathbb R^3$ with

\mathbf j(t,x)_k=\operatorname{Re}\left[\frac{\hbar}{2mi}\Big(\overline{\Psi(t,x)}\,\partial_k\Psi(t,\cdot)(x)-\Psi(t,x)\,\partial_k\overline{\Psi(t,\cdot)}(x)\Big)\right].

Conclusion: for all $t\in\mathbb R$ , $x\in\mathbb R^3$ ,

\sum_{k=0}^{2}\partial_k\big(\mathbf j(t,\cdot)_k\big)(x)+\partial_t\rho(t,x)=0 .

View graph

Quantum probability current: ∇⋅j+∂t∣Ψ∣2=0\nabla\cdot\mathbf j+\partial_t|\Psi|^2=0∇⋅j+∂t​∣Ψ∣2=0 from the Schrödinger equation

Quantum probability current: $\nabla\cdot\mathbf j+\partial_t|\Psi|^2=0$ from the Schrödinger equation