From a25b541d5e812d29569074d36cdae6860925a654 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 16:49:54 -0400
Subject: [PATCH 1/4] 9g: drop Riem(X, Y) Z notation, inline as
 riemannCurvature HasMetric.metric X Y Z

---
 .../Riemannian/Connection/LeviCivita.lean     | 16 ++---
 .../Curvature/RiemannCurvature.lean           | 64 +++++++++----------
 2 files changed, 37 insertions(+), 43 deletions(-)

diff --git a/OpenGALib/Riemannian/Connection/LeviCivita.lean b/OpenGALib/Riemannian/Connection/LeviCivita.lean
index a42fc2f..7880379 100644
--- a/OpenGALib/Riemannian/Connection/LeviCivita.lean
+++ b/OpenGALib/Riemannian/Connection/LeviCivita.lean
@@ -660,12 +660,6 @@ noncomputable def riemannCurvature
   covDeriv g X (covDeriv g Y Z) x - covDeriv g Y (covDeriv g X Z) x
     - covDeriv g (mlieBracket I X Y) Z x
 
-/-- **Math.** Notation `Riem(X, Y) Z` for `riemannCurvature (HasMetric.metric) X Y Z`.
-The notation pipes the ambient `[HasMetric I M]` metric so downstream code
-continues to write `Riem(X, Y) Z` unchanged during Phase 1. -/
-scoped[Riemannian] notation:max "Riem(" X ", " Y ") " Z:max =>
-  riemannCurvature (HasMetric.metric) X Y Z
-
 /-! ### `riem_simp` lemmas
 
 Two rewrites that drive the `riem_simp` simp set, populated for the
@@ -703,7 +697,7 @@ theorem covDeriv_mlieBracket_swap_apply
       ((leviCivitaConnection (I := I) (M := M) g).toFun Z x).map_neg]
 
 -- riemannCurvature_antisymm lives in Curvature.lean: its statement
--- uses the post-Bianchi `Riem(X, Y) Z` notation, so it must be in a
+-- uses the post-Bianchi `riemannCurvature HasMetric.metric X Y Z` notation, so it must be in a
 -- file that imports `Util/Notation/Curvature`.
 
 /-! ## Algebraic Bianchi I
