feat(FluidDynamics): Adding more fluid dynamics - continuation of PR #949 and #1112 ,

[FloWsnr]

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]

should be e.g. euler_iff_convectiveEuler

[FloWsnr]

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

[jstoobysmith]

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]

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

[jstoobysmith]

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

[FloWsnr]

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

[jstoobysmith]

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

[jstoobysmith]

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.

[FloWsnr]

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]

All these should be in the FluidState namespac

[jstoobysmith]

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]

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]

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

[jstoobysmith]

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

[FloWsnr]

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]

How does viscosity come into this all?

[FloWsnr]

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]

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]

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]

Yeah - ok let’s keep names as they are