Rename Foundations/ → Util/, lift HessianLie/ to Riemannian root

Foundations/ was a misnomer: it bundled engineering infrastructure
(Notation, Tactic, Attributes — no mathematical content) with HessianLie
(genuine manifold lemma: mfderiv_iterate_sub_eq_mlieBracket_apply).
Splitting cleanly:

- OpenGALib/Riemannian/Foundations/{Notation,Tactic,Attributes}.lean
  → OpenGALib/Riemannian/Util/{Notation,Tactic,Attributes}.lean
  (engineering layer, Mathlib-style: notation macros, simp set
  declarations, tactic re-exports)
- OpenGALib/Riemannian/Foundations/HessianLie.lean
  → OpenGALib/Riemannian/HessianLie.lean
  OpenGALib/Riemannian/Foundations/HessianLie/{ChartHelpers,Flat,Manifold}.lean
  → OpenGALib/Riemannian/HessianLie/{...}.lean
  (peer to Connection/, Curvature/, etc.)
- 11 import lines rewritten across Riemannian + Curvature + Metric/Basic.
- Riemannian.lean docstring section "Foundations" → "Util — engineering
  layer (no mathematical content)"; UXTestFoundations section renamed.

Author: Xinze-Li-Moqian

OpenGALib/Riemannian.lean

@@ -1,8 +1,8 @@
 import OpenGALib.Riemannian.BumpFunction
 import OpenGALib.Riemannian.Connection
 import OpenGALib.Riemannian.Curvature
-import OpenGALib.Riemannian.Foundations.Notation
-import OpenGALib.Riemannian.Foundations.Tactic
+import OpenGALib.Riemannian.Util.Notation
+import OpenGALib.Riemannian.Util.Tactic
 import OpenGALib.Riemannian.Gradient
 import OpenGALib.Riemannian.LoopSpace
 import OpenGALib.Riemannian.Metric
@@ -48,8 +48,6 @@ Regularity                   ← consumer
     $|A|^2$, mean curvature.
   * `Gradient.lean`   — manifold gradient via Riesz duality, gradient norm
     squared.
-  * `LoopSpace.lean` — based and free loop-space primitives over a
-    topological space, parameterized by `[0, 1]`.
   * `BumpFunction.lean` — scalar / radial / manifold bumps + tangent
     vector field extension (`OpenGALib.BumpFunction`).
 
@@ -116,12 +114,12 @@ intermediate identities) are internal and may change without notice.
     `TangentBundle.symmLFlat_mdifferentiableAt`
   * `OpenGALib.MDifferentiableAt.metricInner_smoothAt`
 
-**Foundations** (`Foundations/`):
-  * `Foundations/Notation.lean` — textbook notation: `⟪V, W⟫_g`,
+**Util — engineering layer** (`Util/`, no mathematical content):
+  * `Util/Notation.lean` — textbook notation: `⟪V, W⟫_g`,
     `‖V‖²_g`, `∇[X] Y`, `Riem(X, Y) Z` (scoped to `OpenGALib` /
     `Riemannian` scopes; `open scoped` to enable).
-  * `Foundations/Attributes.lean` — `metric_simp` simp set declaration.
-  * `Foundations/Tactic.lean` — user-facing entry point for tactic
+  * `Util/Attributes.lean` — `metric_simp` simp set declaration.
+  * `Util/Tactic.lean` — user-facing entry point for tactic
     infrastructure.
 
 Stability tier: pre-`v0.1.0` everything is **experimental**. The
@@ -143,13 +141,13 @@ typeclass diamond resolved without deep unfolding. No proof is on a
 heartbeat-limit hot edge; future expansion has comfortable headroom.
 -/
 
-/-! ## UXTest — Foundations layer
+/-! ## UXTest — Util layer
 
 Verifies that the notation + `metric_simp` tactic infrastructure resolve
 end-to-end. Regression guard against signature drift in the notation
 elaboration. -/
 
-section UXTestFoundations
+section UXTestUtil
 
 open OpenGALib
 open scoped ContDiff
@@ -194,4 +192,4 @@ example
     ⟪V - 0, -W + W⟫_g = 0 := by
   simp [metric_simp]
 
-end UXTestFoundations
+end UXTestUtil

OpenGALib/Riemannian/Curvature.lean

