diff --git a/OpenGALib/Riemannian/Connection/LeviCivita.lean b/OpenGALib/Riemannian/Connection/LeviCivita.lean
index 211e996..a42fc2f 100644
--- a/OpenGALib/Riemannian/Connection/LeviCivita.lean
+++ b/OpenGALib/Riemannian/Connection/LeviCivita.lean
@@ -325,13 +325,6 @@ noncomputable def covDeriv
     TangentSpace I x :=
   ((leviCivitaConnection (I := I) (M := M) g).toFun Y x) (X x)
 
-/-- **Math.** Notation `∇[X] Y` for `covDeriv (HasMetric.metric) X Y`. The
-notation pipes the ambient `[HasMetric I M]` metric so downstream code
-continues to write `∇[X] Y` unchanged during Phase 1 (typeclass retained
-until #19). -/
-scoped[Riemannian] notation:max "∇[" X "] " Y:max =>
-  covDeriv (HasMetric.metric) X Y
-
 /-- **Math.** Notation `⟦X, Y⟧` for the manifold Lie bracket
 `mlieBracket _ X Y` (model `I` inferred from section types). -/
 scoped[Riemannian] notation:max "⟦" X ", " Y "⟧" =>
@@ -927,10 +920,10 @@ This is the standard $(1,4)$-tensor covariant-derivative pattern: $\nabla$
 acts on each slot of $R$ as a derivation. -/
 noncomputable def covDerivRiemann
     (X Y Z W : SmoothVectorField I M) (x : M) : TangentSpace I x :=
-  (∇[X] (Riem(Y, Z) W)) x
-    - Riem(∇[X] Y, Z) W x
-    - Riem(Y, ∇[X] Z) W x
-    - Riem(Y, Z) (∇[X] W) x
+  covDeriv HasMetric.metric X.toFun (Riem(Y, Z) W) x
+    - Riem(covDeriv HasMetric.metric X Y, Z) W x
+    - Riem(Y, covDeriv HasMetric.metric X Z) W x
+    - Riem(Y, Z) (covDeriv HasMetric.metric X W) x
 
 /-- **Math.** Notation `(∇R)[X](Y, Z) W` for `covDerivRiemann X Y Z W`. -/
 scoped[Riemannian] notation:max "(∇R)[" X "](" Y ", " Z ") " W:max =>
diff --git a/OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean b/OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean
index 7d7bcba..c3816fc 100644
--- a/OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean
+++ b/OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean
@@ -552,18 +552,7 @@ noncomputable def scalarCurvature
     (g : RiemannianMetric I M) (x : M) : ℝ :=
   LinearMap.trace ℝ (TangentSpace I x) (ricciSharp (I := I) (M := M) g x)
 
-/-- **Math.** Notation `scal_g[I]` for the scalar curvature on the ambient
-`[HasMetric I M]` metric. `I` is bracketed because `x : M` does not expose
-the model with corners. The notation pipes `HasMetric.metric` so downstream
-consumers continue to write `scal_g[I] x` during Phase 1 (typeclass
-retained until #19). -/
-scoped[Riemannian] notation:max "scal_g[" I "]" =>
-  scalarCurvature (I := I) (HasMetric.metric)
 
-/-- **Math.** Notation `Ric_g(v, w) x` for `ricciTensor HasMetric.metric x v w`
-on the ambient `[HasMetric I M]` metric. -/
-scoped[Riemannian] notation:max "Ric_g(" v ", " w ") " x:max =>
-  ricciTensor (HasMetric.metric) x v w
 
 /-! ## Ricci-flat and Einstein metric predicates
 
@@ -575,7 +564,7 @@ explicit argument because the underlying notations (`Ric_g`,
 /-- **Math.** The ambient Riemannian metric is **Ricci-flat** if its
 Ricci tensor vanishes pointwise. -/
 def IsRicciFlat : Prop :=
-  ∀ (x : M) (V W : TangentSpace I x), Ric_g(V, W) x = 0
+  ∀ (x : M) (V W : TangentSpace I x), ricciTensor HasMetric.metric x V W = 0
 
 /-- **Math.** The ambient Riemannian metric is **Einstein** if its Ricci
 tensor is a constant scalar multiple of the metric:
@@ -585,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),
-    Ric_g(V, W) x = c * metricInner x V W
+    ricciTensor HasMetric.metric x V W = c * metricInner x V W
 
 end Riemannian
 
diff --git a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
index d2f601e..b9cab59 100644
--- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
+++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
@@ -215,13 +215,6 @@ noncomputable def ricci
     (X Y : SmoothVectorField I M) (x : M) : ℝ :=
   LinearMap.trace ℝ (TangentSpace I x) (curvatureEndo g X Y x)
 
-/-- **Math.** The Ricci curvature as a scalar function on the manifold:
-`(Ric(X, Y))(x) = ricci HasMetric.metric X Y x`. The notation pipes the
-ambient `[HasMetric I M]` metric so downstream consumers continue to
-write `Ric(X, Y)` unchanged during Phase 1 (typeclass retained). -/
-scoped[Riemannian] notation:max "Ric(" X ", " Y ")" =>
-  ricci (HasMetric.metric) X Y
-
 /-! ### Diagonal `(3,4)` vanishing: $g(R(X,Y)Z, Z) = 0$
 
 do Carmo §4 Proposition 2.5(iii) closure. The proof reduces, via metric
@@ -759,12 +752,12 @@ theorem ricci_symm
   set b := stdOrthonormalBasis ℝ (TangentSpace I x) with hb_def
   -- Expand each Ricci scalar as `∑ i, ⟪b i, R(const b i, ·) · x⟫_ℝ` via
   -- `LinearMap.trace_eq_sum_inner`.
-  have h_RXY : Ric(X, Y) x =
+  have h_RXY : ricci HasMetric.metric X Y x =
       ∑ i, ⟪b i, riemannCurvature HasMetric.metric (fun _ : M => (b i : E)) X.toFun Y.toFun x⟫_ℝ := by
     show LinearMap.trace ℝ (TangentSpace I x)
           (curvatureEndo (HasMetric.metric) X Y x) = _
     exact LinearMap.trace_eq_sum_inner _ b
-  have h_RYX : Ric(Y, X) x =
+  have h_RYX : ricci HasMetric.metric Y X x =
       ∑ i, ⟪b i, riemannCurvature HasMetric.metric (fun _ : M => (b i : E)) Y.toFun X.toFun x⟫_ℝ := by
     show LinearMap.trace ℝ (TangentSpace I x)
           (curvatureEndo (HasMetric.metric) Y X x) = _
@@ -806,7 +799,7 @@ is by isometries).
 Reference: do Carmo §3 Ex. 5; Petersen Ch. 8. -/
 def IsKilling (X : SmoothVectorField I M) : Prop :=
   ∀ (U W : SmoothVectorField I M) (y : M),
-    metricInner y ((∇[U] X) y) (W y) + metricInner y ((∇[W] X) y) (U y) = 0
+    metricInner y ((covDeriv HasMetric.metric U X) y) (W y) + metricInner y ((covDeriv HasMetric.metric W X) y) (U y) = 0
 
 /-- **Math.** Covariantly differentiating the Killing equation.
 
@@ -956,7 +949,9 @@ Cheeger–Ebin §1.84. -/
 theorem IsKilling.second_covDeriv_eq_curvature
     (X : SmoothVectorField I M) (hX : IsKilling X)
     (Y Z : SmoothVectorField I M) (x : M) :
-    (∇[Y] (∇[Z] X)) x - (∇[∇[Y] Z] X) x = Riem(Y, X) Z x := by
+    covDeriv HasMetric.metric Y.toFun (covDeriv HasMetric.metric Z X) x
+      - covDeriv HasMetric.metric (covDeriv HasMetric.metric Y Z) X.toFun x
+      = Riem(Y, X) Z x := by
   classical
   apply (metricInner_eq_iff_eq x _ _).mp
   intro w
@@ -1067,10 +1062,6 @@ noncomputable def sectionalCurvature
     (metricInner x (X x) (X x) * metricInner x (Y x) (Y x)
       - metricInner x (X x) (Y x) ^ 2)
 
-/-- **Math.** Notation `K_g[I](X, Y)` for `sectionalCurvature X Y`. -/
-scoped[Riemannian] notation:max "K_g[" I "](" X ", " Y ")" =>
-  sectionalCurvature (I := I) X Y
-
 /-- **Math.** **Tangent-vector form** of sectional curvature: same
 formula as `sectionalCurvature` but consuming the pointwise tangent
 vectors $v, w \in T_xM$ directly via constant-section lifts. Useful when
@@ -1093,7 +1084,7 @@ Denominator: symmetric in $X, Y$ via `metricInner_comm`. -/
 theorem sectionalCurvature_symmetric
     [IsManifold I 2 M]
     (X Y : SmoothVectorField I M) (x : M) :
-    K_g[I](X, Y) x = K_g[I](Y, X) x := by
+    sectionalCurvature (I := I) X Y x = sectionalCurvature (I := I) Y X x := by
   unfold sectionalCurvature
   congr 1
   · -- Numerator: g(R(X,Y) Y, X) = g(R(Y,X) X, Y) via pair-symmetry + double antisym.
diff --git a/OpenGALib/Riemannian/Operators/Bochner.lean b/OpenGALib/Riemannian/Operators/Bochner.lean
index 7765c68..04c3bbb 100644
--- a/OpenGALib/Riemannian/Operators/Bochner.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner.lean
@@ -56,12 +56,14 @@ Combines `hessian_gradientNormSq_apply_chartFrame` summed over
 theorem bochner_leibniz_trace_reduction
     [IsManifold I 2 M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
-    (1 / 2 : ℝ) * (Δ_g[I] ‖grad_g[I] f‖²_g) x
-      = ⟪connectionLaplacian HasMetric.metric (grad_g[I] f) x, (grad_g[I] f) x⟫_g
-        + ‖hess_g[I] f‖²_g x := by
+    (1 / 2 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x
+      = HasMetric.metric.metricInner x
+            (connectionLaplacian HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
+            ((manifoldGradient (I := I) HasMetric.metric f) x)
+        + ‖Operators.hessianBilin (I := I) HasMetric.metric f‖²_g x := by
   classical
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
-  show (1 / 2 : ℝ) * Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g) x
+  show (1 / 2 : ℝ) * Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x
       = metricInner x
           (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
           (manifoldGradient (I := I) HasMetric.metric f x)
@@ -73,23 +75,23 @@ theorem bochner_leibniz_trace_reduction
   -- Step 1: convert `scalarLaplacian` from std-basis trace to smoothOrthoFrame trace
   -- via Stage 7 basis-invariance of trace (`sum_diagonal_smoothOrthoFrame_eq_std`).
   have h_scalarLap_eq :
-      Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g) x
-        = ∑ i, hessian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g)
+      Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x
+        = ∑ i, hessian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)
             (Bi i).toFun (Bi i).toFun x := by
     rw [scalarLaplacian_eq_laplacian_hessianBilin HasMetric.metric]
     show laplacian (I := I) (M := M)
-        (hessianBilin (I := I) HasMetric.metric (‖grad_g[I] f‖²_g)) x = _
+        (hessianBilin (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x = _
     unfold laplacian
     rw [trace_def]
     rw [← Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x
-          (hessianBilin (I := I) HasMetric.metric (‖grad_g[I] f‖²_g) x)]
+          (hessianBilin (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x)]
     refine Finset.sum_congr rfl ?_
     intro i _
     rfl
   rw [h_scalarLap_eq, Finset.mul_sum]
   -- Step 2: per-summand section-form Hess identity (`hessian_gradientNormSq_apply_section`).
   have h_summand : ∀ i,
-      (1 / 2 : ℝ) * hessian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g)
+      (1 / 2 : ℝ) * hessian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)
         (Bi i).toFun (Bi i).toFun x
       = metricInner x
             (secondCovDerivSection (I := I) (M := M) HasMetric.metric
@@ -239,10 +241,11 @@ Reference: Petersen Ch. 7 §1 Prop 33; do Carmo §6; Schoen-Simon 1981 §1. -/
 theorem bochner_weitzenboeck
     [IsManifold I 2 M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
-    (1 / 2 : ℝ) * (Δ_g[I] ‖grad_g[I] f‖²_g) x =
-      ‖hess_g[I] f‖²_g x
-      + ⟪(grad_g[I] f) x, (grad_g[I] (Δ_g[I] f)) x⟫_g
-      + Ric_g((grad_g[I] f) x, (grad_g[I] f) x) x := by
+    (1 / 2 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x =
+      ‖Operators.hessianBilin (I := I) HasMetric.metric f‖²_g 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 [bochner_leibniz_trace_reduction f hf x,
       bochner_connectionLaplacian_grad_decomposition f hf x]
   abel
diff --git a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
index 19265eb..8b2011c 100644
--- a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
@@ -61,7 +61,7 @@ endomorphism. -/
 theorem ricciTensor_eq_sum_inner_orthonormal
     [IsManifold I 2 M]
     (x : M) (V W : TangentSpace I x) :
-    Ric_g(V, W) x =
+    ricciTensor HasMetric.metric x V W =
       ∑ i, ⟪(stdOrthonormalBasis ℝ (TangentSpace I x)) i,
             curvatureEndo (HasMetric.metric)
               (SmoothVectorField.const (I := I) (M := M) V)
@@ -339,7 +339,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i)
           W.toFun (manifoldGradient (I := I) HasMetric.metric f) x)
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
-      = Ric_g(manifoldGradient (I := I) HasMetric.metric f x, W.toFun x) x := by
+      = ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x) (W.toFun x) := by
   classical
   have h_interior : extChartAt I x x ∈ closure (interior (Set.range I)) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
@@ -401,7 +401,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
     _ = ∑ i, Φ ((stdOrthonormalBasis ℝ (TangentSpace I x)) i)
                 ((stdOrthonormalBasis ℝ (TangentSpace I x)) i) :=
         Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x Φ
-    _ = Ric_g(W.toFun x, gradF.toFun x) x := by
+    _ = ricciTensor HasMetric.metric x (W.toFun x) (gradF.toFun x) := by
         rw [ricciTensor_eq_sum_inner_orthonormal x (W.toFun x) (gradF.toFun x)]
         apply Finset.sum_congr rfl
         intro i _
@@ -413,7 +413,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
             = ⟪(stdOrthonormalBasis ℝ (TangentSpace I x)) i,
                 curvatureEndo (HasMetric.metric) WV GV x ((stdOrthonormalBasis ℝ (TangentSpace I x)) i)⟫_ℝ
         exact real_inner_comm _ _
-    _ = Ric_g(gradF.toFun x, W.toFun x) x := by
+    _ = ricciTensor HasMetric.metric x (gradF.toFun x) (W.toFun x) := by
         show ricciTensor (HasMetric.metric) x (W.toFun x) (gradF.toFun x)
           = ricciTensor (HasMetric.metric) x (gradF.toFun x) (W.toFun x)
         show ricci (HasMetric.metric) WV GV x
@@ -431,7 +431,7 @@ theorem sum_hessianBilin_smoothOrthoFrame_eventuallyEq_laplacian
     (fun b => ∑ i, hessianBilin (I := I) HasMetric.metric f b
                     (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b)
                     (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b))
-      =ᶠ[𝓝 x] (Δ_g[I] f : M → ℝ) := by
+      =ᶠ[𝓝 x] (Operators.scalarLaplacian (I := I) HasMetric.metric f : M → ℝ) := by
   filter_upwards [Riemannian.Tensor.smoothOrthoFrameNbhd_mem_nhds (I := I) (M := M) x]
     with b hb
   -- At b ∈ nbhd, basis-invariance of trace of `hessianBilin f b`.
@@ -656,17 +656,17 @@ theorem sum_inner_secondCovDerivAt_grad_smoothOrthoFrame_of_inner_form
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x))
           w
