The probability current, the continuity equation, and the two single-trajectory readings

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #46.

Glossary: https://glossary.constraintsurfacedynamics.com/nelson-stochastic-mechanics/ Plain-language, CSD-role and formal statements of Nelson stochastic mechanics, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

For a wavefunction ψ(t, x) solving i ∂_t ψ = −½ ∂²_x ψ + V ψ with V real (units ℏ = m = 1), the Born density ρ = |ψ|² and the current J = Im(ψ̄ ∂_x ψ) satisfy

∂_t ρ + ∂_x J = 0,

and that one identity is what both single-trajectory formulations of quantum mechanics run on:

• Bohm. In polar form ψ = R e^{iS} the current is J = R² ∂_x S = ρ v with v = ∂_x S the guidance velocity, so the continuity equation reads ∂_t ρ + ∂_x(ρ v) = 0: the Born density is transported by the guidance field — equivariance. Along a trajectory ẋ = v that is dρ/dt = −ρ ∂_x v (hasDerivAt_density_along_trajectory), the Lagrangian form.
• Nelson. The same flux, split as ρ v + ½ ∂_x ρ = ρ b with b = v + ½ ∂_x log ρ the osmotic drift, turns the continuity equation into the Fokker–Planck equation of a diffusion with constant coefficient ½: ∂_t ρ = −∂_x(ρ b) + ½ ∂²_x ρ (nelson_fokkerPlanck). So |ψ|² is the law of Nelson's diffusion at every time, as an identity between derivatives.

Contents:

• probDensity, probCurrent;
• ★ hasDerivAt_probCurrent — ∂_x J = Im(ψ̄ ∂²_x ψ): the Im(∂ψ̄ ∂ψ) = 0 cancellation;
• ★ hasDerivAt_probDensity_time — ∂_t ρ = 2 Re(ψ̄ ∂_t ψ);
• ★★ continuity_equation — ∂_t ρ + ∂_x J = 0 from the pointwise Schrödinger equation;
• hasDerivAt_polar, ★ probCurrent_polar — J = R² ∂_x S;
• ★★ continuity_polar — ∂_t ρ + ∂_x(ρ v) = 0, equivariance;
• ★★ hasDerivAt_density_along_trajectory — dρ/dt = −ρ ∂_x v along a Bohmian trajectory;
• ★★ nelson_fokkerPlanck — the Fokker–Planck form with the osmotic drift.

Honest scope

⚠️ One dimension. ∂_x is deriv; nothing here is stated on ℝᵈ, where the divergence would have to be assembled coordinatewise.

⚠️ The Schrödinger equation is a hypothesis, pointwise. This module proves an identity about any ψ that satisfies it at the point in question, together with the differentiability the identity needs; it does not solve the equation and does not connect to the semigroup of Analysis/Semigroup/SchrodingerSchwartz.lean (that would need the strong L² derivative to be read pointwise, which is a regularity theorem, not this identity).

⚠️ No diffusion process. nelson_fokkerPlanck is the Fokker–Planck equation, an identity between derivatives of ρ. That some diffusion process has ρ as its law at every time — Nelson's theorem — needs stochastic differential equations, which Mathlib does not have at the pin (MATHLIB-ABSENT(ProbabilityTheory.itoIntegral)): that half of BACKLOG #46 stays unclaimed, and the row says so.

⚠️ No trajectory existence. hasDerivAt_density_along_trajectory takes a trajectory as given (a curve whose velocity is the guidance field at the point). Existence and uniqueness of Bohmian trajectories — the flow of v, which is singular at the nodes of ψ — is not addressed.

References: D. Bohm, Phys. Rev. 85 (1952) 166, §4 (the guidance equation and equivariance); E. Nelson, Phys. Rev. 150 (1966) 1079 (the osmotic drift and the Fokker–Planck equation); specs/bohm-nelson-scoping.md; specs/BACKLOG.md #46; specs/future-work.md.

noncomputable def Schrodinger.probDensity (ψ : ℝ → ℝ → ℂ) (t x : ℝ) : ℝ

The Born density of a wavefunction.

Equations

• Schrodinger.probDensity ψ t x = ‖ψ t x‖ ^ 2

def Schrodinger.probCurrent (ψ ψx : ℝ → ℝ → ℂ) (t x : ℝ) : ℝ

The probability current Im(ψ̄ ∂_x ψ), in units ℏ = m = 1, read off the wavefunction and its spatial derivative.

