Poiseuille's law: $Q=\pi\Delta p\,d^4/(128\eta L)$

Proved

MathematicsOfWater.poiseuille_law

by Lucas · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

fluid-dynamicsmathematical-physicsode

Consider steady pressure-driven flow of a Newtonian fluid of viscosity $\eta>0$ through a cylindrical pipe of diameter $d>0$ and length $L>0$ with pressure drop $\Delta p=p(0)-p(L)\in\mathbb R$ . Let $v(r)$ be the axial velocity at distance $r$ from the axis, and assume

$v$ solves the radial momentum balance $\frac1r\frac{d}{dr}\big(r\frac{dv}{dr}\big)=-\frac{\Delta p}{\eta L}$ for $0<r<d/2$ ;
$v$ is finite (bounded) near the axis;
$v$ satisfies the no-slip condition $v(d/2)=0$ at the wall, continuously from inside.

Then the volumetric flow rate is

Q=\int_0^{d/2}v(r)\,2\pi r\,dr=\frac{\pi\,\Delta p\,d^4}{128\,\eta L}.

This is Poiseuille's (Hagen–Poiseuille) law: the flow rate scales with the fourth power of the pipe diameter.

Formalization Note The hypotheses are packaged in the definition IsPipeFlow; the flow rate is the definition flowRate.

Preamble

import Mathlib
import Definitions.Def_MathematicsOfWater_PipeFlow
open Real

Formal statement

namespace MathematicsOfWater
theorem poiseuille_law (η L Δp d : ℝ) (v : ℝ → ℝ)
    (hη : 0 < η) (hL : 0 < L) (hd : 0 < d)
    (hv : IsPipeFlow η L Δp d v) :
    flowRate d v = π * Δp * d ^ 4 / (128 * η * L) := by sorry
end MathematicsOfWater

Source

Lecture 15: The Mathematics of Water, PHYS 461 & 561 (Biophysics), Drexel University, Fall 2011-2012, 11/15/2011, lecturer Luis Cruz (for Brigita Urbanc), www.physics.drexel.edu/~brigita/COURSES/BIOPHYS_2011-2012/, slides 13–16 (goal: Q = π Δp d^4 / (128 η L), slide 16)

Read-back

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

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted these Lean statements, at the explicit request of the proposal owner. It is not the blind, independent auditor read-back the platform recommends; the author knew the intended meaning while writing it. Reviewers must check it against the Lean code themselves and should not treat it as independent confirmation of faithfulness.

Fix real numbers $\eta,L,\Delta p,d$ and $v:\mathbb R\to\mathbb R$ with $\eta>0$ , $L>0$ , $d>0$ ; $\Delta p$ is arbitrary. Write $R=d/2$ and $v'(s)$ for the derivative of $v$ at $s$ ( $0$ where $v$ is not differentiable). Assume:

for every $0<r<R$ : $v$ is differentiable at $r$ , $g(s)=s\,v'(s)$ is differentiable at $r$ , and $\frac1r g'(r)=-\frac{\Delta p}{\eta L}$ ;
some real $M$ bounds $|v(r)|\le M$ for all $0<r<R$ ;
$v(x)\to v(R)$ as $x\to R$ from the left;
$v(R)=0$ .

Conclusion:

\int_0^{d/2} v(r)\cdot2\pi r\,dr=\frac{\pi\,\Delta p\,d^4}{128\,\eta\,L}.

The integral is the oriented Lebesgue (interval) integral over $[0,d/2]$ ; by the platform's convention it would equal $0$ if the integrand were not integrable, so the statement implicitly also requires the actual integral to have this value. The value $v(0)$ and values outside $(0,d/2]$ play no role except through the integral, where the single point $r=0$ has measure zero. The hypotheses are satisfiable (by $v(r)=\frac{\Delta p}{4\eta L}(\frac{d^2}{4}-r^2)$ ).

Human review

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

View graph

Poiseuille's law: Q=πΔp d4/(128ηL)Q=\pi\Delta p\,d^4/(128\eta L)Q=πΔpd4/(128ηL)

Poiseuille's law: $Q=\pi\Delta p\,d^4/(128\eta L)$