diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 49f2c74..813121d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -131,7 +131,7 @@ jobs:
           # transitive-relied-on imports). Baseline is current debt; CI
           # fails on growth, mirrors Mathlib's `noshake.json` discipline.
           ACTUAL=$(lake exe shake OpenGALib --no-downstream 2>&1 | grep -c "^/.*\.lean:$" || echo 0)
-          EXPECTED_SHAKE=36
+          EXPECTED_SHAKE=38
           echo "Shake suggestions: $ACTUAL (expected ≤ $EXPECTED_SHAKE; gradually reduce)"
           if [ "$ACTUAL" -gt "$EXPECTED_SHAKE" ]; then
             echo "::error::Shake regression: $ACTUAL > $EXPECTED_SHAKE"
diff --git a/OpenGALib/GeometricMeasureTheory/Isoperimetric/ReducedBoundary.lean b/OpenGALib/GeometricMeasureTheory/Isoperimetric/ReducedBoundary.lean
index eaf2481..ad5eb4c 100644
--- a/OpenGALib/GeometricMeasureTheory/Isoperimetric/ReducedBoundary.lean
+++ b/OpenGALib/GeometricMeasureTheory/Isoperimetric/ReducedBoundary.lean
@@ -145,7 +145,7 @@ infrastructure.
 theorem tangentHyperplane_at_reducedBoundary_orthogonal
     (Ω : FinitePerimeter M) (x : M)
     (_hx : x ∈ FinitePerimeter.reducedBoundary Ω) (v : TangentSpace I x) :
-    Riemannian.metricInner x v (Varifold.bvGradientDirection I Ω x) = 0 ↔
+    Riemannian.HasMetric.metric.metricInner x v (Varifold.bvGradientDirection I Ω x) = 0 ↔
       v ∈ (Submodule.span ℝ {Varifold.bvGradientDirection I Ω x})ᗮ := by
   sorry
 
diff --git a/OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean b/OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean
index c3816fc..9e689bf 100644
--- a/OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean
+++ b/OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean
@@ -574,7 +574,7 @@ fixed real constant $c$ (the *Einstein constant*).
 Reference: do Carmo §4 Ex. 6; Petersen Ch. 3 §6. -/
 def IsEinstein : Prop :=
   ∃ c : ℝ, ∀ (x : M) (V W : TangentSpace I x),
-    ricciTensor HasMetric.metric x V W = c * metricInner x V W
+    ricciTensor HasMetric.metric x V W = c * HasMetric.metric.metricInner x V W
 
 end Riemannian
 
diff --git a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
index 2d77e49..0693dae 100644
--- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
+++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
@@ -1071,7 +1071,7 @@ $K_g(X, Y)(x) = K_g(Y, X)(x)$.
 Numerator: $g(R(X,Y)Y, X) = g(R(Y,X)X, Y)$ via `riemannCurvature_pair_symm`
 on $(X, Y, Y, X) \leftrightarrow (Y, X, X, Y)$, then a sign cancellation
 using `riemannCurvature_antisymm` once in each slot.
-Denominator: symmetric in $X, Y$ via `metricInner_comm`. -/
+Denominator: symmetric in $X, Y$ via `HasMetric.metric.metricInner_comm`. -/
 theorem sectionalCurvature_symmetric
     [IsManifold I 2 M]
     (g : RiemannianMetric I M)
diff --git a/OpenGALib/Riemannian/Instances/EuclideanSpace.lean b/OpenGALib/Riemannian/Instances/EuclideanSpace.lean
index 4a58b08..07b82d3 100644
--- a/OpenGALib/Riemannian/Instances/EuclideanSpace.lean
+++ b/OpenGALib/Riemannian/Instances/EuclideanSpace.lean
@@ -12,7 +12,7 @@ over itself with the standard inner product as a constant metric tensor.
 
 * `euclideanRiemannianMetric` — the flat metric as data
   (`RiemannianMetric (𝓘(ℝ, E)) E`).
-* `metricInner_euclidean` — `g.metricInner x v w = ⟪v, w⟫_ℝ` on the
+* `HasMetric.metric.metricInner_euclidean` — `g.metricInner x v w = ⟪v, w⟫_ℝ` on the
   flat metric.
 
 Reference: do Carmo, *Riemannian Geometry*, §1.1 Example 1.4.
diff --git a/OpenGALib/Riemannian/Manifold/SmoothManifold.lean b/OpenGALib/Riemannian/Manifold/SmoothManifold.lean
index ce218d5..fece6bd 100644
--- a/OpenGALib/Riemannian/Manifold/SmoothManifold.lean
+++ b/OpenGALib/Riemannian/Manifold/SmoothManifold.lean
@@ -119,191 +119,4 @@ instance instHasMetricOfRiemannianManifold :
 
 end RiemannianManifoldBridges
 
