feat(FluidDynamics): Adding more fluid dynamics - continuation of PR #949 and #1112 , by FloWsnr · Pull Request #1125 · leanprover-community/physlib

FloWsnr · 2026-05-26T13:48:51Z

Summary

This PR extends the fluid dynamics API with reusable foundations for incompressibility, continuity, momentum balance, Euler flow, and Bernoulli flow based. It copies PR #949 ideas refactored based on the structure agreed upon in #1112 .

Changes

Structure

I realized that we previously placed general equations into the Navier-Stokes namespace which instead should be general FluidDynamics, since they will be reused by systems other than Navier-Stokes.

Moves the continuity equation out of NavierStokes/ into reusable FluidDynamics/Continuity.lean.
Extracts generic momentum-density, momentum-flux, material-acceleration, and conservative/convective momentum LHS definitions into FluidDynamics/Momentum.lean.
Updates Navier-Stokes files to reuse the shared continuity and momentum infrastructure.

Additions

Adds general incompressibility predicates in FluidDynamics/Incompressible.lean. This can be reused in Navier-Stokes, Euler and other fluid systems.
Adds Euler momentum equations in conservative and convective form.
Adds Bernoulli-flow data, steady-flow, material-derivative, isentropic-flow, Bernoulli-function, and Bernoulli-law predicates.

Notes

This branch intentionally keeps the new fluid definitions dimension-generic and avoids recreating the older IdealFluid wrapper from PR #949.

jstoobysmith · 2026-05-27T04:34:01Z

+
+/-- The conservative and convective Euler forms are equivalent when the fields are
+differentiable enough for the product rules. -/
+theorem Euler_iff_ConvectiveEuler


should be e.g. euler_iff_convectiveEuler

done. Btw, is there a way to bake these rules into the linter since I keep making the same mistake?

This should be possible. If you make a comment here about this, someone might pick it up as something to do: https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Infrastructure.20ideas/with/597860431

jstoobysmith · 2026-05-27T13:16:14Z

+-/
+
+/-- The fields needed for Euler momentum balance: fluid state, pressure, and body force. -/
+structure FluidInEulerBalance (d : ℕ) extends FluidState d where


This is ok for now - but I think we should have a think about how we name all of these things

The idea would be to have some key data structures FluidState, FluidInEulerBalance, etc. with which we organize the folders around.

Yes, I am not happy with the naming of all the structures, except FluidState which is fine.
I don't have a great idea tho.
Perhaps it's better to define a few overarching structures like

FluidState

ThermodynamicFluidState

which provide "all" parameters we might need. The functions (NavierStokes, Euler, Bernoulli) would then all use these even though some fields are not needed for this.
But again, not super convinced yet

Would splitting based on kinematics vs dynamics work? Which of these quantities are actually derived and which define the system?

jstoobysmith · 2026-05-27T13:16:57Z

+-/
+
+/-- The right-hand side of Euler momentum balance, `-grad p + rho f`. -/
+noncomputable def eulerMomentumRHS (d : ℕ) (data : FluidInEulerBalance d) : VectorField d :=


Is there a better name for this which gives across the physical meaning? If not, maybe we should not define it explicitly. Similarly with other definitions like this.

I now called it eulerForceDensity which is accurate but not really great. We can also inline twice, for both Euler equations. It really depends on whether future lemma will be using this. I don't know...

jstoobysmith · 2026-05-27T18:36:04Z

+-/
+
+/-- The momentum density `rho u`. -/
+def momentumDensity (d : ℕ) (fluid : FluidState d) : MomentumDensityField d :=


All these should be in the FluidState namespac

jstoobysmith · 2026-05-28T05:49:22Z

I think it might be best to sort this Fluid structure out first before merging this, as I think it will help with the organization of things.

FloWsnr · 2026-05-28T14:56:36Z

I spent some time thinking about this and this is my current favorite:

Two main fluid data structures:

The generic kinematic fluid data

structure FluidFlow (d : ℕ) where
    massDensity : MassDensity d
    velocity : VelocityField d

and the generic dynamic fluid data, based on the generic Cauchy momentum equation.

structure CauchyFlow (d : ℕ) extends FluidFlow d where
    stress : CauchyStress d
    bodyForce : SpecificBodyForce d

We can then use definitions/predicates for the physical cases.

def IsUnforced (d : ℕ) (flow : CauchyFlow d) : Prop :=
    ∀ t x, flow.bodyForce t x = 0

