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

Physlib.lean

@@ -74,10 +74,23 @@ public import Physlib.Electromagnetism.ThreeDimension.MaxwellEquations
 public import Physlib.Electromagnetism.Vacuum.Constant
 public import Physlib.Electromagnetism.Vacuum.HarmonicWave
 public import Physlib.Electromagnetism.Vacuum.IsPlaneWave
-public import Physlib.FluidDynamics.FluidState
-public import Physlib.FluidDynamics.NavierStokes.Basic
-public import Physlib.FluidDynamics.NavierStokes.Continuity
-public import Physlib.FluidDynamics.NavierStokes.Momentum
+public import Physlib.FluidDynamics.Basic
+public import Physlib.FluidDynamics.CauchyFlow.Basic
+public import Physlib.FluidDynamics.CauchyFlow.BodyForce
+public import Physlib.FluidDynamics.CauchyFlow.Inviscid
+public import Physlib.FluidDynamics.CauchyFlow.Momentum
+public import Physlib.FluidDynamics.CauchyFlow.NavierStokes
+public import Physlib.FluidDynamics.CauchyFlow.Newtonian
+public import Physlib.FluidDynamics.Euler.Basic
+public import Physlib.FluidDynamics.FluidFlow.Basic
+public import Physlib.FluidDynamics.FluidFlow.Continuity
+public import Physlib.FluidDynamics.FluidFlow.Incompressible
+public import Physlib.FluidDynamics.FluidFlow.Kinematics
+public import Physlib.FluidDynamics.FluidFlow.Momentum
+public import Physlib.FluidDynamics.FluidFlow.Newtonian
+public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Basic
+public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Bernoulli
+public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Isentropic
 public import Physlib.Mathematics.Calculus.AdjFDeriv
 public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.Calculus.ParametricIntegration

Physlib/FluidDynamics/FluidState.lean → Physlib/FluidDynamics/Basic.lean

@@ -9,13 +9,13 @@ public import Physlib.SpaceAndTime.Space.Basic
 public import Physlib.SpaceAndTime.Time.Basic
 /-!
 
-# Fluid states
+# Basic field types for fluid dynamics
 
 ## i. Overview
 
-This module defines the basic fields used to describe a fluid on `d`-dimensional space.
-The core structure `FluidState` contains only the density and velocity fields. Additional
-fields used by specific balance laws are provided by extension structures.
+This module defines the basic field types used to describe a fluid on `d`-dimensional space.
+The structure-specific APIs are organized in the corresponding `FluidFlow`, `CauchyFlow`, and
+`ThermodynamicCauchyFlow` subdirectories.
 
 ## ii. Key results
 
@@ -25,21 +25,20 @@ fields used by specific balance laws are provided by extension structures.
 - `VelocityField` : A time-dependent vector velocity field.
 - `MomentumDensityField` : A time-dependent vector momentum density field.
 - `StressTensor` : A time-dependent matrix-valued stress field.
-- `BodyForce` : A time-dependent vector body-force field per unit mass.
-- `FluidState` : The density and velocity fields of a fluid.
-- `FluidInMomentumBalance` : A fluid state with stress and body force.
 
 ## iii. Table of contents
 
 - A. Field types
-- B. Fluid state structures
 
 ## iv. References
 
 -/
 
 @[expose] public section
 
+open Space
+open Time
+
 namespace FluidDynamics
 
 /-!
@@ -66,27 +65,4 @@ abbrev MomentumDensityField (d : ℕ) := VectorField d
 /-- A matrix-valued stress tensor field on `d`-dimensional space. -/
 abbrev StressTensor (d : ℕ) := Time → Space d → Matrix (Fin d) (Fin d) ℝ
 
-/-- A body-force field per unit mass on `d`-dimensional space. -/
-abbrev BodyForce (d : ℕ) := VectorField d
-
-/-!
-
-## B. Fluid state structures
-
--/
-
-/-- The density and velocity fields of a fluid on `d`-dimensional space. -/
-structure FluidState (d : ℕ) where
-  /-- The mass density field. -/
-  rho : MassDensity d
-  /-- The velocity field. -/
-  velocity : VelocityField d
-
-/-- The fields needed for a momentum balance: fluid state, stress, and body force. -/
-structure FluidInMomentumBalance (d : ℕ) extends FluidState d where
-  /-- The stress tensor field. -/
-  stress : StressTensor d
-  /-- The body-force field per unit mass. -/
-  bodyForce : BodyForce d
-
 end FluidDynamics

Physlib/FluidDynamics/CauchyFlow/Basic.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner
+-/
+module
+
+public import Physlib.FluidDynamics.FluidFlow.Basic
+/-!
+
+# Basic API for Cauchy flows
+
+## i. Overview
+
+This module defines `CauchyFlow`, the momentum-balance layer of the fluid API.
+Specialized predicates and equations for Cauchy flows are organized in sibling modules.
+
+A local Cauchy momentum balance needs two kinds of force data beyond density and velocity. The
+stress tensor encodes contact forces through its divergence, while the specific body force encodes
+volumetric forces per unit mass and therefore contributes mass density times specific body force.
+Together these fields are sufficient to state the balance without choosing a material model.
+
+The momentum equation constrains the flow and forces but does not define a constitutive relation
+between them. Pressure and viscosity are therefore not stored as additional fields.
+They enter through constitutive stress laws, such as the inviscid and Newtonian predicates,
+which avoids duplicating data and imposing consistency conditions inside the carrier.
+Thermodynamic data is deferred to `ThermodynamicCauchyFlow` because it is not needed
+for momentum balance alone.
+
+## ii. Key results
+
+- `CauchyFlow` : A fluid flow with Cauchy stress and specific body force.
+
+## iii. Table of contents
+
+- A. Cauchy-flow structure
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+/-!
+
+## A. Cauchy-flow structure
+
+-/
+
+/-- A fluid flow equipped with Cauchy stress and specific body-force fields.
+
+These are the additional independent fields needed to state a local momentum balance. The Cauchy
+stress represents contact forces, and the specific body force represents volumetric force per unit
+mass. Pressure and viscosity enter through stress laws rather than as redundant fields of
+`CauchyFlow` itself. -/
+structure CauchyFlow (d : ℕ) extends FluidFlow d where
+  /-- The Cauchy stress tensor field. -/
+  stress : StressTensor d
+  /-- The specific body-force field, i.e. force per unit mass. -/
+  specificBodyForce : VectorField d
+
+end FluidDynamics