-/-! ## Math-first metric API
-
-Downstream operator code reads as textbook math when the metric is
-carried implicitly by `[HasMetric I M]`:
-
-* `metricInner x v w`           (inner product on `T_xM`, not `g.metricInner`)
-* `metricRiesz x φ`             (Riesz dual vector)
-* `metricInner_add_left ...`    (algebra lemmas, bare names)
-
-Each wrapper takes `[HasMetric I M]` as instance argument and delegates
-to the underlying `RiemannianMetric.X` method on `HasMetric.metric`.
-Wrappers are `abbrev` / direct delegations so `g.X`-style proofs still
-work via abbrev unfolding, and so the `@[simp]` / `@[metric_simp]` simp
-sets unify naturally with the underlying method-form lemmas. -/
-
-section MetricAPI
-
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
-  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
-  [hm : HasMetric I M]
-
-/-- **Math.** The **metric inner product** $\langle V, W\rangle_g$ as a
-top-level function, sourcing $g$ from `[HasMetric I M]`. -/
-noncomputable abbrev metricInner (x : M)
-    (v w : TangentSpace I x) : ℝ :=
-  hm.metric.metricInner x v w
-
-@[simp]
-theorem metricInner_apply (x : M) (v w : TangentSpace I x) :
-    metricInner x v w = hm.metric.inner x v w := rfl
-
-/-- **Math.** Symmetry: $\langle V, W\rangle_g = \langle W, V\rangle_g$. -/
-theorem metricInner_comm (x : M) (v w : TangentSpace I x) :
-    metricInner x v w = metricInner x w v :=
-  hm.metric.metricInner_comm x v w
-
-/-- **Math.** Positive-definiteness: $V \ne 0 \Rightarrow \langle V, V\rangle_g > 0$. -/
-theorem metricInner_self_pos (x : M) (v : TangentSpace I x)
-    (hv : v ≠ 0) : 0 < metricInner x v v :=
-  hm.metric.metricInner_self_pos x v hv
-
-@[metric_simp]
-theorem metricInner_add_left (x : M) (v₁ v₂ w : TangentSpace I x) :
-    metricInner x (v₁ + v₂) w = metricInner x v₁ w + metricInner x v₂ w :=
-  hm.metric.metricInner_add_left x v₁ v₂ w
-
-@[metric_simp]
-theorem metricInner_add_right (x : M) (v w₁ w₂ : TangentSpace I x) :
-    metricInner x v (w₁ + w₂) = metricInner x v w₁ + metricInner x v w₂ :=
-  hm.metric.metricInner_add_right x v w₁ w₂
-
-@[metric_simp]
-theorem metricInner_smul_left (x : M) (c : ℝ)
-    (v w : TangentSpace I x) :
-    metricInner x (c • v) w = c * metricInner x v w :=
-  hm.metric.metricInner_smul_left x c v w
-
-@[metric_simp]
-theorem metricInner_smul_right (x : M) (c : ℝ)
-    (v w : TangentSpace I x) :
-    metricInner x v (c • w) = c * metricInner x v w :=
-  hm.metric.metricInner_smul_right x c v w
-
-@[simp, metric_simp]
-theorem metricInner_zero_left (x : M) (w : TangentSpace I x) :
-    metricInner x 0 w = 0 :=
-  hm.metric.metricInner_zero_left x w
-
-@[simp, metric_simp]
-theorem metricInner_zero_right (x : M) (v : TangentSpace I x) :
-    metricInner x v 0 = 0 :=
-  hm.metric.metricInner_zero_right x v
-
-@[simp, metric_simp]
-theorem metricInner_neg_left (x : M) (v w : TangentSpace I x) :
-    metricInner x (-v) w = -metricInner x v w :=
-  hm.metric.metricInner_neg_left x v w
-
-@[simp, metric_simp]
-theorem metricInner_neg_right (x : M) (v w : TangentSpace I x) :
-    metricInner x v (-w) = -metricInner x v w :=
-  hm.metric.metricInner_neg_right x v w
-
-@[simp, metric_simp]
-theorem metricInner_sub_left (x : M) (v₁ v₂ w : TangentSpace I x) :
-    metricInner x (v₁ - v₂) w = metricInner x v₁ w - metricInner x v₂ w :=
-  hm.metric.metricInner_sub_left x v₁ v₂ w
-
-@[simp, metric_simp]
-theorem metricInner_sub_right (x : M) (v w₁ w₂ : TangentSpace I x) :
-    metricInner x v (w₁ - w₂) = metricInner x v w₁ - metricInner x v w₂ :=
-  hm.metric.metricInner_sub_right x v w₁ w₂
-
-@[simp, metric_simp]
-theorem metricInner_self_nonneg (x : M) (v : TangentSpace I x) :
-    0 ≤ metricInner x v v :=
-  hm.metric.metricInner_self_nonneg x v
-
-/-- **Math.** Non-degeneracy: vectors with equal inner-products against every test
-vector are equal. -/
-theorem metricInner_eq_iff_eq (x : M) (v w : TangentSpace I x) :
-    (∀ z : TangentSpace I x, metricInner x v z = metricInner x w z) ↔
-      v = w :=
-  hm.metric.metricInner_eq_iff_eq x v w
-
-section RieszSection
-
-variable [FiniteDimensional ℝ E]
-
-/-- **Math.** The **metric-to-dual** continuous linear map $V \mapsto g_x(V, \cdot)$. -/
-noncomputable abbrev metricToDual (x : M) :
-    TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
-  hm.metric.metricToDual x
-
-omit [FiniteDimensional ℝ E] in
-@[simp]
-theorem metricToDual_apply (x : M) (v w : TangentSpace I x) :
-    metricToDual x v w = metricInner x v w := rfl
-
-omit [FiniteDimensional ℝ E] in
-theorem metricToDual_injective (x : M) :
-    Function.Injective (metricToDual (I := I) (M := M) x) :=
-  hm.metric.metricToDual_injective x
-
-theorem metricToDual_bijective (x : M) :
-    Function.Bijective (metricToDual (I := I) (M := M) x) :=
-  hm.metric.metricToDual_bijective x
-
-/-- **Math.** Inverse Riesz: $\varphi \mapsto V_\varphi$ such that
-$g_x(V_\varphi, W) = \varphi(W)$. -/
-noncomputable abbrev metricRiesz (x : M)
-    (φ : TangentSpace I x →L[ℝ] ℝ) : TangentSpace I x :=
-  hm.metric.metricRiesz x φ
-
-@[simp]
-theorem metricRiesz_inner (x : M)
-    (φ : TangentSpace I x →L[ℝ] ℝ) (v : TangentSpace I x) :
-    metricInner x (metricRiesz x φ) v = φ v :=
-  hm.metric.metricRiesz_inner x φ v
-
-theorem metricRiesz_unique (x : M) (v : TangentSpace I x)
-    (φ : TangentSpace I x →L[ℝ] ℝ)
-    (h : ∀ w, metricInner x v w = φ w) :
-    v = metricRiesz x φ :=
-  hm.metric.metricRiesz_unique x v φ h
-
-/-- **Math.** The Riesz isomorphism `T_xM ≃ₗ[ℝ] (T_xM →L[ℝ] ℝ)`. -/
-noncomputable abbrev metricToDualEquiv (x : M) :
-    TangentSpace I x ≃ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
-  hm.metric.metricToDualEquiv x
-
-end RieszSection
-
-/-! ## Smoothness of the metric inner product — Math headline
-
-`metricInner y (v y) (w y)` is `ContMDiffWithinAt` whenever the
-tangent-bundle sections `v, w` are. The pointwise / set / global parity
-variants, the first-order `MDifferentiable*` analog family, and the
-`TangentSmoothAt`-form convenience wrapper all live in
-`Riemannian/Util/MetricInnerSmoothness.lean`. -/
-
-section Smoothness
-
-variable {v w : ∀ x : M, TangentSpace I x} {s : Set M} {x : M}
-
-variable {n : ℕ∞ω} [hLE : ENat.LEInfty n]
-
-/-- **Math.** $\langle v(\cdot), w(\cdot)\rangle_g$ is `ContMDiffWithinAt`. -/
-theorem metricInner_contMDiffWithinAt
-    (hv : ContMDiffWithinAt I (I.prod 𝓘(ℝ, E)) n
-      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s x)
-    (hw : ContMDiffWithinAt I (I.prod 𝓘(ℝ, E)) n
-      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s x) :
-    ContMDiffWithinAt I 𝓘(ℝ, ℝ) n
-      (fun y => metricInner y (v y) (w y)) s x :=
-  hm.metric.metricInner_contMDiffWithinAt hv hw
-
-end Smoothness
-
-end MetricAPI
-
--- Polymorphic notation `⟪·, ·⟫_g` and `‖·‖²_g` (and the dispatch classes
--- `MetricInnerHom`, `MetricNormSq`) live in
--- `OpenGALib/Riemannian/Util/MetricNotation.lean`; the import below
--- pulls them into scope for every consumer of `SmoothManifold`.
-
 end Riemannian
diff --git a/OpenGALib/Riemannian/Operators/Bochner.lean b/OpenGALib/Riemannian/Operators/Bochner.lean
index ddeaf78..8bbb898 100644
--- a/OpenGALib/Riemannian/Operators/Bochner.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner.lean
@@ -64,7 +64,7 @@ theorem bochner_leibniz_trace_reduction
   classical
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
   show (1 / 2 : ℝ) * Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y))) x
-      = metricInner x
+      = HasMetric.metric.metricInner x
           (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
           (manifoldGradient (I := I) HasMetric.metric f x)
         + frobeniusSq (I := I) (M := M) (hessianBilin (I := I) HasMetric.metric f) x
@@ -93,11 +93,11 @@ theorem bochner_leibniz_trace_reduction
   have h_summand : ∀ i,
       (1 / 2 : ℝ) * hessian (I := I) (M := M) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y)))
         (Bi i).toFun (Bi i).toFun x