@@ -1,7 +1,7 @@
 import OpenGALib.Riemannian.Connection
 import OpenGALib.Riemannian.Connection.Smoothness
 import OpenGALib.Riemannian.TangentBundle.SmoothVectorField
-import OpenGALib.Riemannian.Foundations.HessianLie
+import OpenGALib.Riemannian.HessianLie
 import Mathlib.LinearAlgebra.Trace
 import Mathlib.Analysis.InnerProductSpace.PiL2
 

…b/Riemannian/Foundations/HessianLie.lean OpenGALib/Riemannian/HessianLie.leanOpenGALib/Riemannian/Foundations/HessianLie.lean renamed to OpenGALib/Riemannian/HessianLie.lean OpenGALib/Riemannian/Foundations/HessianLie.lean renamed to OpenGALib/Riemannian/HessianLie.lean

@@ -1,6 +1,6 @@
-import OpenGALib.Riemannian.Foundations.HessianLie.Flat
-import OpenGALib.Riemannian.Foundations.HessianLie.ChartHelpers
-import OpenGALib.Riemannian.Foundations.HessianLie.Manifold
+import OpenGALib.Riemannian.HessianLie.Flat
+import OpenGALib.Riemannian.HessianLie.ChartHelpers
+import OpenGALib.Riemannian.HessianLie.Manifold
 
 /-!
 # Scalar Hessian–Lie identity (facade)

…Foundations/HessianLie/ChartHelpers.lean …/Riemannian/HessianLie/ChartHelpers.leanOpenGALib/Riemannian/Foundations/HessianLie/ChartHelpers.lean renamed to OpenGALib/Riemannian/HessianLie/ChartHelpers.lean OpenGALib/Riemannian/Foundations/HessianLie/ChartHelpers.lean renamed to OpenGALib/Riemannian/HessianLie/ChartHelpers.lean

@@ -1,7 +1,7 @@
 import Mathlib.Geometry.Manifold.VectorField.LieBracket
 import Mathlib.Geometry.Manifold.VectorField.Pullback
-import OpenGALib.Riemannian.Foundations.HessianLie.Flat
-import OpenGALib.Riemannian.Foundations.HessianLie.ChartHelpers
+import OpenGALib.Riemannian.HessianLie.Flat
+import OpenGALib.Riemannian.HessianLie.ChartHelpers
 
 /-!
 # Scalar Hessian–Lie identity — manifold version

…mannian/Foundations/HessianLie/Flat.lean OpenGALib/Riemannian/HessianLie/Flat.leanOpenGALib/Riemannian/Foundations/HessianLie/Flat.lean renamed to OpenGALib/Riemannian/HessianLie/Flat.lean OpenGALib/Riemannian/Foundations/HessianLie/Flat.lean renamed to OpenGALib/Riemannian/HessianLie/Flat.lean

@@ -4,7 +4,7 @@ import Mathlib.Geometry.Manifold.VectorBundle.Tangent
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.LinearAlgebra.BilinearMap
 import OpenGALib.Algebraic.BilinearForm.Basic
-import OpenGALib.Riemannian.Foundations.Attributes
+import OpenGALib.Riemannian.Util.Attributes
 
 /-!
 # RiemannianMetric — typeclass + inner product API + tangent-space bridges

…ian/Foundations/HessianLie/Manifold.lean …ALib/Riemannian/HessianLie/Manifold.leanOpenGALib/Riemannian/Foundations/HessianLie/Manifold.lean renamed to OpenGALib/Riemannian/HessianLie/Manifold.lean OpenGALib/Riemannian/Foundations/HessianLie/Manifold.lean renamed to OpenGALib/Riemannian/HessianLie/Manifold.lean

@@ -1,14 +1,14 @@
-import OpenGALib.Riemannian.Foundations.Attributes
+import OpenGALib.Riemannian.Util.Attributes
 import OpenGALib.Riemannian.Metric.Basic
 
 /-!
 # Riemannian tactic infrastructure
 
 User-facing entry point for the framework's domain-specific simp
-attributes. Re-exports `Foundations/Attributes.lean` so downstream
+attributes. Re-exports `Util/Attributes.lean` so downstream
 code can simply
 ```
-import OpenGALib.Riemannian.Foundations.Tactic
+import OpenGALib.Riemannian.Util.Tactic
 ```
 to obtain both the attribute declarations and (transitively) the
 metric algebra lemmas tagged with them.