diff --git a/Physlib.lean b/Physlib.lean
index a3e75b400..b11d09a80 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -60,10 +60,14 @@ 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.Basic
+public import Physlib.FluidDynamics.CauchyMomentum
+public import Physlib.FluidDynamics.Continuity
+public import Physlib.FluidDynamics.Euler.Basic
+public import Physlib.FluidDynamics.Euler.Bernoulli
+public import Physlib.FluidDynamics.Incompressible
+public import Physlib.FluidDynamics.Momentum
 public import Physlib.FluidDynamics.NavierStokes.Basic
-public import Physlib.FluidDynamics.NavierStokes.Continuity
-public import Physlib.FluidDynamics.NavierStokes.Momentum
 public import Physlib.Mathematics.Calculus.AdjFDeriv
 public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
diff --git a/Physlib/FluidDynamics/Basic.lean b/Physlib/FluidDynamics/Basic.lean
new file mode 100644
index 000000000..d927ba6a9
--- /dev/null
+++ b/Physlib/FluidDynamics/Basic.lean
@@ -0,0 +1,178 @@
+/-
+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.SpaceAndTime.Space.Derivatives.Grad
+public import Physlib.SpaceAndTime.Time.Derivatives
+/-!
+
+# Fluid flows
+
+## i. Overview
+
+This module defines the basic fields used to describe a fluid on `d`-dimensional space.
+The core structure `FluidFlow` contains only the density and velocity fields, so it is the
+minimal data needed for kinematic and mass-transport constructions such as continuity,
+incompressibility, momentum density, and material derivatives. The structure `CauchyFlow`
+adds Cauchy stress and specific body-force fields, the extra data used for momentum balances.
+The structure `ThermodynamicCauchyFlow` adds entropy and enthalpy fields for thermodynamic
+laws such as Bernoulli-type statements.
+
+## ii. Key results
+
+- `ScalarField` : A time-dependent scalar field on space.
+- `VectorField` : A time-dependent vector field on space.
+- `MassDensity` : A time-dependent scalar density field.
+- `VelocityField` : A time-dependent vector velocity field.
+- `MomentumDensityField` : A time-dependent vector momentum density field.
+- `StressTensor` : A time-dependent matrix-valued stress field.
+- `FluidFlow` : The density and velocity fields of a fluid.
+- `CauchyFlow` : A fluid flow with Cauchy stress and specific body force.
+- `ThermodynamicCauchyFlow` : A Cauchy flow with entropy and enthalpy fields.
+- `FluidFlow.DensityTimeIndependent` : A fluid flow whose density has zero time derivative.
+- `FluidFlow.VelocityTimeIndependent` : A fluid flow whose velocity has zero time derivative.
+- `FluidFlow.materialDerivative` : The material derivative along a fluid velocity field.
+- `FluidFlow.specificKineticEnergy` : The specific kinetic energy `|u|^2 / 2`.
+- `ThermodynamicCauchyFlow.IsIsentropic` : A thermodynamic Cauchy flow whose entropy is
+  materially conserved.
+
+## iii. Table of contents
+
+- A. Field types
+- B. Fluid flow structures
+- C. Time-independence predicates
+- D. Flow-derived scalar quantities
+- E. Thermodynamic-flow predicates
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open scoped InnerProductSpace
+open Space
+open Time
+
+namespace FluidDynamics
+
+/-!
+
+## A. Field types
+
+-/
+
+/-- A scalar field on `d`-dimensional space, depending on time. -/
+abbrev ScalarField (d : ℕ) := Time → Space d → ℝ
+
+/-- A vector field on `d`-dimensional space, depending on time. -/
+abbrev VectorField (d : ℕ) := Time → Space d → EuclideanSpace ℝ (Fin d)
+
+/-- A mass density field on `d`-dimensional space. -/
+abbrev MassDensity (d : ℕ) := ScalarField d
+
+/-- A velocity field on `d`-dimensional space. -/
+abbrev VelocityField (d : ℕ) := VectorField d
+
+/-- A momentum density field on `d`-dimensional space. -/
+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) ℝ
+
+/-!
+
+## B. Fluid flow structures
+
+-/
+
+/-- The density and velocity fields of a fluid on `d`-dimensional space.
+
+This is the kinematic/mass-transport layer of the fluid API. It intentionally contains no
+stress, body force, or thermodynamic fields. Those are introduced only by the extension
+structures that need them. -/
+structure FluidFlow (d : ℕ) where
+  /-- The mass density field. -/
+  rho : MassDensity d
+  /-- The velocity field. -/
+  velocity : VelocityField d
+
+/-- A fluid flow equipped with Cauchy stress and specific body-force fields.
+
+This is the momentum-balance layer of the fluid API. The Cauchy stress is the primitive
+dynamic field; pressure and viscosity enter through stress laws rather than as 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
+
+/-- A Cauchy flow equipped with thermodynamic entropy and enthalpy fields.
+
+This extends the kinematic and momentum-balance data with thermodynamic fields used by
+isentropic and Bernoulli-type laws. -/
+structure ThermodynamicCauchyFlow (d : ℕ) extends CauchyFlow d where
+  /-- The specific entropy field. -/
+  entropy : ScalarField d
+  /-- The specific enthalpy field. -/
+  enthalpy : ScalarField d
+
+/-!
+
+## C. Time-independence predicates
+
+-/
+
+namespace FluidFlow
+
+/-- 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
+
+end FluidFlow
+
+/-!
+
+## D. Flow-derived scalar quantities
+
+-/
+
+namespace FluidFlow
+
+/-- 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
+
+/-!
+
+## E. Thermodynamic-flow predicates
+
+-/
+
+namespace ThermodynamicCauchyFlow
+
+/-- 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
diff --git a/Physlib/FluidDynamics/CauchyMomentum.lean b/Physlib/FluidDynamics/CauchyMomentum.lean
new file mode 100644
index 000000000..90ac28caa
--- /dev/null
+++ b/Physlib/FluidDynamics/CauchyMomentum.lean
@@ -0,0 +1,139 @@
+/-
+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.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
+
+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.conservativeMomentumLHS 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)`.
+-/
+theorem 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
+  constructor
+  · intro hConservative t x
+    have hMassFluxSpace :
+        DifferentiableAt ℝ (fun x' => flow.rho t x' • flow.velocity t x') x := by
+      simpa [FluidFlow.momentumDensity] using (hMomentumDensity t).differentiableAt
+    have hResidual : FluidFlow.continuityResidual d flow.toFluidFlow t x = 0 := by
+      simpa [FluidFlow.continuityResidual] using
+        hContinuity t x (by simpa using hRhoTime t x) hMassFluxSpace
+    have hLhs :=
+      FluidFlow.conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+        d flow.toFluidFlow t x (hRhoTime t x) (hVelocityTime t x)
+        (hMomentumDensity t) (hVelocitySpace t)
+    have hLhs' :
+        FluidFlow.conservativeMomentumLHS d flow.toFluidFlow t x =
+          FluidFlow.convectiveMomentumLHS d flow.toFluidFlow t x := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    change FluidFlow.convectiveMomentumLHS d flow.toFluidFlow t x =
+      matrixDiv d (flow.stress t) x + flow.rho t x • flow.specificBodyForce t x
+    rw [← hLhs']
+    exact hConservative t x
+  · intro hConvective t x
+    have hMassFluxSpace :
+        DifferentiableAt ℝ (fun x' => flow.rho t x' • flow.velocity t x') x := by
+      simpa [FluidFlow.momentumDensity] using (hMomentumDensity t).differentiableAt
+    have hResidual : FluidFlow.continuityResidual d flow.toFluidFlow t x = 0 := by
+      simpa [FluidFlow.continuityResidual] using
+        hContinuity t x (by simpa using hRhoTime t x) hMassFluxSpace
+    have hLhs :=
+      FluidFlow.conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+        d flow.toFluidFlow t x (hRhoTime t x) (hVelocityTime t x)
+        (hMomentumDensity t) (hVelocitySpace t)
+    have hLhs' :
+        FluidFlow.conservativeMomentumLHS d flow.toFluidFlow t x =
+          FluidFlow.convectiveMomentumLHS d flow.toFluidFlow t x := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    change FluidFlow.conservativeMomentumLHS d flow.toFluidFlow t x =
+      matrixDiv d (flow.stress t) x + flow.rho t x • flow.specificBodyForce t x
+    rw [hLhs']
+    exact hConvective t x
+
+end CauchyFlow
+
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/NavierStokes/Continuity.lean b/Physlib/FluidDynamics/Continuity.lean
similarity index 68%
rename from Physlib/FluidDynamics/NavierStokes/Continuity.lean
rename to Physlib/FluidDynamics/Continuity.lean
index 458070d7b..8ee3a538e 100644
--- a/Physlib/FluidDynamics/NavierStokes/Continuity.lean
+++ b/Physlib/FluidDynamics/Continuity.lean
@@ -5,24 +5,26 @@ Authors: Florian Wiesner
 -/
 module
 
-public import Physlib.FluidDynamics.FluidState
+public import Physlib.FluidDynamics.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.SmoothContinuityEquation.toClassical` : Smooth continuity implies classical
+  continuity.
 
 ## 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,17 @@ 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 SmoothContinuityEquation.toClassical (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/Euler/Basic.lean b/Physlib/FluidDynamics/Euler/Basic.lean