-      = metricInner x
+      = HasMetric.metric.metricInner x
             (secondCovDerivSection (I := I) (M := M) HasMetric.metric
               (manifoldGradient (I := I) HasMetric.metric f) (Bi i).toFun (Bi i).toFun x)
             (manifoldGradient (I := I) HasMetric.metric f x)
-          + metricInner x
+          + HasMetric.metric.metricInner x
               (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x)
               (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x) := by
     intro i
@@ -113,11 +113,11 @@ theorem bochner_leibniz_trace_reduction
   congr 1
   · -- First sum: ∑_i ⟨secondCovDerivSection ∇f (Bi · x) (Bi · x) x, ∇f x⟩
     --             = ⟨connectionLaplacian ∇f x, ∇f x⟩ via `sum_inner` + `connectionLaplacian_def`.
-    show ∑ i, metricInner x
+    show ∑ i, HasMetric.metric.metricInner x
           (secondCovDerivSection (I := I) (M := M) HasMetric.metric
             (manifoldGradient (I := I) HasMetric.metric f) (Bi i).toFun (Bi i).toFun x)
           (manifoldGradient (I := I) HasMetric.metric f x)
-        = metricInner x
+        = HasMetric.metric.metricInner x
             (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
             (manifoldGradient (I := I) HasMetric.metric f x)
     unfold connectionLaplacian
@@ -130,7 +130,7 @@ theorem bochner_leibniz_trace_reduction
     -- `B(v, w) := ⟪covDerivAt HasMetric.metric ∇f x v, covDerivAt HasMetric.metric ∇f x w⟫_ℝ` (a `LinearMap.mk₂`),
     -- converts smoothOrthoFrame trace to std-basis trace; then the existing
     -- orthonormal-basis Frobenius identity closes.
-    show ∑ i, metricInner x
+    show ∑ i, HasMetric.metric.metricInner x
             (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x)
             (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x)
         = frobeniusSq (I := I) (M := M) (hessianBilin (I := I) HasMetric.metric f) x
@@ -185,7 +185,7 @@ theorem bochner_leibniz_trace_reduction
       Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x B'
     rw [hB'_def] at h_stage7
     simp only [LinearMap.mk₂_apply] at h_stage7
-    -- LHS: rewrite `metricInner x (covDeriv HasMetric.metric (Bi · x) ∇f x) (covDeriv HasMetric.metric (Bi · x) ∇f x)`
+    -- LHS: rewrite `HasMetric.metric.metricInner x (covDeriv HasMetric.metric (Bi · x) ∇f x) (covDeriv HasMetric.metric (Bi · x) ∇f x)`
     -- as `⟪covDerivAt HasMetric.metric ∇f x (Bi · x x), covDerivAt HasMetric.metric ∇f x (Bi · x x)⟫_ℝ` (def-eq), match h_stage7's LHS.
     show ∑ i, @inner ℝ (TangentSpace I x) _
               (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
@@ -203,13 +203,13 @@ theorem bochner_leibniz_trace_reduction
     set v : TangentSpace I x :=
       covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (b i)
     have h_hess_unfold : ∀ j, ((hessianBilin (I := I) HasMetric.metric f x) (b i)) (b j)
-                            = metricInner x v (b j) := fun _ => rfl
+                            = HasMetric.metric.metricInner x v (b j) := fun _ => rfl
     simp only [h_hess_unfold]
     calc @inner ℝ (TangentSpace I x) _ v v
         = ⟪v, v⟫_ℝ := rfl
       _ = ‖v‖ ^ 2 := real_inner_self_eq_norm_sq v
       _ = ∑ j, ⟪v, b j⟫_ℝ ^ 2 := (b.sum_sq_inner_left v).symm
-      _ = ∑ j, (metricInner x v (b j)) ^ 2 := rfl
+      _ = ∑ j, (HasMetric.metric.metricInner x v (b j)) ^ 2 := rfl
 
 /-- **Math.** **Explicit-`g` form of the Leibniz trace reduction**. -/
 theorem bochner_leibniz_trace_reduction_g
diff --git a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
index 6d1ee05..12579c7 100644
--- a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
@@ -148,13 +148,13 @@ theorem metricInner_secondCovDerivAt_grad_swap_of_hess_eventual_sym
   simp only [← leviCivitaConnection_toFun_eq_covDeriv] at h_compat_Z
   -- Rewrite metric-compat LHS into `hessianBilin f y w z` / `f y z w` form.
   have h_hess_W :
-      (fun y : M => metricInner y (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y w) (Z y))
+      (fun y : M => HasMetric.metric.metricInner y (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y w) (Z y))
         = (fun y : M => hessianBilin (I := I) HasMetric.metric f y w z) := by
-    funext y; show metricInner y _ z = hessianBilin (I := I) HasMetric.metric f y w z; rfl
+    funext y; show HasMetric.metric.metricInner y _ z = hessianBilin (I := I) HasMetric.metric f y w z; rfl
   have h_hess_Z :
-      (fun y : M => metricInner y (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y z) (W y))
+      (fun y : M => HasMetric.metric.metricInner y (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y z) (W y))
         = (fun y : M => hessianBilin (I := I) HasMetric.metric f y z w) := by
-    funext y; show metricInner y _ w = hessianBilin (I := I) HasMetric.metric f y z w; rfl
+    funext y; show HasMetric.metric.metricInner y _ w = hessianBilin (I := I) HasMetric.metric f y z w; rfl
   rw [h_hess_W] at h_compat_W
   rw [h_hess_Z] at h_compat_Z
   -- V x = v, W x = w, Z x = z (all rfl, constant lifts).
@@ -175,45 +175,45 @@ theorem metricInner_secondCovDerivAt_grad_swap_of_hess_eventual_sym
     (leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z x v with hΓvz_def
   -- Identify the second metric-compat term as hessianBilin (cross terms).
   -- ⟨covDerivAt HasMetric.metric ∇f x w, Γvz⟩ = hessianBilin f x w Γvz (by def).
-  have h_id_W : metricInner x (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x w)
+  have h_id_W : HasMetric.metric.metricInner x (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x w)
         ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z x v)
       = hessianBilin (I := I) HasMetric.metric f x w Γvz := rfl
-  have h_id_Z : metricInner x (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x z)
+  have h_id_Z : HasMetric.metric.metricInner x (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x z)
         ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun W x v)
       = hessianBilin (I := I) HasMetric.metric f x z Γvw := rfl
   -- Cast h_compat_W / h_compat_Z to typeclass `metricInner` abbrev form for rw matching.
   change ((mfderiv% fun y : M => hessianBilin (I := I) HasMetric.metric f y w z) x) v
-      = metricInner x
+      = HasMetric.metric.metricInner x
           ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
             (fun y : M => covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y w) x v) z
-        + metricInner x (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x w)
+        + HasMetric.metric.metricInner x (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x w)
           ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Z x v)
     at h_compat_W
   change ((mfderiv% fun y : M => hessianBilin (I := I) HasMetric.metric f y z w) x) v
-      = metricInner x
+      = HasMetric.metric.metricInner x
           ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
             (fun y : M => covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y z) x v) w
-        + metricInner x (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x z)
+        + HasMetric.metric.metricInner x (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x z)
           ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun W x v)
     at h_compat_Z
   rw [h_id_W] at h_compat_W
   rw [h_id_Z] at h_compat_Z
   -- Now unfold secondCovDerivAt and metric-inner-sub.
