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]

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

[FloWsnr]

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]

@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]

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

[FloWsnr]

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]

@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]

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

[FloWsnr]

@jstoobysmith Sorry for the long cycles. I applied your comments.

[jstoobysmith]

Would it be possible to include the motivation behind the different data structures within the files:

e.g. for FluidFlow etc. why they have the fields that they do, why is that enough, why are non redundent etc. As well as motivation for why we have split things up into these data structures.

[FloWsnr]

@jstoobysmith Added documentation and removed the LHS stuff

[jstoobysmith]

I think we are getting there :). Would you mind fixing the merge-conflicts.

[jstoobysmith]

Approved - will merge shortly. Thanks for iterating with me on this.