From 347df8fa66985bd575c7e516db8540a77eaed181 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Mon, 16 Feb 2026 10:19:00 +0000
Subject: [PATCH 01/33] Initial IdealFluid structure

---
 PhysLean/FluidMechanics/Basic.lean            | 23 +++++++++++++++++++
 .../FluidMechanics/IdealFluid/Bernoulli.lean  |  5 ++++
 .../FluidMechanics/IdealFluid/Continuity.lean |  5 ++++
 PhysLean/FluidMechanics/IdealFluid/Euler.lean |  8 +++++++
 4 files changed, 41 insertions(+)
 create mode 100644 PhysLean/FluidMechanics/Basic.lean
 create mode 100644 PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
 create mode 100644 PhysLean/FluidMechanics/IdealFluid/Continuity.lean
 create mode 100644 PhysLean/FluidMechanics/IdealFluid/Euler.lean

diff --git a/PhysLean/FluidMechanics/Basic.lean b/PhysLean/FluidMechanics/Basic.lean
new file mode 100644
index 000000000..3b4cc332c
--- /dev/null
+++ b/PhysLean/FluidMechanics/Basic.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+import PhysLean.SpaceAndTime.Space.Basic
+import PhysLean.SpaceAndTime.Time.Basic
+/-!
+This module introduces the idea of an ideal fluid and the mass flux density. The rest of the early workings is to be seen in ./IdealFluid/
+-/
+open scoped InnerProductSpace
+
+structure IdealFluid where
+  density: Time → Space → ℝ
+  velocity: Time → Space→ Space
+  pressure: Time → Space → ℝ
+
+namespace IdealFluid
+
+def massFluxDensity (F: IdealFluid) (t : Time) (pos : Space ) :
+    Space := (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+
+end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
new file mode 100644
index 000000000..3901414b5
--- /dev/null
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -0,0 +1,5 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
new file mode 100644
index 000000000..3901414b5
--- /dev/null
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -0,0 +1,5 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
new file mode 100644
index 000000000..7d1d49546
--- /dev/null
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+/-!
+This module introduces Euler's equation
+-/

From 503a3eefd1d8ba0812da763042d2436ac651cd24 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Mon, 23 Feb 2026 14:08:06 +0000
Subject: [PATCH 02/33] Added definitions and fixed the properties of earlier
 defined IdealFluid

---
 PhysLean/FluidMechanics/Basic.lean            | 23 -------
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 63 +++++++++++++++++++
 PhysLean/FluidMechanics/IdealFluid/Euler.lean |  3 -
 3 files changed, 63 insertions(+), 26 deletions(-)
 delete mode 100644 PhysLean/FluidMechanics/Basic.lean
 create mode 100644 PhysLean/FluidMechanics/IdealFluid/Basic.lean

diff --git a/PhysLean/FluidMechanics/Basic.lean b/PhysLean/FluidMechanics/Basic.lean
deleted file mode 100644
index 3b4cc332c..000000000
--- a/PhysLean/FluidMechanics/Basic.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michał Mogielnicki
--/
-import PhysLean.SpaceAndTime.Space.Basic
-import PhysLean.SpaceAndTime.Time.Basic
-/-!
-This module introduces the idea of an ideal fluid and the mass flux density. The rest of the early workings is to be seen in ./IdealFluid/
--/
-open scoped InnerProductSpace
-
-structure IdealFluid where
-  density: Time → Space → ℝ
-  velocity: Time → Space→ Space
-  pressure: Time → Space → ℝ
-
-namespace IdealFluid
-
-def massFluxDensity (F: IdealFluid) (t : Time) (pos : Space ) :
-    Space := (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
-
-end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
new file mode 100644
index 000000000..15dd0d9d9
--- /dev/null
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Mogielnicki
+-/
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import PhysLean.SpaceAndTime.Space.Basic
+import PhysLean.SpaceAndTime.Time.Basic
+/-!
+This module introduces the idea of an ideal fluid and the mass flux density
+and basic physical properties, meant to be later used for proofs.
+-/
+open scoped InnerProductSpace
+
+structure IdealFluid where
+  density: Time → Space → ℝ
+  velocity: Time → Space → EuclideanSpace ℝ (Fin 3)
+  pressure: Time → Space → ℝ
+
+  entropy: Time → Space → ℝ
+  enthlapy: Time → Space → ℝ
+
+  density_pos: ∀ t, pos 0 < density t pos
+
+  /-- Ensuring that all are differentiable for more complex equations. -/
+  density_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>density s.1 s.2)
+  velocity_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>velocity s.1 s.2)
+  pressure_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>pressure s.1 s.2)
+
+  entropy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>entropy s.1 s.2)
+  enthlapy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthlapy s.1 s.2)
+
+namespace IdealFluid
+
+/-!
+Here lays defined:
+  the mass flux density
+  entropy flux density
+  energy flux density
+  flow out of a volume
+-/
+
+def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+    EuclideanSpace ℝ (Fin 3) :=
+     (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+
+def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+    EuclideanSpace ℝ (Fin 3) :=
+      (IdealFluid.entropy F t pos) • (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+
+noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+    EuclideanSpace ℝ (Fin 3) :=
+      let w := IdealFluid.enthlapy F t pos
+      let v := IdealFluid.velocity F t pos
+      let v_sq: ℝ := ⟪v,v⟫_ℝ
+      let scalar := (IdealFluid.density F t pos)*(0.5*v_sq + w)
+
+      scalar • v
+
+/-Still a need to introduce flow out of volume-/
+
+end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index 7d1d49546..3901414b5 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -3,6 +3,3 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
-/-!
-This module introduces Euler's equation
--/

From 818fd23ff19916f5bec77fcecb0ac79a939040de Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Tue, 24 Feb 2026 10:16:02 +0000
Subject: [PATCH 03/33] Imported to PhysLean.lean and added the flow out of the
 volume

---
 PhysLean.lean                                 |  4 +++
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 31 ++++++++++++++++---
 2 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/PhysLean.lean b/PhysLean.lean
index 283c464e5..160955282 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -41,6 +41,10 @@ import PhysLean.Electromagnetism.PointParticle.ThreeDimension
 import PhysLean.Electromagnetism.Vacuum.Constant
 import PhysLean.Electromagnetism.Vacuum.HarmonicWave
 import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
+import PhysLean.FluidMechanics.IdealFluid.Basic
+import PhysLean.FluidMechanics.IdealFluid.Bernoulli
+import PhysLean.FluidMechanics.IdealFluid.Continuity
+import PhysLean.FluidMechanics.IdealFluid.Euler
 import PhysLean.Mathematics.Calculus.AdjFDeriv
 import PhysLean.Mathematics.Calculus.Divergence
 import PhysLean.Mathematics.DataStructures.FourTree.Basic
diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 15dd0d9d9..cd57cb894 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -21,7 +21,7 @@ structure IdealFluid where
   entropy: Time → Space → ℝ
   enthlapy: Time → Space → ℝ
 
-  density_pos: ∀ t, pos 0 < density t pos
+  density_pos: ∀ t pos, 0 < density t pos
 
   /-- Ensuring that all are differentiable for more complex equations. -/
   density_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>density s.1 s.2)
@@ -32,13 +32,12 @@ structure IdealFluid where
   enthlapy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthlapy s.1 s.2)
 
 namespace IdealFluid
-
+open MeasureTheory
 /-!
 Here lays defined:
   the mass flux density
   entropy flux density
   energy flux density
-  flow out of a volume
 -/
 
 def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
@@ -58,6 +57,30 @@ noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
 
       scalar • v
 
-/-Still a need to introduce flow out of volume-/
+/-I hereby describe the:
+FluidVolume structure
+surface integral
+flow out of volume-/
+
+structure FluidVolume where
+  region: Set Space
+  normal: Space → EuclideanSpace ℝ (Fin 3)
+  surfaceMeasure: Measure Space
+
+noncomputable def surfaceIntegral (V: FluidVolume) (flux: Space → EuclideanSpace ℝ (Fin 3)):
+    ℝ :=
+      ∫ (pos: Space) in frontier V.region, ⟪flux pos, V.normal pos⟫_ℝ ∂V.surfaceMeasure
+
+noncomputable def massFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (fun pos => IdealFluid.massFluxDensity F t pos)
+
+noncomputable def entropyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (fun pos => IdealFluid.entropyFluxDensity F t pos)
+
+noncomputable def energyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+    ℝ :=
+      surfaceIntegral V (fun pos => IdealFluid.energyFluxDensity F t pos)
 
 end IdealFluid

From 53e4dc1c4d985310d53aeb0867be66b59aa98b3e Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Thu, 26 Feb 2026 14:45:41 +0000
Subject: [PATCH 04/33] pls linters (oh and continuity, isentropy and
 steadiness)

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 34 ++++++++++++-------
 .../FluidMechanics/IdealFluid/Bernoulli.lean  | 29 ++++++++++++++++
 .../FluidMechanics/IdealFluid/Continuity.lean | 27 +++++++++++++++
 3 files changed, 77 insertions(+), 13 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index cd57cb894..9fc4840a0 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -3,27 +3,35 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
+
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import PhysLean.SpaceAndTime.Space.Basic
 import PhysLean.SpaceAndTime.Time.Basic
+
 /-!
 This module introduces the idea of an ideal fluid and the mass flux density
 and basic physical properties, meant to be later used for proofs.
 -/
+
 open scoped InnerProductSpace
 
+/- Introducing the structure of Ideal Fluids -/
 structure IdealFluid where
+  /- The density at a specific point and time -/
   density: Time → Space → ℝ
+  /- The velocity at a specific point and time -/
   velocity: Time → Space → EuclideanSpace ℝ (Fin 3)
+  /- The pressure at a specific point and time -/
   pressure: Time → Space → ℝ
-
+  /- The entropy at a specific point and time -/
   entropy: Time → Space → ℝ
+  /- The enthlapy at a specific point and time -/
   enthlapy: Time → Space → ℝ
 
   density_pos: ∀ t pos, 0 < density t pos
 
-  /-- Ensuring that all are differentiable for more complex equations. -/
+  /- Ensuring that all are differentiable for more complex equations. -/
   density_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>density s.1 s.2)
   velocity_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>velocity s.1 s.2)
   pressure_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>pressure s.1 s.2)
@@ -33,21 +41,18 @@ structure IdealFluid where
 
 namespace IdealFluid
 open MeasureTheory
-/-!
-Here lays defined:
-  the mass flux density
-  entropy flux density
-  energy flux density
--/
 
+/- Mass flux density j=ρv -/
 def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
      (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
 
+/- Entropy flux density ρsv -/
 def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
       (IdealFluid.entropy F t pos) • (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
 
+/- Energy flux density ρv(1/2 |v|^2 + w) -/
 noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
       let w := IdealFluid.enthlapy F t pos
@@ -57,28 +62,31 @@ noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
 
       scalar • v
 
-/-I hereby describe the:
-FluidVolume structure
-surface integral
-flow out of volume-/
-
+/- Volume to introduce surface integrals -/
 structure FluidVolume where
+  /- The 3D region -/
   region: Set Space
+  /- The normal pointing outwards -/
   normal: Space → EuclideanSpace ℝ (Fin 3)
+  /- 2D measure of the boundary -/
   surfaceMeasure: Measure Space
 
+/- Surface integral of a vector field -/
 noncomputable def surfaceIntegral (V: FluidVolume) (flux: Space → EuclideanSpace ℝ (Fin 3)):
     ℝ :=
       ∫ (pos: Space) in frontier V.region, ⟪flux pos, V.normal pos⟫_ℝ ∂V.surfaceMeasure
 
+/- Mass flow out of volume -/
 noncomputable def massFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
       surfaceIntegral V (fun pos => IdealFluid.massFluxDensity F t pos)
 
+/- Entropy flow out of volume -/
 noncomputable def entropyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
       surfaceIntegral V (fun pos => IdealFluid.entropyFluxDensity F t pos)
 
+/- Energy flow out of volume -/
 noncomputable def energyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
       surfaceIntegral V (fun pos => IdealFluid.energyFluxDensity F t pos)
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index 3901414b5..a9245b215 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -3,3 +3,32 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
+
+import PhysLean.FluidMechanics.IdealFluid.Basic
+import PhysLean.Mathematics.Calculus.Divergence
+
+/-
+This module introduces:
+steady flow,
+... (still under construction)
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+namespace IdealFluid
+
+/- Determines whether a flow is steady -/
+def isSteady (F: IdealFluid) :
+    Prop :=
+      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => IdealFluid.velocity F t' pos) t = 0
+
+/- Determines whether a flow is isentropic -/
+def isIsentropic (F: IdealFluid):
+    Prop :=
+      ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => IdealFluid.entropy F t' pos) t = 0
+
+-- TODO: Provide the Bernoulli's equation (after fun derivatoins)
+
+end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 3901414b5..9f41a2f9e 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -3,3 +3,30 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
+
+import PhysLean.FluidMechanics.IdealFluid.Basic
+import PhysLean.Mathematics.Calculus.Divergence
+
+/-
+This module introduces the continuity criterium.
+There is potential to add various different lemmas expanding on this.
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+namespace IdealFluid
+
+/- defining satisfying the equation of continuity -/
+def satisfiesContinuity (F : IdealFluid):
+    Prop :=
+      ∀ (t : Time) (pos : Space),
+      ∂ₜ (fun t' => IdealFluid.density F t' pos) t +
+      Space.div (fun pos' => IdealFluid.massFluxDensity F t pos') pos = 0
+
+
+-- TODO: Add lemmas for continuity with different models.
+-- TODO: Add definition and lemmas for Incompressibility.
+
+end IdealFluid

From 75daca2847378ac490e2eb86c6698ac4a53fca51 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Mon, 9 Mar 2026 15:28:09 +0000
Subject: [PATCH 05/33] hope for linters finally and continuity

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 36 +++++++++----------
 .../FluidMechanics/IdealFluid/Bernoulli.lean  |  6 ++--
 .../FluidMechanics/IdealFluid/Continuity.lean |  4 +--
 PhysLean/FluidMechanics/IdealFluid/Euler.lean | 16 +++++++++
 4 files changed, 39 insertions(+), 23 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 9fc4840a0..75c1cf630 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -16,22 +16,22 @@ and basic physical properties, meant to be later used for proofs.
 
 open scoped InnerProductSpace
 
-/- Introducing the structure of Ideal Fluids -/
+/-- Introducing the structure of Ideal Fluids -/
 structure IdealFluid where
-  /- The density at a specific point and time -/
+  /-- The density at a specific point and time -/
   density: Time → Space → ℝ
-  /- The velocity at a specific point and time -/
+  /-- The velocity at a specific point and time -/
   velocity: Time → Space → EuclideanSpace ℝ (Fin 3)
-  /- The pressure at a specific point and time -/
+  /-- The pressure at a specific point and time -/
   pressure: Time → Space → ℝ
-  /- The entropy at a specific point and time -/
+  /-- The entropy at a specific point and time -/
   entropy: Time → Space → ℝ
-  /- The enthlapy at a specific point and time -/
+  /-- The enthlapy at a specific point and time -/
   enthlapy: Time → Space → ℝ
 
   density_pos: ∀ t pos, 0 < density t pos
 
-  /- Ensuring that all are differentiable for more complex equations. -/
+  /-- Ensuring that all are differentiable for more complex equations. -/
   density_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>density s.1 s.2)
   velocity_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>velocity s.1 s.2)
   pressure_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>pressure s.1 s.2)
@@ -42,17 +42,17 @@ structure IdealFluid where
 namespace IdealFluid
 open MeasureTheory
 
-/- Mass flux density j=ρv -/
+/-- Mass flux density j=ρv -/
 def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
      (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
 
-/- Entropy flux density ρsv -/
+/-- Entropy flux density ρsv -/
 def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
       (IdealFluid.entropy F t pos) • (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
 
-/- Energy flux density ρv(1/2 |v|^2 + w) -/
+/-- Energy flux density ρv(1/2 |v|^2 + w) -/
 noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
       let w := IdealFluid.enthlapy F t pos
@@ -62,31 +62,31 @@ noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
 
       scalar • v
 
-/- Volume to introduce surface integrals -/
+/-- Volume to introduce surface integrals -/
 structure FluidVolume where
-  /- The 3D region -/
+  /-- The 3D region -/
   region: Set Space
-  /- The normal pointing outwards -/
+  /-- The normal pointing outwards -/
   normal: Space → EuclideanSpace ℝ (Fin 3)
-  /- 2D measure of the boundary -/
+  /-- 2D measure of the boundary -/
   surfaceMeasure: Measure Space
 
-/- Surface integral of a vector field -/
+/-- Surface integral of a vector field -/
 noncomputable def surfaceIntegral (V: FluidVolume) (flux: Space → EuclideanSpace ℝ (Fin 3)):
     ℝ :=
       ∫ (pos: Space) in frontier V.region, ⟪flux pos, V.normal pos⟫_ℝ ∂V.surfaceMeasure
 
-/- Mass flow out of volume -/
+/-- Mass flow out of volume -/
 noncomputable def massFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
       surfaceIntegral V (fun pos => IdealFluid.massFluxDensity F t pos)
 
-/- Entropy flow out of volume -/
+/-- Entropy flow out of volume -/
 noncomputable def entropyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
       surfaceIntegral V (fun pos => IdealFluid.entropyFluxDensity F t pos)
 
-/- Energy flow out of volume -/
+/-- Energy flow out of volume -/
 noncomputable def energyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
       surfaceIntegral V (fun pos => IdealFluid.energyFluxDensity F t pos)
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index a9245b215..80dc877e2 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -7,7 +7,7 @@ Authors: Michał Mogielnicki
 import PhysLean.FluidMechanics.IdealFluid.Basic
 import PhysLean.Mathematics.Calculus.Divergence
 
-/-
+/-!
 This module introduces:
 steady flow,
 ... (still under construction)
@@ -19,12 +19,12 @@ open Space
 
 namespace IdealFluid
 
-/- Determines whether a flow is steady -/
+/-- Determines whether a flow is steady -/
 def isSteady (F: IdealFluid) :
     Prop :=
       ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => IdealFluid.velocity F t' pos) t = 0
 
-/- Determines whether a flow is isentropic -/
+/-- Determines whether a flow is isentropic -/
 def isIsentropic (F: IdealFluid):
     Prop :=
       ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => IdealFluid.entropy F t' pos) t = 0
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 9f41a2f9e..8b3bf666f 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -7,7 +7,7 @@ Authors: Michał Mogielnicki
 import PhysLean.FluidMechanics.IdealFluid.Basic
 import PhysLean.Mathematics.Calculus.Divergence
 
-/-
+/-!
 This module introduces the continuity criterium.
 There is potential to add various different lemmas expanding on this.
 -/
@@ -18,7 +18,7 @@ open Space
 
 namespace IdealFluid
 
-/- defining satisfying the equation of continuity -/
+/-- defining satisfying the equation of continuity -/
 def satisfiesContinuity (F : IdealFluid):
     Prop :=
       ∀ (t : Time) (pos : Space),
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index 3901414b5..25ae92c36 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -3,3 +3,19 @@ Copyright (c) 2026 Michał Mogielnicki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
+
+import PhysLean.FluidMechanics.IdealFluid.Basic
+import PhysLean.Mathematics.Calculus.Divergence
+
+/-!
+This module introduces the Euler's equation.
+-/
+
+open scoped InnerProductSpace
+open Time
+open Space
+
+namespace IdealFluid
+
+--TODO: Introduce
+end IdealFluid

From 834062ecca9d45ec0e6b3bfb5430ac5437cc0c40 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Mon, 9 Mar 2026 16:17:17 +0000
Subject: [PATCH 06/33] fixed imports eaten by changes

---
 PhysLean.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/PhysLean.lean b/PhysLean.lean
index 59e125dd1..210da9550 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -44,6 +44,10 @@ public import PhysLean.Electromagnetism.PointParticle.ThreeDimension
 public import PhysLean.Electromagnetism.Vacuum.Constant
 public import PhysLean.Electromagnetism.Vacuum.HarmonicWave
 public import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
+public import PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.FluidMechanics.IdealFluid.Bernoulli
+public import PhysLean.FluidMechanics.IdealFluid.Continuity
+public import PhysLean.FluidMechanics.IdealFluid.Euler
 public import PhysLean.Mathematics.Calculus.AdjFDeriv
 public import PhysLean.Mathematics.Calculus.Divergence
 public import PhysLean.Mathematics.DataStructures.FourTree.Basic

From 1df9a86a72cfe4cf2011dc5cacb6bfa575869ea3 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Tue, 17 Mar 2026 09:37:25 +0000
Subject: [PATCH 07/33] Build working

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean | 16 +++++++++-------
 .../FluidMechanics/IdealFluid/Bernoulli.lean  | 19 +++++++++----------
 .../FluidMechanics/IdealFluid/Continuity.lean | 18 +++++++++---------
 PhysLean/FluidMechanics/IdealFluid/Euler.lean |  9 +++++++--
 4 files changed, 34 insertions(+), 28 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 75c1cf630..ef4626745 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
 
-import Mathlib.Analysis.InnerProductSpace.PiL2
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import PhysLean.SpaceAndTime.Space.Basic
-import PhysLean.SpaceAndTime.Time.Basic
+module
+
+public import Mathlib.Analysis.InnerProductSpace.PiL2
+public import Mathlib.Analysis.Calculus.ContDiff.Basic
+public import PhysLean.SpaceAndTime.Space.Module
+public import PhysLean.SpaceAndTime.Time.Basic
 
 /-!
 This module introduces the idea of an ideal fluid and the mass flux density
@@ -17,7 +19,7 @@ and basic physical properties, meant to be later used for proofs.
 open scoped InnerProductSpace
 
 /-- Introducing the structure of Ideal Fluids -/
-structure IdealFluid where
+public structure IdealFluid where
   /-- The density at a specific point and time -/
   density: Time → Space → ℝ
   /-- The velocity at a specific point and time -/
@@ -43,12 +45,12 @@ namespace IdealFluid
 open MeasureTheory
 
 /-- Mass flux density j=ρv -/
-def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+public def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
      (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
 
 /-- Entropy flux density ρsv -/
-def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+public def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
       (IdealFluid.entropy F t pos) • (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
 
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index 80dc877e2..8ded3bcdc 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -4,8 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
 
-import PhysLean.FluidMechanics.IdealFluid.Basic
-import PhysLean.Mathematics.Calculus.Divergence
+module
+
+public import PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.Mathematics.Calculus.Divergence
+public import PhysLean.SpaceAndTime.Time.Derivatives
 
 /-!
 This module introduces:
@@ -17,18 +20,14 @@ open scoped InnerProductSpace
 open Time
 open Space
 
-namespace IdealFluid
-
 /-- Determines whether a flow is steady -/
-def isSteady (F: IdealFluid) :
+def IdealFluid.isSteady (F: IdealFluid) :
     Prop :=
-      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => IdealFluid.velocity F t' pos) t = 0
+      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => F.velocity t' pos) t = (0 : EuclideanSpace ℝ (Fin 3))
 
 /-- Determines whether a flow is isentropic -/
-def isIsentropic (F: IdealFluid):
+def IdealFluid.isIsentropic (F: IdealFluid):
     Prop :=
-      ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => IdealFluid.entropy F t' pos) t = 0
+      ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => F.entropy t' pos) t = (0 : ℝ)
 
 -- TODO: Provide the Bernoulli's equation (after fun derivatoins)
-
-end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 8b3bf666f..09ca420d4 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
 
-import PhysLean.FluidMechanics.IdealFluid.Basic
-import PhysLean.Mathematics.Calculus.Divergence
+module
+
+public import PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.Mathematics.Calculus.Divergence
+public import PhysLean.SpaceAndTime.Time.Derivatives
+public import PhysLean.SpaceAndTime.Space.Derivatives.Div
 
 /-!
 This module introduces the continuity criterium.
@@ -16,17 +20,13 @@ open scoped InnerProductSpace
 open Time
 open Space
 
-namespace IdealFluid
-
 /-- defining satisfying the equation of continuity -/
-def satisfiesContinuity (F : IdealFluid):
+def IdealFluid.satisfiesContinuity (F : IdealFluid):
     Prop :=
       ∀ (t : Time) (pos : Space),
-      ∂ₜ (fun t' => IdealFluid.density F t' pos) t +
-      Space.div (fun pos' => IdealFluid.massFluxDensity F t pos') pos = 0
+      ∂ₜ (fun t' => F.density t' pos) t +
+      Space.div (fun pos' => F.massFluxDensity t pos') pos = (0 : ℝ)
 
 
 -- TODO: Add lemmas for continuity with different models.
 -- TODO: Add definition and lemmas for Incompressibility.
-
-end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index 25ae92c36..a36fad807 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -4,8 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michał Mogielnicki
 -/
 
-import PhysLean.FluidMechanics.IdealFluid.Basic
-import PhysLean.Mathematics.Calculus.Divergence
+module
+
+public import PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.Mathematics.Calculus.Divergence
+public import PhysLean.SpaceAndTime.Time.Derivatives
+public import PhysLean.SpaceAndTime.Space.Derivatives.Grad
+public import PhysLean.SpaceAndTime.Space.Derivatives.Div
 
 /-!
 This module introduces the Euler's equation.

From 3dc2ff3b6beede98a8abe20c1e89aec3d3bb8df1 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Tue, 17 Mar 2026 13:10:43 +0000
Subject: [PATCH 08/33] hope

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean |  8 +++---
 .../FluidMechanics/IdealFluid/Bernoulli.lean  | 26 ++++++++++++++++---
 .../FluidMechanics/IdealFluid/Continuity.lean |  6 +----
 PhysLean/FluidMechanics/IdealFluid/Euler.lean | 12 ++++++---
 4 files changed, 36 insertions(+), 16 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index ef4626745..237fb8c39 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -28,8 +28,8 @@ public structure IdealFluid where
   pressure: Time → Space → ℝ
   /-- The entropy at a specific point and time -/
   entropy: Time → Space → ℝ
-  /-- The enthlapy at a specific point and time -/
-  enthlapy: Time → Space → ℝ
+  /-- The enthalpy at a specific point and time -/
+  enthalpy: Time → Space → ℝ
 
   density_pos: ∀ t pos, 0 < density t pos
 
@@ -39,7 +39,7 @@ public structure IdealFluid where
   pressure_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>pressure s.1 s.2)
 
   entropy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>entropy s.1 s.2)
-  enthlapy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthlapy s.1 s.2)
+  enthalpy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthalpy s.1 s.2)
 
 namespace IdealFluid
 open MeasureTheory