def HasConservativeBodyForce
      (d : ℕ) (flow : CauchyFlow d) (potential : Space d → ℝ) : Prop :=
    ∀ t x, flow.bodyForce t x = -(∇ potential x)

def IsInviscid
      (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d) : Prop :=
    ∀ t x, flow.stress t x = -pressure t x • 1

def IsNewtonian
      (d : ℕ) (flow : CauchyFlow d)
      (pressure shearViscosity bulkViscosity : ScalarField d) : Prop :=

And define force-density helpers:

noncomputable def bodyForceDensity (d : ℕ) (flow : CauchyFlow d) : VectorField d :=
    fun t x => flow.massDensity t x • flow.bodyForce t x

noncomputable def stressForceDensity (d : ℕ) (flow : CauchyFlow d) : VectorField d :=
    fun t x => matrixDiv d (flow.stress t) x

noncomputable def totalForceDensity (d : ℕ) (flow : CauchyFlow d) : VectorField d :=
    fun t x => stressForceDensity d flow t x + bodyForceDensity d flow t x

Then the aforementioned Cauchy momentum equation is the generic:

def CauchyMomentumEquation (d : ℕ) (flow : CauchyFlow d) : Prop :=
    ∀ t x, conservativeMomentumLHS d flow.toFluidFlow t x = totalForceDensity d flow t x

Euler becomes:

def Euler (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d) : Prop :=
    ClassicalContinuityEquation d flow.toFluidFlow ∧
      CauchyMomentumEquation d flow ∧
        IsInviscid d flow pressure

Navier-Stokes becomes:

def NavierStokes
      (d : ℕ) (flow : CauchyFlow d)
      (pressure shearViscosity bulkViscosity : ScalarField d) : Prop :=
    ClassicalContinuityEquation d flow.toFluidFlow ∧
      CauchyMomentumEquation d flow ∧
        IsNewtonian d flow pressure shearViscosity bulkViscosity

If we want to work with thermodynamic equations (Bernoulli, energy balances etc), we should introduce a single new structure with combines flow with thermodynamics.

structure ThermodynamicCauchyFlow (d : ℕ) extends CauchyFlow d where
    entropy : ScalarField d
    enthalpy : ScalarField d
-- perhaps also
    temperature : ScalarField d
    heatFlux : VectorField d

With this, we can basically describe all fluid flow situations.
What do you think of this?

jstoobysmith · 2026-05-28T15:21:19Z

It is unclear why something like pressure is not in FluidFlow here? Maybe because you can get it from the stress?

jstoobysmith · 2026-05-28T15:26:20Z

I also think something like HasConservativeBodyForce should be an exists statement, not include a potential.

FloWsnr · 2026-05-28T15:29:02Z

yes exactly, you get it from the stress:

In my idea, FluidFlow is meant to be the minimal kinematic/mass-transport object, not the full dynamic fluid model. Pressure is not needed for continuity, incompressibility, material derivatives, or kinetic quantities.

Once we move to momentum balance, I think the more invariant field is the Cauchy stress tensor; pressure then appears through stress laws, e.g. inviscid stress σ = -p I or Newtonian stress σ = -p I + τ.

jstoobysmith · 2026-05-28T15:31:02Z

How does viscosity come into this all?

FloWsnr · 2026-05-28T15:36:19Z

Viscosity is just another form of stress in the Cauchy version.
As above for the Newtonian stress:

σ = -p I + viscousStress

The total stress is pressure (p) plus viscosity.

jstoobysmith · 2026-05-28T15:39:35Z

Ok great! This looks good then. I wonder if FluidKinematics and FluidDynamics would be better names, but I’m also happy with what you have callled them. Would you be able to restructure the API around these?

FloWsnr · 2026-05-28T15:43:02Z

Great!
FluidKinematics could be okay, but FluidDynamics would be ugly inside the namespace which is already called FluidDynamics as well, right?

I will get right onto it and refactor...

jstoobysmith · 2026-05-28T15:46:49Z

Yeah - ok let’s keep names as they are

FloWsnr · 2026-05-30T13:36:37Z

okay, check out the new structure and let me know what you think:

Main changes