new file mode 100644
index 000000000..5da65a05b
--- /dev/null
+++ b/Physlib/FluidDynamics/Euler/Basic.lean
@@ -0,0 +1,139 @@
+/-
+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.CauchyMomentum
+public import Physlib.SpaceAndTime.Space.Derivatives.Grad
+/-!
+
+# 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
+
+- `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.
+- `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. Inviscid stress law
+- B. Euler equations
+- C. Equivalence of conservative and convective Euler forms
+
+## 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
+
+/-!
+
+## B. 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
+
+/-!
+
+## C. 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/Euler/Bernoulli.lean b/Physlib/FluidDynamics/Euler/Bernoulli.lean
new file mode 100644
index 000000000..b7c47cf6e
--- /dev/null
+++ b/Physlib/FluidDynamics/Euler/Bernoulli.lean
@@ -0,0 +1,88 @@
+/-
+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.Euler.Basic
+public import Physlib.SpaceAndTime.Space.Derivatives.Grad
+/-!
+
+# Bernoulli theory for Euler flows
+
+## i. Overview
+
+This module is reserved for Bernoulli definitions and results derived from Euler-flow
+assumptions. The intended development uses the shared `ThermodynamicCauchyFlow` data together
+with an explicit external potential parameter, rather than defining a separate Bernoulli-flow
+structure.
+
+## ii. Key results
+
+- `HasBodyForcePotential` : Predicate encoding the convention `specificBodyForce = -grad Phi`.
+- `HasConservativeBodyForce` : Predicate saying a specific body force has some potential.
+- `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. Conservative-force convention
+- B. Bernoulli function
+- C. Bernoulli-law predicates
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+
+namespace FluidDynamics
+
+/-!
+
+## 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
+
+/-!
+
+## B. 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
+
+/-!
+
+## C. 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/FluidState.lean b/Physlib/FluidDynamics/FluidState.lean
deleted file mode 100644
index ffa17c4f2..000000000
--- a/Physlib/FluidDynamics/FluidState.lean
+++ /dev/null
@@ -1,92 +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.SpaceAndTime.Space.Basic
-public import Physlib.SpaceAndTime.Time.Basic
-/-!
-
-# Fluid states
-
-## 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.
-
-## ii. Key results
-
-- `ScalarField` : A time-dependent scalar field on space.
-- `VectorField` : A time-dependent vector field on space.
-- `MassDensity` : A time-dependent scalar density field.
-- `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
-
-namespace FluidDynamics
-
-/-!
-
-## A. Field types
-
--/
-
-/-- A scalar field on `d`-dimensional space, depending on time. -/
-abbrev ScalarField (d : ℕ) := Time → Space d → ℝ
-
-/-- A vector field on `d`-dimensional space, depending on time. -/
-abbrev VectorField (d : ℕ) := Time → Space d → EuclideanSpace ℝ (Fin d)
-
-/-- A mass density field on `d`-dimensional space. -/
-abbrev MassDensity (d : ℕ) := ScalarField d
-
-/-- A velocity field on `d`-dimensional space. -/
-abbrev VelocityField (d : ℕ) := VectorField d
-
-/-- A momentum density field on `d`-dimensional space. -/
-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/Incompressible.lean b/Physlib/FluidDynamics/Incompressible.lean
new file mode 100644
index 000000000..7b6ee2cf9
--- /dev/null
+++ b/Physlib/FluidDynamics/Incompressible.lean
@@ -0,0 +1,75 @@
+/-
+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.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.SmoothIncompressible.toClassical` : 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 SmoothIncompressible.toClassical (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/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/Momentum.lean
similarity index 54%
rename from Physlib/FluidDynamics/NavierStokes/Momentum.lean
rename to Physlib/FluidDynamics/Momentum.lean
index b2dbc1911..142b7f5d0 100644
--- a/Physlib/FluidDynamics/NavierStokes/Momentum.lean
+++ b/Physlib/FluidDynamics/Momentum.lean
@@ -5,35 +5,34 @@ Authors: Florian Wiesner
 -/
 module
 
-public import Physlib.FluidDynamics.NavierStokes.Continuity
+public import Physlib.FluidDynamics.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 the generic momentum fields and conservative/convective momentum left-hand
+sides for fluid flow. 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.conservativeMomentumLHS` : The conservative momentum-balance left-hand side.
+- `FluidFlow.convectiveMomentumLHS` : The convective momentum-balance left-hand side.
+- `FluidFlow.conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul` :
+  The bridge between conservative and convective momentum forms.
 
 ## iii. Table of contents
 
 - A. Momentum fields