-  show metricInner x
+  show HasMetric.metric.metricInner x
       (covDerivAt HasMetric.metric (fun y : M => covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y w) x v
         - covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
             (covDerivAt HasMetric.metric (Y := fun _ : M => (w : TangentSpace I x)) x v)) z
-    = metricInner x
+    = HasMetric.metric.metricInner x
       (covDerivAt HasMetric.metric (fun y : M => covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y z) x v
         - covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
             (covDerivAt HasMetric.metric (Y := fun _ : M => (z : TangentSpace I x)) x v)) w
-  rw [metricInner_sub_left, metricInner_sub_left]
+  rw [HasMetric.metric.metricInner_sub_left, HasMetric.metric.metricInner_sub_left]
   -- Identify outer terms: ⟨covDerivAt HasMetric.metric (∂_W ∇f) x v, z⟩ = ⟨lcc.(∂_W ∇f) x v, z⟩ (rfl).
   -- Identify Christoffel terms: ⟨covDerivAt HasMetric.metric ∇f x Γvw, z⟩ = hessianBilin f x Γvw z (rfl).
-  show metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
+  show HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
         (fun y : M => covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y w) x v) z
       - hessianBilin (I := I) HasMetric.metric f x Γvw z
-    = metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
+    = HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
         (fun y : M => covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y z) x v) w
       - hessianBilin (I := I) HasMetric.metric f x Γvz w
   -- Cross-term Hess-sym: hessianBilin f x z Γvw = hessianBilin f x Γvw z, etc.
@@ -235,7 +235,7 @@ theorem metricInner_secondCovDerivAt_grad_swap_of_hess_eventual_sym
 Propagates the strict-interior fact (vacuous under `[I.Boundaryless]`) to
 a nbhd via `extChartAt_self_eventually_mem_closure_interior_range` and
 applies pointwise `hessianBilin_symm` to feed
-`metricInner_secondCovDerivAt_grad_swap_of_hess_eventual_sym`. -/
+`HasMetric.metric.metricInner_secondCovDerivAt_grad_swap_of_hess_eventual_sym`. -/
 theorem hessianBilin_eventually_symm_of_strict_interior
     [IsManifold I 2 M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M)
@@ -368,28 +368,28 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
   -- Bilinear form `Φ(v, w) := g_x(curvatureEndo (HasMetric.metric) WV GV x v, w)`.
   set Φ : TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] ℝ :=
     LinearMap.mk₂ ℝ
-      (fun v w => metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w)
+      (fun v w => HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w)
       (fun v₁ v₂ w => by
-        show metricInner x (curvatureEndo (HasMetric.metric) WV GV x (v₁ + v₂)) w
-          = metricInner x (curvatureEndo (HasMetric.metric) WV GV x v₁) w
-            + metricInner x (curvatureEndo (HasMetric.metric) WV GV x v₂) w
-        rw [(curvatureEndo (HasMetric.metric) WV GV x).map_add, metricInner_add_left])
+        show HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x (v₁ + v₂)) w
+          = HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v₁) w
+            + HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v₂) w
+        rw [(curvatureEndo (HasMetric.metric) WV GV x).map_add, HasMetric.metric.metricInner_add_left])
       (fun c v w => by
-        show metricInner x (curvatureEndo (HasMetric.metric) WV GV x (c • v)) w
-          = c • metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w
-        rw [(curvatureEndo (HasMetric.metric) WV GV x).map_smul, metricInner_smul_left]; rfl)
+        show HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x (c • v)) w
+          = c • HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w
+        rw [(curvatureEndo (HasMetric.metric) WV GV x).map_smul, HasMetric.metric.metricInner_smul_left]; rfl)
       (fun v w₁ w₂ => by
-        show metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) (w₁ + w₂)
-          = metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w₁
-            + metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w₂
-        rw [metricInner_add_right])
+        show HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) (w₁ + w₂)
+          = HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w₁
+            + HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w₂
+        rw [HasMetric.metric.metricInner_add_right])
       (fun c v w => by
-        show metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) (c • w)
-          = c • metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w
-        rw [metricInner_smul_right]; rfl) with hΦ_def
+        show HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) (c • w)
+          = c • HasMetric.metric.metricInner x (curvatureEndo (HasMetric.metric) WV GV x v) w
+        rw [HasMetric.metric.metricInner_smul_right]; rfl) with hΦ_def
   -- Step 1: per-`i` pointwise-eq reduction.
   have h_per_i : ∀ i,
-      metricInner x
+      HasMetric.metric.metricInner x
           (riemannCurvature HasMetric.metric (Bi i).toFun W.toFun gradF.toFun x) ((Bi i).toFun x)
         = Φ ((Bi i).toFun x) ((Bi i).toFun x) := by
     intro i
@@ -404,7 +404,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
         W WV gradF GV x h_interior rfl rfl rfl
     rw [hR_eq]; rfl
   -- Step 2 + 3 + 4: rewrite via h_per_i, Stage 7, identify with Ric, ricci_symm.
-  calc ∑ i, metricInner x
+  calc ∑ i, HasMetric.metric.metricInner x
         (riemannCurvature HasMetric.metric (Bi i).toFun W.toFun gradF.toFun x) ((Bi i).toFun x)
       = ∑ i, Φ ((Bi i).toFun x) ((Bi i).toFun x) :=
         Finset.sum_congr rfl (fun i _ => h_per_i i)
@@ -415,7 +415,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
         rw [ricciTensor_eq_sum_inner_orthonormal HasMetric.metric rfl x (W.toFun x) (gradF.toFun x)]
         apply Finset.sum_congr rfl
         intro i _
-        -- Φ v v = metricInner (curvatureEndo (HasMetric.metric) WV GV x v) v
+        -- Φ v v = HasMetric.metric.metricInner (curvatureEndo (HasMetric.metric) WV GV x v) v
         --       = ⟪curvatureEndo (HasMetric.metric) WV GV x v, v⟫_ℝ (def-eq)
         --       = ⟪v, curvatureEndo (HasMetric.metric) WV GV x v⟫_ℝ (real_inner_comm).
         show ⟪curvatureEndo (HasMetric.metric) WV GV x ((stdOrthonormalBasis ℝ (TangentSpace I x)) i),
@@ -487,18 +487,18 @@ theorem smoothOrthoFrame_cov_skew
     (hBj x).mdifferentiableAt (by simp)
   -- Treat as constant section on the nbhd: `b ↦ g(B_i b, B_j b) =ᶠ if i = j then 1 else 0`.
   have h_constant_on_nbhd : ∀ᶠ b in 𝓝 x,
-      metricInner b (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b)
+      HasMetric.metric.metricInner b (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b)
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j b)
       = (if i = j then (1 : ℝ) else 0) := by
     filter_upwards [Riemannian.Tensor.smoothOrthoFrameNbhd_mem_nhds (I := I) (M := M) x]
       with b hb
     exact Riemannian.Tensor.smoothOrthoFrame_orthonormal (I := I) hm.metric x hb i j
   -- mfderiv equality.
-  have h_eq : (fun b : M => metricInner b
+  have h_eq : (fun b : M => HasMetric.metric.metricInner b
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b)
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j b)) =ᶠ[𝓝 x]
       (fun _ : M => (if i = j then (1 : ℝ) else 0)) := h_constant_on_nbhd
