Refactor Riemannian Util layout and simp helpers (#5 #6 #7)

OpenGALib/Riemannian.lean

@@ -10,11 +10,11 @@ import OpenGALib.Riemannian.Operators.Hessian
 import OpenGALib.Riemannian.Operators.Laplacian
 import OpenGALib.Riemannian.Operators.SecondFundamentalForm
 import OpenGALib.Riemannian.TensorBundle.BundleSectionContinuity
-import OpenGALib.Riemannian.Util.ChartJacobianSmooth
-import OpenGALib.Riemannian.Util.ChartJacobianSmoothness
-import OpenGALib.Riemannian.Util.CovDerivBridges
-import OpenGALib.Riemannian.Util.DivergenceSimp
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
+import OpenGALib.Riemannian.Util.Chart.ChartJacobianCLM
+import OpenGALib.Riemannian.Util.Chart.ChartJacobianEntries
+import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges
+import OpenGALib.Riemannian.Util.Simp.OperatorSimp
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
 import OpenGALib.Riemannian.TensorBundle.Defs
 import OpenGALib.Riemannian.TangentBundle.TangentSmooth
 import OpenGALib.Riemannian.Instances.EuclideanSpace

OpenGALib/Riemannian/Connection/Koszul.lean

@@ -3,7 +3,7 @@ import Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
 import Mathlib.Geometry.Manifold.VectorField.LieBracket
 import OpenGALib.Riemannian.Manifold.SmoothManifold
 import OpenGALib.Riemannian.TangentBundle.TangentSmooth
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
 /-!
 # Koszul functional and its algebraic identities
 

OpenGALib/Riemannian/Connection/LeviCivita.lean

@@ -6,11 +6,11 @@ import Mathlib.Geometry.Manifold.VectorField.LieBracket
 import OpenGALib.Riemannian.Manifold.SmoothManifold
 import OpenGALib.Riemannian.TangentBundle.TangentSmooth
 import OpenGALib.Riemannian.TensorBundle.MusicalIso
-import OpenGALib.Riemannian.Util.TangentHelpers
+import OpenGALib.Riemannian.Util.Tangent.TangentHelpers
 import OpenGALib.Riemannian.Connection.Koszul
 import OpenGALib.Riemannian.Connection.RieszExtraction
-import OpenGALib.Riemannian.Util.CovDerivSmoothness
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
+import OpenGALib.Riemannian.Util.CovDeriv.CovDerivSmoothness
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
 import OpenGALib.Util.Attributes
 
 /-!

OpenGALib/Riemannian/Curvature/RiemannCurvature.lean

@@ -2,16 +2,16 @@ import OpenGALib.Riemannian.Connection.LeviCivita
 import OpenGALib.Riemannian.Connection.LeviCivita
 import OpenGALib.Riemannian.TangentBundle.TangentSmooth
 import OpenGALib.Riemannian.Operators.HessianLie
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
--- `riemannCurvature HasMetric.metric X Y Z` notation is now defined inline in `Connection.lean`
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
+-- `Riem(X, Y) Z` notation is now defined inline in `Connection.lean`
 -- alongside `riemannCurvature`; it transitively reaches us via the
 -- `import OpenGALib.Riemannian.Connection.LeviCivita` above.
 import Mathlib.LinearAlgebra.Trace
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Analysis.InnerProductSpace.Trace
 import Mathlib.Geometry.Manifold.VectorField.LieBracket
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
-import OpenGALib.Riemannian.Util.CovDerivBridges
+import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges
 
 /-!
 # Riemann curvature, Ricci, and scalar curvature
@@ -1086,4 +1086,3 @@ theorem sectionalCurvature_symmetric
     rw [hXY]; ring
 
 end Riemannian
-

OpenGALib/Riemannian/Curvature/Tensoriality.lean

@@ -1,6 +1,6 @@
 import OpenGALib.Riemannian.Curvature.RiemannCurvature
 import OpenGALib.Riemannian.Operators.Gradient
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
 import Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
 import Mathlib.Geometry.Manifold.BumpFunction
 import Mathlib.LinearAlgebra.Dimension.Free

OpenGALib/Riemannian/Manifold/SmoothManifold.lean

@@ -1,5 +1,4 @@
 import OpenGALib.Riemannian.Metric.RiemannianMetric
-import OpenGALib.Riemannian.Util.MetricNotation
 import OpenGALib.Util.Attributes
 import OpenGALib.Riemannian.TangentBundle.LocallyConstant
 

OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean

@@ -9,7 +9,7 @@ import OpenGALib.Riemannian.TensorBundle.SmoothOrthoFrame
 import OpenGALib.Riemannian.TensorBundle.SmoothOrthoFrame.Smoothness
 import OpenGALib.Util.Notation
 import Mathlib.Analysis.InnerProductSpace.Trace
-import OpenGALib.Riemannian.Util.CovDerivBridges
+import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges
 
 /-!
 # Bochner expansion: Ricci-identity-driven chain

OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean

@@ -6,10 +6,10 @@ import OpenGALib.Riemannian.Curvature.Tensoriality
 import OpenGALib.Riemannian.Operators.Gradient
 import OpenGALib.Riemannian.TensorBundle.SmoothOrthoFrame
 import OpenGALib.Riemannian.TensorBundle.SmoothOrthoFrame.Smoothness
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
 import OpenGALib.Util.Notation
 import Mathlib.Analysis.InnerProductSpace.Trace
-import OpenGALib.Riemannian.Util.CovDerivBridges
+import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges
 
 /-!
 # Bochner anchor — Hessian expansion of `|∇f|²`

OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean

@@ -1,10 +1,10 @@
 import OpenGALib.Riemannian.Operators.Bochner.HessianExpansion
 import OpenGALib.Riemannian.Operators.Bochner.BochnerExpansion
 import OpenGALib.Riemannian.Operators.ConnectionLaplacian
-import OpenGALib.Riemannian.Util.ConnectionLaplacianSimp
+import OpenGALib.Riemannian.Util.Simp.OperatorSimp
 import OpenGALib.Util.MFDeriv
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
-import OpenGALib.Riemannian.Util.CovDerivBridges
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
+import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges
 
 /-!
 # Per-summand chain of the heart-of-Bochner identity

OpenGALib/Riemannian/Operators/Gradient.lean

@@ -1,6 +1,6 @@
 import OpenGALib.Riemannian.Connection.LeviCivita
 import OpenGALib.Riemannian.TensorBundle.MusicalIso
-import OpenGALib.Riemannian.Util.MfderivApplySection
+import OpenGALib.Riemannian.Util.Tangent.MfderivApplySection
 
 /-!
 # Manifold gradient

OpenGALib/Riemannian/Operators/Hessian.lean

@@ -5,7 +5,8 @@ import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.LinearAlgebra.Dimension.Free
 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import OpenGALib.Riemannian.Util.CovDerivBridges
+import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges
+import OpenGALib.Riemannian.Util.Metric.MetricNotation
 
 /-!
 # Hessian on a Riemannian manifold

OpenGALib/Riemannian/Operators/Laplacian.lean

@@ -1,6 +1,6 @@
 import OpenGALib.Riemannian.Operators.Hessian
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import OpenGALib.Riemannian.Util.CovDerivBridges
+import OpenGALib.Riemannian.Util.CovDeriv.CovDerivBridges
 
 /-!
 # Laplace–Beltrami operator

OpenGALib/Riemannian/TangentBundle/TangentSmooth.lean

@@ -13,7 +13,7 @@ import Mathlib.LinearAlgebra.Basis.Defs
 import Mathlib.LinearAlgebra.Dimension.Finite
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import OpenGALib.Riemannian.TangentBundle.LocallyConstant
-import OpenGALib.Riemannian.Util.FlatChartDerivs
+import OpenGALib.Riemannian.Util.Chart.FlatChartDerivs
 
 /-!
 # Tangent bundle smoothness API

OpenGALib/Riemannian/Util/ChartJacobianSmooth.lean → OpenGALib/Riemannian/Util/Chart/ChartJacobianCLM.lean

@@ -10,7 +10,7 @@ import Mathlib.LinearAlgebra.Basis.Defs
 import Mathlib.LinearAlgebra.Dimension.Free
 
 /-!
-# Smoothness of chart-Jacobian-related continuous linear map-valued functions
+# Smoothness of chart-Jacobian CLM-valued functions
 
 For a smooth manifold `M` with model `(I : ModelWithCorners ℝ E H)` and a
 base point `α : M`, the tangent-bundle trivialization at `α` provides

OpenGALib/Riemannian/Util/Chart/README.md

@@ -0,0 +1,9 @@
+# `Util/Chart/`
+
+Chart-frame and chart-Jacobian engineering modules.
+
+| File | Role |
+|------|------|
+| [`ChartJacobianCLM.lean`](./ChartJacobianCLM.lean) | CLM-valued chart-Jacobian smoothness. |
+| [`ChartJacobianEntries.lean`](./ChartJacobianEntries.lean) | Scalar chart-Jacobian matrix-entry smoothness. |
+| [`FlatChartDerivs.lean`](./FlatChartDerivs.lean) | Flat chart derivative engineering for tangent maps. |

OpenGALib/Riemannian/Util/CovDerivSmoothness.lean → OpenGALib/Riemannian/Util/CovDeriv/CovDerivSmoothness.lean

@@ -1,13 +1,13 @@
 import Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
 import Mathlib.Geometry.Manifold.VectorField.LieBracket
 import OpenGALib.Riemannian.Manifold.SmoothManifold
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
 import OpenGALib.Riemannian.TangentBundle.TangentSmooth
 import OpenGALib.Riemannian.TensorBundle.MusicalIso
-import OpenGALib.Riemannian.Util.MfderivApplySection
+import OpenGALib.Riemannian.Util.Tangent.MfderivApplySection
 import OpenGALib.Riemannian.Connection.Koszul
 import OpenGALib.Riemannian.Connection.RieszExtraction
-import OpenGALib.Riemannian.Util.TangentHelpers
+import OpenGALib.Riemannian.Util.Tangent.TangentHelpers
 
 /-!
 # Tensoriality + smoothness machinery for `koszulCovDeriv`

OpenGALib/Riemannian/Util/CovDeriv/README.md

@@ -0,0 +1,6 @@
+# CovDeriv
+
+Covariant-derivative utilities are split by import direction.
+`CovDerivSmoothness.lean` is pre-`LeviCivita` scaffolding used to construct the
+connection. `CovDerivBridges.lean` is post-`LeviCivita` simp glue for
+`covDeriv` and `covDerivAt`, kept separate to avoid an import cycle.

OpenGALib/Riemannian/Util/CotangentFunctional.lean → OpenGALib/Riemannian/Util/Metric/CotangentFunctional.lean

@@ -1,6 +1,6 @@
 import OpenGALib.Riemannian.Connection.Koszul
-import OpenGALib.Riemannian.Util.TangentHelpers
-import OpenGALib.Riemannian.Util.MetricInnerSmoothness
+import OpenGALib.Riemannian.Util.Tangent.TangentHelpers
+import OpenGALib.Riemannian.Util.Metric.MetricInnerSmoothness
 /-!
 # Half-Koszul cotangent functional
 

OpenGALib/Riemannian/Util/Metric/README.md

@@ -0,0 +1,9 @@
+# `Util/Metric/`
+
+Metric notation, smoothness, and cotangent-functional support modules.
+
+| File | Role |
+|------|------|
+| [`MetricNotation.lean`](./MetricNotation.lean) | Polymorphic metric inner-product and norm-squared notation. |
+| [`MetricInnerSmoothness.lean`](./MetricInnerSmoothness.lean) | Pointwise, set, and global `metricInner` smoothness variants. |
+| [`CotangentFunctional.lean`](./CotangentFunctional.lean) | Half-Koszul cotangent-functional construction. |

OpenGALib/Riemannian/Util/README.md

@@ -0,0 +1,37 @@
+# `Riemannian/Util/` — engineering tax for the Riemannian layer
+
+Per OpenGA's anchor-purity discipline, anchor files expose only
+`**Math.**`-tagged declarations; `**Eng.**` and `**Mixed.**` plumbing lives
+under `Util/`. The files are grouped by the downstream layer they support.
+
+## Directories
+
+| Theme | Directory | Files |
+| --- | --- | --- |
+| Chart Jacobian | [`Chart/`](./Chart/) | `ChartJacobianCLM.lean`, `ChartJacobianEntries.lean`, `FlatChartDerivs.lean` |
+| Tangent / section glue | [`Tangent/`](./Tangent/) | `TangentHelpers.lean`, `TensorBundleCoercions.lean`, `MfderivApplySection.lean` |
+| Metric inner / notation | [`Metric/`](./Metric/) | `MetricInnerSmoothness.lean`, `MetricNotation.lean`, `CotangentFunctional.lean` |
+| Covariant derivative | [`CovDeriv/`](./CovDeriv/) | `CovDerivSmoothness.lean`, `CovDerivBridges.lean` |
+| Operator simp lemmas | [`Simp/`](./Simp/) | `OperatorSimp.lean` |
+
+`ChartJacobianSmooth.lean` was renamed to `Chart/ChartJacobianCLM.lean`
+because it proves smoothness of continuous-linear-map-valued chart-Jacobian
+composites. `ChartJacobianSmoothness.lean` was renamed to
+`Chart/ChartJacobianEntries.lean` because it proves scalar matrix-entry
+smoothness.
+
+`ConnectionLaplacianSimp.lean` and `DivergenceSimp.lean` were merged into
+`Simp/OperatorSimp.lean`. `CovDerivBridges.lean` remains a separate
+post-`LeviCivita` bridge file: it imports `Connection.LeviCivita`, while
+`Connection.LeviCivita` imports `CovDerivSmoothness.lean`; absorbing the bridge
+lemmas into `CovDerivSmoothness.lean` would create an import cycle.
+
+## Conventions
+
+* Every declaration docstring starts with `**Math.**`, `**Eng.**`, or
+  `**Mixed.**`.
+* Util files may contain engineering declarations; sibling anchor folders keep
+  the mathematical surface clean.
+* Subdirectory names carry the grouping role. File names describe concrete
+  content and avoid generic `Helpers` / `Base` / `Foundation` suffixes except
+  where the historical API name is retained.

OpenGALib/Riemannian/Util/ConnectionLaplacianSimp.lean → OpenGALib/Riemannian/Util/Simp/OperatorSimp.lean

@@ -1,18 +1,18 @@
 import OpenGALib.Riemannian.Operators.ConnectionLaplacian
+import OpenGALib.Riemannian.Operators.Divergence
 
 /-!
-# Connection Laplacian — simp def-unfold
+# Operator simp def-unfolds
 
-Engineering simp lemma exposing the definition of `connectionLaplacian`
-as a sum of `secondCovDerivSection` over the smooth $g$-orthonormal
-frame. Imported by callers that need to rewrite at the level of the
-frame sum rather than against the opaque operator name.
+Engineering simp lemmas exposing definitions of small Riemannian operators
+against the smooth $g$-orthonormal frame. Imported by callers that need to
+rewrite at the level of frame sums rather than against opaque operator names.
 -/
 
 noncomputable section
 
 open Bundle
-open scoped ContDiff Manifold Bundle Riemannian
+open scoped ContDiff Manifold Bundle Riemannian InnerProductSpace
 
 namespace Riemannian
 namespace Operators
@@ -36,6 +36,18 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa
         (Riemannian.Tensor.smoothOrthoFrame (I := I) g α i) α :=
   rfl
 
+/-- **Eng.** Definitional unfold of `divergence` as a sum of
+`metricInner (∇_{B_i} X) B_i` over the smooth $g$-orthonormal frame. Pure
+`rfl`; tagged `@[simp]` for tactic-level rewrites. -/
+@[simp] lemma divergence_def
+    (g : RiemannianMetric I M)
+    (X : VectorFieldSection I M) (x : M) :
+    divergence (I := I) (M := M) g X x =
+      ∑ i, g.metricInner x
+        (covDeriv g (Riemannian.Tensor.smoothOrthoFrame (I := I) g x i) X x)
+        (Riemannian.Tensor.smoothOrthoFrame (I := I) g x i x) :=
+  rfl
+
 end Operators
 end Riemannian
 

OpenGALib/Riemannian/Util/Simp/README.md

@@ -0,0 +1,5 @@
+# Simp
+
+Simp utilities collect small operator unfoldings used explicitly by downstream
+proofs. `OperatorSimp.lean` combines the connection-Laplacian and divergence
+definitional simp lemmas.

OpenGALib/Riemannian/Util/Tangent/README.md

@@ -0,0 +1,9 @@
+# `Util/Tangent/`
+
+Tangent-bundle glue and section-level helper modules.
+
+| File | Role |
+|------|------|
+| [`TangentHelpers.lean`](./TangentHelpers.lean) | Chart-bundle smoothness bridges. |
+| [`TensorBundleCoercions.lean`](./TensorBundleCoercions.lean) | Tensor-bundle fiber-to-model coercion algebra. |
+| [`MfderivApplySection.lean`](./MfderivApplySection.lean) | Smoothness of `mfderiv f` applied to a tangent-bundle section. |