Physlib/FluidDynamics/CauchyFlow/BodyForce.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner, Michał Mogielnicki
+-/
+module
+
+public import Physlib.FluidDynamics.CauchyFlow.Basic
+public import Physlib.SpaceAndTime.Space.Derivatives.Grad
+/-!
+
+# Body-force predicates for Cauchy flows
+
+## i. Overview
+
+This module defines predicates for conservative specific body forces on `CauchyFlow`.
+
+## ii. Key results
+
+- `CauchyFlow.HasBodyForcePotential` : Predicate encoding the convention
+  `specificBodyForce = -grad Phi`.
+- `CauchyFlow.HasConservativeBodyForce` : Predicate saying the specific body force has some
+  potential.
+
+## iii. Table of contents
+
+- A. Conservative-force convention
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+
+namespace FluidDynamics
+
+namespace CauchyFlow
+
+/-!
+
+## A. Conservative-force convention
+
+-/
+
+/-- A flow has body-force potential `Phi` when its specific body force is minus the gradient of
+`Phi`. -/
+def HasBodyForcePotential (d : ℕ) (flow : CauchyFlow d) (potential : Space d → ℝ) : Prop :=
+  ∀ t x, flow.specificBodyForce t x = -(∇ potential x)
+
+/-- A flow has conservative body force when its specific body force has some potential. -/
+def HasConservativeBodyForce (d : ℕ) (flow : CauchyFlow d) : Prop :=
+  ∃ potential : Space d → ℝ, HasBodyForcePotential d flow potential
+
+end CauchyFlow
+
+end FluidDynamics

Physlib/FluidDynamics/CauchyFlow/Inviscid.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2026 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner, Michał Mogielnicki
+-/
+module
+
+public import Physlib.FluidDynamics.CauchyFlow.Basic
+public import Physlib.SpaceAndTime.Space.Derivatives.MatrixDiv
+/-!
+
+# Inviscid stress laws for Cauchy flows
+
+## i. Overview
+
+This module defines the inviscid stress law for `CauchyFlow` and the corresponding
+matrix-divergence identity for pressure stress.
+
+## ii. Key results
+
+- `CauchyFlow.IsInviscid` : Predicate saying the Cauchy stress is the inviscid pressure stress.
+- `CauchyFlow.matrixDiv_stress_eq_neg_grad_pressure_of_is_inviscid` : The inviscid stress
+  contributes the usual pressure-gradient force term.
+
+## iii. Table of contents
+
+- A. Inviscid stress law
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+
+namespace FluidDynamics
+
+namespace CauchyFlow
+
+/-!
+
+## A. Inviscid stress law
+
+-/
+
+/-- A Cauchy flow is inviscid with pressure `p` when its stress is the isotropic pressure stress
+`-p I`.
+
+In this formulation, inviscid means that the Cauchy stress has no viscous or shear contribution.
+It does not rule out body forces; those are carried separately by `CauchyFlow.specificBodyForce`.
+-/
+def IsInviscid (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d) : Prop :=
+  ∀ t x, flow.stress t x = (-(pressure t x)) • (1 : Matrix (Fin d) (Fin d) ℝ)
+
+/-- The matrix divergence of the inviscid pressure stress `-p I` is `-grad p`. -/
+lemma matrixDiv_inviscid_pressure_stress (d : ℕ) (pressureAtTime : Space d → ℝ) :
+    matrixDiv d (fun x => (-(pressureAtTime x)) • (1 : Matrix (Fin d) (Fin d) ℝ)) =
+      -∇ pressureAtTime := by
+  ext x i
+  rw [matrixDiv_apply]
+  rw [Finset.sum_eq_single i]
+  · simp [grad, Space.deriv_eq]
+  · intro j _ hji
+    have hij : i ≠ j := fun h => hji h.symm
+    simp [hij]
+  · intro hi
+    simp at hi
+
+/-- In an inviscid Cauchy flow, the stress-divergence force is the usual
+negative pressure-gradient term. -/
+theorem matrixDiv_stress_eq_neg_grad_pressure_of_is_inviscid
+    (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d)
+    (hInviscid : IsInviscid d flow pressure) :
+    ∀ t, matrixDiv d (flow.stress t) = -∇ (pressure t) := by
+  intro t
+  rw [show flow.stress t =
+      fun x => (-(pressure t x)) • (1 : Matrix (Fin d) (Fin d) ℝ) by
+    funext x
+    exact hInviscid t x]
+  exact matrixDiv_inviscid_pressure_stress d (pressure t)
+
+end CauchyFlow
+
+end FluidDynamics