diff --git a/Physlib.lean b/Physlib.lean
index cc66b0c10..86371fea3 100644
--- a/Physlib.lean
+++ b/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
diff --git a/Physlib/FluidDynamics/FluidState.lean b/Physlib/FluidDynamics/Basic.lean
similarity index 57%
rename from Physlib/FluidDynamics/FluidState.lean
rename to Physlib/FluidDynamics/Basic.lean
index ffa17c4f2..618b0f3c5 100644
--- a/Physlib/FluidDynamics/FluidState.lean
+++ b/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,14 +25,10 @@ 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
 
@@ -40,6 +36,9 @@ fields used by specific balance laws are provided by extension structures.
 
 @[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
diff --git a/Physlib/FluidDynamics/CauchyFlow/Basic.lean b/Physlib/FluidDynamics/CauchyFlow/Basic.lean
new file mode 100644
index 000000000..96cf572b4
--- /dev/null
+++ b/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
diff --git a/Physlib/FluidDynamics/CauchyFlow/BodyForce.lean b/Physlib/FluidDynamics/CauchyFlow/BodyForce.lean
new file mode 100644
index 000000000..2ae8a5a64
--- /dev/null
+++ b/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
diff --git a/Physlib/FluidDynamics/CauchyFlow/Inviscid.lean b/Physlib/FluidDynamics/CauchyFlow/Inviscid.lean
new file mode 100644
index 000000000..af0547ef0
--- /dev/null
+++ b/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
diff --git a/Physlib/FluidDynamics/CauchyFlow/Momentum.lean b/Physlib/FluidDynamics/CauchyFlow/Momentum.lean
new file mode 100644
index 000000000..1e734f1ae
--- /dev/null
+++ b/Physlib/FluidDynamics/CauchyFlow/Momentum.lean
@@ -0,0 +1,116 @@
+/-
+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.CauchyFlow.Basic
+public import Physlib.FluidDynamics.FluidFlow.Momentum
+/-!
+
+# Cauchy momentum equations
+
+## i. Overview
+
+This module defines the conservative and convective Cauchy momentum equations for a fluid flow
+with stress and specific body-force fields. The stress tensor is left as an input field, so this
+is the balance-law layer before specializing to a constitutive law, such as Euler or
+Navier-Stokes.
+
+## ii. Key results
+
+- `CauchyFlow.CauchyMomentumEquation` : Conservation of momentum using `Space.matrixDiv`.
+- `CauchyFlow.ConvectiveCauchyMomentumEquation` : The Cauchy momentum equation in convective
+  form.
+- `CauchyFlow.cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation` : Equivalence of the
+  two Cauchy momentum equations when continuity holds and the fields are differentiable.
+
+## iii. Table of contents
+
+- A. Cauchy momentum equations
+- B. Equivalence of conservative and convective Cauchy momentum
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+open Time
+
+namespace FluidDynamics
+
+namespace CauchyFlow
+
+/-!
+
+## A. Cauchy momentum equations
+
+-/
+
+/-- Conservation of momentum in conservative matrix-divergence form.
+
+The equation is
+
+`partial_t (rho u) + matrixDiv (rho u ⊗ u) = matrixDiv sigma + rho f`.
+
+Here `stress` is intentionally not yet specialized to a constitutive law.
+-/
+def CauchyMomentumEquation (d : ℕ) (flow : CauchyFlow d) : Prop :=
+  ∀ t x,
+    ∂ₜ (FluidFlow.momentumDensity d flow.toFluidFlow · x) t +
+        matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
+      matrixDiv d (flow.stress t) x + flow.rho t x • flow.specificBodyForce t x
+
+/-- Conservation of momentum in convective form.
+
+The equation is
+
+`rho (partial_t u + (u · ∇)u) = matrixDiv sigma + rho f`.
+
+Here `stress` is intentionally not yet specialized to a constitutive law.
+-/
+def ConvectiveCauchyMomentumEquation (d : ℕ) (flow : CauchyFlow d) : Prop :=
+  ∀ t x,
+    flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x =
+      matrixDiv d (flow.stress t) x + flow.rho t x • flow.specificBodyForce t x
+
+/-!
+
+## B. Equivalence of conservative and convective Cauchy momentum
+
+-/
+
+/-- The conservative and convective Cauchy momentum equations are equivalent when the classical
+continuity equation holds.
+
+The differentiability assumptions are exactly the product-rule assumptions used to rewrite
+`partial_t (rho u)` and `matrixDiv (rho u ⊗ u)`.
+-/
+lemma cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation
+    (d : ℕ) (flow : CauchyFlow d)
+    (hContinuity : FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow)
+    (hRhoTime : ∀ t x, DifferentiableAt ℝ (flow.rho · x) t)
+    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (flow.velocity · x) t)
+    (hMomentumDensity : ∀ t, Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t))
+    (hVelocitySpace : ∀ t, Differentiable ℝ (flow.velocity t)) :
+    CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow := by
+  have conservative_eq_convective_lhs : ∀ t x,
+      ∂ₜ (FluidFlow.momentumDensity d flow.toFluidFlow · x) t +
+          matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =
+        flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x := by
+    intro t x
+    have hResidual : FluidFlow.continuityResidual d flow.toFluidFlow t x = 0 := by
+      simpa [FluidFlow.continuityResidual] using
+        hContinuity t x (by simpa using hRhoTime t x) (hMomentumDensity t).differentiableAt
+    rw [FluidFlow.momentumTransport_eq_materialAcceleration_add_continuityResidual
+        d flow.toFluidFlow t x (hRhoTime t x) (hVelocityTime t x)
+        (hMomentumDensity t) (hVelocitySpace t), hResidual, zero_smul, add_zero]
+  exact ⟨fun h t x => (conservative_eq_convective_lhs t x).symm.trans (h t x),
+    fun h t x => (conservative_eq_convective_lhs t x).trans (h t x)⟩
+
+end CauchyFlow
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/CauchyFlow/NavierStokes.lean b/Physlib/FluidDynamics/CauchyFlow/NavierStokes.lean
new file mode 100644
index 000000000..57150a459
--- /dev/null
+++ b/Physlib/FluidDynamics/CauchyFlow/NavierStokes.lean
@@ -0,0 +1,101 @@
+/-
+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.CauchyFlow.Momentum
+public import Physlib.FluidDynamics.CauchyFlow.Newtonian
+/-!
+
+# The Navier-Stokes equations
+
+## i. Overview
+
+The Navier-Stokes equations are a set of partial differential equations that describe
+the motion of viscous fluid substances. They are fundamental in fluid dynamics and are
+used to model the behavior of fluids in various contexts, including gas flow and water flow.
+
+This file defines the Navier-Stokes equations as continuity, Cauchy momentum, and a Newtonian
+stress law. The Cauchy momentum equation supplies the balance-law layer, while
+`CauchyFlow.IsNewtonian` specializes the stress tensor through pressure and viscosity fields.
+
+## ii. Key results
+
+- `NavierStokes` : Classical continuity, Cauchy momentum, and Newtonian stress together.
+- `ConvectiveNavierStokes` : Classical continuity, convective Cauchy momentum, and Newtonian
+  stress together.
+- `navier_stokes_iff_convective_navier_stokes` : Equivalence of the two forms when the fields
+  are differentiable.
+
+## iii. Table of contents
+
+- A. Navier-Stokes equations
+- B. Equivalence of conservative and convective Navier-Stokes forms
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+/-!
+
+## A. Navier-Stokes equations
+
+-/
+
+/-- The conservative Navier-Stokes equations: continuity, Cauchy momentum, and Newtonian
+stress. -/
+def NavierStokes
+    (d : ℕ) (flow : CauchyFlow d)
+    (pressure shearViscosity secondViscosity : ScalarField d) : Prop :=
+  FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow ∧
+    CauchyFlow.CauchyMomentumEquation d flow ∧
+      CauchyFlow.IsNewtonian d flow pressure shearViscosity secondViscosity
+
+/-- The convective Navier-Stokes equations: continuity, convective Cauchy momentum, and
+Newtonian stress. -/
+def ConvectiveNavierStokes
+    (d : ℕ) (flow : CauchyFlow d)
+    (pressure shearViscosity secondViscosity : ScalarField d) : Prop :=
+  FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow ∧
+    CauchyFlow.ConvectiveCauchyMomentumEquation d flow ∧
+      CauchyFlow.IsNewtonian d flow pressure shearViscosity secondViscosity
+
+/-!
+
+## B. Equivalence of conservative and convective Navier-Stokes forms
+
+-/
+
+/-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
+differentiable enough for the product rules. -/
+theorem navier_stokes_iff_convective_navier_stokes
+    (d : ℕ) (flow : CauchyFlow d)
+    (pressure shearViscosity secondViscosity : ScalarField d)
+    (hRhoTime : ∀ t x, DifferentiableAt ℝ (flow.rho · x) t)
+    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (flow.velocity · x) t)
+    (hMomentumDensity : ∀ t,
+      Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t))
+    (hVelocitySpace : ∀ t, Differentiable ℝ (flow.velocity t)) :
+    NavierStokes d flow pressure shearViscosity secondViscosity ↔
+      ConvectiveNavierStokes d flow pressure shearViscosity secondViscosity := by
+  constructor
+  · intro hConservative
+    refine ⟨hConservative.1, ?_, hConservative.2.2⟩
+    exact
+      (CauchyFlow.cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation d flow
+        hConservative.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp
+          hConservative.2.1
+  · intro hConvective
+    refine ⟨hConvective.1, ?_, hConvective.2.2⟩
+    exact
+      (CauchyFlow.cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation d flow
+        hConvective.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr
+          hConvective.2.1
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/CauchyFlow/Newtonian.lean b/Physlib/FluidDynamics/CauchyFlow/Newtonian.lean
new file mode 100644
index 000000000..73d793e6f
--- /dev/null
+++ b/Physlib/FluidDynamics/CauchyFlow/Newtonian.lean
@@ -0,0 +1,53 @@
+/-
+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.CauchyFlow.Basic
+public import Physlib.FluidDynamics.FluidFlow.Newtonian
+/-!
+
+# Newtonian stress law for Cauchy flows
+
+## i. Overview
+
+This module defines the Newtonian constitutive stress law for `CauchyFlow`.
+
+## ii. Key results
+
+- `CauchyFlow.IsNewtonian` : Predicate saying the Cauchy stress has Newtonian constitutive form.
+
+## iii. Table of contents
+
+- A. Newtonian Cauchy flows
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+namespace CauchyFlow
+
+/-!
+
+## A. Newtonian Cauchy flows
+
+-/
+
+/-- A Cauchy flow is Newtonian when its stress tensor has the Newtonian constitutive form. -/
+def IsNewtonian
+    (d : ℕ) (flow : CauchyFlow d)
+    (pressure shearViscosity secondViscosity : ScalarField d) : Prop :=
+  ∀ t x,
+    flow.stress t x =
+      FluidFlow.newtonianStressTensor d flow.toFluidFlow
+        pressure shearViscosity secondViscosity t x
+
+end CauchyFlow
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/Euler/Basic.lean b/Physlib/FluidDynamics/Euler/Basic.lean
new file mode 100644
index 000000000..93d70b0c9
--- /dev/null
+++ b/Physlib/FluidDynamics/Euler/Basic.lean
@@ -0,0 +1,87 @@
+/-
+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.Inviscid
+public import Physlib.FluidDynamics.CauchyFlow.Momentum
+/-!
+
+# Euler equation for fluid flows
+
+## i. Overview
+
+This module defines the Euler equations for inviscid fluid flow as continuity, Cauchy momentum,
+and an inviscid stress law. The pressure field appears through the constitutive relation for
+the Cauchy stress tensor rather than as a field of the flow data.
+
+## ii. Key results
+
+- `Euler` : Classical continuity, Cauchy momentum, and inviscid stress together.
+- `ConvectiveEuler` : Classical continuity, convective Cauchy momentum, and inviscid stress.
+- `euler_iff_convectiveEuler` : Equivalence of the conservative and convective forms when the
+  fields are differentiable.
+
+## iii. Table of contents
+
+- A. Euler equations
+- B. Equivalence of conservative and convective Euler forms
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+/-!
+
+## A. Euler equations
+
+-/
+
+/-- The conservative Euler equations: continuity, Cauchy momentum, and inviscid stress. -/
+def Euler (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d) : Prop :=
+  FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow ∧
+    CauchyFlow.CauchyMomentumEquation d flow ∧ CauchyFlow.IsInviscid d flow pressure
+
+/-- The convective Euler equations: continuity, convective Cauchy momentum, and inviscid
+stress. -/
+def ConvectiveEuler (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d) : Prop :=
+  FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow ∧
+    CauchyFlow.ConvectiveCauchyMomentumEquation d flow ∧ CauchyFlow.IsInviscid d flow pressure
+
+/-!
+
+## B. Equivalence of conservative and convective Euler forms
+
+-/
+
+/-- The conservative and convective Euler forms are equivalent when the fields are
+differentiable enough for the product rules. -/
+theorem euler_iff_convectiveEuler
+    (d : ℕ) (flow : CauchyFlow d) (pressure : ScalarField d)
+    (hRhoTime : ∀ t x, DifferentiableAt ℝ (flow.rho · x) t)
+    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (flow.velocity · x) t)
+    (hMomentumDensity : ∀ t,
+      Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t))
+    (hVelocitySpace : ∀ t, Differentiable ℝ (flow.velocity t)) :
+    Euler d flow pressure ↔ ConvectiveEuler d flow pressure := by
+  constructor
+  · intro hConservative
+    refine ⟨hConservative.1, ?_, hConservative.2.2⟩
+    exact
+      (CauchyFlow.cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation d flow
+        hConservative.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp
+          hConservative.2.1
+  · intro hConvective
+    refine ⟨hConvective.1, ?_, hConvective.2.2⟩
+    exact
+      (CauchyFlow.cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation d flow
+        hConvective.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr
+          hConvective.2.1
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/FluidFlow/Basic.lean b/Physlib/FluidDynamics/FluidFlow/Basic.lean
new file mode 100644
index 000000000..f96e1e346
--- /dev/null
+++ b/Physlib/FluidDynamics/FluidFlow/Basic.lean
@@ -0,0 +1,63 @@
+/-
+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.Basic
+/-!
+
+# Basic API for fluid flows
+
+## i. Overview
+
+This module defines `FluidFlow`, the kinematic and mass-transport layer of the fluid API.
+
+The fluid API is split according to which physical processes require which data. Density and
+velocity are sufficient at this first layer: they determine the mass flux, momentum density,
+convective momentum flux, and material derivatives used in continuity and kinematic statements.
+
+Stress, body force, and thermodynamic fields are deliberately excluded. Kinematic and
+mass-transport statements do not require them, while adding them here would force those statements
+to depend on unrelated dynamic or constitutive choices. The extension structures add such data
+only at the layer where it becomes necessary.
+
+## ii. Key results
+
+- `FluidFlow` : The density and velocity fields of a fluid.
+
+## iii. Table of contents
+
+- A. Fluid-flow structure
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+/-!
+
+## A. Fluid-flow structure
+
+-/
+
+/-- The density and velocity fields of a fluid on `d`-dimensional space.
+
+These fields are the independent data needed for kinematics and mass transport. Quantities such as
+mass flux, momentum density, and material acceleration are derived from them. Dynamic and
+thermodynamic fields are introduced only by extension structures whose statements need them. -/
+structure FluidFlow (d : ℕ) where
+  /-- The mass density field. -/
+  rho : MassDensity d
+  /-- The velocity field. -/
+  velocity : VelocityField d
+
+namespace FluidFlow
+
+end FluidFlow
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/NavierStokes/Continuity.lean b/Physlib/FluidDynamics/FluidFlow/Continuity.lean
similarity index 64%
rename from Physlib/FluidDynamics/NavierStokes/Continuity.lean
rename to Physlib/FluidDynamics/FluidFlow/Continuity.lean
index 458070d7b..af461afdb 100644
--- a/Physlib/FluidDynamics/NavierStokes/Continuity.lean
+++ b/Physlib/FluidDynamics/FluidFlow/Continuity.lean
@@ -5,24 +5,26 @@ Authors: Florian Wiesner
 -/
 module
 
-public import Physlib.FluidDynamics.FluidState
+public import Physlib.FluidDynamics.FluidFlow.Basic
 public import Physlib.SpaceAndTime.Space.Derivatives.Div
 public import Physlib.SpaceAndTime.Time.Derivatives
 /-!
 
-# The Navier-Stokes continuity equation
+# Continuity equation for fluid flows
 
 ## i. Overview
 
-This module defines the classical conservative mass-balance equation for a fluid state and
-the corresponding continuity residual.
+This module defines the classical conservative mass-balance equation for a fluid flow and the
+corresponding continuity residual. These definitions are independent of a particular momentum
+equation, so they can be reused by Navier-Stokes, Euler, and other fluid models.
 
 ## ii. Key results
 
-- `ClassicalContinuityEquation` : Classical conservation of mass in conservative form.
-- `continuityResidual` : The scalar residual `partial_t rho + div (rho u)`.
-- `SmoothContinuityEquation` : Continuity for globally differentiable fields.
-- `SmoothContinuityEquation.toClassical` : Smooth continuity implies classical continuity.
+- `FluidFlow.ClassicalContinuityEquation` : Classical conservation of mass in conservative form.
+- `FluidFlow.continuityResidual` : The scalar residual `partial_t rho + div (rho u)`.
+- `FluidFlow.SmoothContinuityEquation` : Continuity for globally differentiable fields.
+- `FluidFlow.classicalContinuityEquation_of_smoothContinuityEquation` : A smooth continuity
+  equation implies the classical continuity equation.
 
 ## iii. Table of contents
 
@@ -38,7 +40,8 @@ open Space
 open Time
 
 namespace FluidDynamics
-namespace NavierStokes
+
+namespace FluidFlow
 
 /-!
 
@@ -51,14 +54,14 @@ namespace NavierStokes
 The equation is asserted at points where the time derivative of `rho` and the spatial
 divergence of `rho u` are classical derivatives.
 -/
-def ClassicalContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
+def ClassicalContinuityEquation (d : ℕ) (fluid : FluidFlow d) : Prop :=
   ∀ t x, DifferentiableAt ℝ (fluid.rho · x) t →
       DifferentiableAt ℝ (fun x' => fluid.rho t x' • fluid.velocity t x') x →
         ∂ₜ (fluid.rho · x) t + (∇ ⬝ fun x' => fluid.rho t x' • fluid.velocity t x') x = 0
 
 /-- The scalar continuity-equation residual
 `partial_t rho + div (rho u)`. -/
-noncomputable def continuityResidual (d : ℕ) (fluid : FluidState d) : Time → Space d → ℝ :=
+noncomputable def continuityResidual (d : ℕ) (fluid : FluidFlow d) : Time → Space d → ℝ :=
   fun t x => ∂ₜ (fluid.rho · x) t + (∇ ⬝ fun x' => fluid.rho t x' • fluid.velocity t x') x
 
 /-- A stronger continuity equation for globally differentiable fields.
@@ -67,16 +70,18 @@ This version records the first-order regularity needed by the classical continui
 the density is differentiable in time, the mass flux `rho u` is differentiable in space, and
 the continuity residual vanishes everywhere.
 -/
-def SmoothContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
+def SmoothContinuityEquation (d : ℕ) (fluid : FluidFlow d) : Prop :=
   (∀ x, Differentiable ℝ (fluid.rho · x)) ∧
     (∀ t, Differentiable ℝ (fun x => fluid.rho t x • fluid.velocity t x)) ∧
       ∀ t x, continuityResidual d fluid t x = 0
 
 /-- A smooth continuity equation satisfies the guarded classical continuity equation. -/
-lemma SmoothContinuityEquation.toClassical (d : ℕ) (fluid : FluidState d) :
+lemma classicalContinuityEquation_of_smoothContinuityEquation
+    (d : ℕ) (fluid : FluidFlow d) :
     SmoothContinuityEquation d fluid → ClassicalContinuityEquation d fluid := by
   intro hSmooth t x _ _
   simpa [continuityResidual] using hSmooth.2.2 t x
 
-end NavierStokes
+end FluidFlow
+
 end FluidDynamics
diff --git a/Physlib/FluidDynamics/FluidFlow/Incompressible.lean b/Physlib/FluidDynamics/FluidFlow/Incompressible.lean
new file mode 100644
index 000000000..0a76699b9
--- /dev/null
+++ b/Physlib/FluidDynamics/FluidFlow/Incompressible.lean
@@ -0,0 +1,76 @@
+/-
+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.FluidFlow.Basic
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
+/-!
+
+# Incompressible fluid flows
+
+## i. Overview
+
+This module defines general incompressibility predicates for fluid flows. These predicates are
+not tied to a particular equation of motion, so they can be reused later by incompressible
+Navier-Stokes, incompressible Euler, and Bernoulli-style developments.
+
+## ii. Key results
+
+- `FluidFlow.incompressibilityResidual` : The divergence of the velocity field.
+- `FluidFlow.ClassicalIncompressible` : Incompressibility guarded by velocity differentiability.
+- `FluidFlow.SmoothIncompressible` : Incompressibility with globally differentiable velocity.
+- `FluidFlow.classicalIncompressible_of_smoothIncompressible` : Smooth incompressibility implies
+  classical incompressibility.
+
+## iii. Table of contents
+
+- A. Incompressibility predicates
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+
+namespace FluidDynamics
+
+namespace FluidFlow
+
+/-!
+
+## A. Incompressibility predicates
+
+-/
+
+/-- The incompressibility residual, given by the divergence of the velocity field. -/
+noncomputable def incompressibilityResidual (d : ℕ) (fluid : FluidFlow d) :
+    Time → Space d → ℝ :=
+  fun t x => (∇ ⬝ fluid.velocity t) x
+
+/-- A classical incompressible flow has divergence-free velocity at points where the velocity
+field is differentiable. -/
+def ClassicalIncompressible (d : ℕ) (fluid : FluidFlow d) : Prop :=
+  ∀ t x, DifferentiableAt ℝ (fluid.velocity t) x →
+    incompressibilityResidual d fluid t x = 0
+
+/-- A smooth incompressible flow has globally differentiable velocity and vanishing
+incompressibility residual everywhere. -/
+def SmoothIncompressible (d : ℕ) (fluid : FluidFlow d) : Prop :=
+  (∀ t, Differentiable ℝ (fluid.velocity t)) ∧
+    ∀ t x, incompressibilityResidual d fluid t x = 0
+
+/-- A smooth incompressible flow is classically incompressible. -/
+lemma classicalIncompressible_of_smoothIncompressible
+    (d : ℕ) (fluid : FluidFlow d) :
+    SmoothIncompressible d fluid → ClassicalIncompressible d fluid := by
+  intro hSmooth t x _
+  simpa [incompressibilityResidual] using hSmooth.2 t x
+
+end FluidFlow
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/FluidFlow/Kinematics.lean b/Physlib/FluidDynamics/FluidFlow/Kinematics.lean
new file mode 100644
index 000000000..009b3d082
--- /dev/null
+++ b/Physlib/FluidDynamics/FluidFlow/Kinematics.lean
@@ -0,0 +1,59 @@
+/-
+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
+public import Physlib.SpaceAndTime.Space.Derivatives.Grad
+public import Physlib.SpaceAndTime.Time.Derivatives
+/-!
+
+# Kinematic quantities for fluid flows
+
+## i. Overview
+
+This module defines basic kinematic scalar quantities associated to `FluidFlow`.
+
+## ii. Key results
+
+- `FluidFlow.materialDerivative` : The material derivative along a fluid velocity field.
+- `FluidFlow.specificKineticEnergy` : The specific kinetic energy `|u|^2 / 2`.
+
+## iii. Table of contents
+
+- A. Flow-derived scalar quantities
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open scoped InnerProductSpace
+open Space
+open Time
+
+namespace FluidDynamics
+
+namespace FluidFlow
+
+/-!
+
+## A. Flow-derived scalar quantities
+
+-/
+
+/-- The material derivative `D_t f = partial_t f + u · grad f` of a scalar field. -/
+noncomputable def materialDerivative (d : ℕ) (fluid : FluidFlow d)
+    (field : ScalarField d) : ScalarField d :=
+  fun t x => ∂ₜ (field · x) t + ⟪fluid.velocity t x, ∇ (field t) x⟫_ℝ
+
+/-- The specific kinetic energy `|u|^2 / 2` of a fluid flow. -/
+noncomputable def specificKineticEnergy (d : ℕ) (fluid : FluidFlow d) : ScalarField d :=
+  fun t x => (1 / 2 : ℝ) * ⟪fluid.velocity t x, fluid.velocity t x⟫_ℝ
+
+end FluidFlow
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/FluidFlow/Momentum.lean
similarity index 50%
rename from Physlib/FluidDynamics/NavierStokes/Momentum.lean
rename to Physlib/FluidDynamics/FluidFlow/Momentum.lean
index 40928d4fd..469a3b9fa 100644
--- a/Physlib/FluidDynamics/NavierStokes/Momentum.lean
+++ b/Physlib/FluidDynamics/FluidFlow/Momentum.lean
@@ -5,35 +5,31 @@ Authors: Florian Wiesner
 -/
 module
 
-public import Physlib.FluidDynamics.NavierStokes.Continuity
+public import Physlib.FluidDynamics.FluidFlow.Continuity
 public import Physlib.SpaceAndTime.Space.Derivatives.MatrixDiv
 /-!
 
-# The Navier-Stokes momentum equations
+# Momentum fields for fluid flows
 
 ## i. Overview
 
-This module defines the conservative and convective momentum equations for a fluid with
-stress and body-force fields. The stress tensor is left as an input field, so this is the
-balance-law layer before specializing to a Newtonian stress law.
+This module defines generic momentum fields for fluid flow and relates conservative momentum
+transport to mass density times material acceleration. The definitions do not choose a particular
+force law or stress model, so they can be reused by Navier-Stokes, Euler, and related systems.
 
 ## ii. Key results
 
-- `momentumDensity` : The vector momentum density `rho u`.
-- `momentumFlux` : The convective momentum flux `rho u ⊗ u`.
-- `MomentumEquation` : Conservation of momentum using `Space.matrixDiv`.
-- `convectiveTerm` : The nonlinear transport term `(u · ∇)u`.
-- `materialAcceleration` : The material acceleration `∂ₜ u + (u · ∇)u`.
-- `ConvectiveMomentumEquation` : The momentum equation in convective form.
-- `momentumEquation_iff_convectiveMomentumEquation` : Equivalence of the two
-  momentum equations when continuity holds and the fields are differentiable.
+- `FluidFlow.momentumDensity` : The vector momentum density `rho u`.
+- `FluidFlow.momentumFlux` : The convective momentum flux `rho u ⊗ u`.
+- `FluidFlow.convectiveTerm` : The nonlinear transport term `(u · ∇)u`.
+- `FluidFlow.materialAcceleration` : The material acceleration `∂ₜ u + (u · ∇)u`.
+- `FluidFlow.momentumTransport_eq_materialAcceleration_add_continuityResidual` :
+  The momentum-transport identity relating conservative and convective quantities.
 
 ## iii. Table of contents
 
 - A. Momentum fields
-- B. Conservative momentum equation
-- C. Convective momentum equation
-- D. Equivalence of conservative and convective momentum
+- B. Momentum transport identity
 
 ## iv. References
 
@@ -45,7 +41,8 @@ open Space
 open Time
 
 namespace FluidDynamics
-namespace NavierStokes
+
+namespace FluidFlow
 
 /-!
 
@@ -54,76 +51,29 @@ namespace NavierStokes
 -/
 
 /-- The momentum density `rho u`. -/
-def momentumDensity (d : ℕ) (fluid : FluidState d) : MomentumDensityField d :=
+def momentumDensity (d : ℕ) (fluid : FluidFlow d) : MomentumDensityField d :=
   fun t x => fluid.rho t x • fluid.velocity t x
 
 /-- The convective momentum flux `rho u ⊗ u`. -/
-def momentumFlux (d : ℕ) (fluid : FluidState d) : Time → Space d → Matrix (Fin d) (Fin d) ℝ :=
+def momentumFlux (d : ℕ) (fluid : FluidFlow d) : Time → Space d → Matrix (Fin d) (Fin d) ℝ :=
   fun t x =>
     fluid.rho t x • Matrix.vecMulVec (fun i => fluid.velocity t x i)
       (fun j => fluid.velocity t x j)
 
-/-!
-
-## B. Conservative momentum equation
-
--/
-
-/-- Conservation of momentum in conservative matrix-divergence form.
-
-The equation is
-
-`partial_t (rho u) + matrixDiv (rho u ⊗ u) = matrixDiv sigma + rho f`.
-
-Here `stress` is intentionally not yet specialized to a Newtonian stress law.
--/
-def MomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
-  ∀ t x,
-    ∂ₜ (momentumDensity d data.toFluidState · x) t +
-        matrixDiv d (momentumFlux d data.toFluidState t) x =
-      matrixDiv d (data.stress t) x + data.rho t x • data.bodyForce t x
-
-/-!
-
-## C. Convective momentum equation
-
--/
-
 /-- The nonlinear transport term `(u · ∇)u`. -/
-noncomputable def convectiveTerm (d : ℕ) (fluid : FluidState d) : VectorField d :=
+noncomputable def convectiveTerm (d : ℕ) (fluid : FluidFlow d) : VectorField d :=
   fun t x => ∑ j, fluid.velocity t x j • ∂[j] (fluid.velocity t) x
 
 /-- The material acceleration `∂ₜ u + (u · ∇)u`. -/
-noncomputable def materialAcceleration (d : ℕ) (fluid : FluidState d) : VectorField d :=
+noncomputable def materialAcceleration (d : ℕ) (fluid : FluidFlow d) : VectorField d :=
   fun t x => ∂ₜ (fluid.velocity · x) t + convectiveTerm d fluid t x
 
-/-- Conservation of momentum in convective form.
-
-The equation is
-
-`rho (partial_t u + (u · ∇)u) = matrixDiv sigma + rho f`.
-
-Here `stress` is intentionally not yet specialized to a Newtonian stress law.
--/
-def ConvectiveMomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
-  ∀ t x,
-    data.rho t x • materialAcceleration d data.toFluidState t x =
-      matrixDiv d (data.stress t) x + data.rho t x • data.bodyForce t x
-
 /-!
 
-## D. Equivalence of conservative and convective momentum
+## B. Momentum transport identity
 
 -/
 
-/-- The left-hand side of the conservative momentum equation. -/
-noncomputable def conservativeMomentumLHS (d : ℕ) (fluid : FluidState d) : VectorField d :=
-  fun t x => ∂ₜ (momentumDensity d fluid · x) t + matrixDiv d (momentumFlux d fluid t) x
-
-/-- The left-hand side of the convective momentum equation. -/
-noncomputable def convectiveMomentumLHS (d : ℕ) (fluid : FluidState d) : VectorField d :=
-  fun t x => fluid.rho t x • materialAcceleration d fluid t x
-
 /-- Product rule for the time derivative of a scalar field times a velocity field. -/
 lemma timeDeriv_smul_velocity (d : ℕ) (rhoAtPosition : Time → ℝ)
     (velocityAtPosition : Time → EuclideanSpace ℝ (Fin d)) (t : Time)
@@ -139,7 +89,7 @@ lemma timeDeriv_smul_velocity (d : ℕ) (rhoAtPosition : Time → ℝ)
   rfl
 
 /-- Product rule for the time derivative of the momentum density `rho u`. -/
-lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidState d)
+lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidFlow d)
     (t : Time) (x : Space d)
     (hRho : DifferentiableAt ℝ (fluid.rho · x) t)
     (hVelocity : DifferentiableAt ℝ (fluid.velocity · x) t) :
@@ -149,24 +99,25 @@ lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidState d)
     timeDeriv_smul_velocity d (fluid.rho · x) (fluid.velocity · x) t hRho hVelocity
 
 /-- Product rule for one spatial derivative of one component of `rho u ⊗ u`. -/
-lemma spaceDeriv_momentumFlux_component (d : ℕ) (fluid : FluidState d)
+lemma spaceDeriv_momentumFlux_component (d : ℕ) (fluid : FluidFlow d)
     (t : Time) (x : Space d) (i j : Fin d)
     (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid t))
     (hVelocity : Differentiable ℝ (fluid.velocity t)) :
     ∂[j] (fun x' => momentumFlux d fluid t x' i j) x =
       fluid.velocity t x i • ∂[j] (fun x' => momentumDensity d fluid t x' j) x +
       ∂[j] (fun x' => fluid.velocity t x' i) x • momentumDensity d fluid t x j := by
-  rw [← Space.deriv_smul (u := j) (x := x)
+  have hProduct := Space.deriv_smul (u := j) (x := x)
     (c := fun x' => fluid.velocity t x' i)
     (f := fun x' => momentumDensity d fluid t x' j)
     ((differentiable_euclidean.mp hVelocity i).differentiableAt)
-    ((differentiable_euclidean.mp hMomentumDensity j).differentiableAt)]
+    ((differentiable_euclidean.mp hMomentumDensity j).differentiableAt)
+  rw [← hProduct]
   congr
   funext x'
   simp [momentumFlux, momentumDensity, Matrix.vecMulVec_apply, mul_left_comm]
 
 /-- The matrix divergence of `rho u ⊗ u` split into continuity and convective parts. -/
-lemma matrixDiv_momentumFlux (d : ℕ) (fluid : FluidState d)
+lemma matrixDiv_momentumFlux (d : ℕ) (fluid : FluidFlow d)
     (t : Time) (x : Space d)
     (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid t))
     (hVelocity : Differentiable ℝ (fluid.velocity t)) :
