Steady state of Fick's second law in one dimension is linear

Proved

FickDiffusion.steady_state_linear

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

diffusionpde

Let $D>0$ be a constant diffusion coefficient and let $c:\mathbb R\to\mathbb R$ be a twice continuously differentiable, time-independent concentration profile. If $c$ is a steady state of Fick's second law, i.e.

D\,c''(x)=0\quad\text{for all }x\in\mathbb R,

then $c$ is linear (affine): there are constants $a,b\in\mathbb R$ with

c(x)=a x+b\qquad\text{for all }x\in\mathbb R.

Formalization Note A steady state is modelled as a function of $x$ alone (so $\partial_t\varphi=0$ ). The hypothesis that $c$ is $C^2$ is the field's standing smoothness convention; without it Lean's deriv (which is $0$ at non-differentiable points) would let non-smooth functions such as $|x|$ satisfy the equation. $D>0$ is the physical sign of a diffusion coefficient.

Preamble

import Mathlib
import Definitions.Def_FickDiffusion_defs

open Real Filter Topology MeasureTheory

Formal statement

namespace FickDiffusion

theorem steady_state_linear (D : ℝ) (hD : 0 < D) (c : ℝ → ℝ) (hc : ContDiff ℝ 2 c)
    (hsteady : ∀ x, D * deriv (deriv c) x = 0) :
    ∃ a b : ℝ, ∀ x, c x = a * x + b := 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), paragraph beginning "An important example is the case where φ is at a steady state"

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$ with $D>0$ and every function $c:\mathbb R\to\mathbb R$ that is $C^2$ (twice continuously differentiable on all of $\mathbb R$ ), assume that for every $x\in\mathbb R$ ,

D\cdot c''(x)=0,

where $c''(x)$ is the derivative at $x$ of the derivative function $c'$ . Then there exist real numbers $a,b$ such that $c(x)=a\,x+b$ for every $x\in\mathbb R$ . The constants $a,b$ may depend on $c$ (and $D$ ); nothing is asserted about their values.

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