-        = metricInner x (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x) w
-          + Ric_g(manifoldGradient (I := I) HasMetric.metric f x, w) x) :
+        = metricInner x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x) w
+          + ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x) w) :
     ∑ i, 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 (manifoldGradient (I := I) HasMetric.metric f x)
-            (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x)
-        + Ric_g((manifoldGradient (I := I) HasMetric.metric f x),
-                (manifoldGradient (I := I) HasMetric.metric f x)) x := by
+            (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
   classical
   -- Specialise hInner at w = ∇f x.
   have h := hInner (manifoldGradient (I := I) HasMetric.metric f x)
@@ -685,15 +685,15 @@ theorem sum_inner_secondCovDerivAt_grad_smoothOrthoFrame_of_inner_form
             (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 (Δ_g[I] f) x)
+    _ = metricInner x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)
             (manifoldGradient (I := I) HasMetric.metric f x)
-          + Ric_g(manifoldGradient (I := I) HasMetric.metric f x,
-                  manifoldGradient (I := I) HasMetric.metric f x) x := h
+          + 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)
-            (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x)
-          + Ric_g(manifoldGradient (I := I) HasMetric.metric f x,
-                  manifoldGradient (I := I) HasMetric.metric f x) x := by
-        rw [metricInner_comm x (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] 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)]
 
 end Operators
 end Riemannian