@@ -920,10 +914,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 :=
-  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
+  covDeriv HasMetric.metric X.toFun (riemannCurvature HasMetric.metric Y Z W) x
+    - riemannCurvature HasMetric.metric (covDeriv HasMetric.metric X Y) Z.toFun W.toFun x
+    - riemannCurvature HasMetric.metric Y.toFun (covDeriv HasMetric.metric X Z) W.toFun x
+    - riemannCurvature HasMetric.metric Y.toFun Z.toFun (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/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
index b9cab59..9282484 100644
--- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
+++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
@@ -3,7 +3,7 @@ import OpenGALib.Riemannian.Connection.LeviCivita
 import OpenGALib.Riemannian.TangentBundle.TangentSmooth
 import OpenGALib.Riemannian.Operators.HessianLie
 import OpenGALib.Riemannian.Util.MetricInnerSmoothness
--- `Riem(X, Y) Z` notation is now defined inline in `Connection.lean`
+-- `riemannCurvature HasMetric.metric 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
@@ -583,8 +583,8 @@ theorem riemannCurvature_metric_skew
     [IsManifold I 2 M]
     (X Y Z W : SmoothVectorField I M) (x : M)
     (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) :
-    metricInner x (Riem(X.toFun, Y.toFun) Z.toFun x) (W x)
-      + metricInner x (Riem(X.toFun, Y.toFun) W.toFun x) (Z x) = 0 := by
+    metricInner x (riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x) (W x)
+      + metricInner x (riemannCurvature HasMetric.metric X.toFun Y.toFun W.toFun x) (Z x) = 0 := by
   -- Diagonal-zero applied to U = Z+W, Z, W.
   have h_ZW := riemannCurvature_inner_self_zero HasMetric.metric X Y (Z + W) x h_interior
   have h_Z := riemannCurvature_inner_self_zero HasMetric.metric X Y Z x h_interior
@@ -614,21 +614,21 @@ Reference: do Carmo §4 Proposition 2.5 (iv); Petersen Ch. 3. -/
 theorem riemannCurvature_pair_symm
     [IsManifold I 2 M]
     (X Y Z W : SmoothVectorField I M) (x : M) :
-    metricInner x (Riem(X, Y) Z x) (W x)
-      = metricInner x (Riem(Z, W) X x) (Y x) := by
+    metricInner x (riemannCurvature HasMetric.metric X Y Z x) (W x)
+      = metricInner x (riemannCurvature HasMetric.metric Z W X x) (Y x) := by
   -- Strict-interior hypothesis used by `riemannCurvature_metric_skew`.
   have h_interior : extChartAt I x x ∈ closure (interior (Set.range I)) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
     exact Set.mem_univ _
   -- Four cyclic Bianchi I instances, paired with the respective 4th vector.
   have bianchi_inner : ∀ (A B C D : SmoothVectorField I M),
-      metricInner x (Riem(A, B) C x) (D x)
-        + metricInner x (Riem(B, C) A x) (D x)
-        + metricInner x (Riem(C, A) B x) (D x) = 0 := by
+      metricInner x (riemannCurvature HasMetric.metric A B C x) (D x)
+        + metricInner x (riemannCurvature HasMetric.metric B C A x) (D x)
+        + metricInner x (riemannCurvature HasMetric.metric C A B x) (D x) = 0 := by
     intro A B C D
     have h := bianchi_first HasMetric.metric A B C x
     have : metricInner x
-              (Riem(A, B) C x + Riem(B, C) A x + Riem(C, A) B x) (D x)
+              (riemannCurvature HasMetric.metric A B C x + riemannCurvature HasMetric.metric B C A x + riemannCurvature HasMetric.metric C A B x) (D x)
             = metricInner x (0 : TangentSpace I x) (D x) := by rw [h]
     rw [metricInner_add_left, metricInner_add_left] at this
     -- `metricInner x 0 (D x) = 0`.
@@ -643,14 +643,14 @@ theorem riemannCurvature_pair_symm
   have b4 := bianchi_inner W X Y Z
   -- (1,2)-antisymmetry, scalar form via metricInner congrArg.
   have antisym12 : ∀ (A B C D : SmoothVectorField I M),
-      metricInner x (Riem(A, B) C x) (D x)
-        = -metricInner x (Riem(B, A) C x) (D x) := by
+      metricInner x (riemannCurvature HasMetric.metric A B C x) (D x)
+        = -metricInner x (riemannCurvature HasMetric.metric B A C x) (D x) := by
     intro A B C D
     rw [riemannCurvature_antisymm HasMetric.metric A B C x, metricInner_neg_left]
   -- (3,4)-antisymmetry from `riemannCurvature_metric_skew`.
   have antisym34 : ∀ (A B C D : SmoothVectorField I M),
-      metricInner x (Riem(A, B) C x) (D x)
-        = -metricInner x (Riem(A, B) D x) (C x) := by
+      metricInner x (riemannCurvature HasMetric.metric A B C x) (D x)
+        = -metricInner x (riemannCurvature HasMetric.metric A B D x) (C x) := by
     intro A B C D
     have h := riemannCurvature_metric_skew A B C D x h_interior
     linarith
@@ -786,7 +786,7 @@ already consume the metric through the typeclass. -/
 /-- **Math.** The ambient Riemannian metric is **flat** if its Riemann
 curvature tensor vanishes pointwise. -/
 def IsFlat : Prop :=
-  ∀ (X Y Z : VectorFieldSection I M) (x : M), Riem(X, Y) Z x = 0
+  ∀ (X Y Z : VectorFieldSection I M) (x : M), riemannCurvature HasMetric.metric X Y Z x = 0
 
 /-! ## Killing vector fields -/
 
@@ -921,7 +921,7 @@ private lemma second_covDeriv_commutator
         - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric U.toFun V.toFun y) X.toFun x)
       - (covDeriv HasMetric.metric V.toFun (fun y => covDeriv HasMetric.metric U.toFun X.toFun y) x
         - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric V.toFun U.toFun y) X.toFun x)
-      = Riem(U, V) X x := by
+      = riemannCurvature HasMetric.metric U V X x := by
   rw [riemannCurvature_commutator_form]
   have h_torsion := covDeriv_sub_swap_eq_mlieBracket HasMetric.metric U.toFun V.toFun x
     (U.smoothAt x) (V.smoothAt x)
@@ -942,7 +942,7 @@ of constant-sectional-curvature manifolds.
 
 With OpenGA's convention
 `Riem(U,V)X = ∇_U∇_V X - ∇_V∇_U X - ∇_[U,V] X`, the right-hand side is
-`Riem(Y, X) Z`, equivalently `-Riem(X, Y) Z`.
+`riemannCurvature HasMetric.metric Y X Z`, equivalently `-riemannCurvature HasMetric.metric X Y Z`.
 
 Reference: do Carmo, *Riemannian Geometry*, §3 Ex. 5; Petersen, Ch. 8 §2;
 Cheeger–Ebin §1.84. -/
@@ -951,7 +951,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
     (Y Z : SmoothVectorField I M) (x : M) :
     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
+      = riemannCurvature HasMetric.metric Y X Z x := by
   classical
   apply (metricInner_eq_iff_eq x _ _).mp
   intro w
@@ -961,7 +961,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
       (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric V.toFun X.toFun y) x
         - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric U.toFun V.toFun y) X.toFun x) (W x)
   let C (U V W : SmoothVectorField I M) : ℝ :=
-    metricInner x (Riem(U, V) X x) (W x)
+    metricInner x (riemannCurvature HasMetric.metric U V X x) (W x)
   have h_skew_Y : A Y Z W + A Y W Z = 0 := by
     simpa [A] using IsKilling.second_covDeriv_inner_skew X hX Y Z W x
   have h_skew_Z : A Z W Y + A Z Y W = 0 := by
@@ -976,7 +976,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) X.toFun x)
           - (covDeriv HasMetric.metric Z.toFun (fun y => covDeriv HasMetric.metric Y.toFun X.toFun y) x
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric Z.toFun Y.toFun y) X.toFun x)) (W x)
-        = metricInner x (Riem(Y, Z) X x) (W x) at h
+        = metricInner x (riemannCurvature HasMetric.metric Y Z X x) (W x) at h
     rw [metricInner_sub_left] at h
     simpa [A, C] using h
   have h_comm_ZW : A Z W Y - A W Z Y = C Z W Y := by
@@ -987,7 +987,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric Z.toFun W.toFun y) X.toFun x)
           - (covDeriv HasMetric.metric W.toFun (fun y => covDeriv HasMetric.metric Z.toFun X.toFun y) x
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric W.toFun Z.toFun y) X.toFun x)) (Y x)
-        = metricInner x (Riem(Z, W) X x) (Y x) at h
+        = metricInner x (riemannCurvature HasMetric.metric Z W X x) (Y x) at h
     rw [metricInner_sub_left] at h
     simpa [A, C] using h
   have h_comm_WY : A W Y Z - A Y W Z = C W Y Z := by
@@ -998,31 +998,31 @@ theorem IsKilling.second_covDeriv_eq_curvature
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric W.toFun Y.toFun y) X.toFun x)
           - (covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric W.toFun X.toFun y) x
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric Y.toFun W.toFun y) X.toFun x)) (Z x)
-        = metricInner x (Riem(W, Y) X x) (Z x) at h
+        = metricInner x (riemannCurvature HasMetric.metric W Y X x) (Z x) at h
     rw [metricInner_sub_left] at h
     simpa [A, C] using h
   have h_curv : C Y Z W - C Z W Y + C W Y Z
-      = 2 * metricInner x (Riem(Y, X) Z x) (W x) := by
+      = 2 * metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
     have h_bianchi := bianchi_first HasMetric.metric X W Y x
     have h_inner :
-        metricInner x (Riem(X, W) Y x + Riem(W, Y) X x + Riem(Y, X) W x) (Z x)
+        metricInner x (riemannCurvature HasMetric.metric X W Y x + riemannCurvature HasMetric.metric W Y X x + riemannCurvature HasMetric.metric Y X W x) (Z x)
           = 0 := by
       rw [h_bianchi]
       exact metricInner_zero_left x (Z x)
     rw [metricInner_add_left, metricInner_add_left] at h_inner
-    have h_pair₁ : C Y Z W = metricInner x (Riem(X, W) Y x) (Z x) := by
+    have h_pair₁ : C Y Z W = metricInner x (riemannCurvature HasMetric.metric X W Y x) (Z x) := by
       simpa [C] using riemannCurvature_pair_symm Y Z X W x
-    have h_pair₂ : C Z W Y = metricInner x (Riem(X, Y) Z x) (W x) := by
+    have h_pair₂ : C Z W Y = metricInner x (riemannCurvature HasMetric.metric X Y Z x) (W x) := by
       simpa [C] using riemannCurvature_pair_symm Z W X Y x
-    have h_pair₃ : C W Y Z = metricInner x (Riem(X, Z) W x) (Y x) := by
+    have h_pair₃ : C W Y Z = metricInner x (riemannCurvature HasMetric.metric X Z W x) (Y x) := by
       simpa [C] using riemannCurvature_pair_symm W Y X Z x
     have h_antisym12 :
-        metricInner x (Riem(X, Y) Z x) (W x)
-          = -metricInner x (Riem(Y, X) Z x) (W x) := by
+        metricInner x (riemannCurvature HasMetric.metric X Y Z x) (W x)
+          = -metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
       rw [riemannCurvature_antisymm HasMetric.metric X.toFun Y.toFun Z.toFun x, metricInner_neg_left]
     have h_antisym34 :
-        metricInner x (Riem(Y, X) W x) (Z x)
-          = -metricInner x (Riem(Y, X) Z x) (W x) := by
+        metricInner x (riemannCurvature HasMetric.metric Y X W x) (Z x)
+          = -metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
       have h := riemannCurvature_metric_skew Y X W Z x (by
         rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
         exact Set.mem_univ _)
@@ -1031,7 +1031,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
     linarith [h_inner, h_antisym12, h_antisym34]
   have h_A : 2 * A Y Z W = C Y Z W - C Z W Y + C W Y Z := by
     linarith [h_skew_Y, h_skew_Z, h_skew_W, h_comm_YZ, h_comm_ZW, h_comm_WY]
-  have h_target : A Y Z W = metricInner x (Riem(Y, X) Z x) (W x) := by
+  have h_target : A Y Z W = metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
     linarith [h_A, h_curv]
   simpa [A, hW_def] using h_target
 
@@ -1058,7 +1058,7 @@ independent (denominator non-zero). At linearly dependent inputs, the
 formula returns the junk value $0$ via division by zero. -/
 noncomputable def sectionalCurvature
     (X Y : VectorFieldSection I M) (x : M) : ℝ :=
-  metricInner x (Riem(X, Y) Y x) (X x) /
+  metricInner x (riemannCurvature HasMetric.metric X Y Y x) (X x) /
     (metricInner x (X x) (X x) * metricInner x (Y x) (Y x)
       - metricInner x (X x) (Y x) ^ 2)
 

From ac6aae7d2c3dd1b8b0444d98b040cbb8a470df87 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 16:54:01 -0400
Subject: [PATCH 2/4] =?UTF-8?q?9g:=20drop=20=E2=80=96V=E2=80=96=C2=B2=5Fg?=
 =?UTF-8?q?=20notation=20+=20MetricNormSq=20class=20+=203=20instances=20+?=
 =?UTF-8?q?=20Bilin=20instance?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 OpenGALib/Riemannian/Operators/Bochner.lean   | 20 ++++----
 OpenGALib/Riemannian/Operators/Hessian.lean   |  7 ---
 OpenGALib/Riemannian/Util/MetricNotation.lean | 51 ++++---------------
 3 files changed, 19 insertions(+), 59 deletions(-)

diff --git a/OpenGALib/Riemannian/Operators/Bochner.lean b/OpenGALib/Riemannian/Operators/Bochner.lean
index 04c3bbb..34eec55 100644
--- a/OpenGALib/Riemannian/Operators/Bochner.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner.lean
@@ -56,14 +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 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x
+    (1 / 2 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y)))) 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
+        + frobeniusSq (I := I) (M := M) (Operators.hessianBilin (I := I) HasMetric.metric f) 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 (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x
+  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
           (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
           (manifoldGradient (I := I) HasMetric.metric f x)
@@ -75,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 (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x
-        = ∑ i, hessian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)
+      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
+        = ∑ i, 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 := by
     rw [scalarLaplacian_eq_laplacian_hessianBilin HasMetric.metric]
     show laplacian (I := I) (M := M)
-        (hessianBilin (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x = _
+        (hessianBilin (I := I) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y)))) x = _
     unfold laplacian
     rw [trace_def]
     rw [← Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x
-          (hessianBilin (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x)]
+          (hessianBilin (I := I) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y))) 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 (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)
+      (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
             (secondCovDerivSection (I := I) (M := M) HasMetric.metric
@@ -241,8 +241,8 @@ 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 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x =
-      ‖Operators.hessianBilin (I := I) HasMetric.metric f‖²_g x
+    (1 / 2 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y)))) x =
+      frobeniusSq (I := I) (M := M) (Operators.hessianBilin (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
diff --git a/OpenGALib/Riemannian/Operators/Hessian.lean b/OpenGALib/Riemannian/Operators/Hessian.lean
index 95ec831..ed9cf33 100644
--- a/OpenGALib/Riemannian/Operators/Hessian.lean
+++ b/OpenGALib/Riemannian/Operators/Hessian.lean
@@ -396,11 +396,4 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [T2Space M]
   [HasMetric I M]
 
-/-- **Math.** Frobenius squared norm on `(0,2)`-tensor sections, w.r.t. a $g$-orthonormal
-frame: `‖B‖²_g x = ∑_{ij} B(x)(εᵢ, εⱼ)²` where $\{\varepsilon_i\}$ is the
-`stdOrthonormalBasis` of $T_x M$ (geometric Hilbert-Schmidt norm). -/
-noncomputable instance instMetricNormSqBilin :
-    MetricNormSq (Riemannian.Operators.Bilin (M := M) I) (M → ℝ) where
-  normSqG B := fun x => Riemannian.Operators.frobeniusSq (I := I) (M := M) B x
-
 end Riemannian
diff --git a/OpenGALib/Riemannian/Util/MetricNotation.lean b/OpenGALib/Riemannian/Util/MetricNotation.lean
index 307904d..bae1a07 100644
--- a/OpenGALib/Riemannian/Util/MetricNotation.lean
+++ b/OpenGALib/Riemannian/Util/MetricNotation.lean
@@ -1,46 +1,13 @@
 import OpenGALib.Riemannian.Metric.RiemannianMetric
 
 /-!
-# Polymorphic metric notation — `⟪·, ·⟫_g` and `‖·‖²_g`
-
-Engineering typeclass dispatch for the metric inner product and squared
-norm notations so the same syntax works on tangent vectors (yielding `ℝ`)
-and on tangent-bundle sections / vector fields (yielding `M → ℝ`).
-
-Reference: do Carmo 1992 §1.2 (inner product).
+# (Stub) Polymorphic metric notation file
+
+Previously hosted `⟪·, ·⟫_g` and `‖·‖²_g` polymorphic dispatch notations
+together with their `MetricInnerHom` / `MetricNormSq` typeclass plumbing.
+Both notations and their dispatch classes have been dropped in favor of
+explicit `g.metricInner` / `frobeniusSq` / Pi-form expansions, in line with
+the explicit-`g` cascade (umbrella #9). The file is retained as an import
+stub for now to avoid breaking the import graph; it can be deleted once
+all imports of `OpenGALib.Riemannian.Util.MetricNotation` are removed.
 -/
-
-open scoped ContDiff Manifold
-
-namespace Riemannian
-
-/-- **Eng.** Polymorphic squared norm typeclass dispatch. -/
-class MetricNormSq (V : Type*) (R : outParam Type*) where
-  /-- The squared norm `‖·‖²_g`. -/
-  normSqG : V → R
-
-section MetricNotationInstances
-
-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]
-  [HasMetric I M]
-
-/-- **Math.** Pointwise tangent-vector squared norm $\|V\|^2_g$. -/
-noncomputable instance instMetricNormSqTangent (x : M) :
-    MetricNormSq (TangentSpace I x) ℝ where
-  normSqG v := HasMetric.metric.metricInner x v v
-
-/-- **Math.** Section-level squared norm: vector field `V` ↦ scalar function
-`y ↦ ⟨V(y), V(y)⟩_g`. -/
-noncomputable instance instMetricNormSqSection :
-    MetricNormSq ((y : M) → TangentSpace I y) (M → ℝ) where
-  normSqG V := fun y => HasMetric.metric.metricInner y (V y) (V y)
-
-end MetricNotationInstances
-
-/-- **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
-
-end Riemannian

From a0c52335d4cb08315dddd6a76382aef87a4dd68c Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 16:56:48 -0400
Subject: [PATCH 3/4] =?UTF-8?q?9g:=20drop=20II(X,=20Y)=20and=20(=E2=88=87R?=
 =?UTF-8?q?)[X](Y,=20Z)=20W=20notations?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 OpenGALib/Riemannian/Connection/LeviCivita.lean           | 5 +----
 OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean | 7 -------
 2 files changed, 1 insertion(+), 11 deletions(-)

diff --git a/OpenGALib/Riemannian/Connection/LeviCivita.lean b/OpenGALib/Riemannian/Connection/LeviCivita.lean
index 7880379..db2527b 100644
--- a/OpenGALib/Riemannian/Connection/LeviCivita.lean
+++ b/OpenGALib/Riemannian/Connection/LeviCivita.lean
@@ -919,9 +919,6 @@ noncomputable def covDerivRiemann
     - riemannCurvature HasMetric.metric Y.toFun (covDeriv HasMetric.metric X Z) W.toFun x
     - riemannCurvature HasMetric.metric Y.toFun Z.toFun (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 =>
-  covDerivRiemann X Y Z W
 
 /-- **Math.** **Second (differential) Bianchi identity** for the
 Levi-Civita connection:
@@ -942,7 +939,7 @@ Estimated 80-120 LOC; repair tracked separately. -/
 theorem bianchi_second
     [IsManifold I 3 M]
     (X Y Z W : SmoothVectorField I M) (x : M) :
-    (∇R)[X](Y, Z) W x + (∇R)[Y](Z, X) W x + (∇R)[Z](X, Y) W x = 0 := by
+    covDerivRiemann X Y Z W x + covDerivRiemann Y Z X W x + covDerivRiemann Z X Y W x = 0 := by
   sorry
 
 end Riemannian
diff --git a/OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean b/OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean
index a7c0905..ff59181 100644
--- a/OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean
+++ b/OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean
@@ -46,13 +46,6 @@ noncomputable def secondFundamentalFormScalar
     (ν X Y : VectorFieldSection I M) (x : M) : ℝ :=
   g.metricInner x (covDeriv g X Y x) (ν x)
 
-/-- **Math.** Notation `II(X, Y)` for the codim-1 second fundamental form
-scalar, with the unit normal `ν` from context. The notation pipes the
-ambient `[HasMetric I M]` metric so downstream code keeps using
-`II(X, Y)` during Phase 1 (typeclass retained until #19). -/
-scoped[Riemannian] notation:max "II(" X ", " Y ")" =>
-  secondFundamentalFormScalar HasMetric.metric X Y
-
 set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** $|A|^2(x) = \sum_{i,j} A(e_i, e_j)^2$ over the standard
 orthonormal basis of `TangentSpace I x`. Basis-independent for

From 85d17b5a7a006fb093ace7914d89c23db2bf69e7 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 16:57:32 -0400
Subject: [PATCH 4/4] 9g: update Util/Notation.lean docstring (drop references
 to removed _g notations)

---
 OpenGALib/Util/Notation.lean | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/OpenGALib/Util/Notation.lean b/OpenGALib/Util/Notation.lean
index d243d7b..3977d86 100644
--- a/OpenGALib/Util/Notation.lean
+++ b/OpenGALib/Util/Notation.lean
@@ -17,14 +17,16 @@ import OpenGALib.Util.Notation
 open scoped Riemannian
 ```
 
-Notation summary (each definition file has the canonical comment):
+Remaining scoped notation:
 
-  * `∇[X] Y`, `⟦X, Y⟧`, `Riem(X, Y) Z`         — connection / curvature
-  * `⟪V, W⟫_g`, `‖V‖²_g`                       — polymorphic inner / sq norm
-  * `Ric(X, Y)`, `Ric_g(v, w) x`, `scal_g[I]`  — Ricci, scalar curvature
-  * `II(X, Y)`, `H_g[I]`                       — second fundamental form, mean curvature
-  * `grad_g[I] f`, `Δ_g[I] f`, `hess_g[I] f`   — gradient, Laplacian, Hessian
+  * `⟦X, Y⟧`  — manifold Lie bracket `VectorField.mlieBracket _ X Y`
+    (metric-independent; kept post-9g)
 
-Bracketed `[I]` is required where bare `M` does not expose the model with
-corners to typeclass synthesis.
+Previously hosted typeclass-dispatched `_g` notations
+(`∇[X] Y`, `Riem(X, Y) Z`, `Ric(X, Y)`, `Ric_g`, `scal_g[I]`, `II(X, Y)`,
+`H_g[I]`, `grad_g[I] f`, `Δ_g[I] f`, `hess_g[I] f`, `K_g[I](X, Y)`,
+`(∇R)[X](Y, Z) W`, `⟪V, W⟫_g`, `‖V‖²_g`) were dropped in 9g
+(umbrella #9) in favor of explicit `HasMetric.metric`/`g` forms, so that
+multiple metrics (Ricci flow, conformal change, comparison geometry)
+can coexist on the same manifold.
 -/