-- B. Conservative momentum equation
-- C. Convective momentum equation
-- D. Equivalence of conservative and convective momentum
+- B. Conservative and convective left-hand sides
+- C. Equivalence of conservative and convective momentum left-hand sides
 
 ## iv. References
 
@@ -45,7 +44,8 @@ open Space
 open Time
 
 namespace FluidDynamics
-namespace NavierStokes
+
+namespace FluidFlow
 
 /-!
 
@@ -54,76 +54,43 @@ 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. Conservative and convective left-hand sides
 
 -/
 
 /-- 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 :=
   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 :=
+noncomputable def convectiveMomentumLHS (d : ℕ) (fluid : FluidFlow d) : VectorField d :=
   fun t x => fluid.rho t x • materialAcceleration d fluid t x
 
+/-!
+
+## C. Equivalence of conservative and convective momentum left-hand sides
+
+-/
+
 /-- 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 +106,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,7 +116,7 @@ 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)) :
@@ -167,7 +134,7 @@ lemma spaceDeriv_momentumFlux_component (d : ℕ) (fluid : FluidState d)
   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)) :
@@ -210,7 +177,7 @@ The conservative momentum left-hand side equals the convective momentum left-han
 the continuity residual times the velocity field.
 -/
 lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-    (d : ℕ) (fluid : FluidState d)