@@ -57,7 +57,7 @@ public def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
 /-- Energy flux density ρv(1/2 |v|^2 + w) -/
 noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
-      let w := IdealFluid.enthlapy F t pos
+      let w := IdealFluid.enthalpy F t pos
       let v := IdealFluid.velocity F t pos
       let v_sq: ℝ := ⟪v,v⟫_ℝ
       let scalar := (IdealFluid.density F t pos)*(0.5*v_sq + w)
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index 8ded3bcdc..a7af2e56a 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -7,6 +7,7 @@ Authors: Michał Mogielnicki
 module
 
 public import PhysLean.FluidMechanics.IdealFluid.Basic
+public import PhysLean.FluidMechanics.IdealFluid.Euler
 public import PhysLean.Mathematics.Calculus.Divergence
 public import PhysLean.SpaceAndTime.Time.Derivatives
 
@@ -23,11 +24,30 @@ open Space
 /-- Determines whether a flow is steady -/
 def IdealFluid.isSteady (F: IdealFluid) :
     Prop :=
-      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => F.velocity t' pos) t = (0 : EuclideanSpace ℝ (Fin 3))
+      ∀ (t : Time) (pos : Space),
+      ∂ₜ (fun t' => F.velocity t' pos) t = (0 : EuclideanSpace ℝ (Fin 3))
 
 /-- Determines whether a flow is isentropic -/
 def IdealFluid.isIsentropic (F: IdealFluid):
     Prop :=
-      ∀ (t: Time) (pos: Space), ∂ₜ (fun t' => F.entropy t' pos) t = (0 : ℝ)
+      ∀ (t: Time) (pos: Space),
+      ∂ₜ (fun t' => F.entropy t' pos) t = (0 : ℝ)
 
--- TODO: Provide the Bernoulli's equation (after fun derivatoins)
+/-- The Bernoulli function (1/2)v^2 + w -/
+noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
+(t: Time) (pos: Space) (g: Space → ℝ):
+    ℝ :=
+      let v := F.velocity t pos
+      0.5 * ⟪v, v⟫_ℝ + F.enthalpy t pos + g pos
+
+/-- Derivation:
+  If the flow is steady and isentropic, the bernoulli equation is constant
+-/
+theorem bernoulli_derivation (F: IdealFluid) (Eul: F.satisfiesEuler g) (Stdy: F.isSteady)
+(Istrpc: F.isIsentropic) (g: Space → ℝ) (t: Time) (pos: Space):
+    let v := F.velocity t pos
+    ⟪v, Space.grad (fun pos' => F.bernoulliEquation t pos' g) pos⟫_ℝ = 0
+    := by
+      sorry
+
+--TODO: Complete the proofs
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 09ca420d4..12d037948 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -21,12 +21,8 @@ open Time
 open Space
 
 /-- defining satisfying the equation of continuity -/
-def IdealFluid.satisfiesContinuity (F : IdealFluid):
+public def IdealFluid.satisfiesContinuity (F : IdealFluid):
     Prop :=
       ∀ (t : Time) (pos : Space),
       ∂ₜ (fun t' => F.density t' pos) t +
       Space.div (fun pos' => F.massFluxDensity t pos') pos = (0 : ℝ)
-
-
--- TODO: Add lemmas for continuity with different models.
--- TODO: Add definition and lemmas for Incompressibility.
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index a36fad807..872182dea 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -20,7 +20,11 @@ open scoped InnerProductSpace
 open Time
 open Space
 
-namespace IdealFluid
-
---TODO: Introduce
-end IdealFluid
+/-- Defines the property of satisfying Euler's equation. -/
+public def IdealFluid.satisfiesEuler (F: IdealFluid) (g: Space → ℝ):
+    Prop :=
+      ∀ (t : Time) (pos : Space),
+        let v := F.velocity t pos
+        ∂ₜ (fun t'=> F.velocity t' pos) t +
+        (fun i => ⟪v, Space.grad (fun pos' => F.velocity t pos' i) pos⟫_ℝ)
+        = -(1/F.density t pos) • Space.grad (fun pos' => F.pressure t pos') pos + Space.grad g pos

From d175f46fbc3c497af0e65b0c4eeb82c90a09f5fb Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Wed, 18 Mar 2026 20:11:37 +0000
Subject: [PATCH 09/33] smol changes

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean      |  8 ++++----
 PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean  | 14 +++++++-------
 PhysLean/FluidMechanics/IdealFluid/Continuity.lean |  5 +++++
 3 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 237fb8c39..1879030f3 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -45,17 +45,17 @@ namespace IdealFluid
 open MeasureTheory
 
 /-- Mass flux density j=ρv -/