Equations

• Schrodinger.probCurrent ψ ψx t x = ((starRingEnd ℂ) (ψ t x) * ψx t x).im

theorem Schrodinger.probDensity_apply (ψ : ℝ → ℝ → ℂ) (t x : ℝ) : probDensity ψ t x = ‖ψ t x‖ ^ 2

theorem Schrodinger.probCurrent_apply (ψ ψx : ℝ → ℝ → ℂ) (t x : ℝ) : probCurrent ψ ψx t x = ((starRingEnd ℂ) (ψ t x) * ψx t x).im

The two derivatives

theorem Schrodinger.probDensity_eq_re (ψ : ℝ → ℝ → ℂ) (t x : ℝ) : probDensity ψ t x = ((starRingEnd ℂ) (ψ t x) * ψ t x).re

theorem Schrodinger.hasDerivAt_probCurrent {ψ ψx : ℝ → ℝ → ℂ} {t x : ℝ} {ψxx : ℂ} (h1 : HasDerivAt (ψ t) (ψx t x) x) (h2 : HasDerivAt (ψx t) ψxx x) : HasDerivAt (probCurrent ψ ψx t) ((starRingEnd ℂ) (ψ t x) * ψxx).im x

★ The spatial derivative of the current is Im(ψ̄ ∂²_x ψ): the term from differentiating the conjugate is Im(∂ψ̄ ∂ψ) = 0, because z̄ z is real.

theorem Schrodinger.hasDerivAt_probDensity_time {ψ : ℝ → ℝ → ℂ} {t x : ℝ} {ψt : ℂ} (ht : HasDerivAt (fun (s : ℝ) => ψ s x) ψt t) : HasDerivAt (fun (s : ℝ) => probDensity ψ s x) (2 * ((starRingEnd ℂ) (ψ t x) * ψt).re) t

★ The time derivative of the density is 2 Re(ψ̄ ∂_t ψ).

The continuity equation

theorem Schrodinger.continuity_equation {ψ ψx : ℝ → ℝ → ℂ} {t x : ℝ} {ψt ψxx : ℂ} {V : ℝ → ℝ} (h1 : HasDerivAt (ψ t) (ψx t x) x) (h2 : HasDerivAt (ψx t) ψxx x) (ht : HasDerivAt (fun (s : ℝ) => ψ s x) ψt t) (hschr : Complex.I * ψt = -(1 / 2) * ψxx + ↑(V x) * ψ t x) : deriv (fun (s : ℝ) => probDensity ψ s x) t + deriv (probCurrent ψ ψx t) x = 0

★★ The continuity equation ∂_t ρ + ∂_x J = 0, from the Schrödinger equation at the point with a real potential.

Bohm: the polar form, and equivariance

theorem Schrodinger.hasDerivAt_polar {x : ℝ} {R S : ℝ → ℝ} {R' S' : ℝ} (hR : HasDerivAt R R' x) (hS : HasDerivAt S S' x) : HasDerivAt (fun (y : ℝ) => ↑(R y) * Complex.exp (↑(S y) * Complex.I)) ((↑R' + Complex.I * ↑(R x) * ↑S') * Complex.exp (↑(S x) * Complex.I)) x

The spatial derivative of a polar-form wavefunction: ∂_x (R e^{iS}) = (∂_x R + i R ∂_x S) e^{iS}.

theorem Schrodinger.probDensity_polar {ψ : ℝ → ℝ → ℂ} {t x R S : ℝ} (hval : ψ t x = ↑R * Complex.exp (↑S * Complex.I)) : probDensity ψ t x = R ^ 2

The density in polar form is R².

theorem Schrodinger.probCurrent_polar {ψ ψx : ℝ → ℝ → ℂ} {t x R S R' S' : ℝ} (hval : ψ t x = ↑R * Complex.exp (↑S * Complex.I)) (hder : ψx t x = (↑R' + Complex.I * ↑R * ↑S') * Complex.exp (↑S * Complex.I)) : probCurrent ψ ψx t x = R ^ 2 * S'

★ The current in polar form is R² ∂_x S — the Born density times the guidance velocity.