diff --git a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
index d00c796..8705dee 100644
--- a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
@@ -466,9 +466,12 @@ Hess-symmetry-on-nbhd used inside `bochner_per_summand_swap`. -/
 theorem bochner_connectionLaplacian_grad_decomposition
     [IsManifold I 2 M] [T2Space M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
-    ⟪connectionLaplacian HasMetric.metric (grad_g[I] f) x, (grad_g[I] f) x⟫_g
-      = ⟪(grad_g[I] f) x, (grad_g[I] (Δ_g[I] f)) x⟫_g
-        + Ric_g((grad_g[I] f) x, (grad_g[I] f) x) x := by
+    HasMetric.metric.metricInner x
+          (connectionLaplacian HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) 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
   classical
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
   let gradF : SmoothVectorField I M :=
@@ -509,9 +512,9 @@ theorem bochner_connectionLaplacian_grad_decomposition
         (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)
-          (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x)
-        + Ric_g((manifoldGradient (I := I) HasMetric.metric f x),
-                (manifoldGradient (I := I) HasMetric.metric f x)) 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 :
@@ -533,7 +536,7 @@ theorem bochner_connectionLaplacian_grad_decomposition
   rw [Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.mul_sum]
   -- (1) ∑ R-term = Ric(∇f, ∇f).
   have h_R_eq : (∑ i, Rterm i) =
-      Ric_g(manifoldGradient (I := I) HasMetric.metric f x, gradF.toFun x) x :=
+      ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x) (gradF.toFun x) :=
     heart_curvature_orthonormal_sum_eq_ricci (I := I) f hf gradF x
   -- (2) ∑ H-term = 0.
   have h_H_eq : (∑ i, Hterm i) = 0 :=