-  have h_mfderiv_eq : mfderiv I 𝓘(ℝ, ℝ) (fun b : M => metricInner b
+  have h_mfderiv_eq : mfderiv I 𝓘(ℝ, ℝ) (fun b : M => HasMetric.metric.metricInner b
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b)
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j b)) x =
       mfderiv I 𝓘(ℝ, ℝ) (fun _ : M => (if i = j then (1 : ℝ) else 0)) x :=
@@ -515,7 +515,7 @@ theorem smoothOrthoFrame_cov_skew
     (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j) x hVsm hBi_at hBj_at
   -- hmc : mfderiv (b ↦ g(B_i, B_j)) x ((const v) x) = g(LC B_i x (v), B_j x) + g(B_i x, LC B_j x (v))
   -- (const v) x = v, so this becomes the desired form, but with LHS = 0.
-  have h_lhs_zero : (mfderiv I 𝓘(ℝ, ℝ) (fun b : M => metricInner b
+  have h_lhs_zero : (mfderiv I 𝓘(ℝ, ℝ) (fun b : M => HasMetric.metric.metricInner b
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b)
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j b)) x) v = 0 := by
     rw [h_mfderiv_eq, h_const_zero]; rfl
@@ -548,7 +548,7 @@ theorem sum_hessianBilin_smoothOrthoFrame_cov_eq_zero
     Riemannian.Tensor.smoothOrthoFrameOrthonormalBasis (I := I) x with hbAt_def
   -- Key matrices.
   set a : Fin (Module.finrank ℝ E) → Fin (Module.finrank ℝ E) → ℝ :=
-    fun i j => metricInner x
+    fun i j => HasMetric.metric.metricInner x
       ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i) x (W.toFun x))
       (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j x) with ha_def
@@ -574,17 +574,17 @@ theorem sum_hessianBilin_smoothOrthoFrame_cov_eq_zero
     refine Finset.sum_congr rfl (fun j _ => ?_)
     -- bAt j = smoothOrthoFrame ... j x by `smoothOrthoFrameOrthonormalBasis_apply`.
     rw [Riemannian.Tensor.smoothOrthoFrameOrthonormalBasis_apply]
-    -- ⟪B_j x, v⟫_ℝ = metricInner x (B_j x) v = a i j (by metricInner_comm).
+    -- ⟪B_j x, v⟫_ℝ = HasMetric.metric.metricInner x (B_j x) v = a i j (by HasMetric.metric.metricInner_comm).
     show ⟪Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j x, v⟫_ℝ • _ = a i j • _
-    show metricInner x
+    show HasMetric.metric.metricInner x
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j x) v • _
         = a i j • _
     congr 1
-    show metricInner x
+    show HasMetric.metric.metricInner x
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j x) v
-        = metricInner x v
+        = HasMetric.metric.metricInner x v
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j x)
-    exact metricInner_comm x _ _
+    exact HasMetric.metric.metricInner_comm x _ _
   -- Step 2: rewrite the sum with the Riesz expansion + bilinearity of hessianBilin.
   have h_expand : ∀ i, hessianBilin (I := I) HasMetric.metric f x
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
@@ -610,7 +610,7 @@ theorem sum_hessianBilin_smoothOrthoFrame_cov_eq_zero
   have h_anti : ∀ i j, a i j = -(a j i) := by
     intro i j
     -- From smoothOrthoFrame_cov_skew: a i j + g(B_i, ∇_W B_j) = 0.
-    -- And g(B_i x, ∇_{W x} B_j) = g(∇_{W x} B_j, B_i x) = a j i by metricInner_comm.
+    -- And g(B_i x, ∇_{W x} B_j) = g(∇_{W x} B_j, B_i x) = a j i by HasMetric.metric.metricInner_comm.
     have h := smoothOrthoFrame_cov_skew HasMetric.metric rfl x i j (W.toFun x)
     have h_swap : HasMetric.metric.metricInner x
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
@@ -684,30 +684,30 @@ theorem sum_inner_secondCovDerivAt_grad_smoothOrthoFrame_of_inner_form
   classical
   -- Specialise hInner at w = ∇f x.
   have h := hInner (manifoldGradient (I := I) HasMetric.metric f x)
-  -- Chain: ∑ ⟨A i, ∇f⟩ = ⟨∑ A i, ∇f⟩ (sum_inner, via metricInner = ⟪·,·⟫_ℝ
-  -- def-eq) = ⟨∇Δf, ∇f⟩ + Ric (hInner) = ⟨∇f, ∇Δf⟩ + Ric (metricInner_comm).
-  calc ∑ i, metricInner x
+  -- Chain: ∑ ⟨A i, ∇f⟩ = ⟨∑ A i, ∇f⟩ (sum_inner, via HasMetric.metric.metricInner = ⟪·,·⟫_ℝ
+  -- def-eq) = ⟨∇Δf, ∇f⟩ + Ric (hInner) = ⟨∇f, ∇Δf⟩ + Ric (HasMetric.metric.metricInner_comm).
+  calc ∑ i, HasMetric.metric.metricInner x
           (secondCovDerivAt (I := I) (M := M) HasMetric.metric
             (manifoldGradient (I := I) HasMetric.metric f) x
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x))
           (manifoldGradient (I := I) HasMetric.metric f x)
-      = metricInner x
+      = HasMetric.metric.metricInner x
           (∑ i, secondCovDerivAt (I := I) (M := M) HasMetric.metric
             (manifoldGradient (I := I) HasMetric.metric f) x
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x))
           (manifoldGradient (I := I) HasMetric.metric f x) :=
         (sum_inner Finset.univ _ (manifoldGradient (I := I) HasMetric.metric f x)).symm
-    _ = metricInner x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)
+    _ = HasMetric.metric.metricInner x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)
             (manifoldGradient (I := I) HasMetric.metric f x)
           + ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x)
                                             (manifoldGradient (I := I) HasMetric.metric f x) := h
-    _ = metricInner x (manifoldGradient (I := I) HasMetric.metric f x)
+    _ = HasMetric.metric.metricInner x (manifoldGradient (I := I) HasMetric.metric f x)
             (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)
           + ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x)
                                             (manifoldGradient (I := I) HasMetric.metric f x) := by
-        rw [metricInner_comm x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)]
+        rw [HasMetric.metric.metricInner_comm x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)]
 
 end Operators
 end Riemannian
diff --git a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
index 78df348..fc335ae 100644
--- a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
@@ -99,8 +99,8 @@ theorem bochner_per_summand_swap
   -- Equivalent (def-eq) to the section-level form of
   -- `hessianBilin_section_eventually_symm_of_strict_interior` with X := B, Y := W.
   have h_section_sym :
-      (fun y : M => metricInner y (Q y) (W.toFun y))
-        =ᶠ[𝓝 x] (fun y : M => metricInner y (P y) (B.toFun y)) :=
+      (fun y : M => HasMetric.metric.metricInner y (Q y) (W.toFun y))
+        =ᶠ[𝓝 x] (fun y : M => HasMetric.metric.metricInner y (P y) (B.toFun y)) :=
     hessianBilin_section_eventually_symm_of_strict_interior
       (I := I) HasMetric.metric rfl f hf B.toFun W.toFun x
   -- Step (c): metric compat on `(P, B)` along direction `B x` at `x`.
@@ -110,9 +110,9 @@ theorem bochner_per_summand_swap
   -- Step (d): differentiate `h_section_sym` at `x` along `B x` via `EventuallyEq.mfderiv_eq`.
   have h_mfderiv_eq :
       mfderiv I 𝓘(ℝ, ℝ)