theorem Schrodinger.continuity_polar {ψ ψx : ℝ → ℝ → ℂ} {t x : ℝ} {R S R' S' V : ℝ → ℝ} {ψt ψxx : ℂ} (hval : ∀ (y : ℝ), ψ t y = ↑(R y) * Complex.exp (↑(S y) * Complex.I)) (hder : ∀ (y : ℝ), ψx t y = (↑(R' y) + Complex.I * ↑(R y) * ↑(S' y)) * Complex.exp (↑(S y) * Complex.I)) (h1 : HasDerivAt (ψ t) (ψx t x) x) (h2 : HasDerivAt (ψx t) ψxx x) (ht : HasDerivAt (fun (s : ℝ) => ψ s x) ψt t) (hschr : Complex.I * ψt = -(1 / 2) * ψxx + ↑(V x) * ψ t x) : deriv (fun (s : ℝ) => probDensity ψ s x) t + deriv (fun (y : ℝ) => probDensity ψ t y * S' y) x = 0

★★ Equivariance: with the guidance velocity v = ∂_x S, the continuity equation reads ∂_t ρ + ∂_x (ρ v) = 0 — the Born density is transported by the guidance field, which is Bohm's equivariance.

theorem Schrodinger.hasDerivAt_density_along_trajectory {ρ v : ℝ → ℝ → ℝ} {γ : ℝ → ℝ} {t : ℝ} {L : ℝ × ℝ →L[ℝ] ℝ} {ρt ρx vx : ℝ} (hγ : HasDerivAt γ (v t (γ t)) t) (hρ : HasFDerivAt (fun (p : ℝ × ℝ) => ρ p.1 p.2) L (t, γ t)) (hL1 : L (1, 0) = ρt) (hL2 : L (0, 1) = ρx) (hcont : ρt + (ρx * v t (γ t) + ρ t (γ t) * vx) = 0) : HasDerivAt (fun (s : ℝ) => ρ s (γ s)) (-(ρ t (γ t) * vx)) t

★★ Equivariance in Lagrangian form: along a trajectory whose velocity is the guidance field, the density obeys dρ/dt = −ρ ∂_x v. Stated for any density and velocity field satisfying the continuity equation at the point, which is what continuity_polar provides.

Nelson: the osmotic drift and the Fokker–Planck equation

noncomputable def Schrodinger.nelsonFlux (ρ ρ' v : ℝ → ℝ) (y : ℝ) : ℝ

Nelson's flux ρ b = ρ v + ½ ∂_x ρ: the guidance flux plus the osmotic one.

Equations

• Schrodinger.nelsonFlux ρ ρ' v y = ρ y * v y + 1 / 2 * ρ' y

theorem Schrodinger.nelsonFlux_eq_mul_drift {ρ ρ' v : ℝ → ℝ} {y : ℝ} (hρ : ρ y ≠ 0) : nelsonFlux ρ ρ' v y = ρ y * (v y + 1 / 2 * (ρ' y / ρ y))

The osmotic drift written as a drift: where the density does not vanish, ρ b = ρ (v + ½ ∂_x log ρ).

theorem Schrodinger.hasDerivAt_nelsonFlux {ρ ρ' v : ℝ → ℝ} {dflux ρ'' x : ℝ} (hflux : HasDerivAt (fun (y : ℝ) => ρ y * v y) dflux x) (hρ'' : HasDerivAt ρ' ρ'' x) : HasDerivAt (nelsonFlux ρ ρ' v) (dflux + 1 / 2 * ρ'') x

The spatial derivative of Nelson's flux: the guidance flux's derivative plus ½ ∂²_x ρ.

theorem Schrodinger.nelson_fokkerPlanck {ψ : ℝ → ℝ → ℂ} {t x : ℝ} {v ρ' : ℝ → ℝ} {dflux ρ'' ρt : ℝ} (hflux : HasDerivAt (fun (y : ℝ) => probDensity ψ t y * v y) dflux x) (hρ'' : HasDerivAt ρ' ρ'' x) (hcont : ρt + dflux = 0) : ρt = -deriv (nelsonFlux (probDensity ψ t) ρ' v) x + 1 / 2 * ρ''

★★ The Born density solves the Fokker–Planck equation of Nelson's diffusion. With the osmotic drift b = v + ½ ∂_x log ρ, so that the flux is nelsonFlux, the continuity equation ∂_t ρ + ∂_x(ρ v) = 0 becomes

∂_t ρ = −∂_x(ρ b) + ½ ∂²_x ρ,

the Fokker–Planck equation of a diffusion with constant coefficient ½: the osmotic term of the drift is exactly what cancels the diffusion term. ρ' is the density's spatial derivative and ρ'' its second.