Semiconductor electron continuity equation (product-rule form)

Proved

ContinuityEqWiki.electron_continuity_product_rule

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

continuity-equationmathematical-physics

Consider one-dimensional electron transport in a semiconductor. Let $n(t,x)$ be the electron concentration and $E(t,x)$ the electric field, let $e>0$ be the elementary charge, $\mu_n$ the electron mobility and $D_n$ the diffusion coefficient, and let $G_n(t,x)$ , $R_n(t,x)$ be the generation and recombination rates. Assume $n(t,\cdot)$ is $C^2$ and $E(t,\cdot)$ is differentiable for every $t$ . With the electron current density $J_n=e\,n\,\mu_nE+eD_n\frac{\partial n}{\partial x}$ , suppose the conservation law

\frac{\partial n}{\partial t}=\frac1e\frac{\partial J_n}{\partial x}+(G_n-R_n)

holds everywhere. Then everywhere

\frac{\partial n}{\partial t}=\mu_nE\frac{\partial n}{\partial x}+\mu_n n\frac{\partial E}{\partial x}+D_n\frac{\partial^2n}{\partial x^2}+(G_n-R_n).

This is the final expression of the source's derivation, obtained by applying the product rule.

Formalization Note The source writes $d/dt$ and $d/dx$ ; since $n$ and $E$ depend on both $t$ and $x$ , these are partial derivatives. The mobility and diffusion coefficient are constants.

Preamble

import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs

Formal statement

namespace ContinuityEqWiki

theorem electron_continuity_product_rule (e μ D : ℝ) (he : 0 < e) (n E G R : ℝ → ℝ → ℝ)
    (hn : ∀ t, ContDiff ℝ 2 (n t)) (hE : ∀ t, Differentiable ℝ (E t))
    (conservation : ∀ t x, deriv (fun s => n s x) t =
      1 / e * deriv (fun y => e * n t y * μ * E t y + e * D * deriv (n t) y) x
        + (G t x - R t x)) :
    ∀ t x, deriv (fun s => n s x) t =
      μ * E t x * deriv (n t) x + μ * n t x * deriv (E t) x + D * deriv (deriv (n t)) x
        + (G t x - R 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 "Semiconductor", subsection "Derivation" (final expression)

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 $e,\mu,D$ be real numbers with $e>0$ (no sign condition on $\mu,D$ ), and let $n,E,G,R:\mathbb R\times\mathbb R\to\mathbb R$ (written $f(t,x)$ ). Assume:

for every $t$ , $x\mapsto n(t,x)$ is $C^2$ ;
for every $t$ , $x\mapsto E(t,x)$ is differentiable;
for all $t,x$ :

\frac{d}{ds}\Big|_{s=t}n(s,x)=\frac1e\cdot\frac{d}{dy}\Big|_{y=x}\Big(e\,n(t,y)\,\mu\,E(t,y)+e\,D\,\partial_yn(t,y)\Big)+\big(G(t,x)-R(t,x)\big).

No regularity in $t$ is assumed; the $t$ -derivative is the one-variable derivative (junk $0$ if it does not exist), and $G,R$ are arbitrary. Conclusion: for all $t,x$ ,

\frac{d}{ds}\Big|_{s=t}n(s,x)=\mu\,E(t,x)\,\partial_xn(t,x)+\mu\,n(t,x)\,\partial_xE(t,x)+D\,\partial_x^2n(t,x)+\big(G(t,x)-R(t,x)\big).

View graph