We renamed the minimal carrier from FluidState to FluidFlow. It still contains only rho and velocity,
We replaced the old usage-shaped structures with 2 physically meaningful layers:
- CauchyFlow extends FluidFlow with stress and bodyForce
- ThermodynamicCauchyFlow extends CauchyFlow with entropy and enthalpy.
We added a shared Cauchy momentum layer. This defines the generic balance
conservativeMomentumLHS = matrixDiv stress + rho • bodyForce
plus the convective version and their equivalence theorem. This replaces the old Navier-Stokes-specific momentum module.
Euler now uses CauchyFlow plus an IsInviscid predicate. Pressure appears only through the stress law stress = -p I, not as a field of the flow.
Navier-Stokes now uses CauchyFlow plus an IsNewtonian predicate. Pressure and viscosities are parameters to newtonianStressTensor, so viscosity enters through stress, exactly as discussed in the PR.
Bernoulli no longer has a separate FluidInBernoulliFlow structure. It uses ThermodynamicCauchyFlow and takes the external potential explicitly. HasConservativeBodyForce was changed to existential form: there exists a potential.

Side changes

Reorganized namespaces: FluidFlow.* now contains flow-derived continuity, incompressibility, momentum, acceleration, and time-independence APIs. CauchyFlow.* now contains Cauchy momentum equations and Cauchy stress-law helpers/predicates. Equation systems like Euler, ConvectiveEuler, NavierStokes, and ConvectiveNavierStokes stayed top-level in FluidDynamics.
Added the inviscid bridge theorem: CauchyFlow.matrixDiv_stress_eq_neg_grad_pressure_of_is_inviscid, showing that inviscid stress -p I gives the usual -grad p force term.
Moved flow time-independence predicates into FluidFlow: FluidFlow.DensityTimeIndependent and FluidFlow.VelocityTimeIndependent.
Removed Bernoulli’s local IsSteady, since it only described velocity time-independence and now lives more accurately as FluidFlow.VelocityTimeIndependent.

jstoobysmith

Sorry for my delay here - have been travelling.

jstoobysmith · 2026-06-01T11:17:30Z

I would think about wether it makes sense to have folders

./CaucyFlow ./FluidState ./ThermodynamicFluid

jstoobysmith · 2026-06-10T20:48:53Z

@FloWsnr Regarding this, if you don't think you have time to address the reviews, we could put it in the new PhyslibAlpha directory for now. See:

https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/PhyslibAlpha/with/601570535

FloWsnr · 2026-06-11T15:34:15Z

Hey, I'm sorry, had some travel & new job. Still plan to do the final fixes asap. I'll try this weekend!

FloWsnr · 2026-06-14T13:55:10Z

I think I addressed all comments now except for the larger rename / restructure into subdirs

I would think about whether it makes sense to have folders

Not sure if this split up the code too much, but if you want I can quickly do that

jstoobysmith · 2026-06-26T05:02:21Z

@FloWsnr Sorry I think I missed this comment. I think the larger restructure would be good here, as it will make it easier to see what is related to what structure.

FloWsnr · 2026-06-27T16:42:51Z

@jstoobysmith No problem! I just attempted the restructure. Let me know what you think!

…cs_2 # Conflicts: # Physlib/FluidDynamics/FluidFlow/Momentum.lean

jstoobysmith · 2026-06-28T13:45:21Z


 /-- A smooth continuity equation satisfies the guarded classical continuity equation. -/
-lemma SmoothContinuityEquation.toClassical (d : ℕ) (fluid : FluidState d) :
+lemma SmoothContinuityEquation.toClassical (d : ℕ) (fluid : FluidFlow d) :


this should be called something along the lines classicalContinuityEquation_of_smoothContinuityEquation.

jstoobysmith · 2026-06-28T13:45:58Z

+    ∀ t x, incompressibilityResidual d fluid t x = 0
+
+/-- A smooth incompressible flow is classically incompressible. -/
+lemma SmoothIncompressible.toClassical (d : ℕ) (fluid : FluidFlow d) :


Similar here with the naming.

jstoobysmith · 2026-06-28T13:46:38Z

+
+/-- A fluid flow has time-independent density when the density has zero time derivative at
+each spatial point. -/
+def DensityTimeIndependent (d : ℕ) (fluid : FluidFlow d) : Prop :=
+  ∀ t x, ∂ₜ (fluid.rho · x) t = 0
+
+/-- A fluid flow has time-independent velocity when the velocity has zero time derivative at
+each spatial point. -/
+def VelocityTimeIndependent (d : ℕ) (fluid : FluidFlow d) : Prop :=
+  ∀ t x, ∂ₜ (fluid.velocity · x) t = 0


Not sure how needed these will be, maybe we could just use e.g. ∀ t x, ∂ₜ (fluid.velocity · x) t = 0 explicitly.

jstoobysmith · 2026-06-28T13:47:32Z


 /-- The left-hand side of the conservative momentum equation. -/
