Derivation of Fick's second law from Fick's first law and mass conservation

Proved

FickDiffusion.fick_second_law_of_first_law_and_conservation

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

diffusionpde

Let $D\in\mathbb R$ be a constant diffusion coefficient, let $\varphi(x,t)$ be a concentration and $J(x,t)$ a flux, both real functions of position $x$ and time $t$ . Suppose

(Fick's first law) $J(x,t)=-D\,\dfrac{\partial\varphi}{\partial x}(x,t)$ for all $x,t$ ;
(mass conservation) $\dfrac{\partial\varphi}{\partial t}(x,t)+\dfrac{\partial J}{\partial x}(x,t)=0$ for all $x,t$ .

Then for all $x,t$ ,

\frac{\partial\varphi}{\partial t}(x,t)=D\,\frac{\partial^2\varphi}{\partial x^2}(x,t).

This is the textbook derivation of Fick's second law from the first law and the continuity equation.

Formalization Note Partial derivatives are written with Mathlib's deriv, which returns $0$ at points of non-differentiability. Because pulling a constant out of deriv holds unconditionally over $\mathbb R$ , no differentiability hypothesis is needed for this formal statement.

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem fick_second_law_of_first_law_and_conservation (D : ℝ) (φ J : ℝ → ℝ → ℝ)
    (hfirst : ∀ x t, J x t = -D * deriv (fun y => φ y t) x)
    (hcons : ∀ x t, deriv (fun s => φ x s) t + deriv (fun y => J y t) x = 0) :
    ∀ x t, deriv (fun s => φ x s) t = D * deriv (fun y => deriv (fun z => φ z t) y) x := by sorry

end FickDiffusion

Source

Wikipedia, "Fick's laws of diffusion" (PDF snapshot supplied by the proposer, 21 pp.), https://en.wikipedia.org/wiki/Fick%27s_laws_of_diffusion, section "Derivation of Fick's second law" (p. 5), first two displayed equations

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter (non-blind)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements, with full knowledge of the source and of the intended meaning, at the explicit instruction of the account owner. It is not a blind audit. Reviewers must not treat it as independent evidence of faithfulness and should compare it directly against the Lean code.

For every real number $D$ and all functions $\varphi,J:\mathbb R\times\mathbb R\to\mathbb R$ (arguments written $(x,t)$ ), assume:

for all $x,t$ : $J(x,t)=-D\cdot\partial_x\varphi(x,t)$ , where $\partial_x\varphi(x,t)$ denotes the derivative at $x$ of $y\mapsto\varphi(y,t)$ ;
for all $x,t$ : $\partial_t\varphi(x,t)+\partial_xJ(x,t)=0$ , where $\partial_t\varphi(x,t)$ is the derivative at $t$ of $s\mapsto\varphi(x,s)$ and $\partial_xJ(x,t)$ the derivative at $x$ of $y\mapsto J(y,t)$ .

Here every "derivative" is the one-variable derivative with the convention that it equals $0$ wherever the function is not differentiable. Conclusion: for all real $x,t$ ,

\partial_t\varphi(x,t)=D\cdot\partial_x\big(\partial_x\varphi(\cdot,t)\big)(x),

i.e. $D$ times the derivative at $x$ of the function $y\mapsto\partial_x\varphi(y,t)$ . No differentiability, sign or nonvanishing assumption is made on $D$ , $\varphi$ or $J$ ; the case $D=0$ is included.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph