Example solution 1 (infinite medium): n(x,t) = (n₀/2) erfc(x / (2√(Dt)))

Proved

FickDiffusion.erfc_solution_infinite_medium

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

diffusionpde

Let $D>0$ and $n_0\in\mathbb R$ , and set

n(x,t)=\frac{n_0}{2}\,\operatorname{erfc}\Big(\frac{x}{2\sqrt{Dt}}\Big).

Then:

$\dfrac{\partial n}{\partial t}(x,t)=D\,\dfrac{\partial^2 n}{\partial x^2}(x,t)$ for all $x\in\mathbb R$ and $t>0$ ;
for every $x>0$ , $n(x,t)\to0$ as $t\to0^+$ ;
for every $x<0$ , $n(x,t)\to n_0$ as $t\to0^+$ .

So $n$ solves Fick's second law on the whole line with initial profile $n_0$ on $x<0$ and $0$ on $x>0$ : a solution of concentration $n_0$ brought into contact with pure solvent.

Formalization Note The initial condition is expressed as pointwise limits as $t\to0^+$ away from the interface $x=0$ (at $x=0$ the value is $n_0/2$ for all $t>0$ , consistent with any choice of $n(0,0)$ ).

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem erfc_solution_infinite_medium (D n₀ : ℝ) (hD : 0 < D) :
    (∀ x t : ℝ, 0 < t →
      deriv (fun s => n₀ / 2 * erfc (x / (2 * Real.sqrt (D * s)))) t =
        D * deriv (fun y => deriv (fun z => n₀ / 2 * erfc (z / (2 * Real.sqrt (D * t)))) y) x) ∧
    (∀ x : ℝ, 0 < x →
      Tendsto (fun t => n₀ / 2 * erfc (x / (2 * Real.sqrt (D * t)))) (𝓝[>] 0) (𝓝 0)) ∧
    (∀ x : ℝ, x < 0 →
      Tendsto (fun t => n₀ / 2 * erfc (x / (2 * Real.sqrt (D * t)))) (𝓝[>] 0) (𝓝 n₀)) := 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 "Example solution 1: constant concentration source and diffusion length" (p. 6), sentence beginning "If, in its turn, the diffusion space is infinite"

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 all real $D,n_0$ with $D>0$ , with $\operatorname{erfc}(u)=\frac{2}{\sqrt\pi}\int_{(u,\infty)}e^{-s^2}ds$ and real square root ( $0$ on negatives), the following three statements all hold:

for all real $x$ and $t>0$ : the derivative at $s=t$ of $s\mapsto\frac{n_0}{2}\operatorname{erfc}\big(x/(2\sqrt{Ds})\big)$ equals $D$ times the derivative at $y=x$ of the derivative function of $z\mapsto\frac{n_0}{2}\operatorname{erfc}\big(z/(2\sqrt{Dt})\big)$ (one-variable derivatives, $0$ where not differentiable);
for every $x>0$ : $\frac{n_0}{2}\operatorname{erfc}\big(x/(2\sqrt{Dt})\big)\to0$ as $t\to0$ with $t>0$ ;
for every $x<0$ : $\frac{n_0}{2}\operatorname{erfc}\big(x/(2\sqrt{Dt})\big)\to n_0$ as $t\to0$ with $t>0$ .

Nothing is asserted at $x=0$ in clauses 2–3; $n_0$ has no sign condition.

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