-noncomputable def conservativeMomentumLHS (d : ℕ) (fluid : FluidState d) : VectorField d :=
+noncomputable def conservativeMomentumLHS (d : ℕ) (fluid : FluidFlow d) : VectorField d :=


Still not sure about these definitions, if they only appear in a given lemma, then we should write it out explicitly in that lemma or prop.

jstoobysmith · 2026-06-28T13:48:44Z

Would move to the CauchyFlow file.

jstoobysmith · 2026-06-28T13:50:13Z

+-/
+
+/-- The spatial velocity-gradient matrix, with entries `partial_j u_i`. -/
+noncomputable def velocityGradient (d : ℕ) (flow : FluidFlow d) :


This should be in FluidFlow, no need to redefine it here.

jstoobysmith · 2026-06-28T13:50:22Z

+`-p I + mu (grad u + grad u^T) + lambda (div u) I`.
+
+The scalar fields are pressure, shear viscosity, and second viscosity.
+-/


Likewise, should be in FluidFlow

FloWsnr added 4 commits May 26, 2026 15:14

feat(FluidDynamics): add incompressibility predicates

e6e290b

refactor(FluidDynamics): extract shared continuity and momentum

ed9ebc5

feat(FluidDynamics): add Euler Bernoulli setup

c2c135c

feat(FluidDynamics): record Bernoulli force convention

8696eec

jstoobysmith reviewed May 27, 2026

View reviewed changes

refactor(FluidDynamics): inline Euler convective form

2bebbc2

jstoobysmith reviewed May 27, 2026

View reviewed changes

refactor(FluidDynamics): rename Euler predicates

58b969a

jstoobysmith reviewed May 27, 2026

View reviewed changes

FloWsnr added 9 commits May 29, 2026 15:37

refactor(FluidDynamics): introduce Cauchy flow data

d59db4c

refactor(FluidDynamics): rename fluid flow carrier

7b35664

refactor(FluidDynamics): add shared Cauchy momentum

4119cf2

refactor(FluidDynamics): use Cauchy flows in Euler theory

94cd05c

refactor(FluidDynamics): express Navier-Stokes via Cauchy momentum

e0890ac

refactor(FluidDynamics): clarify force and viscosity names

1324844

feat(FluidDynamics): relate inviscid stress to pressure gradient

8f00c5e

refactor(FluidDynamics): move flow time-independence predicates

9b6eb71

refactor(FluidDynamics): namespace flow-derived APIs

1df0fbf

jstoobysmith reviewed Jun 1, 2026

View reviewed changes

FloWsnr added 2 commits June 7, 2026 18:37

refactor(FluidDynamics): address review naming and docs

5ab5fc4

refactor(FluidDynamics): move flow-derived scalar APIs

99098ec

jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Jun 11, 2026

refactor(FluidDynamics): rename flow core module

e5dcd53

jstoobysmith mentioned this pull request Jun 26, 2026

feat(FluidDynamics): add pressure field API #1272

Closed

refactor(FluidDynamics): organize flow APIs by structure

ced67cb

jstoobysmith removed the awaiting-author A reviewer has asked the author a question or requested changes label Jun 27, 2026

Merge remote-tracking branch 'upstream/master' into feat/fluid_dynami…

e151a98

…cs_2 # Conflicts: # Physlib/FluidDynamics/FluidFlow/Momentum.lean

jstoobysmith reviewed Jun 28, 2026

View reviewed changes

jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Jun 28, 2026

Uh oh!

Conversation

FloWsnr commented May 26, 2026

Summary

Changes

Structure

Additions

Notes

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented May 28, 2026

Uh oh!

FloWsnr commented May 28, 2026

Uh oh!

jstoobysmith commented May 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jstoobysmith commented May 28, 2026

Uh oh!

FloWsnr commented May 28, 2026

Uh oh!

jstoobysmith commented May 28, 2026

Uh oh!

FloWsnr commented May 28, 2026

Uh oh!

jstoobysmith commented May 28, 2026

Uh oh!

FloWsnr commented May 28, 2026

Uh oh!

jstoobysmith commented May 28, 2026

Uh oh!

FloWsnr commented May 30, 2026

Main changes

Side changes

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented Jun 10, 2026

Uh oh!

FloWsnr commented Jun 11, 2026

Uh oh!

FloWsnr commented Jun 14, 2026

Uh oh!

jstoobysmith commented Jun 26, 2026

Uh oh!

FloWsnr commented Jun 27, 2026

Uh oh!

jstoobysmith commented May 28, 2026 •

edited

Loading