@@ -203,53 +154,26 @@ lemma matrixDiv_momentumFlux (d : ℕ) (fluid : FluidState d)
         fluid.rho t x * (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i) := by
           ring
 
-/-- The algebraic bridge between conservative and convective momentum.
-
-The conservative momentum left-hand side equals the convective momentum left-hand side plus
-the continuity residual times the velocity field.
+/-- The conservative momentum transport terms equal mass density times material acceleration plus
+the continuity residual times velocity.
 -/
-lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-    (d : ℕ) (fluid : FluidState d)
+lemma momentumTransport_eq_materialAcceleration_add_continuityResidual
+    (d : ℕ) (fluid : FluidFlow d)
     (t : Time) (x : Space d)
     (hRhoTime : DifferentiableAt ℝ (fluid.rho · x) t)
     (hVelocityTime : DifferentiableAt ℝ (fluid.velocity · x) t)
     (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid t))
     (hVelocitySpace : Differentiable ℝ (fluid.velocity t)) :
-    conservativeMomentumLHS d fluid t x =
-      convectiveMomentumLHS d fluid t x + continuityResidual d fluid t x • fluid.velocity t x := by
-  rw [conservativeMomentumLHS, convectiveMomentumLHS, continuityResidual,
-    timeDeriv_momentumDensity d fluid t x hRhoTime hVelocityTime,
-    matrixDiv_momentumFlux d fluid t x hMomentumDensity hVelocitySpace]
+    ∂ₜ (momentumDensity d fluid · x) t + matrixDiv d (momentumFlux d fluid t) x =
+      fluid.rho t x • materialAcceleration d fluid t x +
+        continuityResidual d fluid t x • fluid.velocity t x := by
+  rw [continuityResidual]
+  rw [timeDeriv_momentumDensity d fluid t x hRhoTime hVelocityTime]
+  rw [matrixDiv_momentumFlux d fluid t x hMomentumDensity hVelocitySpace]
   ext i
   simp [materialAcceleration, convectiveTerm, div, momentumDensity, smul_eq_mul]
   ring_nf
 