-          (fun y : M => metricInner y (Q y) (W.toFun y)) x (B.toFun x)
+          (fun y : M => HasMetric.metric.metricInner y (Q y) (W.toFun y)) x (B.toFun x)
         = mfderiv I 𝓘(ℝ, ℝ)
-          (fun y : M => metricInner y (P y) (B.toFun y)) x (B.toFun x) := by
+          (fun y : M => HasMetric.metric.metricInner y (P y) (B.toFun y)) x (B.toFun x) := by
     rw [Filter.EventuallyEq.mfderiv_eq h_section_sym]
     rfl
   -- `h_mfderiv_eq : mfderiv (...g(Q, W)) x (B x) = mfderiv (...g(P, B)) x (B x)`.
@@ -122,13 +122,13 @@ theorem bochner_per_summand_swap
   --   = mfderiv (b ↦ g(P, B)) x (B x)   [h_mfderiv_eq]
   --   = g(LC P x (B x), B x) + g(P x, LC B x (B x))  [h_compat_PB]
   have h_combined :
-      metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Q x (B.toFun x))
+      HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Q x (B.toFun x))
           (W.toFun x)
-        + metricInner x (Q x)
+        + HasMetric.metric.metricInner x (Q x)
             ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun W.toFun x (B.toFun x))
-      = metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun P x (B.toFun x))
+      = HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun P x (B.toFun x))
           (B.toFun x)
-        + metricInner x (P x)
+        + HasMetric.metric.metricInner x (P x)
             ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun B.toFun x (B.toFun x)) := by
     rw [← h_compat_QW, h_mfderiv_eq, h_compat_PB]
   -- Step (e): identify `g(Q x, LC W x (B x))` via `hessianBilin_symm` at `x`.
@@ -162,36 +162,36 @@ theorem bochner_per_summand_swap
             ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun B.toFun x (B.toFun x))
             (W.toFun x) :=
     h_hess_sym _ _
-  -- Unfold `hessianBilin f x a b = metricInner x (covDerivAt HasMetric.metric ∇f x a) b` (rfl).
-  -- LHS of h_sym_BW : `metricInner x (Q x) (LC W x (B x)) = metricInner x (LC ∇f x (LC W x (B x))) (B x)`.
-  -- LHS of h_sym_WB : `metricInner x (P x) (LC B x (B x)) = metricInner x (LC ∇f x (LC B x (B x))) (W x)`.
+  -- Unfold `hessianBilin f x a b = HasMetric.metric.metricInner x (covDerivAt HasMetric.metric ∇f x a) b` (rfl).
+  -- LHS of h_sym_BW : `HasMetric.metric.metricInner x (Q x) (LC W x (B x)) = HasMetric.metric.metricInner x (LC ∇f x (LC W x (B x))) (B x)`.
+  -- LHS of h_sym_WB : `HasMetric.metric.metricInner x (P x) (LC B x (B x)) = HasMetric.metric.metricInner x (LC ∇f x (LC B x (B x))) (W x)`.
   -- Note Q x = LC ∇f x (B x) and P x = LC ∇f x (W x) (def-eq).
-  -- We need `metricInner x (Q x) (LC W x (B x))` form on LHS of h_sym_BW.
-  -- `hessianBilin f x (B x) v = metricInner x (covDerivAt HasMetric.metric ∇f x (B x)) v = metricInner x (Q x) v`
+  -- We need `HasMetric.metric.metricInner x (Q x) (LC W x (B x))` form on LHS of h_sym_BW.
+  -- `hessianBilin f x (B x) v = HasMetric.metric.metricInner x (covDerivAt HasMetric.metric ∇f x (B x)) v = HasMetric.metric.metricInner x (Q x) v`
   -- by def (covDerivAt HasMetric.metric ∇f x (B x) = (lcc ∇f) x (B x) = Q x def-eq).
-  have h_QcovBW : metricInner x (Q x)
+  have h_QcovBW : HasMetric.metric.metricInner x (Q x)
         ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun W.toFun x (B.toFun x))
-      = metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun gradF.toFun x
+      = HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun gradF.toFun x
           ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun W.toFun x (B.toFun x)))
           (B.toFun x) := h_sym_BW
-  have h_PcovBB : metricInner x (P x)
+  have h_PcovBB : HasMetric.metric.metricInner x (P x)
         ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun B.toFun x (B.toFun x))
-      = metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun gradF.toFun x
+      = HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun gradF.toFun x
           ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun B.toFun x (B.toFun x)))
           (W.toFun x) := h_sym_WB
   rw [h_QcovBW, h_PcovBB] at h_combined
   -- Rearrange to match the goal: LHS - LCBB term = RHS - LCWB term.
   -- The goal uses `covDerivAt HasMetric.metric ∇f x v` form rather than `lcc.toFun ∇f x v`.
   -- These are definitionally equal: `covDerivAt HasMetric.metric Y x v := (lcc.toFun Y x) v`.
-  show metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Q x (B.toFun x))
+  show HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Q x (B.toFun x))
           (W.toFun x)
-        - metricInner x
+        - HasMetric.metric.metricInner x
             ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun gradF.toFun x
               ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun B.toFun x (B.toFun x)))
             (W.toFun x)
-      = metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun P x (B.toFun x))
+      = HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun P x (B.toFun x))
           (B.toFun x)
-        - metricInner x
+        - HasMetric.metric.metricInner x
             ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun gradF.toFun x
               ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun W.toFun x (B.toFun x)))
             (B.toFun x)
@@ -274,7 +274,7 @@ theorem bochner_per_summand_riemann_form
   rw [h_riem, h_lieb_dir]
   -- Now: g(∇_B ∇_W ∇f - ∇_W ∇_B ∇f - (covDeriv HasMetric.metric ∇f (∇_B W) - covDeriv HasMetric.metric ∇f (∇_W B)), B x)
   --     = g(∇_B ∇_W ∇f, B) - g(∇_W ∇_B ∇f, B) - g(covDeriv HasMetric.metric ∇f (∇_B W), B) + g(covDeriv HasMetric.metric ∇f (∇_W B), B)
-  -- (by metricInner_sub_left distribution × 2 + metricInner_add_left for the inner +).
+  -- (by HasMetric.metric.metricInner_sub_left distribution × 2 + HasMetric.metric.metricInner_add_left for the inner +).
   -- Goal becomes pure algebra; linarith with metricInner-sub distribution closes.
   rw [HasMetric.metric.metricInner_sub_left, HasMetric.metric.metricInner_sub_left,
       HasMetric.metric.metricInner_sub_left]
@@ -331,12 +331,12 @@ theorem bochner_per_summand_assembled
   have h_compat_QB := leviCivitaConnection_metric_compatible HasMetric.metric
     W.toFun Q B.toFun x (W.smoothAt x) hQ_smooth (B.smoothAt x)
   simp only [← leviCivitaConnection_toFun_eq_covDeriv] at h_compat_QB
-  -- Identify `(fun y => metricInner y (Q y) (B y)) = (fun y => hessianBilin f y (B y) (B y))`.
+  -- Identify `(fun y => HasMetric.metric.metricInner y (Q y) (B y)) = (fun y => hessianBilin f y (B y) (B y))`.
   have h_QB_section :
-      (fun y : M => metricInner y (Q y) (B.toFun y))
+      (fun y : M => HasMetric.metric.metricInner y (Q y) (B.toFun y))
         = (fun y : M => hessianBilin (I := I) HasMetric.metric f y (B.toFun y) (B.toFun y)) := by
     funext y