-public def massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+public abbrev massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
-     (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+      F.density t pos • F.velocity t pos
 
 /-- Entropy flux density ρsv -/
-public def entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+public abbrev entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
       (IdealFluid.entropy F t pos) • (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
 
 /-- Energy flux density ρv(1/2 |v|^2 + w) -/
-noncomputable def energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+noncomputable abbrev energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
     EuclideanSpace ℝ (Fin 3) :=
       let w := IdealFluid.enthalpy F t pos
       let v := IdealFluid.velocity F t pos
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index a7af2e56a..b2329d75d 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -43,11 +43,11 @@ noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
 /-- Derivation:
   If the flow is steady and isentropic, the bernoulli equation is constant
 -/
-theorem bernoulli_derivation (F: IdealFluid) (Eul: F.satisfiesEuler g) (Stdy: F.isSteady)
-(Istrpc: F.isIsentropic) (g: Space → ℝ) (t: Time) (pos: Space):
+theorem bernoulli_derivation (F : IdealFluid) (g : Space → ℝ) (t : Time) (pos : Space)
+    (Eul : F.satisfiesEuler g)
+    (Stdy : F.isSteady)
+    (Istrpc : F.isIsentropic) :
     let v := F.velocity t pos
-    ⟪v, Space.grad (fun pos' => F.bernoulliEquation t pos' g) pos⟫_ℝ = 0
-    := by
-      sorry
-
---TODO: Complete the proofs
+    ⟪v, Space.grad (fun pos' => F.bernoulliEquation t pos' g) pos⟫_ℝ = 0 :=
+      by
+        sorry
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 12d037948..826bf01c7 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -26,3 +26,8 @@ public def IdealFluid.satisfiesContinuity (F : IdealFluid):
       ∀ (t : Time) (pos : Space),
       ∂ₜ (fun t' => F.density t' pos) t +
       Space.div (fun pos' => F.massFluxDensity t pos') pos = (0 : ℝ)
+
+/-- Criterion for incompressibility -/
+public def IdealFluid.isIncompressible (F : IdealFluid):
+    Prop :=
+      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => F.density t' pos) t = 0

From ad5f26ce4640fedad916eb5a043579420cf58530 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Wed, 18 Mar 2026 20:16:18 +0000
Subject: [PATCH 10/33] a sorryful theorem

---
 PhysLean/FluidMechanics/IdealFluid/Continuity.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index 826bf01c7..ecea01b9f 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -31,3 +31,12 @@ public def IdealFluid.satisfiesContinuity (F : IdealFluid):
 public def IdealFluid.isIncompressible (F : IdealFluid):
     Prop :=
       ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => F.density t' pos) t = 0
+
+
+/-- Theorem: If constant density and incompressible div(v)=0-/
+theorem incompress_const_density_implies_div_v_eq_zero (F : IdealFluid)
+    (Cont      : F.satisfiesContinuity)
+    (Incomp    : F.isIncompressible)
+    (ConstDens : ∀ (t : Time) (pos : Space), Space.grad (fun pos' => F.density t pos') pos = 0) :
+    ∀ (t : Time) (pos : Space), Space.div (fun pos' => F.velocity t pos') pos = 0 := by
+      sorry

From d020adb1bde6d08f07caa209cf280bad4b3ecd51 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Thu, 19 Mar 2026 12:51:19 +0000
Subject: [PATCH 11/33] suggestions for myself

---
 PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean  | 4 ++++
 PhysLean/FluidMechanics/IdealFluid/Continuity.lean | 1 -
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index b2329d75d..451de1836 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -33,6 +33,8 @@ def IdealFluid.isIsentropic (F: IdealFluid):
       ∀ (t: Time) (pos: Space),
       ∂ₜ (fun t' => F.entropy t' pos) t = (0 : ℝ)
 
+-- TODO: Make into material derivative
+
 /-- The Bernoulli function (1/2)v^2 + w -/
 noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
 (t: Time) (pos: Space) (g: Space → ℝ):
@@ -40,6 +42,8 @@ noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
       let v := F.velocity t pos
       0.5 * ⟪v, v⟫_ℝ + F.enthalpy t pos + g pos
 
+-- TODO: Recheck signs
+
 /-- Derivation:
   If the flow is steady and isentropic, the bernoulli equation is constant
 -/
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index ecea01b9f..f537b01fd 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -32,7 +32,6 @@ public def IdealFluid.isIncompressible (F : IdealFluid):
     Prop :=
       ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => F.density t' pos) t = 0
 
-
 /-- Theorem: If constant density and incompressible div(v)=0-/
 theorem incompress_const_density_implies_div_v_eq_zero (F : IdealFluid)
     (Cont      : F.satisfiesContinuity)

From 49a87206de8e7f9c8eba9db3e1317c5310776392 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Wed, 29 Apr 2026 09:43:56 +0000
Subject: [PATCH 12/33] Mderiv and fun

---
 PhysLean/FluidMechanics/IdealFluid/Basic.lean   |  6 +++---
 .../FluidMechanics/IdealFluid/Bernoulli.lean    | 17 ++++++++++++-----
 .../FluidMechanics/IdealFluid/Continuity.lean   | 10 +++++-----
 PhysLean/FluidMechanics/IdealFluid/Euler.lean   |  6 +++---
 4 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/PhysLean/FluidMechanics/IdealFluid/Basic.lean b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
index 1879030f3..6d22a02fe 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Basic.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Basic.lean
@@ -81,16 +81,16 @@ noncomputable def surfaceIntegral (V: FluidVolume) (flux: Space → EuclideanSpa
 /-- Mass flow out of volume -/
 noncomputable def massFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
-      surfaceIntegral V (fun pos => IdealFluid.massFluxDensity F t pos)
+      surfaceIntegral V (IdealFluid.massFluxDensity F t ·)
 
 /-- Entropy flow out of volume -/
 noncomputable def entropyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
-      surfaceIntegral V (fun pos => IdealFluid.entropyFluxDensity F t pos)
+      surfaceIntegral V (IdealFluid.entropyFluxDensity F t ·)
 
 /-- Energy flow out of volume -/
 noncomputable def energyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
     ℝ :=
-      surfaceIntegral V (fun pos => IdealFluid.energyFluxDensity F t pos)
+      surfaceIntegral V (IdealFluid.energyFluxDensity F t ·)
 
 end IdealFluid
diff --git a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
index 451de1836..48c9cc8d7 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Bernoulli.lean
@@ -24,14 +24,21 @@ open Space
 /-- Determines whether a flow is steady -/
 def IdealFluid.isSteady (F: IdealFluid) :
     Prop :=
-      ∀ (t : Time) (pos : Space),
-      ∂ₜ (fun t' => F.velocity t' pos) t = (0 : EuclideanSpace ℝ (Fin 3))
+      ∀ (pos : Space),
+      ∂ₜ (F.velocity · pos) = 0
+
+/-- Definition of a material derivative -/
+noncomputable def IdealFluid.materialDerivative (t: Time) (pos: Space)
+(F: IdealFluid) (f: Time → Space → ℝ) :
+    ℝ :=
+      ∂ₜ (f · pos) t +
+      ⟪F.velocity t pos, ∇ (f t ·) pos ⟫_ℝ
 
 /-- Determines whether a flow is isentropic -/
 def IdealFluid.isIsentropic (F: IdealFluid):
     Prop :=
       ∀ (t: Time) (pos: Space),
-      ∂ₜ (fun t' => F.entropy t' pos) t = (0 : ℝ)
+      F.materialDerivative t pos F.entropy = 0
 
 -- TODO: Make into material derivative
 
@@ -42,7 +49,7 @@ noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
       let v := F.velocity t pos
       0.5 * ⟪v, v⟫_ℝ + F.enthalpy t pos + g pos
 
--- TODO: Recheck signs
+-- TODO: Recheck sign
 
 /-- Derivation:
   If the flow is steady and isentropic, the bernoulli equation is constant
@@ -52,6 +59,6 @@ theorem bernoulli_derivation (F : IdealFluid) (g : Space → ℝ) (t : Time) (po
     (Stdy : F.isSteady)
     (Istrpc : F.isIsentropic) :
     let v := F.velocity t pos
-    ⟪v, Space.grad (fun pos' => F.bernoulliEquation t pos' g) pos⟫_ℝ = 0 :=
+    ⟪v, Space.grad (F.bernoulliEquation t · g) pos⟫_ℝ = 0 :=
       by
         sorry
diff --git a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
index f537b01fd..fa6313e69 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Continuity.lean
@@ -24,18 +24,18 @@ open Space
 public def IdealFluid.satisfiesContinuity (F : IdealFluid):
     Prop :=
       ∀ (t : Time) (pos : Space),
-      ∂ₜ (fun t' => F.density t' pos) t +
-      Space.div (fun pos' => F.massFluxDensity t pos') pos = (0 : ℝ)
+      ∂ₜ (F.density · pos) t +
+      Space.div (F.massFluxDensity t ·) pos = (0 : ℝ)
 
 /-- Criterion for incompressibility -/
 public def IdealFluid.isIncompressible (F : IdealFluid):
     Prop :=
-      ∀ (t : Time) (pos : Space), ∂ₜ (fun t' => F.density t' pos) t = 0
+      ∀ (t : Time) (pos : Space), ∂ₜ (F.density · pos) t = 0
 
 /-- Theorem: If constant density and incompressible div(v)=0-/
 theorem incompress_const_density_implies_div_v_eq_zero (F : IdealFluid)
     (Cont      : F.satisfiesContinuity)
     (Incomp    : F.isIncompressible)
-    (ConstDens : ∀ (t : Time) (pos : Space), Space.grad (fun pos' => F.density t pos') pos = 0) :
-    ∀ (t : Time) (pos : Space), Space.div (fun pos' => F.velocity t pos') pos = 0 := by
+    (ConstDens : ∀ (t : Time) (pos : Space), Space.grad (F.density t ·) pos = 0) :
+    ∀ (t : Time) (pos : Space), Space.div (F.velocity t ·) pos = 0 := by
       sorry
diff --git a/PhysLean/FluidMechanics/IdealFluid/Euler.lean b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
index 872182dea..e5af22296 100644
--- a/PhysLean/FluidMechanics/IdealFluid/Euler.lean
+++ b/PhysLean/FluidMechanics/IdealFluid/Euler.lean
@@ -25,6 +25,6 @@ public def IdealFluid.satisfiesEuler (F: IdealFluid) (g: Space → ℝ):
     Prop :=
       ∀ (t : Time) (pos : Space),
         let v := F.velocity t pos
-        ∂ₜ (fun t'=> F.velocity t' pos) t +
-        (fun i => ⟪v, Space.grad (fun pos' => F.velocity t pos' i) pos⟫_ℝ)
-        = -(1/F.density t pos) • Space.grad (fun pos' => F.pressure t pos') pos + Space.grad g pos
+        ∂ₜ (F.velocity · pos) t +
+        (fun i => ⟪v, Space.grad (F.velocity t · i) pos⟫_ℝ)
+        = -(1/F.density t pos) • Space.grad (F.pressure t ·) pos + Space.grad g pos

From 00c4ed9f6fc27efce9a13036d6fe02cfa7dcbf0c Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Mon, 18 May 2026 09:53:40 +0200
Subject: [PATCH 13/33] feat: Add initial documentation for Navier-Stokes
 equations

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 Physlib/FluidDynamics/NavierStokes/Basic.lean

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
new file mode 100644
index 000000000..ca165912b
--- /dev/null
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner
+-/
+
+module
+
+
+/-!
+
+# 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.
+
+-/

From 30e3d23c02aedaf1f9141dc14917267c2e466279 Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Tue, 19 May 2026 16:39:36 +0200
Subject: [PATCH 14/33] feat(Space): add tensor divergence

---
 Physlib.lean                                  |   1 +
 .../Space/Derivatives/TensorDiv.lean          | 144 ++++++++++++++++++
 2 files changed, 145 insertions(+)
 create mode 100644 Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean

diff --git a/Physlib.lean b/Physlib.lean
index 460066d22..a5fa29c22 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -361,6 +361,7 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Grad
 public import Physlib.SpaceAndTime.Space.Derivatives.Iterated
 public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian
 public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex
+public import Physlib.SpaceAndTime.Space.Derivatives.TensorDiv
 public import Physlib.SpaceAndTime.Space.DistConst
 public import Physlib.SpaceAndTime.Space.DistOfFunction
 public import Physlib.SpaceAndTime.Space.Integrals.Basic
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean b/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean
new file mode 100644
index 000000000..dcf2b2c1e
--- /dev/null
+++ b/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean
@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2025 Florian Wiesner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florian Wiesner
+-/
+module
+
+public import Mathlib.Data.Matrix.Basic
+public import Physlib.SpaceAndTime.Space.Derivatives.Basic
+/-!
+
+# Tensor divergence on Space
+
+## i. Overview
+
+In this module we define the tensor divergence operator on matrix-valued
+functions from `Space d`.
+
+For a field `T : Space d → Matrix (Fin d) (Fin d) ℝ`, the tensor divergence is
+the vector field whose `i`th component is
+
+`∑ j, ∂[j] (fun x => T x i j) x`.
+
+## ii. Key results
+
+- `tensorDiv` : The divergence of a matrix-valued function on `Space d`.
+
+## iii. Table of contents
+
+- A. The tensor divergence on functions
+  - A.1. Basic equalities
+  - A.2. The tensor divergence on the zero function
+  - A.3. The tensor divergence on a constant function
+  - A.4. The tensor divergence distributes over addition
+  - A.5. The tensor divergence distributes over scalar multiplication
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Physlib
+
+namespace Space
+
+/-!
+
+## A. The tensor divergence on functions
+
+-/
+
+/-- The divergence of a matrix-valued spatial field.
+
+For a field `T : Space d → Matrix (Fin d) (Fin d) ℝ`, `tensorDiv T` is the
+vector field whose `i`th component is
+
+`∑ j, ∂[j] (fun x => T x i j) x`.
+-/
+noncomputable def tensorDiv (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ) :
+    Space d → EuclideanSpace ℝ (Fin d) := fun x => WithLp.toLp 2 fun i =>
+  ∑ j, ∂[j] (fun x => T x i j) x
+
+/-!
+
+### A.1. Basic equalities
+
+-/
+
+@[simp]
+lemma tensorDiv_apply (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ)
+    (x : Space d) (i : Fin d) :
+    tensorDiv d T x i = ∑ j, ∂[j] (fun x => T x i j) x := rfl
+
+/-!
+
+### A.2. The tensor divergence on the zero function
+
+-/
+
+@[simp]
+lemma tensorDiv_zero (d : ℕ) :
+    tensorDiv d (0 : Space d → Matrix (Fin d) (Fin d) ℝ) = 0 := by
+  ext x i
+  change (∑ j : Fin d, ∂[j] (fun _ : Space d => (0 : ℝ)) x) = 0
+  simp
+
+/-!
+
+### A.3. The tensor divergence on a constant function
+
+-/
+
+@[simp]
+lemma tensorDiv_const (d : ℕ) (T : Matrix (Fin d) (Fin d) ℝ) :
+    tensorDiv d (fun _ : Space d => T) = 0 := by
+  ext x i
+  change (∑ j : Fin d, ∂[j] (fun _ : Space d => T i j) x) = 0
+  simp
+
+/-!
+
+### A.4. The tensor divergence distributes over addition
+
+-/
+
+lemma tensorDiv_add (d : ℕ) (T1 T2 : Space d → Matrix (Fin d) (Fin d) ℝ)
+    (hT1 : Differentiable ℝ T1) (hT2 : Differentiable ℝ T2) :
+    tensorDiv d (T1 + T2) = tensorDiv d T1 + tensorDiv d T2 := by
+  ext x i
+  change (∑ j, ∂[j] (fun x => (T1 x + T2 x) i j) x) =
+    (∑ j, ∂[j] (fun x => T1 x i j) x) +
+      ∑ j, ∂[j] (fun x => T2 x i j) x
+  rw [← Finset.sum_add_distrib]
+  congr
+  funext j
+  change ∂[j] ((fun x => T1 x i j) + fun x => T2 x i j) x =
+    ∂[j] (fun x => T1 x i j) x + ∂[j] (fun x => T2 x i j) x
+  rw [deriv_add]
+  · rfl
+  · exact differentiable_pi.mp (differentiable_pi.mp hT1 i) j
+  · exact differentiable_pi.mp (differentiable_pi.mp hT2 i) j
+
+/-!
+
+### A.5. The tensor divergence distributes over scalar multiplication
+
+-/
+
+lemma tensorDiv_smul (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ) (k : ℝ)
+    (hT : Differentiable ℝ T) :
+    tensorDiv d (k • T) = k • tensorDiv d T := by
+  ext x i
+  change (∑ j, ∂[j] (fun x => (k • T x) i j) x) =
+    k * ∑ j, ∂[j] (fun x => T x i j) x
+  rw [Finset.mul_sum]
+  congr
+  funext j
+  change ∂[j] (k • fun x => T x i j) x = k • ∂[j] (fun x => T x i j) x
+  rw [deriv_const_smul]
+  · rfl
+  · exact differentiable_pi.mp (differentiable_pi.mp hT i) j
+
+end Space

From a52f20a063ed322dedabb6902d7099eb9a44901a Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Tue, 19 May 2026 16:57:21 +0200
Subject: [PATCH 15/33] feat(FluidDynamics): add conservative Navier-Stokes
 form

---
 Physlib.lean                                  |   1 +
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 121 +++++++++++++++++-
 2 files changed, 120 insertions(+), 2 deletions(-)

diff --git a/Physlib.lean b/Physlib.lean
index a5fa29c22..996cdce21 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -50,6 +50,7 @@ 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.NavierStokes.Basic
 public import Physlib.Mathematics.Calculus.AdjFDeriv
 public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index ca165912b..cc1bb4b48 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -3,10 +3,12 @@ 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 Mathlib.Data.Matrix.Mul
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
+public import Physlib.SpaceAndTime.Space.Derivatives.TensorDiv
+public import Physlib.SpaceAndTime.Time.Derivatives
 /-!
 
 # The Navier-Stokes equations
@@ -17,4 +19,119 @@ 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 starts with the conservative tensor-divergence form. 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
+
+- `MassDensity` : A time-dependent scalar density field.
+- `VelocityField` : A time-dependent vector velocity field.
+- `StressTensor` : A time-dependent matrix-valued stress field.
+- `momentumDensity` : The vector momentum density `rho u`.
+- `momentumFlux` : The convective momentum flux `rho u ⊗ u`.
+- `ContinuityEquation` : Conservation of mass.
+- `ConservativeMomentumEquation` : Conservation of momentum using `Space.tensorDiv`.
+- `ConservativeForm` : Continuity and conservative momentum equations together.
+
+## iii. Table of contents
+
+- A. Field types
+- B. Momentum fields
+- C. Conservative equations
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+open Time
+
+namespace FluidDynamics
+namespace NavierStokes
+
+/-!
+
+## A. Field types
+
+-/
+
+/-- A mass density field on `d`-dimensional space. -/
+abbrev MassDensity (d : ℕ) := Time → Space d → ℝ
+
+/-- A velocity field on `d`-dimensional space. -/
+abbrev VelocityField (d : ℕ) := Time → Space d → EuclideanSpace ℝ (Fin 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 : ℕ) := Time → Space d → EuclideanSpace ℝ (Fin d)
+
+/-!
+
+## B. Momentum fields
+
 -/
+
+/-- The momentum density `rho u`. -/
+def momentumDensity (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
+    VelocityField d :=
+  fun time position => rho time position • velocity time position
+
+/-- The convective momentum flux `rho u ⊗ u`. -/
+def momentumFlux (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
+    Time → Space d → Matrix (Fin d) (Fin d) ℝ :=
+  fun time position =>
+    rho time position • Matrix.vecMulVec
+      (fun i => velocity time position i) (fun j => velocity time position j)
+
+lemma momentumDensity_apply (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (time : Time) (position : Space d) :
+    momentumDensity d rho velocity time position =
+      rho time position • velocity time position := rfl
+
+lemma momentumFlux_apply (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (time : Time) (position : Space d) (i j : Fin d) :
+    momentumFlux d rho velocity time position i j =
+      rho time position * velocity time position i * velocity time position j := by
+  simp [momentumFlux, Matrix.vecMulVec_apply, mul_assoc]
+
+/-!
+
+## C. Conservative equations
+
+-/
+
+/-- Conservation of mass in conservative form, `partial_t rho + div (rho u) = 0`. -/
+def ContinuityEquation (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
+    Prop :=
+  ∀ time position,
+    ∂ₜ (fun time' => rho time' position) time +
+      (∇ ⬝ fun position' => rho time position' • velocity time position') position = 0
+
+/-- Conservation of momentum in conservative tensor-divergence form.
+
+The equation is
+
+`partial_t (rho u) + div_tensor (rho u ⊗ u) = div_tensor sigma + rho f`.
+
+Here `stress` is intentionally not yet specialized to a Newtonian stress law.
+-/
+def ConservativeMomentumEquation (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (stress : StressTensor d) (bodyForce : BodyForce d) : Prop :=
+  ∀ time position,
+    ∂ₜ (fun time' => momentumDensity d rho velocity time' position) time +
+        tensorDiv d (momentumFlux d rho velocity time) position =
+      tensorDiv d (stress time) position + rho time position • bodyForce time position
+
+/-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
+def ConservativeForm (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (stress : StressTensor d) (bodyForce : BodyForce d) : Prop :=
+  ContinuityEquation d rho velocity ∧
+    ConservativeMomentumEquation d rho velocity stress bodyForce
+
+end NavierStokes
+end FluidDynamics

From 7d0486768faa91e4650709119521654f75eb6124 Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Tue, 19 May 2026 17:01:29 +0200
Subject: [PATCH 16/33] feat(FluidDynamics): add convective Navier-Stokes form

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 58 ++++++++++++++++++-
 1 file changed, 55 insertions(+), 3 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index cc1bb4b48..ed504e087 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -19,9 +19,9 @@ 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 starts with the conservative tensor-divergence form. 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 starts with the conservative tensor-divergence form and the convective form. 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
 
@@ -30,15 +30,20 @@ law.
 - `StressTensor` : A time-dependent matrix-valued stress field.
 - `momentumDensity` : The vector momentum density `rho u`.
 - `momentumFlux` : The convective momentum flux `rho u ⊗ u`.
+- `convectiveTerm` : The nonlinear transport term `(u · ∇)u`.
+- `materialAcceleration` : The material acceleration `∂ₜ u + (u · ∇)u`.
 - `ContinuityEquation` : Conservation of mass.
 - `ConservativeMomentumEquation` : Conservation of momentum using `Space.tensorDiv`.
 - `ConservativeForm` : Continuity and conservative momentum equations together.
+- `ConvectiveMomentumEquation` : The momentum equation in convective form.
+- `ConvectiveForm` : Continuity and convective momentum equations together.
 
 ## iii. Table of contents
 
 - A. Field types
 - B. Momentum fields
 - C. Conservative equations
+- D. Convective equations
 
 ## iv. References
 
@@ -133,5 +138,52 @@ def ConservativeForm (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d
   ContinuityEquation d rho velocity ∧
     ConservativeMomentumEquation d rho velocity stress bodyForce
 
+/-!
+
+## D. Convective equations
+
+-/
+
+/-- The nonlinear transport term `(u · ∇)u`. -/
+noncomputable def convectiveTerm (d : ℕ) (velocity : VelocityField d) : VelocityField d :=
+  fun time position => ∑ j, velocity time position j • ∂[j] (velocity time) position
+
+/-- The material acceleration `∂ₜ u + (u · ∇)u`. -/
+noncomputable def materialAcceleration (d : ℕ) (velocity : VelocityField d) : VelocityField d :=
+  fun time position =>
+    ∂ₜ (fun time' => velocity time' position) time +
+      convectiveTerm d velocity time position
+
+lemma convectiveTerm_apply (d : ℕ) (velocity : VelocityField d)
+    (time : Time) (position : Space d) :
+    convectiveTerm d velocity time position =
+      ∑ j, velocity time position j • ∂[j] (velocity time) position := rfl
+
+lemma materialAcceleration_apply (d : ℕ) (velocity : VelocityField d)
+    (time : Time) (position : Space d) :
+    materialAcceleration d velocity time position =
+      ∂ₜ (fun time' => velocity time' position) time +
+        convectiveTerm d velocity time position := rfl
+
+/-- Conservation of momentum in convective form.
+
+The equation is
+
+`rho (partial_t u + (u · ∇)u) = div_tensor sigma + rho f`.
+
+Here `stress` is intentionally not yet specialized to a Newtonian stress law.
+-/
+def ConvectiveMomentumEquation (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (stress : StressTensor d) (bodyForce : BodyForce d) : Prop :=
+  ∀ time position,
+    rho time position • materialAcceleration d velocity time position =
+      tensorDiv d (stress time) position + rho time position • bodyForce time position
+
+/-- The convective Navier-Stokes form with an externally supplied stress tensor. -/
+def ConvectiveForm (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (stress : StressTensor d) (bodyForce : BodyForce d) : Prop :=
+  ContinuityEquation d rho velocity ∧
+    ConvectiveMomentumEquation d rho velocity stress bodyForce
+
 end NavierStokes
 end FluidDynamics

From 4bf2c6e291bc4db30fb4dc25800ce71abbd3469d Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Tue, 19 May 2026 17:33:17 +0200
Subject: [PATCH 17/33] feat(FluidDynamics): prove Navier-Stokes form
 equivalence

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 228 ++++++++++++++++++
 1 file changed, 228 insertions(+)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index ed504e087..409a5c3f5 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -37,6 +37,10 @@ to a Newtonian stress law.
 - `ConservativeForm` : Continuity and conservative momentum equations together.
 - `ConvectiveMomentumEquation` : The momentum equation in convective form.
 - `ConvectiveForm` : Continuity and convective momentum equations together.
+- `ConservativeMomentumEquation_iff_ConvectiveMomentumEquation` : Equivalence of the two
+  momentum equations when continuity holds and the fields are differentiable.
+- `ConservativeForm_iff_ConvectiveForm` : Equivalence of the two forms when the
+  fields are differentiable.
 
 ## iii. Table of contents
 
@@ -44,6 +48,7 @@ to a Newtonian stress law.
 - B. Momentum fields
 - C. Conservative equations
 - D. Convective equations
+- E. Equivalence of conservative and convective forms
 
 ## iv. References
 
@@ -93,11 +98,13 @@ def momentumFlux (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
     rho time position • Matrix.vecMulVec
       (fun i => velocity time position i) (fun j => velocity time position j)
 
+/-- The value of `momentumDensity` at a time and position. -/
 lemma momentumDensity_apply (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
     (time : Time) (position : Space d) :
     momentumDensity d rho velocity time position =
       rho time position • velocity time position := rfl
 
+/-- The `(i, j)` component of the convective momentum flux `rho u ⊗ u`. -/
 lemma momentumFlux_apply (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
     (time : Time) (position : Space d) (i j : Fin d) :
     momentumFlux d rho velocity time position i j =
@@ -154,11 +161,13 @@ noncomputable def materialAcceleration (d : ℕ) (velocity : VelocityField d) :
     ∂ₜ (fun time' => velocity time' position) time +
       convectiveTerm d velocity time position
 
+/-- The value of the convective term `(u · ∇)u` at a time and position. -/
 lemma convectiveTerm_apply (d : ℕ) (velocity : VelocityField d)
     (time : Time) (position : Space d) :
     convectiveTerm d velocity time position =
       ∑ j, velocity time position j • ∂[j] (velocity time) position := rfl
 
+/-- The value of the material acceleration `∂ₜ u + (u · ∇)u` at a time and position. -/
 lemma materialAcceleration_apply (d : ℕ) (velocity : VelocityField d)
     (time : Time) (position : Space d) :
     materialAcceleration d velocity time position =
@@ -185,5 +194,224 @@ def ConvectiveForm (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
   ContinuityEquation d rho velocity ∧
     ConvectiveMomentumEquation d rho velocity stress bodyForce
 
+/-!
+
+## E. Equivalence of conservative and convective forms
+
+-/
+
+/-- The scalar continuity-equation residual
+`partial_t rho + div (rho u)`. -/
+noncomputable def continuityResidual (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
+    Time → Space d → ℝ :=
+  fun time position =>
+    ∂ₜ (fun time' => rho time' position) time +
+      (∇ ⬝ fun position' => rho time position' • velocity time position') position
+
+/-- The left-hand side of the conservative momentum equation. -/
+noncomputable def conservativeMomentumLHS (d : ℕ) (rho : MassDensity d)
+    (velocity : VelocityField d) : VelocityField d :=
+  fun time position =>
+    ∂ₜ (fun time' => momentumDensity d rho velocity time' position) time +
+      tensorDiv d (momentumFlux d rho velocity time) position
+
+/-- The left-hand side of the convective momentum equation. -/
+noncomputable def convectiveMomentumLHS (d : ℕ) (rho : MassDensity d)
+    (velocity : VelocityField d) : VelocityField d :=
+  fun time position => rho time position • materialAcceleration d velocity time position
+
+/-- 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)) (time : Time)
+    (hRho : DifferentiableAt ℝ rhoAtPosition time)
+    (hVelocity : DifferentiableAt ℝ velocityAtPosition time) :
+    ∂ₜ (fun time' => rhoAtPosition time' • velocityAtPosition time') time =
+      rhoAtPosition time • ∂ₜ velocityAtPosition time +
+        ∂ₜ rhoAtPosition time • velocityAtPosition time := by
+  rw [Time.deriv_eq, Time.deriv_eq, Time.deriv_eq]
+  change (fderiv ℝ (rhoAtPosition • velocityAtPosition) time) 1 =
+    rhoAtPosition time • (fderiv ℝ velocityAtPosition time) 1 +
+      (fderiv ℝ rhoAtPosition time) 1 • velocityAtPosition time
+  rw [fderiv_smul hRho hVelocity]
+  rfl
+
+/-- Product rule for the time derivative of the momentum density `rho u`. -/
+lemma timeDeriv_momentumDensity (d : ℕ) (rho : MassDensity d)
+    (velocity : VelocityField d) (time : Time) (position : Space d)
+    (hRho : DifferentiableAt ℝ (fun time' => rho time' position) time)
+    (hVelocity : DifferentiableAt ℝ (fun time' => velocity time' position) time) :
+    ∂ₜ (fun time' => momentumDensity d rho velocity time' position) time =
+      rho time position • ∂ₜ (fun time' => velocity time' position) time +
+        ∂ₜ (fun time' => rho time' position) time • velocity time position := by
+  simpa [momentumDensity] using
+    timeDeriv_smul_velocity d (fun time' => rho time' position)
+      (fun time' => velocity time' position) time hRho hVelocity
+
+/-- Product rule for one spatial derivative of one component of `rho u ⊗ u`. -/
+lemma spaceDeriv_momentumFlux_component (d : ℕ) (rho : MassDensity d)
+    (velocity : VelocityField d) (time : Time) (position : Space d) (i j : Fin d)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d rho velocity time))
+    (hVelocity : Differentiable ℝ (velocity time)) :
+    ∂[j] (fun position' => momentumFlux d rho velocity time position' i j) position =
+      velocity time position i •
+        ∂[j] (fun position' => momentumDensity d rho velocity time position' j) position +
+      ∂[j] (fun position' => velocity time position' i) position •
+        momentumDensity d rho velocity time position j := by
+  have hProduct := Space.deriv_smul (u := j) (x := position)
+    (c := fun position' => velocity time position' i)
+    (f := fun position' => momentumDensity d rho velocity time position' j)
+    ((differentiable_euclidean.mp hVelocity i).differentiableAt)
+    ((differentiable_euclidean.mp hMomentumDensity j).differentiableAt)
+  rw [← hProduct]
+  congr
+  funext position'
+  simp [momentumFlux, momentumDensity, Matrix.vecMulVec_apply, mul_left_comm]
+
+/-- The tensor divergence of `rho u ⊗ u` split into continuity and convective parts. -/
+lemma tensorDiv_momentumFlux (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (time : Time) (position : Space d)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d rho velocity time))
+    (hVelocity : Differentiable ℝ (velocity time)) :
+    tensorDiv d (momentumFlux d rho velocity time) position =
+      (∇ ⬝ momentumDensity d rho velocity time) position • velocity time position +
+        rho time position • convectiveTerm d velocity time position := by
+  ext i
+  simp [tensorDiv_apply, div, convectiveTerm, smul_eq_mul]
+  change (∑ j, ∂[j] (fun position' =>
+      momentumFlux d rho velocity time position' i j) position) =
+    (∑ j, ∂[j] (fun position' =>
+      momentumDensity d rho velocity time position' j) position) *
+        velocity time position i +
+      rho time position *
+        (∑ j, velocity time position j * ∂[j] (velocity time) position i)
+  calc
+    (∑ j, ∂[j] (fun position' =>
+        momentumFlux d rho velocity time position' i j) position)
+        = ∑ j,
+            (velocity time position i *
+                ∂[j] (fun position' =>
+                  momentumDensity d rho velocity time position' j) position +
+              ∂[j] (fun position' => velocity time position' i) position *
+                momentumDensity d rho velocity time position j) := by
+          apply Finset.sum_congr rfl
+          intro j _
+          rw [spaceDeriv_momentumFlux_component d rho velocity time position i j
+            hMomentumDensity hVelocity]
+          simp [smul_eq_mul]
+    _ = velocity time position i *
+          (∑ j, ∂[j] (fun position' =>
+            momentumDensity d rho velocity time position' j) position) +
+        rho time position *
+          (∑ j, velocity time position j * ∂[j] (velocity time) position i) := by
+          rw [Finset.sum_add_distrib]
+          congr 1
+          · rw [Finset.mul_sum]
+          · rw [Finset.mul_sum]
+            apply Finset.sum_congr rfl
+            intro j _
+            rw [Space.deriv_euclid (ν := j) (μ := i) (f := velocity time) hVelocity position]
+            simp [momentumDensity, mul_comm, mul_assoc]
+    _ = (∑ j, ∂[j] (fun position' =>
+          momentumDensity d rho velocity time position' j) position) *
+          velocity time position i +
+        rho time position *
+          (∑ j, velocity time position j * ∂[j] (velocity time) position 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.
+-/
+lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+    (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (time : Time) (position : Space d)
+    (hRhoTime : DifferentiableAt ℝ (fun time' => rho time' position) time)
+    (hVelocityTime : DifferentiableAt ℝ (fun time' => velocity time' position) time)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d rho velocity time))
+    (hVelocitySpace : Differentiable ℝ (velocity time)) :
+    conservativeMomentumLHS d rho velocity time position =
+      convectiveMomentumLHS d rho velocity time position +
+        continuityResidual d rho velocity time position • velocity time position := by
+  rw [conservativeMomentumLHS, convectiveMomentumLHS, continuityResidual]
+  rw [timeDeriv_momentumDensity d rho velocity time position hRhoTime hVelocityTime]
+  rw [tensorDiv_momentumFlux d rho velocity time position hMomentumDensity hVelocitySpace]
+  ext i
+  simp [materialAcceleration, convectiveTerm, div, momentumDensity, smul_eq_mul]
+  ring_nf
+
+/-- The conservative and convective momentum equations are equivalent when the continuity
+equation holds.
+
+The differentiability assumptions are exactly the product-rule assumptions used to rewrite
+`partial_t (rho u)` and `div_tensor (rho u ⊗ u)`.
+-/
+theorem ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
+    (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (stress : StressTensor d) (bodyForce : BodyForce d)
+    (hContinuity : ContinuityEquation d rho velocity)
+    (hRhoTime : ∀ time position,
+      DifferentiableAt ℝ (fun time' => rho time' position) time)
+    (hVelocityTime : ∀ time position,
+      DifferentiableAt ℝ (fun time' => velocity time' position) time)
+    (hMomentumDensity : ∀ time, Differentiable ℝ (momentumDensity d rho velocity time))
+    (hVelocitySpace : ∀ time, Differentiable ℝ (velocity time)) :
+    ConservativeMomentumEquation d rho velocity stress bodyForce ↔
+      ConvectiveMomentumEquation d rho velocity stress bodyForce := by
+  constructor
+  · intro hConservative time position
+    have hResidual : continuityResidual d rho velocity time position = 0 := by
+      simpa [continuityResidual] using hContinuity time position
+    have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+      d rho velocity time position (hRhoTime time position) (hVelocityTime time position)
+      (hMomentumDensity time) (hVelocitySpace time)
+    have hLhs' :
+        conservativeMomentumLHS d rho velocity time position =
+          convectiveMomentumLHS d rho velocity time position := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    change convectiveMomentumLHS d rho velocity time position =
+      tensorDiv d (stress time) position + rho time position • bodyForce time position
+    rw [← hLhs']
+    exact hConservative time position
+  · intro hConvective time position
+    have hResidual : continuityResidual d rho velocity time position = 0 := by
+      simpa [continuityResidual] using hContinuity time position
+    have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+      d rho velocity time position (hRhoTime time position) (hVelocityTime time position)
+      (hMomentumDensity time) (hVelocitySpace time)
+    have hLhs' :
+        conservativeMomentumLHS d rho velocity time position =
+          convectiveMomentumLHS d rho velocity time position := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    change conservativeMomentumLHS d rho velocity time position =
+      tensorDiv d (stress time) position + rho time position • bodyForce time position
+    rw [hLhs']
+    exact hConvective time position
+
+/-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
+differentiable enough for the product rules. -/
+theorem ConservativeForm_iff_ConvectiveForm
+    (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (stress : StressTensor d) (bodyForce : BodyForce d)
+    (hRhoTime : ∀ time position,
+      DifferentiableAt ℝ (fun time' => rho time' position) time)
+    (hVelocityTime : ∀ time position,
+      DifferentiableAt ℝ (fun time' => velocity time' position) time)
+    (hMomentumDensity : ∀ time, Differentiable ℝ (momentumDensity d rho velocity time))
+    (hVelocitySpace : ∀ time, Differentiable ℝ (velocity time)) :
+    ConservativeForm d rho velocity stress bodyForce ↔
+      ConvectiveForm d rho velocity stress bodyForce := by
+  constructor
+  · intro hConservative
+    refine ⟨hConservative.1, ?_⟩
+    exact (ConservativeMomentumEquation_iff_ConvectiveMomentumEquation d rho velocity stress
+      bodyForce hConservative.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp
+      hConservative.2
+  · intro hConvective
+    refine ⟨hConvective.1, ?_⟩
+    exact (ConservativeMomentumEquation_iff_ConvectiveMomentumEquation d rho velocity stress
+      bodyForce hConvective.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr
+      hConvective.2
+
 end NavierStokes
 end FluidDynamics

From cd7d148d386b5e50722631692d167cc34270ce04 Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Wed, 20 May 2026 12:00:13 +0200
Subject: [PATCH 18/33] refactor(Space): define tensorDiv via div

---
 Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean b/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean
index dcf2b2c1e..1ccadab4b 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean
@@ -6,7 +6,7 @@ Authors: Florian Wiesner
 module
 
 public import Mathlib.Data.Matrix.Basic
-public import Physlib.SpaceAndTime.Space.Derivatives.Basic
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
 /-!
 
 # Tensor divergence on Space
@@ -59,7 +59,7 @@ vector field whose `i`th component is
 -/
 noncomputable def tensorDiv (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ) :
     Space d → EuclideanSpace ℝ (Fin d) := fun x => WithLp.toLp 2 fun i =>
-  ∑ j, ∂[j] (fun x => T x i j) x
+  div (fun y : Space d => WithLp.toLp 2 fun j => T y i j) x
 
 /-!
 
@@ -70,7 +70,8 @@ noncomputable def tensorDiv (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) 
 @[simp]
 lemma tensorDiv_apply (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ)
     (x : Space d) (i : Fin d) :
-    tensorDiv d T x i = ∑ j, ∂[j] (fun x => T x i j) x := rfl
+    tensorDiv d T x i = ∑ j, ∂[j] (fun x => T x i j) x := by
+  simp [tensorDiv, div]
 
 /-!
 

From b2b3ec54507372375159ec03a1792edc3fdf475f Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Wed, 20 May 2026 12:09:23 +0200
Subject: [PATCH 19/33] refactor(FluidDynamics): remove unused apply lemmas

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 26 -------------------
 1 file changed, 26 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 409a5c3f5..f304d10fc 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -98,19 +98,6 @@ def momentumFlux (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
     rho time position • Matrix.vecMulVec
       (fun i => velocity time position i) (fun j => velocity time position j)
 
-/-- The value of `momentumDensity` at a time and position. -/
-lemma momentumDensity_apply (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
-    (time : Time) (position : Space d) :
-    momentumDensity d rho velocity time position =
-      rho time position • velocity time position := rfl
-
-/-- The `(i, j)` component of the convective momentum flux `rho u ⊗ u`. -/
-lemma momentumFlux_apply (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
-    (time : Time) (position : Space d) (i j : Fin d) :
-    momentumFlux d rho velocity time position i j =
-      rho time position * velocity time position i * velocity time position j := by
-  simp [momentumFlux, Matrix.vecMulVec_apply, mul_assoc]
-
 /-!
 
 ## C. Conservative equations
@@ -161,19 +148,6 @@ noncomputable def materialAcceleration (d : ℕ) (velocity : VelocityField d) :
     ∂ₜ (fun time' => velocity time' position) time +
       convectiveTerm d velocity time position
 
-/-- The value of the convective term `(u · ∇)u` at a time and position. -/
-lemma convectiveTerm_apply (d : ℕ) (velocity : VelocityField d)
-    (time : Time) (position : Space d) :
-    convectiveTerm d velocity time position =
-      ∑ j, velocity time position j • ∂[j] (velocity time) position := rfl
-
-/-- The value of the material acceleration `∂ₜ u + (u · ∇)u` at a time and position. -/
-lemma materialAcceleration_apply (d : ℕ) (velocity : VelocityField d)
-    (time : Time) (position : Space d) :
-    materialAcceleration d velocity time position =
-      ∂ₜ (fun time' => velocity time' position) time +
-        convectiveTerm d velocity time position := rfl
-
 /-- Conservation of momentum in convective form.
 
 The equation is

From 8f88ce9202777d8c1dcf6d4d56c0f8da0d55c640 Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Thu, 21 May 2026 13:46:07 +0200
Subject: [PATCH 20/33] refactor(FluidDynamics): add fluid state data

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 289 ++++++++++--------
 1 file changed, 155 insertions(+), 134 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index f304d10fc..18243698a 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -28,6 +28,8 @@ to a Newtonian stress law.
 - `MassDensity` : A time-dependent scalar density field.
 - `VelocityField` : A time-dependent vector velocity field.
 - `StressTensor` : A time-dependent matrix-valued stress field.
+- `FluidState` : The density and velocity fields of a fluid.
+- `MomentumBalanceData` : The fluid state together with stress and body force.
 - `momentumDensity` : The vector momentum density `rho u`.
 - `momentumFlux` : The convective momentum flux `rho u ⊗ u`.
 - `convectiveTerm` : The nonlinear transport term `(u · ∇)u`.
@@ -45,10 +47,11 @@ to a Newtonian stress law.
 ## iii. Table of contents
 
 - A. Field types
-- B. Momentum fields
-- C. Conservative equations
-- D. Convective equations
-- E. Equivalence of conservative and convective forms
+- B. Fluid and momentum-balance data
+- C. Momentum fields
+- D. Conservative equations
+- E. Convective equations
+- F. Equivalence of conservative and convective forms
 
 ## iv. References
 
@@ -82,34 +85,53 @@ abbrev BodyForce (d : ℕ) := Time → Space d → EuclideanSpace ℝ (Fin d)
 
 /-!
 
-## B. Momentum fields
+## B. Fluid and momentum-balance data
+
+-/
+
+/-- 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 data needed for a momentum balance: fluid state, stress, and body force. -/
+structure MomentumBalanceData (d : ℕ) extends FluidState d where
+  /-- The stress tensor field. -/
+  stress : StressTensor d
+  /-- The body-force field per unit mass. -/
+  bodyForce : BodyForce d
+
+/-!
+
+## C. Momentum fields
 
 -/
 
 /-- The momentum density `rho u`. -/
-def momentumDensity (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
-    VelocityField d :=
-  fun time position => rho time position • velocity time position
+def momentumDensity (d : ℕ) (fluid : FluidState d) : VelocityField d :=
+  fun time position => fluid.rho time position • fluid.velocity time position
 
 /-- The convective momentum flux `rho u ⊗ u`. -/
-def momentumFlux (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
+def momentumFlux (d : ℕ) (fluid : FluidState d) :
     Time → Space d → Matrix (Fin d) (Fin d) ℝ :=
   fun time position =>
-    rho time position • Matrix.vecMulVec
-      (fun i => velocity time position i) (fun j => velocity time position j)
+    fluid.rho time position • Matrix.vecMulVec
+      (fun i => fluid.velocity time position i) (fun j => fluid.velocity time position j)
 
 /-!
 
-## C. Conservative equations
+## D. Conservative equations
 
 -/
 
 /-- Conservation of mass in conservative form, `partial_t rho + div (rho u) = 0`. -/
-def ContinuityEquation (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
-    Prop :=
+def ContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
   ∀ time position,
-    ∂ₜ (fun time' => rho time' position) time +
-      (∇ ⬝ fun position' => rho time position' • velocity time position') position = 0
+    ∂ₜ (fun time' => fluid.rho time' position) time +
+      (∇ ⬝ fun position' => fluid.rho time position' • fluid.velocity time position') position =
+        0
 
 /-- Conservation of momentum in conservative tensor-divergence form.
 
@@ -119,22 +141,21 @@ The equation is
 
 Here `stress` is intentionally not yet specialized to a Newtonian stress law.
 -/
-def ConservativeMomentumEquation (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
-    (stress : StressTensor d) (bodyForce : BodyForce d) : Prop :=
+def ConservativeMomentumEquation (d : ℕ) (data : MomentumBalanceData d) : Prop :=
   ∀ time position,
-    ∂ₜ (fun time' => momentumDensity d rho velocity time' position) time +
-        tensorDiv d (momentumFlux d rho velocity time) position =
-      tensorDiv d (stress time) position + rho time position • bodyForce time position
+    ∂ₜ (fun time' => momentumDensity d data.toFluidState time' position) time +
+        tensorDiv d (momentumFlux d data.toFluidState time) position =
+      tensorDiv d (data.stress time) position +
+        data.rho time position • data.bodyForce time position
 
 /-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
-def ConservativeForm (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
-    (stress : StressTensor d) (bodyForce : BodyForce d) : Prop :=
-  ContinuityEquation d rho velocity ∧
-    ConservativeMomentumEquation d rho velocity stress bodyForce
+def ConservativeForm (d : ℕ) (data : MomentumBalanceData d) : Prop :=
+  ContinuityEquation d data.toFluidState ∧
+    ConservativeMomentumEquation d data
 
 /-!
 
-## D. Convective equations
+## E. Convective equations
 
 -/
 
@@ -156,43 +177,40 @@ The equation is
 
 Here `stress` is intentionally not yet specialized to a Newtonian stress law.
 -/
-def ConvectiveMomentumEquation (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
-    (stress : StressTensor d) (bodyForce : BodyForce d) : Prop :=
+def ConvectiveMomentumEquation (d : ℕ) (data : MomentumBalanceData d) : Prop :=
   ∀ time position,
-    rho time position • materialAcceleration d velocity time position =
-      tensorDiv d (stress time) position + rho time position • bodyForce time position
+    data.rho time position • materialAcceleration d data.velocity time position =
+      tensorDiv d (data.stress time) position +
+        data.rho time position • data.bodyForce time position
 
 /-- The convective Navier-Stokes form with an externally supplied stress tensor. -/
-def ConvectiveForm (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
-    (stress : StressTensor d) (bodyForce : BodyForce d) : Prop :=
-  ContinuityEquation d rho velocity ∧
-    ConvectiveMomentumEquation d rho velocity stress bodyForce
+def ConvectiveForm (d : ℕ) (data : MomentumBalanceData d) : Prop :=
+  ContinuityEquation d data.toFluidState ∧
+    ConvectiveMomentumEquation d data
 
 /-!
 
-## E. Equivalence of conservative and convective forms
+## F. Equivalence of conservative and convective forms
 
 -/
 
 /-- The scalar continuity-equation residual
 `partial_t rho + div (rho u)`. -/
-noncomputable def continuityResidual (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d) :
+noncomputable def continuityResidual (d : ℕ) (fluid : FluidState d) :
     Time → Space d → ℝ :=
   fun time position =>
-    ∂ₜ (fun time' => rho time' position) time +
-      (∇ ⬝ fun position' => rho time position' • velocity time position') position
+    ∂ₜ (fun time' => fluid.rho time' position) time +
+      (∇ ⬝ fun position' => fluid.rho time position' • fluid.velocity time position') position
 
 /-- The left-hand side of the conservative momentum equation. -/
-noncomputable def conservativeMomentumLHS (d : ℕ) (rho : MassDensity d)
-    (velocity : VelocityField d) : VelocityField d :=
+noncomputable def conservativeMomentumLHS (d : ℕ) (fluid : FluidState d) : VelocityField d :=
   fun time position =>
-    ∂ₜ (fun time' => momentumDensity d rho velocity time' position) time +
-      tensorDiv d (momentumFlux d rho velocity time) position
+    ∂ₜ (fun time' => momentumDensity d fluid time' position) time +
+      tensorDiv d (momentumFlux d fluid time) position
 
 /-- The left-hand side of the convective momentum equation. -/
-noncomputable def convectiveMomentumLHS (d : ℕ) (rho : MassDensity d)
-    (velocity : VelocityField d) : VelocityField d :=
-  fun time position => rho time position • materialAcceleration d velocity time position
+noncomputable def convectiveMomentumLHS (d : ℕ) (fluid : FluidState d) : VelocityField d :=
+  fun time position => fluid.rho time position • materialAcceleration d fluid.velocity time position
 
 /-- Product rule for the time derivative of a scalar field times a velocity field. -/
 lemma timeDeriv_smul_velocity (d : ℕ) (rhoAtPosition : Time → ℝ)
@@ -210,30 +228,30 @@ lemma timeDeriv_smul_velocity (d : ℕ) (rhoAtPosition : Time → ℝ)
   rfl
 
 /-- Product rule for the time derivative of the momentum density `rho u`. -/
-lemma timeDeriv_momentumDensity (d : ℕ) (rho : MassDensity d)
-    (velocity : VelocityField d) (time : Time) (position : Space d)
-    (hRho : DifferentiableAt ℝ (fun time' => rho time' position) time)
-    (hVelocity : DifferentiableAt ℝ (fun time' => velocity time' position) time) :
-    ∂ₜ (fun time' => momentumDensity d rho velocity time' position) time =
-      rho time position • ∂ₜ (fun time' => velocity time' position) time +
-        ∂ₜ (fun time' => rho time' position) time • velocity time position := by
+lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidState d)
+    (time : Time) (position : Space d)
+    (hRho : DifferentiableAt ℝ (fun time' => fluid.rho time' position) time)
+    (hVelocity : DifferentiableAt ℝ (fun time' => fluid.velocity time' position) time) :
+    ∂ₜ (fun time' => momentumDensity d fluid time' position) time =
+      fluid.rho time position • ∂ₜ (fun time' => fluid.velocity time' position) time +
+        ∂ₜ (fun time' => fluid.rho time' position) time • fluid.velocity time position := by
   simpa [momentumDensity] using
-    timeDeriv_smul_velocity d (fun time' => rho time' position)
-      (fun time' => velocity time' position) time hRho hVelocity
+    timeDeriv_smul_velocity d (fun time' => fluid.rho time' position)
+      (fun time' => fluid.velocity time' position) time hRho hVelocity
 
 /-- Product rule for one spatial derivative of one component of `rho u ⊗ u`. -/
-lemma spaceDeriv_momentumFlux_component (d : ℕ) (rho : MassDensity d)
-    (velocity : VelocityField d) (time : Time) (position : Space d) (i j : Fin d)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d rho velocity time))
-    (hVelocity : Differentiable ℝ (velocity time)) :
-    ∂[j] (fun position' => momentumFlux d rho velocity time position' i j) position =
-      velocity time position i •
-        ∂[j] (fun position' => momentumDensity d rho velocity time position' j) position +
-      ∂[j] (fun position' => velocity time position' i) position •
-        momentumDensity d rho velocity time position j := by
+lemma spaceDeriv_momentumFlux_component (d : ℕ) (fluid : FluidState d)
+    (time : Time) (position : Space d) (i j : Fin d)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
+    (hVelocity : Differentiable ℝ (fluid.velocity time)) :
+    ∂[j] (fun position' => momentumFlux d fluid time position' i j) position =
+      fluid.velocity time position i •
+        ∂[j] (fun position' => momentumDensity d fluid time position' j) position +
+      ∂[j] (fun position' => fluid.velocity time position' i) position •
+        momentumDensity d fluid time position j := by
   have hProduct := Space.deriv_smul (u := j) (x := position)
-    (c := fun position' => velocity time position' i)
-    (f := fun position' => momentumDensity d rho velocity time position' j)
+    (c := fun position' => fluid.velocity time position' i)
+    (f := fun position' => momentumDensity d fluid time position' j)
     ((differentiable_euclidean.mp hVelocity i).differentiableAt)
     ((differentiable_euclidean.mp hMomentumDensity j).differentiableAt)
   rw [← hProduct]
@@ -242,54 +260,55 @@ lemma spaceDeriv_momentumFlux_component (d : ℕ) (rho : MassDensity d)
   simp [momentumFlux, momentumDensity, Matrix.vecMulVec_apply, mul_left_comm]
 
 /-- The tensor divergence of `rho u ⊗ u` split into continuity and convective parts. -/
-lemma tensorDiv_momentumFlux (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+lemma tensorDiv_momentumFlux (d : ℕ) (fluid : FluidState d)
     (time : Time) (position : Space d)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d rho velocity time))
-    (hVelocity : Differentiable ℝ (velocity time)) :
-    tensorDiv d (momentumFlux d rho velocity time) position =
-      (∇ ⬝ momentumDensity d rho velocity time) position • velocity time position +
-        rho time position • convectiveTerm d velocity time position := by
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
+    (hVelocity : Differentiable ℝ (fluid.velocity time)) :
+    tensorDiv d (momentumFlux d fluid time) position =
+      (∇ ⬝ momentumDensity d fluid time) position • fluid.velocity time position +
+        fluid.rho time position • convectiveTerm d fluid.velocity time position := by
   ext i
   simp [tensorDiv_apply, div, convectiveTerm, smul_eq_mul]
   change (∑ j, ∂[j] (fun position' =>
-      momentumFlux d rho velocity time position' i j) position) =
+      momentumFlux d fluid time position' i j) position) =
     (∑ j, ∂[j] (fun position' =>
-      momentumDensity d rho velocity time position' j) position) *
-        velocity time position i +
-      rho time position *
-        (∑ j, velocity time position j * ∂[j] (velocity time) position i)
+      momentumDensity d fluid time position' j) position) *
+        fluid.velocity time position i +
+      fluid.rho time position *
+        (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i)
   calc
     (∑ j, ∂[j] (fun position' =>
-        momentumFlux d rho velocity time position' i j) position)
+        momentumFlux d fluid time position' i j) position)
         = ∑ j,
-            (velocity time position i *
+            (fluid.velocity time position i *
                 ∂[j] (fun position' =>
-                  momentumDensity d rho velocity time position' j) position +
-              ∂[j] (fun position' => velocity time position' i) position *
-                momentumDensity d rho velocity time position j) := by
+                  momentumDensity d fluid time position' j) position +
+              ∂[j] (fun position' => fluid.velocity time position' i) position *
+                momentumDensity d fluid time position j) := by
           apply Finset.sum_congr rfl
           intro j _
-          rw [spaceDeriv_momentumFlux_component d rho velocity time position i j
+          rw [spaceDeriv_momentumFlux_component d fluid time position i j
             hMomentumDensity hVelocity]
           simp [smul_eq_mul]
-    _ = velocity time position i *
+    _ = fluid.velocity time position i *
           (∑ j, ∂[j] (fun position' =>
-            momentumDensity d rho velocity time position' j) position) +
-        rho time position *
-          (∑ j, velocity time position j * ∂[j] (velocity time) position i) := by
+            momentumDensity d fluid time position' j) position) +
+        fluid.rho time position *
+          (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i) := by
           rw [Finset.sum_add_distrib]
           congr 1
           · rw [Finset.mul_sum]
           · rw [Finset.mul_sum]
             apply Finset.sum_congr rfl
             intro j _
-            rw [Space.deriv_euclid (ν := j) (μ := i) (f := velocity time) hVelocity position]
+            rw [Space.deriv_euclid (ν := j) (μ := i) (f := fluid.velocity time)
+              hVelocity position]
             simp [momentumDensity, mul_comm, mul_assoc]
     _ = (∑ j, ∂[j] (fun position' =>
-          momentumDensity d rho velocity time position' j) position) *
-          velocity time position i +
-        rho time position *
-          (∑ j, velocity time position j * ∂[j] (velocity time) position i) := by
+          momentumDensity d fluid time position' j) position) *
+          fluid.velocity time position i +
+        fluid.rho time position *
+          (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i) := by
           ring
 
 /-- The algebraic bridge between conservative and convective momentum.
@@ -298,18 +317,18 @@ 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 : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
+    (d : ℕ) (fluid : FluidState d)
     (time : Time) (position : Space d)
-    (hRhoTime : DifferentiableAt ℝ (fun time' => rho time' position) time)
-    (hVelocityTime : DifferentiableAt ℝ (fun time' => velocity time' position) time)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d rho velocity time))
-    (hVelocitySpace : Differentiable ℝ (velocity time)) :
-    conservativeMomentumLHS d rho velocity time position =
-      convectiveMomentumLHS d rho velocity time position +
-        continuityResidual d rho velocity time position • velocity time position := by
+    (hRhoTime : DifferentiableAt ℝ (fun time' => fluid.rho time' position) time)
+    (hVelocityTime : DifferentiableAt ℝ (fun time' => fluid.velocity time' position) time)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
+    (hVelocitySpace : Differentiable ℝ (fluid.velocity time)) :
+    conservativeMomentumLHS d fluid time position =
+      convectiveMomentumLHS d fluid time position +
+        continuityResidual d fluid time position • fluid.velocity time position := by
   rw [conservativeMomentumLHS, convectiveMomentumLHS, continuityResidual]
-  rw [timeDeriv_momentumDensity d rho velocity time position hRhoTime hVelocityTime]
-  rw [tensorDiv_momentumFlux d rho velocity time position hMomentumDensity hVelocitySpace]
+  rw [timeDeriv_momentumDensity d fluid time position hRhoTime hVelocityTime]
+  rw [tensorDiv_momentumFlux d fluid time position hMomentumDensity hVelocitySpace]
   ext i
   simp [materialAcceleration, convectiveTerm, div, momentumDensity, smul_eq_mul]
   ring_nf
@@ -321,70 +340,72 @@ The differentiability assumptions are exactly the product-rule assumptions used
 `partial_t (rho u)` and `div_tensor (rho u ⊗ u)`.
 -/
 theorem ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
-    (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
-    (stress : StressTensor d) (bodyForce : BodyForce d)
-    (hContinuity : ContinuityEquation d rho velocity)
+    (d : ℕ) (data : MomentumBalanceData d)
+    (hContinuity : ContinuityEquation d data.toFluidState)
     (hRhoTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => rho time' position) time)
+      DifferentiableAt ℝ (fun time' => data.rho time' position) time)
     (hVelocityTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => velocity time' position) time)
-    (hMomentumDensity : ∀ time, Differentiable ℝ (momentumDensity d rho velocity time))
-    (hVelocitySpace : ∀ time, Differentiable ℝ (velocity time)) :
-    ConservativeMomentumEquation d rho velocity stress bodyForce ↔
-      ConvectiveMomentumEquation d rho velocity stress bodyForce := by
+      DifferentiableAt ℝ (fun time' => data.velocity time' position) time)
+    (hMomentumDensity : ∀ time,
+      Differentiable ℝ (momentumDensity d data.toFluidState time))
+    (hVelocitySpace : ∀ time, Differentiable ℝ (data.velocity time)) :
+    ConservativeMomentumEquation d data ↔
+      ConvectiveMomentumEquation d data := by
   constructor
   · intro hConservative time position
-    have hResidual : continuityResidual d rho velocity time position = 0 := by
+    have hResidual : continuityResidual d data.toFluidState time position = 0 := by
       simpa [continuityResidual] using hContinuity time position
     have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-      d rho velocity time position (hRhoTime time position) (hVelocityTime time position)
+      d data.toFluidState time position (hRhoTime time position) (hVelocityTime time position)
       (hMomentumDensity time) (hVelocitySpace time)
     have hLhs' :
-        conservativeMomentumLHS d rho velocity time position =
-          convectiveMomentumLHS d rho velocity time position := by
+        conservativeMomentumLHS d data.toFluidState time position =
+          convectiveMomentumLHS d data.toFluidState time position := by
       rw [hLhs, hResidual, zero_smul, add_zero]
-    change convectiveMomentumLHS d rho velocity time position =
-      tensorDiv d (stress time) position + rho time position • bodyForce time position
+    change convectiveMomentumLHS d data.toFluidState time position =
+      tensorDiv d (data.stress time) position +
+        data.rho time position • data.bodyForce time position
     rw [← hLhs']
     exact hConservative time position
   · intro hConvective time position
-    have hResidual : continuityResidual d rho velocity time position = 0 := by
+    have hResidual : continuityResidual d data.toFluidState time position = 0 := by
       simpa [continuityResidual] using hContinuity time position
     have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-      d rho velocity time position (hRhoTime time position) (hVelocityTime time position)
+      d data.toFluidState time position (hRhoTime time position) (hVelocityTime time position)
       (hMomentumDensity time) (hVelocitySpace time)
     have hLhs' :
-        conservativeMomentumLHS d rho velocity time position =
-          convectiveMomentumLHS d rho velocity time position := by
+        conservativeMomentumLHS d data.toFluidState time position =
+          convectiveMomentumLHS d data.toFluidState time position := by
       rw [hLhs, hResidual, zero_smul, add_zero]
-    change conservativeMomentumLHS d rho velocity time position =
-      tensorDiv d (stress time) position + rho time position • bodyForce time position
+    change conservativeMomentumLHS d data.toFluidState time position =
+      tensorDiv d (data.stress time) position +
+        data.rho time position • data.bodyForce time position
     rw [hLhs']
     exact hConvective time position
 
 /-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
 differentiable enough for the product rules. -/
 theorem ConservativeForm_iff_ConvectiveForm
-    (d : ℕ) (rho : MassDensity d) (velocity : VelocityField d)
-    (stress : StressTensor d) (bodyForce : BodyForce d)
+    (d : ℕ) (data : MomentumBalanceData d)
     (hRhoTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => rho time' position) time)
+      DifferentiableAt ℝ (fun time' => data.rho time' position) time)
     (hVelocityTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => velocity time' position) time)
-    (hMomentumDensity : ∀ time, Differentiable ℝ (momentumDensity d rho velocity time))
-    (hVelocitySpace : ∀ time, Differentiable ℝ (velocity time)) :
-    ConservativeForm d rho velocity stress bodyForce ↔
-      ConvectiveForm d rho velocity stress bodyForce := by
+      DifferentiableAt ℝ (fun time' => data.velocity time' position) time)
+    (hMomentumDensity : ∀ time,
+      Differentiable ℝ (momentumDensity d data.toFluidState time))
+    (hVelocitySpace : ∀ time, Differentiable ℝ (data.velocity time)) :
+    ConservativeForm d data ↔
+      ConvectiveForm d data := by
   constructor
   · intro hConservative
     refine ⟨hConservative.1, ?_⟩
-    exact (ConservativeMomentumEquation_iff_ConvectiveMomentumEquation d rho velocity stress
-      bodyForce hConservative.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp
+    exact (ConservativeMomentumEquation_iff_ConvectiveMomentumEquation d data hConservative.1
+      hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp
       hConservative.2
   · intro hConvective
     refine ⟨hConvective.1, ?_⟩
-    exact (ConservativeMomentumEquation_iff_ConvectiveMomentumEquation d rho velocity stress
-      bodyForce hConvective.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr
+    exact (ConservativeMomentumEquation_iff_ConvectiveMomentumEquation d data hConvective.1
+      hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr
       hConvective.2
 
 end NavierStokes

From e7a6370f4f92041f9a46ca455d7e9119d707cbfa Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Thu, 21 May 2026 15:20:15 +0200
Subject: [PATCH 21/33] refactor(FluidDynamics): split Navier-Stokes modules

---
 Physlib.lean                                  |   5 +-
 Physlib/FluidDynamics/FluidState.lean         |  92 +++++
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 345 +-----------------
 .../NavierStokes/Continuity.lean              |  63 ++++
 .../FluidDynamics/NavierStokes/Momentum.lean  | 306 ++++++++++++++++
 .../{TensorDiv.lean => MatrixDiv.lean}        |  55 ++-
 6 files changed, 501 insertions(+), 365 deletions(-)
 create mode 100644 Physlib/FluidDynamics/FluidState.lean
 create mode 100644 Physlib/FluidDynamics/NavierStokes/Continuity.lean
 create mode 100644 Physlib/FluidDynamics/NavierStokes/Momentum.lean
 rename Physlib/SpaceAndTime/Space/Derivatives/{TensorDiv.lean => MatrixDiv.lean} (57%)

diff --git a/Physlib.lean b/Physlib.lean
index 996cdce21..e773852d8 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -50,7 +50,10 @@ 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.Mathematics.Calculus.AdjFDeriv
 public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
@@ -361,8 +364,8 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Div
 public import Physlib.SpaceAndTime.Space.Derivatives.Grad
 public import Physlib.SpaceAndTime.Space.Derivatives.Iterated
 public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian
+public import Physlib.SpaceAndTime.Space.Derivatives.MatrixDiv
 public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex
-public import Physlib.SpaceAndTime.Space.Derivatives.TensorDiv
 public import Physlib.SpaceAndTime.Space.DistConst
 public import Physlib.SpaceAndTime.Space.DistOfFunction
 public import Physlib.SpaceAndTime.Space.Integrals.Basic
diff --git a/Physlib/FluidDynamics/FluidState.lean b/Physlib/FluidDynamics/FluidState.lean
new file mode 100644
index 000000000..2ce450f0d
--- /dev/null
+++ b/Physlib/FluidDynamics/FluidState.lean
@@ -0,0 +1,92 @@
+/-
+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.
+- `MomentumBalanceFields` : 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 MomentumBalanceFields (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/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 18243698a..9c0c0f159 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -5,10 +5,7 @@ Authors: Florian Wiesner
 -/
 module
 
-public import Mathlib.Data.Matrix.Mul
-public import Physlib.SpaceAndTime.Space.Derivatives.Div
-public import Physlib.SpaceAndTime.Space.Derivatives.TensorDiv
-public import Physlib.SpaceAndTime.Time.Derivatives
+public import Physlib.FluidDynamics.NavierStokes.Momentum
 /-!
 
 # The Navier-Stokes equations
@@ -19,39 +16,20 @@ 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 starts with the conservative tensor-divergence form and the convective form. 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 combines the continuity equation with the conservative and convective momentum
+equations. 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
 
-- `MassDensity` : A time-dependent scalar density field.
-- `VelocityField` : A time-dependent vector velocity field.
-- `StressTensor` : A time-dependent matrix-valued stress field.
-- `FluidState` : The density and velocity fields of a fluid.
-- `MomentumBalanceData` : The fluid state together with stress and body force.
-- `momentumDensity` : The vector momentum density `rho u`.
-- `momentumFlux` : The convective momentum flux `rho u ⊗ u`.
-- `convectiveTerm` : The nonlinear transport term `(u · ∇)u`.
-- `materialAcceleration` : The material acceleration `∂ₜ u + (u · ∇)u`.
-- `ContinuityEquation` : Conservation of mass.
-- `ConservativeMomentumEquation` : Conservation of momentum using `Space.tensorDiv`.
 - `ConservativeForm` : Continuity and conservative momentum equations together.
-- `ConvectiveMomentumEquation` : The momentum equation in convective form.
 - `ConvectiveForm` : Continuity and convective momentum equations together.
-- `ConservativeMomentumEquation_iff_ConvectiveMomentumEquation` : Equivalence of the two
-  momentum equations when continuity holds and the fields are differentiable.
 - `ConservativeForm_iff_ConvectiveForm` : Equivalence of the two forms when the
   fields are differentiable.
 
 ## iii. Table of contents
 
-- A. Field types
-- B. Fluid and momentum-balance data
-- C. Momentum fields
-- D. Conservative equations
-- E. Convective equations
-- F. Equivalence of conservative and convective forms
+- A. Full Navier-Stokes forms
 
 ## iv. References
 
@@ -59,334 +37,29 @@ to a Newtonian stress law.
 
 @[expose] public section
 
-open Space
-open Time
-
 namespace FluidDynamics
 namespace NavierStokes
 
 /-!
 
-## A. Field types
-
--/
-
-/-- A mass density field on `d`-dimensional space. -/
-abbrev MassDensity (d : ℕ) := Time → Space d → ℝ
-
-/-- A velocity field on `d`-dimensional space. -/
-abbrev VelocityField (d : ℕ) := Time → Space d → EuclideanSpace ℝ (Fin 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 : ℕ) := Time → Space d → EuclideanSpace ℝ (Fin d)
-
-/-!
-
-## B. Fluid and momentum-balance data
-
--/
-
-/-- 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 data needed for a momentum balance: fluid state, stress, and body force. -/
-structure MomentumBalanceData (d : ℕ) extends FluidState d where
-  /-- The stress tensor field. -/
-  stress : StressTensor d
-  /-- The body-force field per unit mass. -/
-  bodyForce : BodyForce d
-
-/-!
-
-## C. Momentum fields
+## A. Full Navier-Stokes forms
 
 -/
 
-/-- The momentum density `rho u`. -/
-def momentumDensity (d : ℕ) (fluid : FluidState d) : VelocityField d :=
-  fun time position => fluid.rho time position • fluid.velocity time position
-
-/-- The convective momentum flux `rho u ⊗ u`. -/
-def momentumFlux (d : ℕ) (fluid : FluidState d) :
-    Time → Space d → Matrix (Fin d) (Fin d) ℝ :=
-  fun time position =>
-    fluid.rho time position • Matrix.vecMulVec
-      (fun i => fluid.velocity time position i) (fun j => fluid.velocity time position j)
-
-/-!
-
-## D. Conservative equations
-
--/
-
-/-- Conservation of mass in conservative form, `partial_t rho + div (rho u) = 0`. -/
-def ContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
-  ∀ time position,
-    ∂ₜ (fun time' => fluid.rho time' position) time +
-      (∇ ⬝ fun position' => fluid.rho time position' • fluid.velocity time position') position =
-        0
-
-/-- Conservation of momentum in conservative tensor-divergence form.
-
-The equation is
-
-`partial_t (rho u) + div_tensor (rho u ⊗ u) = div_tensor sigma + rho f`.
-
-Here `stress` is intentionally not yet specialized to a Newtonian stress law.
--/
-def ConservativeMomentumEquation (d : ℕ) (data : MomentumBalanceData d) : Prop :=
-  ∀ time position,
-    ∂ₜ (fun time' => momentumDensity d data.toFluidState time' position) time +
-        tensorDiv d (momentumFlux d data.toFluidState time) position =
-      tensorDiv d (data.stress time) position +
-        data.rho time position • data.bodyForce time position
-
 /-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
-def ConservativeForm (d : ℕ) (data : MomentumBalanceData d) : Prop :=
+def ConservativeForm (d : ℕ) (data : MomentumBalanceFields d) : Prop :=
   ContinuityEquation d data.toFluidState ∧
     ConservativeMomentumEquation d data
 
-/-!
-
-## E. Convective equations
-
--/
-
-/-- The nonlinear transport term `(u · ∇)u`. -/
-noncomputable def convectiveTerm (d : ℕ) (velocity : VelocityField d) : VelocityField d :=
-  fun time position => ∑ j, velocity time position j • ∂[j] (velocity time) position
-
-/-- The material acceleration `∂ₜ u + (u · ∇)u`. -/
-noncomputable def materialAcceleration (d : ℕ) (velocity : VelocityField d) : VelocityField d :=
-  fun time position =>
-    ∂ₜ (fun time' => velocity time' position) time +
-      convectiveTerm d velocity time position
-
-/-- Conservation of momentum in convective form.
-
-The equation is
-
-`rho (partial_t u + (u · ∇)u) = div_tensor sigma + rho f`.
-
-Here `stress` is intentionally not yet specialized to a Newtonian stress law.
--/
-def ConvectiveMomentumEquation (d : ℕ) (data : MomentumBalanceData d) : Prop :=
-  ∀ time position,
-    data.rho time position • materialAcceleration d data.velocity time position =
-      tensorDiv d (data.stress time) position +
-        data.rho time position • data.bodyForce time position
-
 /-- The convective Navier-Stokes form with an externally supplied stress tensor. -/
-def ConvectiveForm (d : ℕ) (data : MomentumBalanceData d) : Prop :=
+def ConvectiveForm (d : ℕ) (data : MomentumBalanceFields d) : Prop :=
   ContinuityEquation d data.toFluidState ∧
     ConvectiveMomentumEquation d data
 
-/-!
-
-## F. Equivalence of conservative and convective forms
-
--/
-
-/-- The scalar continuity-equation residual
-`partial_t rho + div (rho u)`. -/
-noncomputable def continuityResidual (d : ℕ) (fluid : FluidState d) :
-    Time → Space d → ℝ :=
-  fun time position =>
-    ∂ₜ (fun time' => fluid.rho time' position) time +
-      (∇ ⬝ fun position' => fluid.rho time position' • fluid.velocity time position') position
-
-/-- The left-hand side of the conservative momentum equation. -/
-noncomputable def conservativeMomentumLHS (d : ℕ) (fluid : FluidState d) : VelocityField d :=
-  fun time position =>
-    ∂ₜ (fun time' => momentumDensity d fluid time' position) time +
-      tensorDiv d (momentumFlux d fluid time) position
-
-/-- The left-hand side of the convective momentum equation. -/
-noncomputable def convectiveMomentumLHS (d : ℕ) (fluid : FluidState d) : VelocityField d :=
-  fun time position => fluid.rho time position • materialAcceleration d fluid.velocity time position
-
-/-- 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)) (time : Time)
-    (hRho : DifferentiableAt ℝ rhoAtPosition time)
-    (hVelocity : DifferentiableAt ℝ velocityAtPosition time) :
-    ∂ₜ (fun time' => rhoAtPosition time' • velocityAtPosition time') time =
-      rhoAtPosition time • ∂ₜ velocityAtPosition time +
-        ∂ₜ rhoAtPosition time • velocityAtPosition time := by
-  rw [Time.deriv_eq, Time.deriv_eq, Time.deriv_eq]
-  change (fderiv ℝ (rhoAtPosition • velocityAtPosition) time) 1 =
-    rhoAtPosition time • (fderiv ℝ velocityAtPosition time) 1 +
-      (fderiv ℝ rhoAtPosition time) 1 • velocityAtPosition time
-  rw [fderiv_smul hRho hVelocity]
-  rfl
-
-/-- Product rule for the time derivative of the momentum density `rho u`. -/
-lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidState d)
-    (time : Time) (position : Space d)
-    (hRho : DifferentiableAt ℝ (fun time' => fluid.rho time' position) time)
-    (hVelocity : DifferentiableAt ℝ (fun time' => fluid.velocity time' position) time) :
-    ∂ₜ (fun time' => momentumDensity d fluid time' position) time =
-      fluid.rho time position • ∂ₜ (fun time' => fluid.velocity time' position) time +
-        ∂ₜ (fun time' => fluid.rho time' position) time • fluid.velocity time position := by
-  simpa [momentumDensity] using
-    timeDeriv_smul_velocity d (fun time' => fluid.rho time' position)
-      (fun time' => fluid.velocity time' position) time hRho hVelocity
-
-/-- Product rule for one spatial derivative of one component of `rho u ⊗ u`. -/
-lemma spaceDeriv_momentumFlux_component (d : ℕ) (fluid : FluidState d)
-    (time : Time) (position : Space d) (i j : Fin d)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
-    (hVelocity : Differentiable ℝ (fluid.velocity time)) :
-    ∂[j] (fun position' => momentumFlux d fluid time position' i j) position =
-      fluid.velocity time position i •
-        ∂[j] (fun position' => momentumDensity d fluid time position' j) position +
-      ∂[j] (fun position' => fluid.velocity time position' i) position •
-        momentumDensity d fluid time position j := by
-  have hProduct := Space.deriv_smul (u := j) (x := position)
-    (c := fun position' => fluid.velocity time position' i)
-    (f := fun position' => momentumDensity d fluid time position' j)
-    ((differentiable_euclidean.mp hVelocity i).differentiableAt)
-    ((differentiable_euclidean.mp hMomentumDensity j).differentiableAt)
-  rw [← hProduct]
-  congr
-  funext position'
-  simp [momentumFlux, momentumDensity, Matrix.vecMulVec_apply, mul_left_comm]
-
-/-- The tensor divergence of `rho u ⊗ u` split into continuity and convective parts. -/
-lemma tensorDiv_momentumFlux (d : ℕ) (fluid : FluidState d)
-    (time : Time) (position : Space d)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
-    (hVelocity : Differentiable ℝ (fluid.velocity time)) :
-    tensorDiv d (momentumFlux d fluid time) position =
-      (∇ ⬝ momentumDensity d fluid time) position • fluid.velocity time position +
-        fluid.rho time position • convectiveTerm d fluid.velocity time position := by
-  ext i
-  simp [tensorDiv_apply, div, convectiveTerm, smul_eq_mul]
-  change (∑ j, ∂[j] (fun position' =>
-      momentumFlux d fluid time position' i j) position) =
-    (∑ j, ∂[j] (fun position' =>
-      momentumDensity d fluid time position' j) position) *
-        fluid.velocity time position i +
-      fluid.rho time position *
-        (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i)
-  calc
-    (∑ j, ∂[j] (fun position' =>
-        momentumFlux d fluid time position' i j) position)
-        = ∑ j,
-            (fluid.velocity time position i *
-                ∂[j] (fun position' =>
-                  momentumDensity d fluid time position' j) position +
-              ∂[j] (fun position' => fluid.velocity time position' i) position *
-                momentumDensity d fluid time position j) := by
-          apply Finset.sum_congr rfl
-          intro j _
-          rw [spaceDeriv_momentumFlux_component d fluid time position i j
-            hMomentumDensity hVelocity]
-          simp [smul_eq_mul]
-    _ = fluid.velocity time position i *
-          (∑ j, ∂[j] (fun position' =>
-            momentumDensity d fluid time position' j) position) +
-        fluid.rho time position *
-          (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i) := by
-          rw [Finset.sum_add_distrib]
-          congr 1
-          · rw [Finset.mul_sum]
-          · rw [Finset.mul_sum]
-            apply Finset.sum_congr rfl
-            intro j _
-            rw [Space.deriv_euclid (ν := j) (μ := i) (f := fluid.velocity time)
-              hVelocity position]
-            simp [momentumDensity, mul_comm, mul_assoc]
-    _ = (∑ j, ∂[j] (fun position' =>
-          momentumDensity d fluid time position' j) position) *
-          fluid.velocity time position i +
-        fluid.rho time position *
-          (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position 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.
--/
-lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-    (d : ℕ) (fluid : FluidState d)
-    (time : Time) (position : Space d)
-    (hRhoTime : DifferentiableAt ℝ (fun time' => fluid.rho time' position) time)
-    (hVelocityTime : DifferentiableAt ℝ (fun time' => fluid.velocity time' position) time)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
-    (hVelocitySpace : Differentiable ℝ (fluid.velocity time)) :
-    conservativeMomentumLHS d fluid time position =
-      convectiveMomentumLHS d fluid time position +
-        continuityResidual d fluid time position • fluid.velocity time position := by
-  rw [conservativeMomentumLHS, convectiveMomentumLHS, continuityResidual]
-  rw [timeDeriv_momentumDensity d fluid time position hRhoTime hVelocityTime]
-  rw [tensorDiv_momentumFlux d fluid time position hMomentumDensity hVelocitySpace]
-  ext i
-  simp [materialAcceleration, convectiveTerm, div, momentumDensity, smul_eq_mul]
-  ring_nf
-
-/-- The conservative and convective momentum equations are equivalent when the continuity
-equation holds.
-
-The differentiability assumptions are exactly the product-rule assumptions used to rewrite
-`partial_t (rho u)` and `div_tensor (rho u ⊗ u)`.
--/
-theorem ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
-    (d : ℕ) (data : MomentumBalanceData d)
-    (hContinuity : ContinuityEquation d data.toFluidState)
-    (hRhoTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => data.rho time' position) time)
-    (hVelocityTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => data.velocity time' position) time)
-    (hMomentumDensity : ∀ time,
-      Differentiable ℝ (momentumDensity d data.toFluidState time))
-    (hVelocitySpace : ∀ time, Differentiable ℝ (data.velocity time)) :
-    ConservativeMomentumEquation d data ↔
-      ConvectiveMomentumEquation d data := by
-  constructor
-  · intro hConservative time position
-    have hResidual : continuityResidual d data.toFluidState time position = 0 := by
-      simpa [continuityResidual] using hContinuity time position
-    have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-      d data.toFluidState time position (hRhoTime time position) (hVelocityTime time position)
-      (hMomentumDensity time) (hVelocitySpace time)
-    have hLhs' :
-        conservativeMomentumLHS d data.toFluidState time position =
-          convectiveMomentumLHS d data.toFluidState time position := by
-      rw [hLhs, hResidual, zero_smul, add_zero]
-    change convectiveMomentumLHS d data.toFluidState time position =
-      tensorDiv d (data.stress time) position +
-        data.rho time position • data.bodyForce time position
-    rw [← hLhs']
-    exact hConservative time position
-  · intro hConvective time position
-    have hResidual : continuityResidual d data.toFluidState time position = 0 := by
-      simpa [continuityResidual] using hContinuity time position
-    have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-      d data.toFluidState time position (hRhoTime time position) (hVelocityTime time position)
-      (hMomentumDensity time) (hVelocitySpace time)
-    have hLhs' :
-        conservativeMomentumLHS d data.toFluidState time position =
-          convectiveMomentumLHS d data.toFluidState time position := by
-      rw [hLhs, hResidual, zero_smul, add_zero]
-    change conservativeMomentumLHS d data.toFluidState time position =
-      tensorDiv d (data.stress time) position +
-        data.rho time position • data.bodyForce time position
-    rw [hLhs']
-    exact hConvective time position
-
 /-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
 differentiable enough for the product rules. -/
 theorem ConservativeForm_iff_ConvectiveForm
-    (d : ℕ) (data : MomentumBalanceData d)
+    (d : ℕ) (data : MomentumBalanceFields d)
     (hRhoTime : ∀ time position,
       DifferentiableAt ℝ (fun time' => data.rho time' position) time)
     (hVelocityTime : ∀ time position,
diff --git a/Physlib/FluidDynamics/NavierStokes/Continuity.lean b/Physlib/FluidDynamics/NavierStokes/Continuity.lean
new file mode 100644
index 000000000..40c66c343
--- /dev/null
+++ b/Physlib/FluidDynamics/NavierStokes/Continuity.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.FluidState
+public import Physlib.SpaceAndTime.Space.Derivatives.Div
+public import Physlib.SpaceAndTime.Time.Derivatives
+/-!
+
+# The Navier-Stokes continuity equation
+
+## i. Overview
+
+This module defines the conservative mass-balance equation for a fluid state and the
+corresponding continuity residual.
+
+## ii. Key results
+
+- `ContinuityEquation` : Conservation of mass in conservative form.
+- `continuityResidual` : The scalar residual `partial_t rho + div (rho u)`.
+
+## iii. Table of contents
+
+- A. Continuity equation
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+open Time
+
+namespace FluidDynamics
+namespace NavierStokes
+
+/-!
+
+## A. Continuity equation
+
+-/
+
+/-- Conservation of mass in conservative form, `partial_t rho + div (rho u) = 0`. -/
+def ContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
+  ∀ time position,
+    ∂ₜ (fun time' => fluid.rho time' position) time +
+      (∇ ⬝ fun position' => fluid.rho time position' • fluid.velocity time position') position =
+        0
+
+/-- The scalar continuity-equation residual
+`partial_t rho + div (rho u)`. -/
+noncomputable def continuityResidual (d : ℕ) (fluid : FluidState d) :
+    Time → Space d → ℝ :=
+  fun time position =>
+    ∂ₜ (fun time' => fluid.rho time' position) time +
+      (∇ ⬝ fun position' => fluid.rho time position' • fluid.velocity time position') position
+
+end NavierStokes
+end FluidDynamics
diff --git a/Physlib/FluidDynamics/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
new file mode 100644
index 000000000..fc5fb8a87
--- /dev/null
+++ b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
@@ -0,0 +1,306 @@
+/-
+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.Continuity
+public import Physlib.SpaceAndTime.Space.Derivatives.MatrixDiv
+/-!
+
+# The Navier-Stokes momentum equations
+
+## 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.
+
+## ii. Key results
+
+- `momentumDensity` : The vector momentum density `rho u`.
+- `momentumFlux` : The convective momentum flux `rho u ⊗ u`.
+- `ConservativeMomentumEquation` : 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.
+- `ConservativeMomentumEquation_iff_ConvectiveMomentumEquation` : Equivalence of the two
+  momentum equations when continuity holds and the fields are differentiable.
+
+## iii. Table of contents
+
+- A. Momentum fields
+- B. Conservative momentum equation
+- C. Convective momentum equation
+- D. Equivalence of conservative and convective momentum
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open Space
+open Time
+
+namespace FluidDynamics
+namespace NavierStokes
+
+/-!
+
+## A. Momentum fields
+
+-/
+
+/-- The momentum density `rho u`. -/
+def momentumDensity (d : ℕ) (fluid : FluidState d) : MomentumDensityField d :=
+  fun time position => fluid.rho time position • fluid.velocity time position
+
+/-- The convective momentum flux `rho u ⊗ u`. -/
+def momentumFlux (d : ℕ) (fluid : FluidState d) :
+    Time → Space d → Matrix (Fin d) (Fin d) ℝ :=
+  fun time position =>
+    fluid.rho time position • Matrix.vecMulVec
+      (fun i => fluid.velocity time position i) (fun j => fluid.velocity time position 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 ConservativeMomentumEquation (d : ℕ) (data : MomentumBalanceFields d) : Prop :=
+  ∀ time position,
+    ∂ₜ (fun time' => momentumDensity d data.toFluidState time' position) time +
+        matrixDiv d (momentumFlux d data.toFluidState time) position =
+      matrixDiv d (data.stress time) position +
+        data.rho time position • data.bodyForce time position
+
+/-!
+
+## C. Convective momentum equation
+
+-/
+
+/-- The nonlinear transport term `(u · ∇)u`. -/
+noncomputable def convectiveTerm (d : ℕ) (velocity : VelocityField d) : VectorField d :=
+  fun time position => ∑ j, velocity time position j • ∂[j] (velocity time) position
+
+/-- The material acceleration `∂ₜ u + (u · ∇)u`. -/
+noncomputable def materialAcceleration (d : ℕ) (velocity : VelocityField d) : VectorField d :=
+  fun time position =>
+    ∂ₜ (fun time' => velocity time' position) time +
+      convectiveTerm d velocity time position
+
+/-- 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 : MomentumBalanceFields d) : Prop :=
+  ∀ time position,
+    data.rho time position • materialAcceleration d data.velocity time position =
+      matrixDiv d (data.stress time) position +
+        data.rho time position • data.bodyForce time position
+
+/-!
+
+## D. Equivalence of conservative and convective momentum
+
+-/
+
+/-- The left-hand side of the conservative momentum equation. -/
+noncomputable def conservativeMomentumLHS (d : ℕ) (fluid : FluidState d) : VectorField d :=
+  fun time position =>
+    ∂ₜ (fun time' => momentumDensity d fluid time' position) time +
+      matrixDiv d (momentumFlux d fluid time) position
+
+/-- The left-hand side of the convective momentum equation. -/
+noncomputable def convectiveMomentumLHS (d : ℕ) (fluid : FluidState d) : VectorField d :=
+  fun time position => fluid.rho time position • materialAcceleration d fluid.velocity time position
+
+/-- 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)) (time : Time)
+    (hRho : DifferentiableAt ℝ rhoAtPosition time)
+    (hVelocity : DifferentiableAt ℝ velocityAtPosition time) :
+    ∂ₜ (fun time' => rhoAtPosition time' • velocityAtPosition time') time =
+      rhoAtPosition time • ∂ₜ velocityAtPosition time +
+        ∂ₜ rhoAtPosition time • velocityAtPosition time := by
+  rw [Time.deriv_eq, Time.deriv_eq, Time.deriv_eq]
+  change (fderiv ℝ (rhoAtPosition • velocityAtPosition) time) 1 =
+    rhoAtPosition time • (fderiv ℝ velocityAtPosition time) 1 +
+      (fderiv ℝ rhoAtPosition time) 1 • velocityAtPosition time
+  rw [fderiv_smul hRho hVelocity]
+  rfl
+
+/-- Product rule for the time derivative of the momentum density `rho u`. -/
+lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidState d)
+    (time : Time) (position : Space d)
+    (hRho : DifferentiableAt ℝ (fun time' => fluid.rho time' position) time)
+    (hVelocity : DifferentiableAt ℝ (fun time' => fluid.velocity time' position) time) :
+    ∂ₜ (fun time' => momentumDensity d fluid time' position) time =
+      fluid.rho time position • ∂ₜ (fun time' => fluid.velocity time' position) time +
+        ∂ₜ (fun time' => fluid.rho time' position) time • fluid.velocity time position := by
+  simpa [momentumDensity] using
+    timeDeriv_smul_velocity d (fun time' => fluid.rho time' position)
+      (fun time' => fluid.velocity time' position) time hRho hVelocity
+
+/-- Product rule for one spatial derivative of one component of `rho u ⊗ u`. -/
+lemma spaceDeriv_momentumFlux_component (d : ℕ) (fluid : FluidState d)
+    (time : Time) (position : Space d) (i j : Fin d)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
+    (hVelocity : Differentiable ℝ (fluid.velocity time)) :
+    ∂[j] (fun position' => momentumFlux d fluid time position' i j) position =
+      fluid.velocity time position i •
+        ∂[j] (fun position' => momentumDensity d fluid time position' j) position +
+      ∂[j] (fun position' => fluid.velocity time position' i) position •
+        momentumDensity d fluid time position j := by
+  have hProduct := Space.deriv_smul (u := j) (x := position)
+    (c := fun position' => fluid.velocity time position' i)
+    (f := fun position' => momentumDensity d fluid time position' j)
+    ((differentiable_euclidean.mp hVelocity i).differentiableAt)
+    ((differentiable_euclidean.mp hMomentumDensity j).differentiableAt)
+  rw [← hProduct]
+  congr
+  funext position'
+  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)
+    (time : Time) (position : Space d)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
+    (hVelocity : Differentiable ℝ (fluid.velocity time)) :
+    matrixDiv d (momentumFlux d fluid time) position =
+      (∇ ⬝ momentumDensity d fluid time) position • fluid.velocity time position +
+        fluid.rho time position • convectiveTerm d fluid.velocity time position := by
+  ext i
+  simp [matrixDiv_apply, div, convectiveTerm, smul_eq_mul]
+  change (∑ j, ∂[j] (fun position' =>
+      momentumFlux d fluid time position' i j) position) =
+    (∑ j, ∂[j] (fun position' =>
+      momentumDensity d fluid time position' j) position) *
+        fluid.velocity time position i +
+      fluid.rho time position *
+        (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i)
+  calc
+    (∑ j, ∂[j] (fun position' =>
+        momentumFlux d fluid time position' i j) position)
+        = ∑ j,
+            (fluid.velocity time position i *
+                ∂[j] (fun position' =>
+                  momentumDensity d fluid time position' j) position +
+              ∂[j] (fun position' => fluid.velocity time position' i) position *
+                momentumDensity d fluid time position j) := by
+          apply Finset.sum_congr rfl
+          intro j _
+          rw [spaceDeriv_momentumFlux_component d fluid time position i j
+            hMomentumDensity hVelocity]
+          simp [smul_eq_mul]
+    _ = fluid.velocity time position i *
+          (∑ j, ∂[j] (fun position' =>
+            momentumDensity d fluid time position' j) position) +
+        fluid.rho time position *
+          (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i) := by
+          rw [Finset.sum_add_distrib]
+          congr 1
+          · rw [Finset.mul_sum]
+          · rw [Finset.mul_sum]
+            apply Finset.sum_congr rfl
+            intro j _
+            rw [Space.deriv_euclid (ν := j) (μ := i) (f := fluid.velocity time)
+              hVelocity position]
+            simp [momentumDensity, mul_comm, mul_assoc]
+    _ = (∑ j, ∂[j] (fun position' =>
+          momentumDensity d fluid time position' j) position) *
+          fluid.velocity time position i +
+        fluid.rho time position *
+          (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position 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.
+-/
+lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+    (d : ℕ) (fluid : FluidState d)
+    (time : Time) (position : Space d)
+    (hRhoTime : DifferentiableAt ℝ (fun time' => fluid.rho time' position) time)
+    (hVelocityTime : DifferentiableAt ℝ (fun time' => fluid.velocity time' position) time)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
+    (hVelocitySpace : Differentiable ℝ (fluid.velocity time)) :
+    conservativeMomentumLHS d fluid time position =
+      convectiveMomentumLHS d fluid time position +
+        continuityResidual d fluid time position • fluid.velocity time position := by
+  rw [conservativeMomentumLHS, convectiveMomentumLHS, continuityResidual]
+  rw [timeDeriv_momentumDensity d fluid time position hRhoTime hVelocityTime]
+  rw [matrixDiv_momentumFlux d fluid time position hMomentumDensity hVelocitySpace]
+  ext i
+  simp [materialAcceleration, convectiveTerm, div, momentumDensity, smul_eq_mul]
+  ring_nf
+
+/-- The conservative and convective momentum equations are equivalent when the 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 ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
+    (d : ℕ) (data : MomentumBalanceFields d)
+    (hContinuity : ContinuityEquation d data.toFluidState)
+    (hRhoTime : ∀ time position,
+      DifferentiableAt ℝ (fun time' => data.rho time' position) time)
+    (hVelocityTime : ∀ time position,
+      DifferentiableAt ℝ (fun time' => data.velocity time' position) time)
+    (hMomentumDensity : ∀ time,
+      Differentiable ℝ (momentumDensity d data.toFluidState time))
+    (hVelocitySpace : ∀ time, Differentiable ℝ (data.velocity time)) :
+    ConservativeMomentumEquation d data ↔
+      ConvectiveMomentumEquation d data := by
+  constructor
+  · intro hConservative time position
+    have hResidual : continuityResidual d data.toFluidState time position = 0 := by
+      simpa [continuityResidual] using hContinuity time position
+    have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+      d data.toFluidState time position (hRhoTime time position) (hVelocityTime time position)
+      (hMomentumDensity time) (hVelocitySpace time)
+    have hLhs' :
+        conservativeMomentumLHS d data.toFluidState time position =
+          convectiveMomentumLHS d data.toFluidState time position := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    change convectiveMomentumLHS d data.toFluidState time position =
+      matrixDiv d (data.stress time) position +
+        data.rho time position • data.bodyForce time position
+    rw [← hLhs']
+    exact hConservative time position
+  · intro hConvective time position
+    have hResidual : continuityResidual d data.toFluidState time position = 0 := by
+      simpa [continuityResidual] using hContinuity time position
+    have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
+      d data.toFluidState time position (hRhoTime time position) (hVelocityTime time position)
+      (hMomentumDensity time) (hVelocitySpace time)
+    have hLhs' :
+        conservativeMomentumLHS d data.toFluidState time position =
+          convectiveMomentumLHS d data.toFluidState time position := by
+      rw [hLhs, hResidual, zero_smul, add_zero]
+    change conservativeMomentumLHS d data.toFluidState time position =
+      matrixDiv d (data.stress time) position +
+        data.rho time position • data.bodyForce time position
+    rw [hLhs']
+    exact hConvective time position
+
+end NavierStokes
+end FluidDynamics
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean b/Physlib/SpaceAndTime/Space/Derivatives/MatrixDiv.lean
similarity index 57%
rename from Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean
rename to Physlib/SpaceAndTime/Space/Derivatives/MatrixDiv.lean
index 1ccadab4b..c7a61b815 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/TensorDiv.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/MatrixDiv.lean
@@ -5,34 +5,33 @@ Authors: Florian Wiesner
 -/
 module
 
-public import Mathlib.Data.Matrix.Basic
 public import Physlib.SpaceAndTime.Space.Derivatives.Div
 /-!
 
-# Tensor divergence on Space
+# Matrix divergence on Space
 
 ## i. Overview
 
-In this module we define the tensor divergence operator on matrix-valued
+In this module we define the matrix divergence operator on matrix-valued
 functions from `Space d`.
 
-For a field `T : Space d → Matrix (Fin d) (Fin d) ℝ`, the tensor divergence is
+For a field `T : Space d → Matrix (Fin d) (Fin d) ℝ`, the matrix divergence is
 the vector field whose `i`th component is
 
 `∑ j, ∂[j] (fun x => T x i j) x`.
 
 ## ii. Key results
 
-- `tensorDiv` : The divergence of a matrix-valued function on `Space d`.
+- `matrixDiv` : The divergence of a matrix-valued function on `Space d`.
 
 ## iii. Table of contents
 
-- A. The tensor divergence on functions
+- A. The matrix divergence on functions
   - A.1. Basic equalities
-  - A.2. The tensor divergence on the zero function
-  - A.3. The tensor divergence on a constant function
-  - A.4. The tensor divergence distributes over addition
-  - A.5. The tensor divergence distributes over scalar multiplication
+  - A.2. The matrix divergence on the zero function
+  - A.3. The matrix divergence on a constant function
+  - A.4. The matrix divergence distributes over addition
+  - A.5. The matrix divergence distributes over scalar multiplication
 
 ## iv. References
 
@@ -46,18 +45,18 @@ namespace Space
 
 /-!
 
-## A. The tensor divergence on functions
+## A. The matrix divergence on functions
 
 -/
 
 /-- The divergence of a matrix-valued spatial field.
 
-For a field `T : Space d → Matrix (Fin d) (Fin d) ℝ`, `tensorDiv T` is the
+For a field `T : Space d → Matrix (Fin d) (Fin d) ℝ`, `matrixDiv T` is the
 vector field whose `i`th component is
 
 `∑ j, ∂[j] (fun x => T x i j) x`.
 -/
-noncomputable def tensorDiv (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ) :
+noncomputable def matrixDiv (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ) :
     Space d → EuclideanSpace ℝ (Fin d) := fun x => WithLp.toLp 2 fun i =>
   div (fun y : Space d => WithLp.toLp 2 fun j => T y i j) x
 
@@ -68,46 +67,46 @@ noncomputable def tensorDiv (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) 
 -/
 
 @[simp]
-lemma tensorDiv_apply (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ)
+lemma matrixDiv_apply (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ)
     (x : Space d) (i : Fin d) :
-    tensorDiv d T x i = ∑ j, ∂[j] (fun x => T x i j) x := by
-  simp [tensorDiv, div]
+    matrixDiv d T x i = ∑ j, ∂[j] (fun x => T x i j) x := by
+  simp [matrixDiv, div]
 
 /-!
 
-### A.2. The tensor divergence on the zero function
+### A.2. The matrix divergence on the zero function
 
 -/
 
 @[simp]
-lemma tensorDiv_zero (d : ℕ) :
-    tensorDiv d (0 : Space d → Matrix (Fin d) (Fin d) ℝ) = 0 := by
+lemma matrixDiv_zero (d : ℕ) :
+    matrixDiv d (0 : Space d → Matrix (Fin d) (Fin d) ℝ) = 0 := by
   ext x i
   change (∑ j : Fin d, ∂[j] (fun _ : Space d => (0 : ℝ)) x) = 0
   simp
 
 /-!
 
-### A.3. The tensor divergence on a constant function
+### A.3. The matrix divergence on a constant function
 
 -/
 
 @[simp]
-lemma tensorDiv_const (d : ℕ) (T : Matrix (Fin d) (Fin d) ℝ) :
-    tensorDiv d (fun _ : Space d => T) = 0 := by
+lemma matrixDiv_const (d : ℕ) (T : Matrix (Fin d) (Fin d) ℝ) :
+    matrixDiv d (fun _ : Space d => T) = 0 := by
   ext x i
   change (∑ j : Fin d, ∂[j] (fun _ : Space d => T i j) x) = 0
   simp
 
 /-!
 
-### A.4. The tensor divergence distributes over addition
+### A.4. The matrix divergence distributes over addition
 
 -/
 
-lemma tensorDiv_add (d : ℕ) (T1 T2 : Space d → Matrix (Fin d) (Fin d) ℝ)
+lemma matrixDiv_add (d : ℕ) (T1 T2 : Space d → Matrix (Fin d) (Fin d) ℝ)
     (hT1 : Differentiable ℝ T1) (hT2 : Differentiable ℝ T2) :
-    tensorDiv d (T1 + T2) = tensorDiv d T1 + tensorDiv d T2 := by
+    matrixDiv d (T1 + T2) = matrixDiv d T1 + matrixDiv d T2 := by
   ext x i
   change (∑ j, ∂[j] (fun x => (T1 x + T2 x) i j) x) =
     (∑ j, ∂[j] (fun x => T1 x i j) x) +
@@ -124,13 +123,13 @@ lemma tensorDiv_add (d : ℕ) (T1 T2 : Space d → Matrix (Fin d) (Fin d) ℝ)
 
 /-!
 
-### A.5. The tensor divergence distributes over scalar multiplication
+### A.5. The matrix divergence distributes over scalar multiplication
 
 -/
 
-lemma tensorDiv_smul (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ) (k : ℝ)
+lemma matrixDiv_smul (d : ℕ) (T : Space d → Matrix (Fin d) (Fin d) ℝ) (k : ℝ)
     (hT : Differentiable ℝ T) :
-    tensorDiv d (k • T) = k • tensorDiv d T := by
+    matrixDiv d (k • T) = k • matrixDiv d T := by
   ext x i
   change (∑ j, ∂[j] (fun x => (k • T x) i j) x) =
     k * ∑ j, ∂[j] (fun x => T x i j) x

From ded11a5fdd228260fbf257022cc2bd4b3bc4c5b6 Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Thu, 21 May 2026 16:15:05 +0200
Subject: [PATCH 22/33] refactor(FluidDynamics): address Navier-Stokes review
 comments

---
 Physlib/FluidDynamics/FluidState.lean         |   4 +-
 Physlib/FluidDynamics/NavierStokes/Basic.lean |  20 +-
 .../NavierStokes/Continuity.lean              |  12 +-
 .../FluidDynamics/NavierStokes/Momentum.lean  | 250 +++++++++---------
 4 files changed, 143 insertions(+), 143 deletions(-)

diff --git a/Physlib/FluidDynamics/FluidState.lean b/Physlib/FluidDynamics/FluidState.lean
index 2ce450f0d..ffa17c4f2 100644
--- a/Physlib/FluidDynamics/FluidState.lean
+++ b/Physlib/FluidDynamics/FluidState.lean
@@ -27,7 +27,7 @@ fields used by specific balance laws are provided by extension structures.
 - `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.
-- `MomentumBalanceFields` : A fluid state with stress and body force.
+- `FluidInMomentumBalance` : A fluid state with stress and body force.
 
 ## iii. Table of contents
 
@@ -83,7 +83,7 @@ structure FluidState (d : ℕ) where
   velocity : VelocityField d
 
 /-- The fields needed for a momentum balance: fluid state, stress, and body force. -/
-structure MomentumBalanceFields (d : ℕ) extends FluidState d where
+structure FluidInMomentumBalance (d : ℕ) extends FluidState d where
   /-- The stress tensor field. -/
   stress : StressTensor d
   /-- The body-force field per unit mass. -/
diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 9c0c0f159..576d51fcc 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -47,26 +47,26 @@ namespace NavierStokes
 -/
 
 /-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
-def ConservativeForm (d : ℕ) (data : MomentumBalanceFields d) : Prop :=
+def ConservativeForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
   ContinuityEquation d data.toFluidState ∧
     ConservativeMomentumEquation d data
 
 /-- The convective Navier-Stokes form with an externally supplied stress tensor. -/
-def ConvectiveForm (d : ℕ) (data : MomentumBalanceFields d) : Prop :=
+def ConvectiveForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
   ContinuityEquation d data.toFluidState ∧
     ConvectiveMomentumEquation d data
 
 /-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
 differentiable enough for the product rules. -/
 theorem ConservativeForm_iff_ConvectiveForm
-    (d : ℕ) (data : MomentumBalanceFields d)
-    (hRhoTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => data.rho time' position) time)
-    (hVelocityTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => data.velocity time' position) time)
-    (hMomentumDensity : ∀ time,
-      Differentiable ℝ (momentumDensity d data.toFluidState time))
-    (hVelocitySpace : ∀ time, Differentiable ℝ (data.velocity time)) :
+    (d : ℕ) (data : FluidInMomentumBalance d)
+    (hRhoTime : ∀ t x,
+      DifferentiableAt ℝ (fun t' => data.rho t' x) t)
+    (hVelocityTime : ∀ t x,
+      DifferentiableAt ℝ (fun t' => data.velocity t' x) t)
+    (hMomentumDensity : ∀ t,
+      Differentiable ℝ (momentumDensity d data.toFluidState t))
+    (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
     ConservativeForm d data ↔
       ConvectiveForm d data := by
   constructor
diff --git a/Physlib/FluidDynamics/NavierStokes/Continuity.lean b/Physlib/FluidDynamics/NavierStokes/Continuity.lean
index 40c66c343..9b07d8c3e 100644
--- a/Physlib/FluidDynamics/NavierStokes/Continuity.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Continuity.lean
@@ -46,18 +46,18 @@ namespace NavierStokes
 
 /-- Conservation of mass in conservative form, `partial_t rho + div (rho u) = 0`. -/
 def ContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
-  ∀ time position,
-    ∂ₜ (fun time' => fluid.rho time' position) time +
-      (∇ ⬝ fun position' => fluid.rho time position' • fluid.velocity time position') position =
+  ∀ t x,
+    ∂ₜ (fun t' => fluid.rho t' 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 → ℝ :=
-  fun time position =>
-    ∂ₜ (fun time' => fluid.rho time' position) time +
-      (∇ ⬝ fun position' => fluid.rho time position' • fluid.velocity time position') position
+  fun t x =>
+    ∂ₜ (fun t' => fluid.rho t' x) t +
+      (∇ ⬝ fun x' => fluid.rho t x' • fluid.velocity t x') x
 
 end NavierStokes
 end FluidDynamics
diff --git a/Physlib/FluidDynamics/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
index fc5fb8a87..02b128a38 100644
--- a/Physlib/FluidDynamics/NavierStokes/Momentum.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
@@ -55,14 +55,14 @@ namespace NavierStokes
 
 /-- The momentum density `rho u`. -/
 def momentumDensity (d : ℕ) (fluid : FluidState d) : MomentumDensityField d :=
-  fun time position => fluid.rho time position • fluid.velocity time position
+  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) ℝ :=
-  fun time position =>
-    fluid.rho time position • Matrix.vecMulVec
-      (fun i => fluid.velocity time position i) (fun j => fluid.velocity time position j)
+  fun t x =>
+    fluid.rho t x • Matrix.vecMulVec
+      (fun i => fluid.velocity t x i) (fun j => fluid.velocity t x j)
 
 /-!
 
@@ -78,12 +78,12 @@ The equation is
 
 Here `stress` is intentionally not yet specialized to a Newtonian stress law.
 -/
-def ConservativeMomentumEquation (d : ℕ) (data : MomentumBalanceFields d) : Prop :=
-  ∀ time position,
-    ∂ₜ (fun time' => momentumDensity d data.toFluidState time' position) time +
-        matrixDiv d (momentumFlux d data.toFluidState time) position =
-      matrixDiv d (data.stress time) position +
-        data.rho time position • data.bodyForce time position
+def ConservativeMomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
+  ∀ t x,
+    ∂ₜ (fun t' => momentumDensity d data.toFluidState t' x) t +
+        matrixDiv d (momentumFlux d data.toFluidState t) x =
+      matrixDiv d (data.stress t) x +
+        data.rho t x • data.bodyForce t x
 
 /-!
 
@@ -93,13 +93,13 @@ def ConservativeMomentumEquation (d : ℕ) (data : MomentumBalanceFields d) : Pr
 
 /-- The nonlinear transport term `(u · ∇)u`. -/
 noncomputable def convectiveTerm (d : ℕ) (velocity : VelocityField d) : VectorField d :=
-  fun time position => ∑ j, velocity time position j • ∂[j] (velocity time) position
+  fun t x => ∑ j, velocity t x j • ∂[j] (velocity t) x
 
 /-- The material acceleration `∂ₜ u + (u · ∇)u`. -/
 noncomputable def materialAcceleration (d : ℕ) (velocity : VelocityField d) : VectorField d :=
-  fun time position =>
-    ∂ₜ (fun time' => velocity time' position) time +
-      convectiveTerm d velocity time position
+  fun t x =>
+    ∂ₜ (fun t' => velocity t' x) t +
+      convectiveTerm d velocity t x
 
 /-- Conservation of momentum in convective form.
 
@@ -109,11 +109,11 @@ The equation is
 
 Here `stress` is intentionally not yet specialized to a Newtonian stress law.
 -/
-def ConvectiveMomentumEquation (d : ℕ) (data : MomentumBalanceFields d) : Prop :=
-  ∀ time position,
-    data.rho time position • materialAcceleration d data.velocity time position =
-      matrixDiv d (data.stress time) position +
-        data.rho time position • data.bodyForce time position
+def ConvectiveMomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
+  ∀ t x,
+    data.rho t x • materialAcceleration d data.velocity t x =
+      matrixDiv d (data.stress t) x +
+        data.rho t x • data.bodyForce t x
 
 /-!
 
@@ -123,111 +123,111 @@ def ConvectiveMomentumEquation (d : ℕ) (data : MomentumBalanceFields d) : Prop
 
 /-- The left-hand side of the conservative momentum equation. -/
 noncomputable def conservativeMomentumLHS (d : ℕ) (fluid : FluidState d) : VectorField d :=
-  fun time position =>
-    ∂ₜ (fun time' => momentumDensity d fluid time' position) time +
-      matrixDiv d (momentumFlux d fluid time) position
+  fun t x =>
+    ∂ₜ (fun t' => momentumDensity d fluid t' 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 time position => fluid.rho time position • materialAcceleration d fluid.velocity time position
+  fun t x => fluid.rho t x • materialAcceleration d fluid.velocity 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)) (time : Time)
-    (hRho : DifferentiableAt ℝ rhoAtPosition time)
-    (hVelocity : DifferentiableAt ℝ velocityAtPosition time) :
-    ∂ₜ (fun time' => rhoAtPosition time' • velocityAtPosition time') time =
-      rhoAtPosition time • ∂ₜ velocityAtPosition time +
-        ∂ₜ rhoAtPosition time • velocityAtPosition time := by
+    (velocityAtPosition : Time → EuclideanSpace ℝ (Fin d)) (t : Time)
+    (hRho : DifferentiableAt ℝ rhoAtPosition t)
+    (hVelocity : DifferentiableAt ℝ velocityAtPosition t) :
+    ∂ₜ (fun t' => rhoAtPosition t' • velocityAtPosition t') t =
+      rhoAtPosition t • ∂ₜ velocityAtPosition t +
+        ∂ₜ rhoAtPosition t • velocityAtPosition t := by
   rw [Time.deriv_eq, Time.deriv_eq, Time.deriv_eq]
-  change (fderiv ℝ (rhoAtPosition • velocityAtPosition) time) 1 =
-    rhoAtPosition time • (fderiv ℝ velocityAtPosition time) 1 +
-      (fderiv ℝ rhoAtPosition time) 1 • velocityAtPosition time
+  change (fderiv ℝ (rhoAtPosition • velocityAtPosition) t) 1 =
+    rhoAtPosition t • (fderiv ℝ velocityAtPosition t) 1 +
+      (fderiv ℝ rhoAtPosition t) 1 • velocityAtPosition t
   rw [fderiv_smul hRho hVelocity]
   rfl
 
 /-- Product rule for the time derivative of the momentum density `rho u`. -/
 lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidState d)
-    (time : Time) (position : Space d)
-    (hRho : DifferentiableAt ℝ (fun time' => fluid.rho time' position) time)
-    (hVelocity : DifferentiableAt ℝ (fun time' => fluid.velocity time' position) time) :
-    ∂ₜ (fun time' => momentumDensity d fluid time' position) time =
-      fluid.rho time position • ∂ₜ (fun time' => fluid.velocity time' position) time +
-        ∂ₜ (fun time' => fluid.rho time' position) time • fluid.velocity time position := by
+    (t : Time) (x : Space d)
+    (hRho : DifferentiableAt ℝ (fun t' => fluid.rho t' x) t)
+    (hVelocity : DifferentiableAt ℝ (fun t' => fluid.velocity t' x) t) :
+    ∂ₜ (fun t' => momentumDensity d fluid t' x) t =
+      fluid.rho t x • ∂ₜ (fun t' => fluid.velocity t' x) t +
+        ∂ₜ (fun t' => fluid.rho t' x) t • fluid.velocity t x := by
   simpa [momentumDensity] using
-    timeDeriv_smul_velocity d (fun time' => fluid.rho time' position)
-      (fun time' => fluid.velocity time' position) time hRho hVelocity
+    timeDeriv_smul_velocity d (fun t' => fluid.rho t' x)
+      (fun t' => fluid.velocity t' 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)
-    (time : Time) (position : Space d) (i j : Fin d)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
-    (hVelocity : Differentiable ℝ (fluid.velocity time)) :
-    ∂[j] (fun position' => momentumFlux d fluid time position' i j) position =
-      fluid.velocity time position i •
-        ∂[j] (fun position' => momentumDensity d fluid time position' j) position +
-      ∂[j] (fun position' => fluid.velocity time position' i) position •
-        momentumDensity d fluid time position j := by
-  have hProduct := Space.deriv_smul (u := j) (x := position)
-    (c := fun position' => fluid.velocity time position' i)
-    (f := fun position' => momentumDensity d fluid time position' j)
+    (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
+  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)
   rw [← hProduct]
   congr
-  funext position'
+  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)
-    (time : Time) (position : Space d)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
-    (hVelocity : Differentiable ℝ (fluid.velocity time)) :
-    matrixDiv d (momentumFlux d fluid time) position =
-      (∇ ⬝ momentumDensity d fluid time) position • fluid.velocity time position +
-        fluid.rho time position • convectiveTerm d fluid.velocity time position := by
+    (t : Time) (x : Space d)
+    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid t))
+    (hVelocity : Differentiable ℝ (fluid.velocity t)) :
+    matrixDiv d (momentumFlux d fluid t) x =
+      (∇ ⬝ momentumDensity d fluid t) x • fluid.velocity t x +
+        fluid.rho t x • convectiveTerm d fluid.velocity t x := by
   ext i
   simp [matrixDiv_apply, div, convectiveTerm, smul_eq_mul]
-  change (∑ j, ∂[j] (fun position' =>
-      momentumFlux d fluid time position' i j) position) =
-    (∑ j, ∂[j] (fun position' =>
-      momentumDensity d fluid time position' j) position) *
-        fluid.velocity time position i +
-      fluid.rho time position *
-        (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i)
+  change (∑ j, ∂[j] (fun x' =>
+      momentumFlux d fluid t x' i j) x) =
+    (∑ j, ∂[j] (fun x' =>
+      momentumDensity d fluid t x' j) x) *
+        fluid.velocity t x i +
+      fluid.rho t x *
+        (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i)
   calc
-    (∑ j, ∂[j] (fun position' =>
-        momentumFlux d fluid time position' i j) position)
+    (∑ j, ∂[j] (fun x' =>
+        momentumFlux d fluid t x' i j) x)
         = ∑ j,
-            (fluid.velocity time position i *
-                ∂[j] (fun position' =>
-                  momentumDensity d fluid time position' j) position +
-              ∂[j] (fun position' => fluid.velocity time position' i) position *
-                momentumDensity d fluid time position j) := by
+            (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
           apply Finset.sum_congr rfl
           intro j _
-          rw [spaceDeriv_momentumFlux_component d fluid time position i j
+          rw [spaceDeriv_momentumFlux_component d fluid t x i j
             hMomentumDensity hVelocity]
           simp [smul_eq_mul]
-    _ = fluid.velocity time position i *
-          (∑ j, ∂[j] (fun position' =>
-            momentumDensity d fluid time position' j) position) +
-        fluid.rho time position *
-          (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i) := by
+    _ = fluid.velocity t x i *
+          (∑ j, ∂[j] (fun x' =>
+            momentumDensity d fluid t x' j) x) +
+        fluid.rho t x *
+          (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i) := by
           rw [Finset.sum_add_distrib]
           congr 1
           · rw [Finset.mul_sum]
           · rw [Finset.mul_sum]
             apply Finset.sum_congr rfl
             intro j _
-            rw [Space.deriv_euclid (ν := j) (μ := i) (f := fluid.velocity time)
-              hVelocity position]
+            rw [Space.deriv_euclid (ν := j) (μ := i) (f := fluid.velocity t)
+              hVelocity x]
             simp [momentumDensity, mul_comm, mul_assoc]
-    _ = (∑ j, ∂[j] (fun position' =>
-          momentumDensity d fluid time position' j) position) *
-          fluid.velocity time position i +
-        fluid.rho time position *
-          (∑ j, fluid.velocity time position j * ∂[j] (fluid.velocity time) position i) := by
+    _ = (∑ j, ∂[j] (fun x' =>
+          momentumDensity d fluid t x' j) x) *
+          fluid.velocity t x i +
+        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.
@@ -237,17 +237,17 @@ the continuity residual times the velocity field.
 -/
 lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
     (d : ℕ) (fluid : FluidState d)
-    (time : Time) (position : Space d)
-    (hRhoTime : DifferentiableAt ℝ (fun time' => fluid.rho time' position) time)
-    (hVelocityTime : DifferentiableAt ℝ (fun time' => fluid.velocity time' position) time)
-    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid time))
-    (hVelocitySpace : Differentiable ℝ (fluid.velocity time)) :
-    conservativeMomentumLHS d fluid time position =
-      convectiveMomentumLHS d fluid time position +
-        continuityResidual d fluid time position • fluid.velocity time position := by
+    (t : Time) (x : Space d)
+    (hRhoTime : DifferentiableAt ℝ (fun t' => fluid.rho t' x) t)
+    (hVelocityTime : DifferentiableAt ℝ (fun t' => fluid.velocity t' 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]
-  rw [timeDeriv_momentumDensity d fluid time position hRhoTime hVelocityTime]
-  rw [matrixDiv_momentumFlux d fluid time position hMomentumDensity hVelocitySpace]
+  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
@@ -259,48 +259,48 @@ The differentiability assumptions are exactly the product-rule assumptions used
 `partial_t (rho u)` and `matrixDiv (rho u ⊗ u)`.
 -/
 theorem ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
-    (d : ℕ) (data : MomentumBalanceFields d)
+    (d : ℕ) (data : FluidInMomentumBalance d)
     (hContinuity : ContinuityEquation d data.toFluidState)
-    (hRhoTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => data.rho time' position) time)
-    (hVelocityTime : ∀ time position,
-      DifferentiableAt ℝ (fun time' => data.velocity time' position) time)
-    (hMomentumDensity : ∀ time,
-      Differentiable ℝ (momentumDensity d data.toFluidState time))
-    (hVelocitySpace : ∀ time, Differentiable ℝ (data.velocity time)) :
+    (hRhoTime : ∀ t x,
+      DifferentiableAt ℝ (fun t' => data.rho t' x) t)
+    (hVelocityTime : ∀ t x,
+      DifferentiableAt ℝ (fun t' => data.velocity t' x) t)
+    (hMomentumDensity : ∀ t,
+      Differentiable ℝ (momentumDensity d data.toFluidState t))
+    (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
     ConservativeMomentumEquation d data ↔
       ConvectiveMomentumEquation d data := by
   constructor
-  · intro hConservative time position
-    have hResidual : continuityResidual d data.toFluidState time position = 0 := by
-      simpa [continuityResidual] using hContinuity time position
+  · intro hConservative t x
+    have hResidual : continuityResidual d data.toFluidState t x = 0 := by
+      simpa [continuityResidual] using hContinuity t x
     have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-      d data.toFluidState time position (hRhoTime time position) (hVelocityTime time position)
-      (hMomentumDensity time) (hVelocitySpace time)
+      d data.toFluidState t x (hRhoTime t x) (hVelocityTime t x)
+      (hMomentumDensity t) (hVelocitySpace t)
     have hLhs' :
-        conservativeMomentumLHS d data.toFluidState time position =
-          convectiveMomentumLHS d data.toFluidState time position := by
+        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 time position =
-      matrixDiv d (data.stress time) position +
-        data.rho time position • data.bodyForce time position
+    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 time position
-  · intro hConvective time position
-    have hResidual : continuityResidual d data.toFluidState time position = 0 := by
-      simpa [continuityResidual] using hContinuity time position
+    exact hConservative t x
+  · intro hConvective t x
+    have hResidual : continuityResidual d data.toFluidState t x = 0 := by
+      simpa [continuityResidual] using hContinuity t x
     have hLhs := conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
-      d data.toFluidState time position (hRhoTime time position) (hVelocityTime time position)
-      (hMomentumDensity time) (hVelocitySpace time)
+      d data.toFluidState t x (hRhoTime t x) (hVelocityTime t x)
+      (hMomentumDensity t) (hVelocitySpace t)
     have hLhs' :
-        conservativeMomentumLHS d data.toFluidState time position =
-          convectiveMomentumLHS d data.toFluidState time position := by
+        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 time position =
-      matrixDiv d (data.stress time) position +
-        data.rho time position • data.bodyForce time position
+    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 time position
+    exact hConvective t x
 
 end NavierStokes
 end FluidDynamics

From d7fc15b6955de3770240905b396caed46afb8598 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Fri, 22 May 2026 18:46:49 +0000
Subject: [PATCH 23/33] getting rid of theorems

---
 Physlib.lean                                   |  8 ++++----
 .../FluidMechanics/IdealFluids/Bernoulli.lean  | 18 +++---------------
 .../FluidMechanics/IdealFluids/Continuity.lean | 12 ++----------
 Physlib/FluidMechanics/IdealFluids/Euler.lean  | 12 ++++++------
 4 files changed, 15 insertions(+), 35 deletions(-)

diff --git a/Physlib.lean b/Physlib.lean
index f3af1dcb8..f00e4f40d 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -48,6 +48,10 @@ public import Physlib.Electromagnetism.Vacuum.Constant
 public import Physlib.Electromagnetism.Vacuum.HarmonicWave
 public import Physlib.Electromagnetism.Vacuum.IsPlaneWave
 public import Physlib.Mathematics.Calculus.AdjFDeriv
+public import Physlib.FluidMechanics.IdealFluids.Basic
+public import Physlib.FluidMechanics.IdealFluids.Bernoulli
+public import Physlib.FluidMechanics.IdealFluids.Continuity
+public import Physlib.FluidMechanics.IdealFluids.Euler
 public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
 public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap
@@ -80,10 +84,6 @@ public import Physlib.Mathematics.VariationalCalculus.HasVarAdjoint
 public import Physlib.Mathematics.VariationalCalculus.HasVarGradient
 public import Physlib.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
 public import Physlib.Mathematics.VariationalCalculus.IsTestFunction
-public import Physlib.FluidMechanics.IdealFluids.Basic
-public import Physlib.FluidMechanics.IdealFluids.Bernoulli
-public import Physlib.FluidMechanics.IdealFluids.Continuity
-public import Physlib.FluidMechanics.IdealFluids.Euler
 public import Physlib.Meta.AllFilePaths
 public import Physlib.Meta.Basic
 public import Physlib.Meta.Informal.Basic
diff --git a/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean b/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
index ea63de2b6..c9d1044e8 100644
--- a/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
@@ -14,7 +14,9 @@ public import Physlib.SpaceAndTime.Time.Derivatives
 /-!
 This module introduces:
 steady flow,
-... (still under construction)
+material derivative,
+isentropic behavious,
+the bernoulli equation
 -/
 
 open scoped InnerProductSpace
@@ -48,17 +50,3 @@ noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
     ℝ :=
       let v := F.velocity t pos
       0.5 * ⟪v, v⟫_ℝ + F.enthalpy t pos + g pos
-
--- TODO: Recheck sign
-
-/-- Derivation:
-  If the flow is steady and isentropic, the bernoulli equation is constant
--/
-theorem bernoulli_derivation (F : IdealFluid) (g : Space → ℝ) (t : Time) (pos : Space)
-    (Eul : F.satisfiesEuler g)
-    (Stdy : F.isSteady)
-    (Istrpc : F.isIsentropic) :
-    let v := F.velocity t pos
-    ⟪v, Space.grad (F.bernoulliEquation t · g) pos⟫_ℝ = 0 :=
-      by
-        sorry
diff --git a/Physlib/FluidMechanics/IdealFluids/Continuity.lean b/Physlib/FluidMechanics/IdealFluids/Continuity.lean
index 07183964a..f66a85336 100644
--- a/Physlib/FluidMechanics/IdealFluids/Continuity.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Continuity.lean
@@ -29,13 +29,5 @@ public def IdealFluid.satisfiesContinuity (F : IdealFluid):
 
 /-- Criterion for incompressibility -/
 public def IdealFluid.isIncompressible (F : IdealFluid):
-    Prop :=
-      ∀ (t : Time) (pos : Space), ∂ₜ (F.density · pos) t = 0
-
-/-- Theorem: If constant density and incompressible div(v)=0-/
-theorem incompress_const_density_implies_div_v_eq_zero (F : IdealFluid)
-    (Cont      : F.satisfiesContinuity)
-    (Incomp    : F.isIncompressible)
-    (ConstDens : ∀ (t : Time) (pos : Space), Space.grad (F.density t ·) pos = 0) :
-    ∀ (t : Time) (pos : Space), Space.div (F.velocity t ·) pos = 0 := by
-      sorry
+  Prop :=
+    ∀ (t : Time) (pos : Space), ∂ₜ (F.density · pos) t = 0
diff --git a/Physlib/FluidMechanics/IdealFluids/Euler.lean b/Physlib/FluidMechanics/IdealFluids/Euler.lean
index c3e091b0a..9b80ed7eb 100644
--- a/Physlib/FluidMechanics/IdealFluids/Euler.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Euler.lean
@@ -22,9 +22,9 @@ open Space
 
 /-- Defines the property of satisfying Euler's equation. -/
 public def IdealFluid.satisfiesEuler (F: IdealFluid) (g: Space → ℝ):
-    Prop :=
-      ∀ (t : Time) (pos : Space),
-        let v := F.velocity t pos
-        ∂ₜ (F.velocity · pos) t +
-        (fun i => ⟪v, Space.grad (F.velocity t · i) pos⟫_ℝ)
-        = -(1/F.density t pos) • Space.grad (F.pressure t ·) pos + Space.grad g pos
+  Prop :=
+    ∀ (t : Time) (pos : Space),
+      let v := F.velocity t pos
+      ∂ₜ (F.velocity · pos) t +
+      (fun i => ⟪v, Space.grad (F.velocity t · i) pos⟫_ℝ)
+      = -(1/F.density t pos) • Space.grad (F.pressure t ·) pos + Space.grad g pos

From ac619ebf0c9b87246c4a9b36a9dbba5c539daf98 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Fri, 22 May 2026 18:51:20 +0000
Subject: [PATCH 24/33] useless comment

---
 Physlib/FluidMechanics/IdealFluids/Bernoulli.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean b/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
index c9d1044e8..dc8749cfe 100644
--- a/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
@@ -42,8 +42,6 @@ def IdealFluid.isIsentropic (F: IdealFluid):
       ∀ (t: Time) (pos: Space),
       F.materialDerivative t pos F.entropy = 0
 
--- TODO: Make into material derivative
-
 /-- The Bernoulli function (1/2)v^2 + w -/
 noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
 (t: Time) (pos: Space) (g: Space → ℝ):

From 38a1a78946d30f41d518bb4b05911d65181947de Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Fri, 22 May 2026 19:06:11 +0000
Subject: [PATCH 25/33] descriptions

---
 Physlib/FluidMechanics/IdealFluids/Basic.lean      |  7 +++++--
 Physlib/FluidMechanics/IdealFluids/Bernoulli.lean  | 12 +++++++-----
 Physlib/FluidMechanics/IdealFluids/Continuity.lean | 10 ++++++++--
 Physlib/FluidMechanics/IdealFluids/Euler.lean      |  3 ++-
 4 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/Physlib/FluidMechanics/IdealFluids/Basic.lean b/Physlib/FluidMechanics/IdealFluids/Basic.lean
index 4a1309768..6d93b1f79 100644
--- a/Physlib/FluidMechanics/IdealFluids/Basic.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Basic.lean
@@ -12,8 +12,11 @@ public import Physlib.SpaceAndTime.Space.Module
 public import Physlib.SpaceAndTime.Time.Basic
 
 /-!
-This module introduces the idea of an ideal fluid and the mass flux density
-and basic physical properties, meant to be later used for proofs.
+This module establishes the core mathematical structure of an ideal fluid. It defines the
+
+- `continuous and differentiable fields` (dencity, velocity, pressure, entropy, and enthalpy)
+- `mass, entropy, energy flux densities`
+- `fluid volume structures` alongside surface integrals to compute various flows
 -/
 
 open scoped InnerProductSpace
diff --git a/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean b/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
index dc8749cfe..001bd57ec 100644
--- a/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
@@ -12,11 +12,13 @@ public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.SpaceAndTime.Time.Derivatives
 
 /-!
-This module introduces:
-steady flow,
-material derivative,
-isentropic behavious,
-the bernoulli equation
+This module focuses on defining specific flow states. It introduces the formal definitions of
+
+- `steady flow`
+- `isentropic behaviour`
+- `material derivative`
+
+after which it defines the `Bernoulli function`.
 -/
 
 open scoped InnerProductSpace
diff --git a/Physlib/FluidMechanics/IdealFluids/Continuity.lean b/Physlib/FluidMechanics/IdealFluids/Continuity.lean
index f66a85336..a16ea49e2 100644
--- a/Physlib/FluidMechanics/IdealFluids/Continuity.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Continuity.lean
@@ -12,8 +12,14 @@ public import Physlib.SpaceAndTime.Time.Derivatives
 public import Physlib.SpaceAndTime.Space.Derivatives.Div
 
 /-!
-This module introduces the continuity criterium.
-There is potential to add various different lemmas expanding on this.
+# Continuity and Incompressibility
+
+This module formulates mass conservation by defining the condidtions for an ideal fluid to satisfy
+the `Continuity Equation`.
+
+Additionally, it defines the mathematical model for `incompressibility` of a fluid.
+
+There is potential to extend this module broadly with various lemmas and theorems.
 -/
 
 open scoped InnerProductSpace
diff --git a/Physlib/FluidMechanics/IdealFluids/Euler.lean b/Physlib/FluidMechanics/IdealFluids/Euler.lean
index 9b80ed7eb..e0641b13a 100644
--- a/Physlib/FluidMechanics/IdealFluids/Euler.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Euler.lean
@@ -13,7 +13,8 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Grad
 public import Physlib.SpaceAndTime.Space.Derivatives.Div
 
 /-!
-This module introduces the Euler's equation.
+This module introduces the conservation of momentum in ideal fluids by formalizing
+the `Euler's equation`.
 -/
 
 open scoped InnerProductSpace

From e1442c20afa8a7266efdd9666fcaac2b0e381125 Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Fri, 22 May 2026 19:20:09 +0000
Subject: [PATCH 26/33] idiom

---
 Physlib/FluidMechanics/IdealFluids/Basic.lean | 40 +++++++++----------
 .../FluidMechanics/IdealFluids/Bernoulli.lean | 18 +++++----
 .../IdealFluids/Continuity.lean               | 10 +++--
 Physlib/FluidMechanics/IdealFluids/Euler.lean |  6 ++-
 4 files changed, 43 insertions(+), 31 deletions(-)

diff --git a/Physlib/FluidMechanics/IdealFluids/Basic.lean b/Physlib/FluidMechanics/IdealFluids/Basic.lean
index 6d93b1f79..bfc2f5c9f 100644
--- a/Physlib/FluidMechanics/IdealFluids/Basic.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Basic.lean
@@ -37,33 +37,33 @@ public structure IdealFluid where
   density_pos: ∀ t pos, 0 < density t pos
 
   /-- Ensuring that all are differentiable for more complex equations. -/
-  density_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>density s.1 s.2)
-  velocity_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>velocity s.1 s.2)
-  pressure_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>pressure s.1 s.2)
+  density_contdiff: ContDiff ℝ 1 (fun (t, pos) => density t pos)
+  velocity_contdiff: ContDiff ℝ 1 ( fun (t, pos) => velocity t pos)
+  pressure_contdiff: ContDiff ℝ 1 ( fun (t, pos) => pressure t pos)
 
-  entropy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>entropy s.1 s.2)
-  enthalpy_contdiff: ContDiff ℝ 1 ( fun(s:Time × Space)=>enthalpy s.1 s.2)
+  entropy_contdiff: ContDiff ℝ 1 ( fun (t, pos) => entropy t pos)
+  enthalpy_contdiff: ContDiff ℝ 1 ( fun(t, pos) => enthalpy t pos)
 
 namespace IdealFluid
 open MeasureTheory
 
 /-- Mass flux density j=ρv -/
-public abbrev massFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+public abbrev massFluxDensity (F : IdealFluid) (t : Time) (pos : Space):
     EuclideanSpace ℝ (Fin 3) :=
       F.density t pos • F.velocity t pos
 
 /-- Entropy flux density ρsv -/
-public abbrev entropyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+public abbrev entropyFluxDensity (F : IdealFluid) (t : Time) (pos : Space):
     EuclideanSpace ℝ (Fin 3) :=
-      (IdealFluid.entropy F t pos) • (IdealFluid.density F t pos) • (IdealFluid.velocity F t pos)
+      F.entropy t pos • F.density t pos • F.velocity t pos
 
 /-- Energy flux density ρv(1/2 |v|^2 + w) -/
-noncomputable abbrev energyFluxDensity (F: IdealFluid) (t: Time) (pos: Space):
+noncomputable abbrev energyFluxDensity (F : IdealFluid) (t : Time) (pos : Space):
     EuclideanSpace ℝ (Fin 3) :=
-      let w := IdealFluid.enthalpy F t pos
-      let v := IdealFluid.velocity F t pos
+      let w := F.enthalpy t pos
+      let v := F.velocity t pos
       let v_sq: ℝ := ⟪v,v⟫_ℝ
-      let scalar := (IdealFluid.density F t pos)*(0.5*v_sq + w)
+      let scalar := (F.density t pos)*(0.5*v_sq + w)
 
       scalar • v
 
@@ -77,23 +77,23 @@ structure FluidVolume where
   surfaceMeasure: Measure Space
 
 /-- Surface integral of a vector field -/
-noncomputable def surfaceIntegral (V: FluidVolume) (flux: Space → EuclideanSpace ℝ (Fin 3)):
+noncomputable def surfaceIntegral (V : FluidVolume) (flux : Space → EuclideanSpace ℝ (Fin 3)):
     ℝ :=
-      ∫ (pos: Space) in frontier V.region, ⟪flux pos, V.normal pos⟫_ℝ ∂V.surfaceMeasure
+      ∫ (pos : Space) in frontier V.region, ⟪flux pos, V.normal pos⟫_ℝ ∂V.surfaceMeasure
 
 /-- Mass flow out of volume -/
-noncomputable def massFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+noncomputable def massFlowOut (F : IdealFluid) (t : Time) (V : FluidVolume):
     ℝ :=
-      surfaceIntegral V (IdealFluid.massFluxDensity F t ·)
+      surfaceIntegral V (F.massFluxDensity t ·)
 
 /-- Entropy flow out of volume -/
-noncomputable def entropyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+noncomputable def entropyFlowOut (F : IdealFluid) (t : Time) (V : FluidVolume):
     ℝ :=
-      surfaceIntegral V (IdealFluid.entropyFluxDensity F t ·)
+      surfaceIntegral V (F.entropyFluxDensity t ·)
 
 /-- Energy flow out of volume -/
-noncomputable def energyFlowOut (F: IdealFluid) (t: Time) (V: FluidVolume):
+noncomputable def energyFlowOut (F : IdealFluid) (t : Time) (V : FluidVolume):
     ℝ :=
-      surfaceIntegral V (IdealFluid.energyFluxDensity F t ·)
+      surfaceIntegral V (F.energyFluxDensity t ·)
 
 end IdealFluid
diff --git a/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean b/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
index 001bd57ec..ea9782bff 100644
--- a/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Bernoulli.lean
@@ -25,28 +25,32 @@ open scoped InnerProductSpace
 open Time
 open Space
 
+namespace IdealFluid
+
 /-- Determines whether a flow is steady -/
-def IdealFluid.isSteady (F: IdealFluid) :
+def isSteady (F : IdealFluid) :
     Prop :=
       ∀ (pos : Space),
       ∂ₜ (F.velocity · pos) = 0
 
 /-- Definition of a material derivative -/
-noncomputable def IdealFluid.materialDerivative (t: Time) (pos: Space)
-(F: IdealFluid) (f: Time → Space → ℝ) :
+noncomputable def materialDerivative ( t: Time) (pos : Space)
+(F : IdealFluid) (f : Time → Space → ℝ) :
     ℝ :=
       ∂ₜ (f · pos) t +
       ⟪F.velocity t pos, ∇ (f t ·) pos ⟫_ℝ
 
 /-- Determines whether a flow is isentropic -/
-def IdealFluid.isIsentropic (F: IdealFluid):
+def isIsentropic (F : IdealFluid):
     Prop :=
-      ∀ (t: Time) (pos: Space),
+      ∀ (t : Time) (pos : Space),
       F.materialDerivative t pos F.entropy = 0
 
 /-- The Bernoulli function (1/2)v^2 + w -/
-noncomputable def IdealFluid.bernoulliEquation (F: IdealFluid)
-(t: Time) (pos: Space) (g: Space → ℝ):
+noncomputable def bernoulliEquation (F : IdealFluid)
+(t : Time) (pos : Space) (g : Space → ℝ):
     ℝ :=
       let v := F.velocity t pos
       0.5 * ⟪v, v⟫_ℝ + F.enthalpy t pos + g pos
+
+end IdealFluid
diff --git a/Physlib/FluidMechanics/IdealFluids/Continuity.lean b/Physlib/FluidMechanics/IdealFluids/Continuity.lean
index a16ea49e2..f1b78f6a3 100644
--- a/Physlib/FluidMechanics/IdealFluids/Continuity.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Continuity.lean
@@ -14,7 +14,7 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Div
 /-!
 # Continuity and Incompressibility
 
-This module formulates mass conservation by defining the condidtions for an ideal fluid to satisfy
+This module formulates mass conservation by defining the conditions for an ideal fluid to satisfy
 the `Continuity Equation`.
 
 Additionally, it defines the mathematical model for `incompressibility` of a fluid.
@@ -26,14 +26,18 @@ open scoped InnerProductSpace
 open Time
 open Space
 
+namespace IdealFluid
+
 /-- defining satisfying the equation of continuity -/
-public def IdealFluid.satisfiesContinuity (F : IdealFluid):
+public def satisfiesContinuity (F : IdealFluid):
     Prop :=
       ∀ (t : Time) (pos : Space),
       ∂ₜ (F.density · pos) t +
       Space.div (F.massFluxDensity t ·) pos = (0 : ℝ)
 
 /-- Criterion for incompressibility -/
-public def IdealFluid.isIncompressible (F : IdealFluid):
+public def isIncompressible (F : IdealFluid):
   Prop :=
     ∀ (t : Time) (pos : Space), ∂ₜ (F.density · pos) t = 0
+
+end IdealFluid
diff --git a/Physlib/FluidMechanics/IdealFluids/Euler.lean b/Physlib/FluidMechanics/IdealFluids/Euler.lean
index e0641b13a..ba7f8b01f 100644
--- a/Physlib/FluidMechanics/IdealFluids/Euler.lean
+++ b/Physlib/FluidMechanics/IdealFluids/Euler.lean
@@ -21,11 +21,15 @@ open scoped InnerProductSpace
 open Time
 open Space
 
+namespace IdealFluid
+
 /-- Defines the property of satisfying Euler's equation. -/
-public def IdealFluid.satisfiesEuler (F: IdealFluid) (g: Space → ℝ):
+public def satisfiesEuler (F : IdealFluid) (g : Space → ℝ):
   Prop :=
     ∀ (t : Time) (pos : Space),
       let v := F.velocity t pos
       ∂ₜ (F.velocity · pos) t +
       (fun i => ⟪v, Space.grad (F.velocity t · i) pos⟫_ℝ)
       = -(1/F.density t pos) • Space.grad (F.pressure t ·) pos + Space.grad g pos
+
+end IdealFluid

From be126a9ee22ea98237956a3f5ae949495ec32b2c Mon Sep 17 00:00:00 2001
From: mog1el <m.mogielnicki@gmail.com>
Date: Sat, 23 May 2026 06:28:00 +0000
Subject: [PATCH 27/33] fix alphabetical order

---
 Physlib.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Physlib.lean b/Physlib.lean
index f00e4f40d..e02979bbd 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -47,11 +47,11 @@ 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.Mathematics.Calculus.AdjFDeriv
 public import Physlib.FluidMechanics.IdealFluids.Basic
 public import Physlib.FluidMechanics.IdealFluids.Bernoulli
 public import Physlib.FluidMechanics.IdealFluids.Continuity
 public import Physlib.FluidMechanics.IdealFluids.Euler
+public import Physlib.Mathematics.Calculus.AdjFDeriv
 public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
 public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap

From 3f089996f892dc1cb19efe2d8a324eabe4d3262f Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Sat, 23 May 2026 16:16:20 +0200
Subject: [PATCH 28/33] refactor(FluidDynamics): clarify continuity regularity

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 14 +++---
 .../NavierStokes/Continuity.lean              | 47 ++++++++++++++-----
 .../FluidDynamics/NavierStokes/Momentum.lean  | 18 +++++--
 3 files changed, 55 insertions(+), 24 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 576d51fcc..ebcb9156e 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -16,14 +16,14 @@ 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 continuity equation with the conservative and convective momentum
-equations. 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 combines the classical continuity equation with the conservative and convective
+momentum equations. 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
 
-- `ConservativeForm` : Continuity and conservative momentum equations together.
-- `ConvectiveForm` : Continuity and convective momentum equations together.
+- `ConservativeForm` : Classical continuity and conservative momentum equations together.
+- `ConvectiveForm` : Classical continuity and convective momentum equations together.
 - `ConservativeForm_iff_ConvectiveForm` : Equivalence of the two forms when the
   fields are differentiable.
 
@@ -48,12 +48,12 @@ namespace NavierStokes
 
 /-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
 def ConservativeForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
-  ContinuityEquation d data.toFluidState ∧
+  ClassicalContinuityEquation d data.toFluidState ∧
     ConservativeMomentumEquation d data
 
 /-- The convective Navier-Stokes form with an externally supplied stress tensor. -/
 def ConvectiveForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
-  ContinuityEquation d data.toFluidState ∧
+  ClassicalContinuityEquation d data.toFluidState ∧
     ConvectiveMomentumEquation d data
 
 /-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
diff --git a/Physlib/FluidDynamics/NavierStokes/Continuity.lean b/Physlib/FluidDynamics/NavierStokes/Continuity.lean
index 9b07d8c3e..6420c8e52 100644
--- a/Physlib/FluidDynamics/NavierStokes/Continuity.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Continuity.lean
@@ -14,17 +14,19 @@ public import Physlib.SpaceAndTime.Time.Derivatives
 
 ## i. Overview
 
-This module defines the 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 state and
+the corresponding continuity residual.
 
 ## ii. Key results
 
-- `ContinuityEquation` : Conservation of mass in conservative form.
+- `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.
 
 ## iii. Table of contents
 
-- A. Continuity equation
+- A. Continuity equations
 
 ## iv. References
 
@@ -40,24 +42,45 @@ namespace NavierStokes
 
 /-!
 
-## A. Continuity equation
+## A. Continuity equations
 
 -/
 
-/-- Conservation of mass in conservative form, `partial_t rho + div (rho u) = 0`. -/
-def ContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
+/-- Classical conservation of mass in conservative form, `partial_t rho + div (rho u) = 0`.
+
+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 :=
   ∀ t x,
-    ∂ₜ (fun t' => fluid.rho t' x) t +
-      (∇ ⬝ fun x' => fluid.rho t x' • fluid.velocity t x') x =
-        0
+    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 → ℝ :=
   fun t x =>
-    ∂ₜ (fun t' => fluid.rho t' x) t +
-      (∇ ⬝ 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
+
+/-- A stronger continuity equation for globally differentiable fields.
+
+This version records the first-order regularity needed by the classical continuity equation:
+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 :=
+  (∀ 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) :
+    SmoothContinuityEquation d fluid →
+      ClassicalContinuityEquation d fluid := by
+  intro hSmooth t x _ _
+  simpa [continuityResidual] using hSmooth.2.2 t x
 
 end NavierStokes
 end FluidDynamics
diff --git a/Physlib/FluidDynamics/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
index 02b128a38..b5f2c9fe9 100644
--- a/Physlib/FluidDynamics/NavierStokes/Momentum.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
@@ -252,15 +252,15 @@ 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 continuity
-equation holds.
+/-- The conservative and convective 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 ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
     (d : ℕ) (data : FluidInMomentumBalance d)
-    (hContinuity : ContinuityEquation d data.toFluidState)
+    (hContinuity : ClassicalContinuityEquation d data.toFluidState)
     (hRhoTime : ∀ t x,
       DifferentiableAt ℝ (fun t' => data.rho t' x) t)
     (hVelocityTime : ∀ t x,
@@ -272,8 +272,12 @@ theorem ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
       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
+      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)
@@ -287,8 +291,12 @@ theorem ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
     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
+      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)

From 68d2a81cf24ef72322da9a81f28ff9271270a1e3 Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Sat, 23 May 2026 16:18:17 +0200
Subject: [PATCH 29/33] refactor(FluidDynamics): simplify momentum equation API

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 12 ++---
 .../FluidDynamics/NavierStokes/Momentum.lean  | 53 +++++++++----------
 2 files changed, 30 insertions(+), 35 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index ebcb9156e..4ddca8846 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -49,7 +49,7 @@ namespace NavierStokes
 /-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
 def ConservativeForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
   ClassicalContinuityEquation d data.toFluidState ∧
-    ConservativeMomentumEquation d data
+    MomentumEquation d data
 
 /-- The convective Navier-Stokes form with an externally supplied stress tensor. -/
 def ConvectiveForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
@@ -60,10 +60,8 @@ def ConvectiveForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
 differentiable enough for the product rules. -/
 theorem ConservativeForm_iff_ConvectiveForm
     (d : ℕ) (data : FluidInMomentumBalance d)
-    (hRhoTime : ∀ t x,
-      DifferentiableAt ℝ (fun t' => data.rho t' x) t)
-    (hVelocityTime : ∀ t x,
-      DifferentiableAt ℝ (fun t' => data.velocity t' x) t)
+    (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)) :
@@ -72,12 +70,12 @@ theorem ConservativeForm_iff_ConvectiveForm
   constructor
   · intro hConservative
     refine ⟨hConservative.1, ?_⟩
-    exact (ConservativeMomentumEquation_iff_ConvectiveMomentumEquation d data hConservative.1
+    exact (MomentumEquation_iff_ConvectiveMomentumEquation d data hConservative.1
       hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp
       hConservative.2
   · intro hConvective
     refine ⟨hConvective.1, ?_⟩
-    exact (ConservativeMomentumEquation_iff_ConvectiveMomentumEquation d data hConvective.1
+    exact (MomentumEquation_iff_ConvectiveMomentumEquation d data hConvective.1
       hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr
       hConvective.2
 
diff --git a/Physlib/FluidDynamics/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
index b5f2c9fe9..81bb1ab43 100644
--- a/Physlib/FluidDynamics/NavierStokes/Momentum.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
@@ -21,11 +21,11 @@ balance-law layer before specializing to a Newtonian stress law.
 
 - `momentumDensity` : The vector momentum density `rho u`.
 - `momentumFlux` : The convective momentum flux `rho u ⊗ u`.
-- `ConservativeMomentumEquation` : Conservation of momentum using `Space.matrixDiv`.
+- `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.
-- `ConservativeMomentumEquation_iff_ConvectiveMomentumEquation` : Equivalence of the two
+- `MomentumEquation_iff_ConvectiveMomentumEquation` : Equivalence of the two
   momentum equations when continuity holds and the fields are differentiable.
 
 ## iii. Table of contents
@@ -78,9 +78,9 @@ The equation is
 
 Here `stress` is intentionally not yet specialized to a Newtonian stress law.
 -/
-def ConservativeMomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
+def MomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
   ∀ t x,
-    ∂ₜ (fun t' => momentumDensity d data.toFluidState t' x) t +
+    ∂ₜ (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
@@ -92,14 +92,14 @@ def ConservativeMomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : P
 -/
 
 /-- The nonlinear transport term `(u · ∇)u`. -/
-noncomputable def convectiveTerm (d : ℕ) (velocity : VelocityField d) : VectorField d :=
-  fun t x => ∑ j, velocity t x j • ∂[j] (velocity t) x
+noncomputable def convectiveTerm (d : ℕ) (fluid : FluidState 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 : ℕ) (velocity : VelocityField d) : VectorField d :=
+noncomputable def materialAcceleration (d : ℕ) (fluid : FluidState d) : VectorField d :=
   fun t x =>
-    ∂ₜ (fun t' => velocity t' x) t +
-      convectiveTerm d velocity t x
+    ∂ₜ (fluid.velocity · x) t +
+      convectiveTerm d fluid t x
 
 /-- Conservation of momentum in convective form.
 
@@ -111,7 +111,7 @@ 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.velocity 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
 
@@ -124,12 +124,12 @@ def ConvectiveMomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : Pro
 /-- The left-hand side of the conservative momentum equation. -/
 noncomputable def conservativeMomentumLHS (d : ℕ) (fluid : FluidState d) : VectorField d :=
   fun t x =>
-    ∂ₜ (fun t' => momentumDensity d fluid t' x) t +
+    ∂ₜ (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.velocity t x
+  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 → ℝ)
@@ -149,14 +149,13 @@ lemma timeDeriv_smul_velocity (d : ℕ) (rhoAtPosition : Time → ℝ)
 /-- Product rule for the time derivative of the momentum density `rho u`. -/
 lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidState d)
     (t : Time) (x : Space d)
-    (hRho : DifferentiableAt ℝ (fun t' => fluid.rho t' x) t)
-    (hVelocity : DifferentiableAt ℝ (fun t' => fluid.velocity t' x) t) :
-    ∂ₜ (fun t' => momentumDensity d fluid t' x) t =
-      fluid.rho t x • ∂ₜ (fun t' => fluid.velocity t' x) t +
-        ∂ₜ (fun t' => fluid.rho t' x) t • fluid.velocity t x := by
+    (hRho : DifferentiableAt ℝ (fluid.rho · x) t)
+    (hVelocity : DifferentiableAt ℝ (fluid.velocity · x) t) :
+    ∂ₜ (momentumDensity d fluid · x) t =
+      fluid.rho t x • ∂ₜ (fluid.velocity · x) t +
+        ∂ₜ (fluid.rho · x) t • fluid.velocity t x := by
   simpa [momentumDensity] using
-    timeDeriv_smul_velocity d (fun t' => fluid.rho t' x)
-      (fun t' => fluid.velocity t' x) t hRho hVelocity
+    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)
@@ -185,7 +184,7 @@ lemma matrixDiv_momentumFlux (d : ℕ) (fluid : FluidState d)
     (hVelocity : Differentiable ℝ (fluid.velocity t)) :
     matrixDiv d (momentumFlux d fluid t) x =
       (∇ ⬝ momentumDensity d fluid t) x • fluid.velocity t x +
-        fluid.rho t x • convectiveTerm d fluid.velocity t x := by
+        fluid.rho t x • convectiveTerm d fluid t x := by
   ext i
   simp [matrixDiv_apply, div, convectiveTerm, smul_eq_mul]
   change (∑ j, ∂[j] (fun x' =>
@@ -238,8 +237,8 @@ the continuity residual times the velocity field.
 lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_smul
     (d : ℕ) (fluid : FluidState d)
     (t : Time) (x : Space d)
-    (hRhoTime : DifferentiableAt ℝ (fun t' => fluid.rho t' x) t)
-    (hVelocityTime : DifferentiableAt ℝ (fun t' => fluid.velocity t' x) t)
+    (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 =
@@ -258,17 +257,15 @@ 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 ConservativeMomentumEquation_iff_ConvectiveMomentumEquation
+theorem MomentumEquation_iff_ConvectiveMomentumEquation
     (d : ℕ) (data : FluidInMomentumBalance d)
     (hContinuity : ClassicalContinuityEquation d data.toFluidState)
-    (hRhoTime : ∀ t x,
-      DifferentiableAt ℝ (fun t' => data.rho t' x) t)
-    (hVelocityTime : ∀ t x,
-      DifferentiableAt ℝ (fun t' => data.velocity t' x) t)
+    (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)) :
-    ConservativeMomentumEquation d data ↔
+    MomentumEquation d data ↔
       ConvectiveMomentumEquation d data := by
   constructor
   · intro hConservative t x

From 9c0190acd186cfda17c09e959322516c925b094b Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Sat, 23 May 2026 16:19:18 +0200
Subject: [PATCH 30/33] refactor(FluidDynamics): make Navier-Stokes canonical

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 44 +++++++++----------
 1 file changed, 20 insertions(+), 24 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 4ddca8846..4632c4d50 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -16,15 +16,15 @@ 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 conservative and convective
-momentum equations. 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 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
 
-- `ConservativeForm` : Classical continuity and conservative momentum equations together.
-- `ConvectiveForm` : Classical continuity and convective momentum equations together.
-- `ConservativeForm_iff_ConvectiveForm` : Equivalence of the two forms when the
+- `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
@@ -38,7 +38,6 @@ balance-law layer before specializing to a Newtonian stress law.
 @[expose] public section
 
 namespace FluidDynamics
-namespace NavierStokes
 
 /-!
 
@@ -47,37 +46,34 @@ namespace NavierStokes
 -/
 
 /-- The conservative Navier-Stokes balance-law form with an externally supplied stress tensor. -/
-def ConservativeForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
-  ClassicalContinuityEquation d data.toFluidState ∧
-    MomentumEquation d data
+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 ConvectiveForm (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
-  ClassicalContinuityEquation d data.toFluidState ∧
-    ConvectiveMomentumEquation d data
+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 ConservativeForm_iff_ConvectiveForm
+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 ℝ (momentumDensity d data.toFluidState t))
+      Differentiable ℝ (FluidDynamics.NavierStokes.momentumDensity d data.toFluidState t))
     (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
-    ConservativeForm d data ↔
-      ConvectiveForm d data := by
+    NavierStokes d data ↔
+      ConvectiveNavierStokes d data := by
   constructor
   · intro hConservative
     refine ⟨hConservative.1, ?_⟩
-    exact (MomentumEquation_iff_ConvectiveMomentumEquation d data hConservative.1
-      hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp
-      hConservative.2
+    exact (FluidDynamics.NavierStokes.MomentumEquation_iff_ConvectiveMomentumEquation d data
+      hConservative.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp hConservative.2
   · intro hConvective
     refine ⟨hConvective.1, ?_⟩
-    exact (MomentumEquation_iff_ConvectiveMomentumEquation d data hConvective.1
-      hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr
-      hConvective.2
+    exact (FluidDynamics.NavierStokes.MomentumEquation_iff_ConvectiveMomentumEquation d data
+      hConvective.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr hConvective.2
 
-end NavierStokes
 end FluidDynamics

From 7e5fbf92dc970ece091f946a0a4682005533d6db Mon Sep 17 00:00:00 2001
From: Florian Wiesner <wiesnerflorian94@gmail.com>
Date: Sat, 23 May 2026 16:31:52 +0200
Subject: [PATCH 31/33] style(FluidDynamics): tighten Navier-Stokes formatting

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean |  3 +-
 .../NavierStokes/Continuity.lean              | 12 +--
 .../FluidDynamics/NavierStokes/Momentum.lean  | 79 ++++++-------------
 3 files changed, 30 insertions(+), 64 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 4632c4d50..3cdf862e1 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -64,8 +64,7 @@ theorem NavierStokes_iff_ConvectiveNavierStokes
     (hMomentumDensity : ∀ t,
       Differentiable ℝ (FluidDynamics.NavierStokes.momentumDensity d data.toFluidState t))
     (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
-    NavierStokes d data ↔
-      ConvectiveNavierStokes d data := by
+    NavierStokes d data ↔ ConvectiveNavierStokes d data := by
   constructor
   · intro hConservative
     refine ⟨hConservative.1, ?_⟩
diff --git a/Physlib/FluidDynamics/NavierStokes/Continuity.lean b/Physlib/FluidDynamics/NavierStokes/Continuity.lean
index 6420c8e52..458070d7b 100644
--- a/Physlib/FluidDynamics/NavierStokes/Continuity.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Continuity.lean
@@ -52,17 +52,14 @@ The equation is asserted at points where the time derivative of `rho` and the sp
 divergence of `rho u` are classical derivatives.
 -/
 def ClassicalContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
-  ∀ t x,
-    DifferentiableAt ℝ (fluid.rho · x) t →
+  ∀ 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 → ℝ :=
-  fun t x =>
-    ∂ₜ (fluid.rho · x) t + (∇ ⬝ fun x' => fluid.rho t x' • fluid.velocity t x') x
+noncomputable def continuityResidual (d : ℕ) (fluid : FluidState 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.
 
@@ -77,8 +74,7 @@ def SmoothContinuityEquation (d : ℕ) (fluid : FluidState d) : Prop :=
 
 /-- A smooth continuity equation satisfies the guarded classical continuity equation. -/
 lemma SmoothContinuityEquation.toClassical (d : ℕ) (fluid : FluidState d) :
-    SmoothContinuityEquation d fluid →
-      ClassicalContinuityEquation d fluid := by
+    SmoothContinuityEquation d fluid → ClassicalContinuityEquation d fluid := by
   intro hSmooth t x _ _
   simpa [continuityResidual] using hSmooth.2.2 t x
 
diff --git a/Physlib/FluidDynamics/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
index 81bb1ab43..3e3fea72f 100644
--- a/Physlib/FluidDynamics/NavierStokes/Momentum.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
@@ -58,11 +58,10 @@ def momentumDensity (d : ℕ) (fluid : FluidState 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 : FluidState 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)
+    fluid.rho t x • Matrix.vecMulVec (fun i => fluid.velocity t x i)
+      (fun j => fluid.velocity t x j)
 
 /-!
 
@@ -82,8 +81,7 @@ 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
+      matrixDiv d (data.stress t) x + data.rho t x • data.bodyForce t x
 
 /-!
 
@@ -97,9 +95,7 @@ noncomputable def convectiveTerm (d : ℕ) (fluid : FluidState d) : VectorField
 
 /-- The material acceleration `∂ₜ u + (u · ∇)u`. -/
 noncomputable def materialAcceleration (d : ℕ) (fluid : FluidState d) : VectorField d :=
-  fun t x =>
-    ∂ₜ (fluid.velocity · x) t +
-      convectiveTerm d fluid t x
+  fun t x => ∂ₜ (fluid.velocity · x) t + convectiveTerm d fluid t x
 
 /-- Conservation of momentum in convective form.
 
@@ -112,8 +108,7 @@ 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
+      matrixDiv d (data.stress t) x + data.rho t x • data.bodyForce t x
 
 /-!
 
@@ -123,9 +118,7 @@ def ConvectiveMomentumEquation (d : ℕ) (data : FluidInMomentumBalance d) : Pro
 
 /-- 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
+  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 :=
@@ -137,8 +130,7 @@ lemma timeDeriv_smul_velocity (d : ℕ) (rhoAtPosition : Time → ℝ)
     (hRho : DifferentiableAt ℝ rhoAtPosition t)
     (hVelocity : DifferentiableAt ℝ velocityAtPosition t) :
     ∂ₜ (fun t' => rhoAtPosition t' • velocityAtPosition t') t =
-      rhoAtPosition t • ∂ₜ velocityAtPosition t +
-        ∂ₜ rhoAtPosition t • velocityAtPosition t := by
+      rhoAtPosition t • ∂ₜ velocityAtPosition t + ∂ₜ rhoAtPosition t • velocityAtPosition t := by
   rw [Time.deriv_eq, Time.deriv_eq, Time.deriv_eq]
   change (fderiv ℝ (rhoAtPosition • velocityAtPosition) t) 1 =
     rhoAtPosition t • (fderiv ℝ velocityAtPosition t) 1 +
@@ -152,8 +144,7 @@ lemma timeDeriv_momentumDensity (d : ℕ) (fluid : FluidState d)
     (hRho : DifferentiableAt ℝ (fluid.rho · x) t)
     (hVelocity : DifferentiableAt ℝ (fluid.velocity · x) t) :
     ∂ₜ (momentumDensity d fluid · x) t =
-      fluid.rho t x • ∂ₜ (fluid.velocity · x) t +
-        ∂ₜ (fluid.rho · x) t • fluid.velocity t x := by
+      fluid.rho t x • ∂ₜ (fluid.velocity · x) t + ∂ₜ (fluid.rho · x) t • fluid.velocity t x := by
   simpa [momentumDensity] using
     timeDeriv_smul_velocity d (fluid.rho · x) (fluid.velocity · x) t hRho hVelocity
 
@@ -163,10 +154,8 @@ lemma spaceDeriv_momentumFlux_component (d : ℕ) (fluid : FluidState 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
+      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
   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)
@@ -187,32 +176,21 @@ lemma matrixDiv_momentumFlux (d : ℕ) (fluid : FluidState d)
         fluid.rho t x • convectiveTerm d fluid t x := by
   ext i
   simp [matrixDiv_apply, div, convectiveTerm, smul_eq_mul]
-  change (∑ j, ∂[j] (fun x' =>
-      momentumFlux d fluid t x' i j) x) =
-    (∑ j, ∂[j] (fun x' =>
-      momentumDensity d fluid t x' j) x) *
-        fluid.velocity t x i +
-      fluid.rho t x *
-        (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i)
+  change (∑ j, ∂[j] (fun x' => momentumFlux d fluid t x' i j) x) =
+    (∑ j, ∂[j] (fun x' => momentumDensity d fluid t x' j) x) * fluid.velocity t x i +
+      fluid.rho t x * (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i)
   calc
-    (∑ j, ∂[j] (fun x' =>
-        momentumFlux d fluid t x' i j) x)
+    (∑ j, ∂[j] (fun x' => momentumFlux d fluid t x' i j) x)
         = ∑ j,
-            (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
+            (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
           apply Finset.sum_congr rfl
           intro j _
           rw [spaceDeriv_momentumFlux_component d fluid t x i j
             hMomentumDensity hVelocity]
           simp [smul_eq_mul]
-    _ = fluid.velocity t x i *
-          (∑ j, ∂[j] (fun x' =>
-            momentumDensity d fluid t x' j) x) +
-        fluid.rho t x *
-          (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i) := by
+    _ = fluid.velocity t x i * (∑ j, ∂[j] (fun x' => momentumDensity d fluid t x' j) x) +
+        fluid.rho t x * (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i) := by
           rw [Finset.sum_add_distrib]
           congr 1
           · rw [Finset.mul_sum]
@@ -222,11 +200,8 @@ lemma matrixDiv_momentumFlux (d : ℕ) (fluid : FluidState d)
             rw [Space.deriv_euclid (ν := j) (μ := i) (f := fluid.velocity t)
               hVelocity x]
             simp [momentumDensity, mul_comm, mul_assoc]
-    _ = (∑ j, ∂[j] (fun x' =>
-          momentumDensity d fluid t x' j) x) *
-          fluid.velocity t x i +
-        fluid.rho t x *
-          (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i) := by
+    _ = (∑ j, ∂[j] (fun x' => momentumDensity d fluid t x' j) x) * fluid.velocity t x i +
+        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.
@@ -242,8 +217,7 @@ lemma conservativeMomentumLHS_eq_convectiveMomentumLHS_add_continuityResidual_sm
     (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
+      convectiveMomentumLHS d fluid t x + continuityResidual d fluid t x • fluid.velocity t x := by
   rw [conservativeMomentumLHS, convectiveMomentumLHS, continuityResidual]
   rw [timeDeriv_momentumDensity d fluid t x hRhoTime hVelocityTime]
   rw [matrixDiv_momentumFlux d fluid t x hMomentumDensity hVelocitySpace]
@@ -265,8 +239,7 @@ theorem MomentumEquation_iff_ConvectiveMomentumEquation
     (hMomentumDensity : ∀ t,
       Differentiable ℝ (momentumDensity d data.toFluidState t))
     (hVelocitySpace : ∀ t, Differentiable ℝ (data.velocity t)) :
-    MomentumEquation d data ↔
-      ConvectiveMomentumEquation d data := by
+    MomentumEquation d data ↔ ConvectiveMomentumEquation d data := by
   constructor
   · intro hConservative t x
     have hMassFluxSpace :
@@ -283,8 +256,7 @@ theorem MomentumEquation_iff_ConvectiveMomentumEquation
           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
+      matrixDiv d (data.stress t) x + data.rho t x • data.bodyForce t x
     rw [← hLhs']
     exact hConservative t x
   · intro hConvective t x
@@ -302,8 +274,7 @@ theorem MomentumEquation_iff_ConvectiveMomentumEquation
           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
+      matrixDiv d (data.stress t) x + data.rho t x • data.bodyForce t x
     rw [hLhs']
     exact hConvective t x
 

From 61c84682223001548f66b2fc489f22e0a1870dc8 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 26 May 2026 08:29:05 +0100
Subject: [PATCH 32/33] refactor: Names

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean    | 2 +-
 Physlib/FluidDynamics/NavierStokes/Momentum.lean | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 3cdf862e1..8778a74e1 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -57,7 +57,7 @@ def ConvectiveNavierStokes (d : ℕ) (data : FluidInMomentumBalance d) : Prop :=
 
 /-- The conservative and convective Navier-Stokes forms are equivalent when the fields are
 differentiable enough for the product rules. -/
-theorem NavierStokes_iff_ConvectiveNavierStokes
+theorem navierStokes_iff_convectiveNavierStokes
     (d : ℕ) (data : FluidInMomentumBalance d)
     (hRhoTime : ∀ t x, DifferentiableAt ℝ (data.rho · x) t)
     (hVelocityTime : ∀ t x, DifferentiableAt ℝ (data.velocity · x) t)
diff --git a/Physlib/FluidDynamics/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
index 3e3fea72f..b2dbc1911 100644
--- a/Physlib/FluidDynamics/NavierStokes/Momentum.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Momentum.lean
@@ -25,7 +25,7 @@ balance-law layer before specializing to a Newtonian stress law.
 - `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
+- `momentumEquation_iff_convectiveMomentumEquation` : Equivalence of the two
   momentum equations when continuity holds and the fields are differentiable.
 
 ## iii. Table of contents
@@ -231,7 +231,7 @@ 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 MomentumEquation_iff_ConvectiveMomentumEquation
+theorem momentumEquation_iff_convectiveMomentumEquation
     (d : ℕ) (data : FluidInMomentumBalance d)
     (hContinuity : ClassicalContinuityEquation d data.toFluidState)
     (hRhoTime : ∀ t x, DifferentiableAt ℝ (data.rho · x) t)

From f9200249da4525701d9f3d6c1d3f185b4b426f11 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 26 May 2026 08:31:45 +0100
Subject: [PATCH 33/33] refactor: LInt

---
 Physlib/FluidDynamics/NavierStokes/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Physlib/FluidDynamics/NavierStokes/Basic.lean b/Physlib/FluidDynamics/NavierStokes/Basic.lean
index 8778a74e1..89fa5e940 100644
--- a/Physlib/FluidDynamics/NavierStokes/Basic.lean
+++ b/Physlib/FluidDynamics/NavierStokes/Basic.lean
@@ -68,11 +68,11 @@ theorem navierStokes_iff_convectiveNavierStokes
   constructor
   · intro hConservative
     refine ⟨hConservative.1, ?_⟩
-    exact (FluidDynamics.NavierStokes.MomentumEquation_iff_ConvectiveMomentumEquation d data
+    exact (FluidDynamics.NavierStokes.momentumEquation_iff_convectiveMomentumEquation d data
       hConservative.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mp hConservative.2
   · intro hConvective
     refine ⟨hConvective.1, ?_⟩
-    exact (FluidDynamics.NavierStokes.MomentumEquation_iff_ConvectiveMomentumEquation d data
+    exact (FluidDynamics.NavierStokes.momentumEquation_iff_convectiveMomentumEquation d data
       hConvective.1 hRhoTime hVelocityTime hMomentumDensity hVelocitySpace).mpr hConvective.2
 
 end FluidDynamics