-/-- The conservative and convective momentum equations are equivalent when the classical
-continuity equation holds.
+end FluidFlow
 
-The differentiability assumptions are exactly the product-rule assumptions used to rewrite
-`partial_t (rho u)` and `matrixDiv (rho u ⊗ u)`.
--/
-theorem momentumEquation_iff_convectiveMomentumEquation
-    (d : ℕ) (data : FluidInMomentumBalance d)
-    (hContinuity : ClassicalContinuityEquation d data.toFluidState)
-    (hRhoTime : ∀ t x, DifferentiableAt ℝ (data.rho · x) t)
-    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (data.velocity · x) t)
-    (hMomentumDensity : ∀ t,
-      Differentiable ℝ (momentumDensity d data.toFluidState t))
-    (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
-    MomentumEquation d data ↔ ConvectiveMomentumEquation d data := by
-  have conservative_eq_convective_lhs : ∀ t x, conservativeMomentumLHS d data.toFluidState t x =
-      convectiveMomentumLHS d data.toFluidState t x := by
-    intro t x
-    have hResidual : continuityResidual d data.toFluidState t x = 0 := by
-      simpa [continuityResidual] using
-        hContinuity t x (by simpa using hRhoTime t x) (hMomentumDensity t).differentiableAt
-    rw [conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-        d data.toFluidState t x (hRhoTime t x) (hVelocityTime t x)
-        (hMomentumDensity t) (hVelocitySpace t), hResidual, zero_smul, add_zero]
-  exact ⟨fun h t x => (conservative_eq_convective_lhs t x).symm.trans (h t x),
-    fun h t x => (conservative_eq_convective_lhs t x).trans (h t x)⟩
-
-end NavierStokes
 end FluidDynamics
diff --git a/Physlib/FluidDynamics/FluidFlow/Newtonian.lean b/Physlib/FluidDynamics/FluidFlow/Newtonian.lean
new file mode 100644
index 000000000..c34033acd
--- /dev/null
+++ b/Physlib/FluidDynamics/FluidFlow/Newtonian.lean
@@ -0,0 +1,68 @@
+/-
+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
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
+/-!
+
+# Newtonian stress tensors for fluid flows
+
+## i. Overview
+
+This module defines the velocity gradient and Newtonian stress tensor associated to a
+`FluidFlow`.
+
+## ii. Key results
+
+- `FluidFlow.velocityGradient` : The spatial velocity-gradient matrix.
+- `FluidFlow.newtonianStressTensor` : The Newtonian stress tensor determined by pressure and
+  viscosity.
+
+## iii. Table of contents
+
+- A. Newtonian stress tensor
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+
+namespace FluidDynamics
+
+namespace FluidFlow
+
+/-!
+
+## A. Newtonian stress tensor
+
+-/
+
+/-- The spatial velocity-gradient matrix, with entries `partial_j u_i`. -/
+noncomputable def velocityGradient (d : ℕ) (flow : FluidFlow d) :
+    Time → Space d → Matrix (Fin d) (Fin d) ℝ :=
+  fun t x i j => ∂[j] (fun x' => flow.velocity t x' i) x
+
+/-- The Newtonian stress tensor
+`-p I + mu (grad u + grad u^T) + lambda (div u) I`.
+
+The scalar fields are pressure, shear viscosity, and second viscosity.
+-/
+noncomputable def newtonianStressTensor (d : ℕ) (flow : FluidFlow d)
+    (pressure shearViscosity secondViscosity : ScalarField d) : StressTensor d :=
+  fun t x =>
+    (-(pressure t x)) • (1 : Matrix (Fin d) (Fin d) ℝ) +
+      shearViscosity t x •
+        (velocityGradient d flow t x + Matrix.transpose (velocityGradient d flow t x)) +
+        (secondViscosity t x * (∇ ⬝ flow.velocity t) x) •
+          (1 : Matrix (Fin d) (Fin d) ℝ)
+
+end FluidFlow
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
deleted file mode 100644
index c402c44dd..000000000
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ /dev/null
@@ -1,72 +0,0 @@
-/-
-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.NavierStokes.Momentum
-/-!
-
-# The Navier-Stokes equations
-
-## i. Overview
-
-The Navier-Stokes equations are a set of partial differential equations that describe
-the motion of viscous fluid substances. They are fundamental in fluid dynamics and are
-used to model the behavior of fluids in various contexts, including gas flow and water flow.
-
-This file combines the classical continuity equation with the momentum equation. The stress
-tensor is left as an input field, so this is the balance-law layer before specializing to a
-Newtonian stress law.
-
-## ii. Key results
-
-- `NavierStokes` : Classical continuity and conservative momentum equations together.
-- `ConvectiveNavierStokes` : Classical continuity and convective momentum equations together.
-- `NavierStokes_iff_ConvectiveNavierStokes` : Equivalence of the two forms when the
-  fields are differentiable.
-
-## iii. Table of contents
-
-- A. Full Navier-Stokes forms
-
-## iv. References
-
--/
-
-@[expose] public section
-
-namespace FluidDynamics
-
-/-!
-
-## A. Full Navier-Stokes forms
-
--/
-
-/-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
-def NavierStokes (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
-  FluidDynamics.NavierStokes.ClassicalContinuityEquation d data.toFluidState ∧
-    FluidDynamics.NavierStokes.MomentumEquation d data
-
-/-- The convective Navier-Stokes form with an externally supplied stress tensor. -/
-def ConvectiveNavierStokes (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
-  FluidDynamics.NavierStokes.ClassicalContinuityEquation d data.toFluidState ∧
-    FluidDynamics.NavierStokes.ConvectiveMomentumEquation d data
-
-/-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
-differentiable enough for the product rules. -/
-theorem navierStokes_iff_convectiveNavierStokes
-    (d : ℕ) (data : FluidInMomentumBalance d)
-    (hRhoTime : ∀ t x, DifferentiableAt ℝ (data.rho · x) t)
-    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (data.velocity · x) t)
-    (hMomentumDensity : ∀ t,
-      Differentiable ℝ (FluidDynamics.NavierStokes.momentumDensity d data.toFluidState t))
-    (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
-    NavierStokes d data ↔ ConvectiveNavierStokes d data :=
-  and_congr_right fun h =>
-    FluidDynamics.NavierStokes.momentumEquation_iff_convectiveMomentumEquation d data h
-      hRhoTime hVelocityTime hMomentumDensity hVelocitySpace
-
-end FluidDynamics
diff --git a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Basic.lean b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Basic.lean
new file mode 100644
index 000000000..b63bc4596
--- /dev/null
+++ b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Basic.lean
@@ -0,0 +1,61 @@
+/-
+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.CauchyFlow.Basic
+/-!
+
+# Basic predicates for thermodynamic Cauchy flows
+
+## i. Overview
+
+This module defines `ThermodynamicCauchyFlow`, the thermodynamic layer currently needed for
+isentropic and Bernoulli-type statements.
+
+This structure is intentionally the minimal carrier for the present thermodynamic API, not a claim
+that entropy and enthalpy describe every thermodynamic process. Temperature, heat flux, and other
+state data should be introduced by a further extension when an energy or heat-transport law needs
+them. Keeping those fields out here lets Bernoulli and isentropic results avoid assumptions
+unrelated to their statements.
+
+## ii. Key results
+
+- `ThermodynamicCauchyFlow` : A Cauchy flow with entropy and enthalpy fields.
+
+## iii. Table of contents
+
+- A. Thermodynamic Cauchy-flow structure
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+/-!
+
+## A. Thermodynamic Cauchy-flow structure
+
+-/
+
+/-- A Cauchy flow equipped with thermodynamic entropy and enthalpy fields.
+
+These fields are independent of the kinematic and momentum-balance data unless additional
+thermodynamic constitutive laws are imposed. They are sufficient for the current isentropic and
+Bernoulli APIs; other thermodynamic fields belong in later extensions that require them. -/
+structure ThermodynamicCauchyFlow (d : ℕ) extends CauchyFlow d where
+  /-- The specific entropy field. -/
+  entropy : ScalarField d
+  /-- The specific enthalpy field. -/
+  enthalpy : ScalarField d
+
+namespace ThermodynamicCauchyFlow
+
+end ThermodynamicCauchyFlow
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean
new file mode 100644
index 000000000..4ee5bcc26
--- /dev/null
+++ b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean
@@ -0,0 +1,70 @@
+/-
+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.BodyForce
+public import Physlib.FluidDynamics.FluidFlow.Kinematics
+public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Basic
+/-!
+
+# Bernoulli theory for thermodynamic Cauchy flows
+
+## i. Overview
+
+This module is reserved for Bernoulli definitions and results based on the shared
+`ThermodynamicCauchyFlow` data together with an explicit external potential parameter, rather
+than defining a separate Bernoulli-flow structure.
+
+## ii. Key results
+
+- `bernoulliFunction` : The Bernoulli function `|u|^2 / 2 + h + Phi`.
+- `LocalBernoulliLaw` : Vanishing spatial gradient of the Bernoulli function.
+- `BernoulliLaw` : Spatial constancy of the Bernoulli function at each time.
+
+## iii. Table of contents
+
+- A. Bernoulli function
+- B. Bernoulli-law predicates
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+
+namespace FluidDynamics
+
+/-!
+
+## A. Bernoulli function
+
+-/
+
+/-- The Bernoulli function `|u|^2 / 2 + h + Phi`. -/
+noncomputable def bernoulliFunction
+    (d : ℕ) (flow : ThermodynamicCauchyFlow d) (potential : Space d → ℝ) : ScalarField d :=
+  fun t x => FluidFlow.specificKineticEnergy d flow.toFluidFlow t x + flow.enthalpy t x +
+    potential x
+
+/-!
+
+## B. Bernoulli-law predicates
+
+-/
+
+/-- A local Bernoulli law: the Bernoulli function has zero spatial gradient. -/
+def LocalBernoulliLaw
+    (d : ℕ) (flow : ThermodynamicCauchyFlow d) (potential : Space d → ℝ) : Prop :=
+  ∀ t x, (∇ (bernoulliFunction d flow potential t)) x = 0
+
+/-- A global Bernoulli law: the Bernoulli function is spatially constant at each time. -/
+def BernoulliLaw
+    (d : ℕ) (flow : ThermodynamicCauchyFlow d) (potential : Space d → ℝ) : Prop :=
+  ∀ t x y, bernoulliFunction d flow potential t x = bernoulliFunction d flow potential t y
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Isentropic.lean b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Isentropic.lean
new file mode 100644
index 000000000..0d371c7e9
--- /dev/null
+++ b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Isentropic.lean
@@ -0,0 +1,50 @@
+/-
+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.Kinematics
+public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Basic
+/-!
+
+# Isentropic thermodynamic Cauchy flows
+
+## i. Overview
+
+This module defines the isentropic predicate for thermodynamic Cauchy flows.
+
+## ii. Key results
+
+- `ThermodynamicCauchyFlow.IsIsentropic` : A thermodynamic Cauchy flow whose entropy is
+  materially conserved.
+
+## iii. Table of contents
+
+- A. Thermodynamic-flow predicates
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace FluidDynamics
+
+namespace ThermodynamicCauchyFlow
+
+/-!
+
+## A. Thermodynamic-flow predicates
+
+-/
+
+/-- A thermodynamic flow is isentropic when the entropy is materially conserved along the
+underlying fluid velocity field. -/
+def IsIsentropic (d : ℕ) (flow : ThermodynamicCauchyFlow d) : Prop :=
+  ∀ t x, FluidFlow.materialDerivative d flow.toFluidFlow flow.entropy t x = 0
+
+end ThermodynamicCauchyFlow
+
+end FluidDynamics