+    (d : ℕ) (fluid : FluidFlow d)
     (t : Time) (x : Space d)
     (hRhoTime : DifferentiableAt ℝ (fluid.rho · x) t)
     (hVelocityTime : DifferentiableAt ℝ (fluid.velocity · x) t)
@@ -225,58 +192,6 @@ lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_sm
   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
-  constructor
-  · intro hConservative t x
-    have hMassFluxSpace :
-        DifferentiableAt ℝ (fun x' => data.rho t x' • data.velocity t x') x := by
-      simpa [momentumDensity] using (hMomentumDensity t).differentiableAt
-    have hResidual : continuityResidual d data.toFluidState t x = 0 := by
-      simpa [continuityResidual] using
-        hContinuity t x (by simpa using hRhoTime t x) hMassFluxSpace
-    have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-      d data.toFluidState t x (hRhoTime t x) (hVelocityTime t x)
-      (hMomentumDensity t) (hVelocitySpace t)
-    have hLhs' :
-        conservativeMomentumLHS d data.toFluidState t x =
-          convectiveMomentumLHS d data.toFluidState t x := by
-      rw [hLhs, hResidual, zero_smul, add_zero]
-    change convectiveMomentumLHS d data.toFluidState t x =
-      matrixDiv d (data.stress t) x + data.rho t x • data.bodyForce t x
-    rw [← hLhs']
-    exact hConservative t x
-  · intro hConvective t x
-    have hMassFluxSpace :
-        DifferentiableAt ℝ (fun x' => data.rho t x' • data.velocity t x') x := by
-      simpa [momentumDensity] using (hMomentumDensity t).differentiableAt
-    have hResidual : continuityResidual d data.toFluidState t x = 0 := by
-      simpa [continuityResidual] using
-        hContinuity t x (by simpa using hRhoTime t x) hMassFluxSpace
-    have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-      d data.toFluidState t x (hRhoTime t x) (hVelocityTime t x)
-      (hMomentumDensity t) (hVelocitySpace t)
-    have hLhs' :
-        conservativeMomentumLHS d data.toFluidState t x =
-          convectiveMomentumLHS d data.toFluidState t x := by
-      rw [hLhs, hResidual, zero_smul, add_zero]
-    change conservativeMomentumLHS d data.toFluidState t x =
-      matrixDiv d (data.stress t) x + data.rho t x • data.bodyForce t x
-    rw [hLhs']
-    exact hConvective t x
-
-end NavierStokes
 end FluidDynamics
diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 89fa5e940..19a76877a 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -5,7 +5,7 @@ Authors: Florian Wiesner
 -/
 module
 
-public import Physlib.FluidDynamics.NavierStokes.Momentum
+public import Physlib.FluidDynamics.CauchyMomentum
 /-!
 
 # The Navier-Stokes equations
@@ -16,20 +16,27 @@ The Navier-Stokes equations are a set of partial differential equations that des
 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.
+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 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.
+- `CauchyFlow.velocityGradient` : The spatial velocity-gradient matrix.
+- `CauchyFlow.newtonianStressTensor` : The Newtonian stress tensor determined by pressure and
+  viscosity.
+- `CauchyFlow.IsNewtonian` : Predicate saying the Cauchy stress has Newtonian constitutive form.
+- `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. Full Navier-Stokes forms
+- A. Newtonian stress law
+- B. Navier-Stokes equations
+- C. Equivalence of conservative and convective Navier-Stokes forms
 
 ## iv. References
 
@@ -37,42 +44,101 @@ Newtonian stress law.
 
 @[expose] public section
 
+open Space
+
 namespace FluidDynamics
 
+namespace CauchyFlow
+
 /-!
 
-## A. Full Navier-Stokes forms
+## A. Newtonian stress law
+
+-/
+
+/-- 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) ℝ)
+
+/-- 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 =
+      newtonianStressTensor d flow.toFluidFlow pressure shearViscosity secondViscosity t x
+
+end CauchyFlow
+
+/-!
 
-/-- 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
+## B. Navier-Stokes equations
 
-/-- 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 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
+
+/-!
+
+## C. 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 navierStokes_iff_convectiveNavierStokes
-    (d : ℕ) (data : FluidInMomentumBalance d)
-    (hRhoTime : ∀ t x, DifferentiableAt ℝ (data.rho · x) t)
-    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (data.velocity · x) t)
+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 ℝ (FluidDynamics.NavierStokes.momentumDensity d data.toFluidState t))
-    (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
-    NavierStokes d data ↔ ConvectiveNavierStokes d data := by
+      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, ?_⟩
-    exact (FluidDynamics.NavierStokes.momentumEquation_iff_convectiveMomentumEquation d data
-      hConservative.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp hConservative.2
+    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, ?_⟩
-    exact (FluidDynamics.NavierStokes.momentumEquation_iff_convectiveMomentumEquation d data
-      hConvective.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr hConvective.2
+    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