@@ -563,16 +566,16 @@ theorem bochner_connectionLaplacian_grad_decomposition
       (mfderiv I 𝓘(ℝ, ℝ)
           (fun b : M => ∑ i, hessianBilin (I := I) HasMetric.metric f b ((Bi i).toFun b)
             ((Bi i).toFun b)) x (gradF.toFun x) : ℝ)
-        = (mfderiv I 𝓘(ℝ, ℝ) (Δ_g[I] f : M → ℝ) x (gradF.toFun x) : ℝ) := by
+        = (mfderiv I 𝓘(ℝ, ℝ) (Operators.scalarLaplacian (I := I) HasMetric.metric f : M → ℝ) x (gradF.toFun x) : ℝ) := by
     congr 1
     exact Filter.EventuallyEq.mfderiv_eq h_eventuallyEq
   have h_grad_dual :
-      (mfderiv I 𝓘(ℝ, ℝ) (Δ_g[I] f : M → ℝ) x (gradF.toFun x) : ℝ)
-        = metricInner x (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x) (gradF.toFun x) :=
-    (manifoldGradient_inner_eq HasMetric.metric (Δ_g[I] f) x (gradF.toFun x)).symm
+      (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) :=
+    (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 (Δ_g[I] f) x)]
+      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/Operators/Divergence.lean b/OpenGALib/Riemannian/Operators/Divergence.lean
index 5077c90..1552de3 100644
--- a/OpenGALib/Riemannian/Operators/Divergence.lean
+++ b/OpenGALib/Riemannian/Operators/Divergence.lean
@@ -56,13 +56,6 @@ noncomputable def divergence
     (covDeriv g (Riemannian.Tensor.smoothOrthoFrame (I := I) g x i) X x)
     (Riemannian.Tensor.smoothOrthoFrame (I := I) g x i x)
 