-    -- hessianBilin f y v w = metricInner y (covDerivAt HasMetric.metric ∇f y v) w (def).
+    -- hessianBilin f y v w = HasMetric.metric.metricInner y (covDerivAt HasMetric.metric ∇f y v) w (def).
     -- Q y = covDeriv HasMetric.metric B ∇f y = covDerivAt HasMetric.metric ∇f y (B y) (def).
     rfl
   rw [h_QB_section] at h_compat_QB
@@ -375,7 +375,7 @@ theorem bochner_per_summand_assembled
   --   g(LC Q x (W x), B) = mfderiv (...) - g(Q x, LC B x (W x))
   --                       = mfderiv (...) - hessianBilin f x (B x) (LC B x (W x))
   -- and g(LC Gf x (LC B x (W x))) (B) = hessianBilin f x (LC B x (W x)) (B x)
-  --   (def: hessianBilin f x v w = metricInner x (covDerivAt HasMetric.metric ∇f x v) w; here v = LC B x (W x) = ∇_W B x, w = B x)
+  --   (def: hessianBilin f x v w = HasMetric.metric.metricInner x (covDerivAt HasMetric.metric ∇f x v) w; here v = LC B x (W x) = ∇_W B x, w = B x)
   --   = hessianBilin f x (B x) (LC B x (W x))   [by h_sym_WB]
   -- So the cancellation:
   --   g(R + g(LC Q W, B) - Hess(LC B W, B)
@@ -390,9 +390,9 @@ theorem bochner_per_summand_assembled
   -- Rewrite h_compat_QB in terms of mf_val.
   have h_compat_QB' :
       mf_val
-        = metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Q x (W.toFun x))
+        = HasMetric.metric.metricInner x ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Q x (W.toFun x))
             (B.toFun x)
-          + metricInner x (Q x)
+          + HasMetric.metric.metricInner x (Q x)
               ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun B.toFun x (W.toFun x)) :=
     h_compat_QB
   have h_id_LCQW :
@@ -441,7 +441,7 @@ without any Hom-bundle Leibniz bridge. -/
 /-- **Eng.** Smoothness of the section-form Hessian summand
 `b ↦ ⟨covDerivAt HasMetric.metric ∇f b (B b), B b⟩_g` at `x`, via composition of
 `leviCivitaConnection_smoothAt_smoothVF_dir` with
-`metricInner_mdifferentiableAt_of_tangentSmoothAt`. -/
+`HasMetric.metric.metricInner_mdifferentiableAt_of_tangentSmoothAt`. -/
 private lemma hessianBilin_smoothVF_diag_mdifferentiableAt
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f)
     (B : SmoothVectorField I M) (x : M) :
@@ -457,9 +457,9 @@ private lemma hessianBilin_smoothVF_diag_mdifferentiableAt
     leviCivitaConnection_smoothAt_smoothVF_dir HasMetric.metric B gradF x
   -- Smoothness of `b ↦ B b` (just B.smoothAt).
   have h_B : TangentSmoothAt B.toFun x := B.smoothAt x
-  -- `hessianBilin f y v w = metricInner y (covDerivAt HasMetric.metric ∇f y v) w` (def).
-  -- So the diagonal is `metricInner y (covDerivAt HasMetric.metric ∇f y (B y)) (B y)`.
-  exact metricInner_mdifferentiableAt_of_tangentSmoothAt h_covAt h_B
+  -- `hessianBilin f y v w = HasMetric.metric.metricInner y (covDerivAt HasMetric.metric ∇f y v) w` (def).
+  -- So the diagonal is `HasMetric.metric.metricInner y (covDerivAt HasMetric.metric ∇f y (B y)) (B y)`.
+  exact HasMetric.metric.metricInner_mdifferentiableAt_of_tangentSmoothAt h_covAt h_B
 
 /-- **Math.** **Heart-of-Bochner reduction (section form, unconditional)**:
 $$\langle \Delta_\nabla \nabla f, \nabla f\rangle_g
@@ -488,7 +488,7 @@ theorem bochner_connectionLaplacian_grad_decomposition
       smooth := Riemannian.Tensor.smoothOrthoFrame_smooth (I := I) hm.metric x i }
   -- Per-summand quantities.
   set Rterm : Fin (Module.finrank ℝ E) → ℝ := fun i =>
-    metricInner x
+    HasMetric.metric.metricInner x
       (riemannCurvature HasMetric.metric (Bi i).toFun gradF.toFun gradF.toFun x)
       ((Bi i).toFun x) with hRterm_def
   set Mterm : Fin (Module.finrank ℝ E) → ℝ := fun i =>
@@ -500,36 +500,36 @@ theorem bochner_connectionLaplacian_grad_decomposition
       (covDeriv HasMetric.metric gradF.toFun (Bi i).toFun x) with hHterm_def
   -- Per-summand: `g(secondCovDerivSection ∇f Bi Bi x, ∇f x) = R + M - 2 H`.
   have h_per_summand : ∀ i,
-      metricInner x
+      HasMetric.metric.metricInner x
           (secondCovDerivSection (I := I) (M := M) HasMetric.metric
             gradF.toFun (Bi i).toFun (Bi i).toFun x)
           (gradF.toFun x)
         = Rterm i + Mterm i - 2 * Hterm i := by
     intro i
-    show metricInner x
+    show HasMetric.metric.metricInner x
           (covDeriv HasMetric.metric (Bi i).toFun (covDeriv HasMetric.metric (Bi i).toFun gradF.toFun) x
             - covDerivAt HasMetric.metric gradF.toFun x (covDeriv HasMetric.metric (Bi i).toFun (Bi i).toFun x))
           (gradF.toFun x) = _
-    rw [metricInner_sub_left]
+    rw [HasMetric.metric.metricInner_sub_left]
     show _ = Rterm i + Mterm i - 2 * Hterm i
     rw [hRterm_def, hMterm_def, hHterm_def]
     exact bochner_per_summand_assembled (I := I) HasMetric.metric rfl f hf (Bi i) gradF x
   -- Main: unfold `connectionLaplacian`, sum_inner pull-out, per_summand, sum-distribute.
-  show metricInner x
+  show HasMetric.metric.metricInner x
         (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
         (manifoldGradient (I := I) HasMetric.metric f x)
-      = metricInner x (manifoldGradient (I := I) HasMetric.metric f x)
+      = HasMetric.metric.metricInner x (manifoldGradient (I := I) HasMetric.metric f x)
           (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)
         + ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x)
                                           (manifoldGradient (I := I) HasMetric.metric f x)
   rw [connectionLaplacian_def]
   -- Pull sum out via `sum_inner`.
   have h_pull :
-      metricInner x
+      HasMetric.metric.metricInner x
           (∑ i, secondCovDerivSection (I := I) (M := M) HasMetric.metric
             gradF.toFun (Bi i).toFun (Bi i).toFun x)
           (gradF.toFun x)
-        = ∑ i, metricInner x
+        = ∑ i, HasMetric.metric.metricInner x
             (secondCovDerivSection (I := I) (M := M) HasMetric.metric
               gradF.toFun (Bi i).toFun (Bi i).toFun x)
             (gradF.toFun x) :=
@@ -578,11 +578,11 @@ theorem bochner_connectionLaplacian_grad_decomposition
     exact Filter.EventuallyEq.mfderiv_eq h_eventuallyEq
   have h_grad_dual :
       (mfderiv I 𝓘(ℝ, ℝ) (Operators.scalarLaplacian (I := I) HasMetric.metric f : M → ℝ) x (gradF.toFun x) : ℝ)
-        = metricInner x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x) (gradF.toFun x) :=
+        = HasMetric.metric.metricInner x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x) (gradF.toFun x) :=
     (manifoldGradient_inner_eq HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x (gradF.toFun x)).symm
   -- Combine.
   rw [h_R_eq, h_H_eq, h_M_factor, h_M_to_lap, h_grad_dual,
-      metricInner_comm x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)]
+      HasMetric.metric.metricInner_comm x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)]
   ring
 
 -- `bochner_weitzenboeck` (the headline) lives in `Operators/Bochner.lean`,
diff --git a/OpenGALib/Riemannian/Util/DivergenceSimp.lean b/OpenGALib/Riemannian/Util/DivergenceSimp.lean
index a628d5c..46c8edc 100644
--- a/OpenGALib/Riemannian/Util/DivergenceSimp.lean
+++ b/OpenGALib/Riemannian/Util/DivergenceSimp.lean
@@ -4,7 +4,7 @@ import OpenGALib.Riemannian.Operators.Divergence
 # Divergence — simp def-unfold
 
 Engineering simp lemma exposing the definition of `divergence` as a sum
-of `metricInner (∇_{B_i} X) B_i` over the smooth $g$-orthonormal frame.
+of `HasMetric.metric.metricInner (∇_{B_i} X) B_i` 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.
 -/
@@ -25,7 +25,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa
   [hm : HasMetric I M]
 
 /-- **Eng.** Definitional unfold of `divergence` as a sum of
-`metricInner (∇_{B_i} X) B_i` over the smooth $g$-orthonormal frame. Pure
+`HasMetric.metric.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)
diff --git a/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean b/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean
index b255444..6c55080 100644
--- a/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean
+++ b/OpenGALib/Riemannian/Util/MetricInnerSmoothness.lean
@@ -13,7 +13,7 @@ Engineering parity API expanding the Math headlines
 
 into the full `_within_at / _at / _on / _` parity for both the
 explicit-metric form `g.metricInner_X` and the typeclass-bound form
-`metricInner_X` keyed on `[HasMetric I M]`. Each variant is a pointwise
+`HasMetric.metric.metricInner_X` keyed on `[HasMetric I M]`. Each variant is a pointwise
 reduction to the Math headline.
 -/
 
@@ -152,7 +152,7 @@ theorem metricInner_contMDiffAt
     (hw : ContMDiffAt I (I.prod 𝓘(ℝ, E)) n
       (fun y => (⟨y, w y⟩ : TangentBundle I M)) x) :
     ContMDiffAt I 𝓘(ℝ, ℝ) n
-      (fun y => metricInner y (v y) (w y)) x :=
+      (fun y => HasMetric.metric.metricInner y (v y) (w y)) x :=
   hm.metric.metricInner_contMDiffAt hv hw
 
 /-- **Eng.** Set-form variant. -/
@@ -162,7 +162,7 @@ theorem metricInner_contMDiffOn
     (hw : ContMDiffOn I (I.prod 𝓘(ℝ, E)) n
       (fun y => (⟨y, w y⟩ : TangentBundle I M)) s) :
     ContMDiffOn I 𝓘(ℝ, ℝ) n
-      (fun y => metricInner y (v y) (w y)) s :=
+      (fun y => HasMetric.metric.metricInner y (v y) (w y)) s :=
   hm.metric.metricInner_contMDiffOn hv hw
 
 /-- **Eng.** Global variant. -/
@@ -172,7 +172,7 @@ theorem metricInner_contMDiff
     (hw : ContMDiff I (I.prod 𝓘(ℝ, E)) n
       (fun y => (⟨y, w y⟩ : TangentBundle I M))) :
     ContMDiff I 𝓘(ℝ, ℝ) n
-      (fun y => metricInner y (v y) (w y)) :=
+      (fun y => HasMetric.metric.metricInner y (v y) (w y)) :=
   hm.metric.metricInner_contMDiff hv hw
 
 /-! ### `MDifferentiable` family — first-order differentiability -/
@@ -184,7 +184,7 @@ theorem metricInner_mdifferentiableWithinAt
     (hw : MDifferentiableWithinAt I (I.prod 𝓘(ℝ, E))
       (fun y => (⟨y, w y⟩ : TangentBundle I M)) s x) :
     MDifferentiableWithinAt I 𝓘(ℝ, ℝ)
-      (fun y => metricInner y (v y) (w y)) s x :=
+      (fun y => HasMetric.metric.metricInner y (v y) (w y)) s x :=
   hm.metric.metricInner_mdifferentiableWithinAt hv hw
 
 /-- **Eng.** Pointwise differentiability. -/
@@ -194,7 +194,7 @@ theorem metricInner_mdifferentiableAt
     (hw : MDifferentiableAt I (I.prod 𝓘(ℝ, E))
       (fun y => (⟨y, w y⟩ : TangentBundle I M)) x) :
     MDifferentiableAt I 𝓘(ℝ, ℝ)
-      (fun y => metricInner y (v y) (w y)) x :=
+      (fun y => HasMetric.metric.metricInner y (v y) (w y)) x :=
   hm.metric.metricInner_mdifferentiableAt hv hw
 
 /-- **Eng.** Set-form differentiability. -/
@@ -204,7 +204,7 @@ theorem metricInner_mdifferentiableOn
     (hw : MDifferentiableOn I (I.prod 𝓘(ℝ, E))
       (fun y => (⟨y, w y⟩ : TangentBundle I M)) s) :
     MDifferentiableOn I 𝓘(ℝ, ℝ)
-      (fun y => metricInner y (v y) (w y)) s :=
+      (fun y => HasMetric.metric.metricInner y (v y) (w y)) s :=
   hm.metric.metricInner_mdifferentiableOn hv hw
 
 /-- **Eng.** Global differentiability. -/
@@ -214,7 +214,7 @@ theorem metricInner_mdifferentiable
     (hw : MDifferentiable I (I.prod 𝓘(ℝ, E))
       (fun y => (⟨y, w y⟩ : TangentBundle I M))) :
     MDifferentiable I 𝓘(ℝ, ℝ)
-      (fun y => metricInner y (v y) (w y)) :=
+      (fun y => HasMetric.metric.metricInner y (v y) (w y)) :=
   hm.metric.metricInner_mdifferentiable hv hw
 
 /-- **Eng.** `TangentSmoothAt`-form pointwise differentiability — convenience
@@ -224,8 +224,8 @@ theorem metricInner_mdifferentiableAt_of_tangentSmoothAt
     {Y Z : ∀ y : M, TangentSpace I y} {x : M}
     (hY : TangentSmoothAt Y x) (hZ : TangentSmoothAt Z x) :
     MDifferentiableAt I 𝓘(ℝ, ℝ)
-      (fun y => metricInner y (Y y) (Z y)) x :=
-  metricInner_mdifferentiableAt hY.toBundleSection hZ.toBundleSection
+      (fun y => HasMetric.metric.metricInner y (Y y) (Z y)) x :=
+  HasMetric.metric.metricInner_mdifferentiableAt hY.toBundleSection hZ.toBundleSection
 
 end MetricInnerSmoothness