-/-- **Math.** Notation `div_g[I] X` for the divergence as a function
-`M → ℝ`; `(div_g[I] X) x` is the value at `x`. The notation pipes the
-ambient `[HasMetric I M]` metric so downstream code keeps using
-`div_g[I] X` during Phase 1 (typeclass retained until #19). -/
-scoped[Riemannian] notation:max "div_g[" I "]" =>
-  Operators.divergence (I := I) HasMetric.metric
-
 /-- **Math.** The divergence of the zero vector field is zero. -/
 @[simp] theorem divergence_zero (g : RiemannianMetric I M) (x : M) :
     divergence (I := I) (M := M) g (0 : VectorFieldSection I M) x = 0 := by
diff --git a/OpenGALib/Riemannian/Operators/Gradient.lean b/OpenGALib/Riemannian/Operators/Gradient.lean
index a1a456d..a80b1b8 100644
--- a/OpenGALib/Riemannian/Operators/Gradient.lean
+++ b/OpenGALib/Riemannian/Operators/Gradient.lean
@@ -44,14 +44,6 @@ noncomputable def manifoldGradient
     (f : M → ℝ) (x : M) : TangentSpace I x :=
   g.metricRiesz x (mfderiv I 𝓘(ℝ, ℝ) f x)
 
-/-- **Math.** Notation `grad_g[I] f` for the manifold gradient section.
-`I` is bracketed because `f : M → ℝ` does not expose the model with
-corners to typeclass synthesis. The notation pipes the ambient
-`[HasMetric I M]` metric so downstream code continues to write
-`grad_g[I] f` unchanged during Phase 1 (typeclass retained until #19). -/
-scoped[Riemannian] notation:max "grad_g[" I "] " f:max =>
-  manifoldGradient (I := I) HasMetric.metric f
-
 omit [CompleteSpace E] in
 /-- **Math.** $\langle \nabla^M f(x), v \rangle_g = (\mathrm{d}f)_x(v)$. -/
 theorem manifoldGradient_inner_eq
diff --git a/OpenGALib/Riemannian/Operators/Hessian.lean b/OpenGALib/Riemannian/Operators/Hessian.lean
index 176a2c9..95ec831 100644
--- a/OpenGALib/Riemannian/Operators/Hessian.lean
+++ b/OpenGALib/Riemannian/Operators/Hessian.lean
@@ -191,13 +191,6 @@ noncomputable def hessianBilin
           = c • g.metricInner x (covDerivAt g (manifoldGradient (I := I) g f) x v) w
       rw [g.metricInner_smul_right]; rfl)
 
-/-- **Math.** Notation `hess_g[I] f` for the Hessian as a `(0,2)`-tensor
-section. `I` is bracketed because `f : M → ℝ` does not expose the model.
-For the Frobenius squared norm use `‖hess_g[I] f‖²_g`. The notation pipes
-the ambient `[HasMetric I M]` metric so downstream code keeps writing
-`hess_g[I] f` during Phase 1 (typeclass retained until #19). -/
-scoped[Riemannian] notation:max "hess_g[" I "] " f:max =>
-  Operators.hessianBilin (I := I) HasMetric.metric f
 
 /-- **Math.** $(\operatorname{trace} B(x))^2 / n \le \operatorname{frobeniusSq} B(x)$. -/
 theorem trace_sq_div_dim_le_frobeniusSq
diff --git a/OpenGALib/Riemannian/Operators/Laplacian.lean b/OpenGALib/Riemannian/Operators/Laplacian.lean
index 7cf441f..7a1934b 100644
--- a/OpenGALib/Riemannian/Operators/Laplacian.lean
+++ b/OpenGALib/Riemannian/Operators/Laplacian.lean
@@ -106,13 +106,6 @@ noncomputable def scalarLaplacian (g : RiemannianMetric I M) (f : M → ℝ) (x
     (fun (_ : M) => (e i : TangentSpace I x))
     x
 
-/-- **Math.** Notation `Δ_g[I] f` for the scalar Laplacian
-$\mathrm{tr}_g(\mathrm{Hess}\,f)$. `I` bracketed since `f : M → ℝ` hides
-the model with corners. The notation pipes the ambient `[HasMetric I M]`
-metric so downstream code keeps using `Δ_g[I] f` during Phase 1
-(typeclass retained until #19). -/
-scoped[Riemannian] notation:max "Δ_g[" I "] " f:max =>
-  Operators.scalarLaplacian (I := I) HasMetric.metric f
 
 /-- **Math.** **Scalar Laplacian as Bilin-trace of the Hessian section.**
 Both unfold to $\sum_i \langle \nabla_{\varepsilon_i} \nabla f,\,
diff --git a/OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean b/OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean
index 83d7d7a..a7c0905 100644
--- a/OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean
+++ b/OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean
@@ -85,8 +85,4 @@ noncomputable def meanCurvature
     (fun (_ : M) => (e i : TangentSpace I x))
     (fun (_ : M) => (e i : TangentSpace I x)) x
 
-/-- **Math.** Notation `H_g[I] ν` for the mean curvature of a hypersurface
-oriented by unit normal `ν`. -/
-scoped[Riemannian] notation:max "H_g[" I "]" => meanCurvature (I := I) HasMetric.metric
-
 end Riemannian
diff --git a/OpenGALib/Riemannian/Util/MetricNotation.lean b/OpenGALib/Riemannian/Util/MetricNotation.lean
index 735d8c1..307904d 100644
--- a/OpenGALib/Riemannian/Util/MetricNotation.lean
+++ b/OpenGALib/Riemannian/Util/MetricNotation.lean
@@ -19,11 +19,6 @@ class MetricNormSq (V : Type*) (R : outParam Type*) where
   /-- The squared norm `‖·‖²_g`. -/
   normSqG : V → R
 
-/-- **Eng.** Polymorphic inner product typeclass dispatch. -/
-class MetricInnerHom (V W : Type*) (R : outParam Type*) where
-  /-- The inner product `⟪·, ·⟫_g`. -/
-  innerG : V → W → R
-
 section MetricNotationInstances
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
@@ -42,24 +37,8 @@ noncomputable instance instMetricNormSqSection :
     MetricNormSq ((y : M) → TangentSpace I y) (M → ℝ) where
   normSqG V := fun y => HasMetric.metric.metricInner y (V y) (V y)
 
-/-- **Math.** Pointwise tangent-vector inner product $\langle V, W\rangle_g$. -/
-noncomputable instance instMetricInnerHomTangent (x : M) :
-    MetricInnerHom (TangentSpace I x) (TangentSpace I x) ℝ where
-  innerG v w := HasMetric.metric.metricInner x v w
-
-/-- **Math.** Section-level inner product: pair of vector fields ↦ scalar function
-`y ↦ ⟨V(y), W(y)⟩_g`. -/
-noncomputable instance instMetricInnerHomSection :
-    MetricInnerHom ((y : M) → TangentSpace I y) ((y : M) → TangentSpace I y)
-      (M → ℝ) where
-  innerG V W := fun y => HasMetric.metric.metricInner y (V y) (W y)
-
 end MetricNotationInstances
 
-/-- **Math.** Notation `⟪V, W⟫_g` for the metric inner product. Pointwise on tangent vectors → `ℝ`;
-on two sections → `M → ℝ`. -/
-scoped notation:max "⟪" V ", " W "⟫_g" => MetricInnerHom.innerG V W
-
 /-- **Math.** Notation `‖V‖²_g` for the squared norm. Pointwise on a tangent vector → `ℝ`;
 on a section → `M → ℝ`. -/
 scoped notation:max "‖" V "‖²_g" => MetricNormSq.normSqG V