From 9608505d0755786a59ce4f491346480811bd9dc0 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 17:07:47 -0400
Subject: [PATCH 1/6] 9h: lift riemannCurvature_metric_skew / _pair_symm /
 sectionalCurvature(At) / _symmetric to explicit g

---
 .../Curvature/RiemannCurvature.lean           | 97 ++++++++-----------
 1 file changed, 42 insertions(+), 55 deletions(-)

diff --git a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
index 9282484..ac3bf08 100644
--- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
+++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
@@ -581,22 +581,18 @@ $$0 = \langle R(X, Y)(Z + W), Z + W\rangle_g
 Reference: do Carmo §4 Proposition 2.5(iv). -/
 theorem riemannCurvature_metric_skew
     [IsManifold I 2 M]
+    (g : RiemannianMetric I M)
     (X Y Z W : SmoothVectorField I M) (x : M)
     (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) :
-    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
-  have h_W := riemannCurvature_inner_self_zero HasMetric.metric X Y W x h_interior
-  -- Additivity of R in 3rd slot.
-  have h_add := riemannCurvature_add_third HasMetric.metric X Y Z W x
-  -- (Z+W) x = Z x + W x.
+    g.metricInner x (riemannCurvature g X.toFun Y.toFun Z.toFun x) (W x)
+      + g.metricInner x (riemannCurvature g X.toFun Y.toFun W.toFun x) (Z x) = 0 := by
+  have h_ZW := riemannCurvature_inner_self_zero g X Y (Z + W) x h_interior
+  have h_Z := riemannCurvature_inner_self_zero g X Y Z x h_interior
+  have h_W := riemannCurvature_inner_self_zero g X Y W x h_interior
+  have h_add := riemannCurvature_add_third g X Y Z W x
   have h_ZW_x : (Z + W) x = Z x + W x := rfl
-  -- Expand h_ZW via h_add and h_ZW_x and bilinearity of metricInner.
-  rw [h_add, h_ZW_x, HasMetric.metric.metricInner_add_left, HasMetric.metric.metricInner_add_right,
-      HasMetric.metric.metricInner_add_right] at h_ZW
-  -- h_ZW : g(R Z, Z) + g(R Z, W) + (g(R W, Z) + g(R W, W)) = 0
+  rw [h_add, h_ZW_x, g.metricInner_add_left, g.metricInner_add_right,
+      g.metricInner_add_right] at h_ZW
   linarith
 
 /-! ### Pair symmetry: $g(R(X,Y)Z, W) = g(R(Z,W)X, Y)$
@@ -613,46 +609,39 @@ $$g_x(R(X,Y)Z, W) \;=\; g_x(R(Z,W)X, Y).$$
 Reference: do Carmo §4 Proposition 2.5 (iv); Petersen Ch. 3. -/
 theorem riemannCurvature_pair_symm
     [IsManifold I 2 M]
+    (g : RiemannianMetric I M)
     (X Y Z W : SmoothVectorField I M) (x : M) :
-    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`.
+    g.metricInner x (riemannCurvature g X Y Z x) (W x)
+      = g.metricInner x (riemannCurvature g Z W X x) (Y x) := by
   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 (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
+      g.metricInner x (riemannCurvature g A B C x) (D x)
+        + g.metricInner x (riemannCurvature g B C A x) (D x)
+        + g.metricInner x (riemannCurvature g 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
-              (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`.
-    have h_zero : metricInner x (0 : TangentSpace I x) (D x) = 0 := by
-      show ⟪(0 : TangentSpace I x), D x⟫_ℝ = 0
-      exact inner_zero_left _
-    rw [h_zero] at this
+    have h := bianchi_first g A B C x
+    have : g.metricInner x
+              (riemannCurvature g A B C x + riemannCurvature g B C A x + riemannCurvature g C A B x) (D x)
+            = g.metricInner x (0 : TangentSpace I x) (D x) := by rw [h]
+    rw [g.metricInner_add_left, g.metricInner_add_left] at this
+    rw [g.metricInner_zero_left] at this
     linarith
   have b1 := bianchi_inner X Y Z W
   have b2 := bianchi_inner Y Z W X
   have b3 := bianchi_inner Z W X Y
   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 (riemannCurvature HasMetric.metric A B C x) (D x)
-        = -metricInner x (riemannCurvature HasMetric.metric B A C x) (D x) := by
+      g.metricInner x (riemannCurvature g A B C x) (D x)
+        = -g.metricInner x (riemannCurvature g 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`.
+    rw [riemannCurvature_antisymm g A B C x, g.metricInner_neg_left]
   have antisym34 : ∀ (A B C D : SmoothVectorField I M),
-      metricInner x (riemannCurvature HasMetric.metric A B C x) (D x)
-        = -metricInner x (riemannCurvature HasMetric.metric A B D x) (C x) := by
+      g.metricInner x (riemannCurvature g A B C x) (D x)
+        = -g.metricInner x (riemannCurvature g A B D x) (C x) := by
     intro A B C D
-    have h := riemannCurvature_metric_skew A B C D x h_interior
+    have h := riemannCurvature_metric_skew g A B C D x h_interior
     linarith
   -- Combine: sum of b1..b4 with the antisymmetries gives 2·σ(X,Y,Z,W) - 2·σ(Z,W,X,Y) = 0.
   -- Specialise antisym to the 12 σ-instances appearing in b1..b4 and feed to linarith.
@@ -1011,11 +1000,11 @@ theorem IsKilling.second_covDeriv_eq_curvature
       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 (riemannCurvature HasMetric.metric X W Y x) (Z x) := by
-      simpa [C] using riemannCurvature_pair_symm Y Z X W x
+      simpa [C] using riemannCurvature_pair_symm HasMetric.metric Y Z X W x
     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
+      simpa [C] using riemannCurvature_pair_symm HasMetric.metric Z W X Y x
     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
+      simpa [C] using riemannCurvature_pair_symm HasMetric.metric W Y X Z x
     have h_antisym12 :
         metricInner x (riemannCurvature HasMetric.metric X Y Z x) (W x)
           = -metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
@@ -1023,7 +1012,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
     have h_antisym34 :
         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
+      have h := riemannCurvature_metric_skew HasMetric.metric Y X W Z x (by
         rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
         exact Set.mem_univ _)
       linarith
@@ -1057,10 +1046,11 @@ parallelogram); $K$ is well-defined when the two vectors are linearly
 independent (denominator non-zero). At linearly dependent inputs, the
 formula returns the junk value $0$ via division by zero. -/
 noncomputable def sectionalCurvature
+    (g : RiemannianMetric I M)
     (X Y : VectorFieldSection I M) (x : M) : ℝ :=
-  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)
+  g.metricInner x (riemannCurvature g X Y Y x) (X x) /
+    (g.metricInner x (X x) (X x) * g.metricInner x (Y x) (Y x)
+      - g.metricInner x (X x) (Y x) ^ 2)
 
 /-- **Math.** **Tangent-vector form** of sectional curvature: same
 formula as `sectionalCurvature` but consuming the pointwise tangent
@@ -1070,8 +1060,9 @@ on vector fields. By $C^\infty(M)$-tensoriality of `riemannCurvature HasMetric.m
 the value depends only on $X(x), Y(x)$, so this is the canonical
 pointwise function. -/
 noncomputable def sectionalCurvatureAt
+    (g : RiemannianMetric I M)
     (x : M) (v w : TangentSpace I x) : ℝ :=
-  sectionalCurvature (I := I) (M := M)
+  sectionalCurvature (I := I) (M := M) g
     (fun _ : M => v) (fun _ : M => w) x
 
 /-- **Math.** **Sectional curvature is symmetric in $X, Y$**:
@@ -1083,19 +1074,15 @@ using `riemannCurvature_antisymm` once in each slot.
 Denominator: symmetric in $X, Y$ via `metricInner_comm`. -/
 theorem sectionalCurvature_symmetric
     [IsManifold I 2 M]
+    (g : RiemannianMetric I M)
     (X Y : SmoothVectorField I M) (x : M) :
-    sectionalCurvature (I := I) X Y x = sectionalCurvature (I := I) Y X x := by
+    sectionalCurvature (I := I) g X Y x = sectionalCurvature (I := I) g 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.
-    -- pair-symm: g(R(X,Y) Y, X) = g(R(Y,X) X, Y) by swapping (1,2) ↔ (3,4) slots and
-    -- using R(Y,X) = -R(X,Y), with the Y, X swap on slot 3,4.
-    have h_pair := riemannCurvature_pair_symm X Y Y X x
-    -- h_pair : g(R(X,Y) Y, X) = g(R(Y,X) X, Y).
+  · have h_pair := riemannCurvature_pair_symm g X Y Y X x
     exact h_pair
-  · -- Denominator: g(X,X) g(Y,Y) - g(X,Y)^2 = g(Y,Y) g(X,X) - g(Y,X)^2.
-    have hXY : metricInner x (X x) (Y x) = metricInner x (Y x) (X x) :=
-      metricInner_comm x _ _
+  · have hXY : g.metricInner x (X x) (Y x) = g.metricInner x (Y x) (X x) :=
+      g.metricInner_comm x _ _
     rw [hXY]; ring
 
 end Riemannian

From 21a7a1057ca45b78b9a15cab037b312e085a9309 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 17:10:49 -0400
Subject: [PATCH 2/6] =?UTF-8?q?9h:=20lift=20IsFlat=20predicate=20to=20expl?=
 =?UTF-8?q?icit=20g=20(IsKilling=20kept=20typeclass=20=E2=80=94=20deep=20p?=
 =?UTF-8?q?roof=20cascade)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 OpenGALib/Riemannian/Curvature/RiemannCurvature.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
index ac3bf08..56e2650 100644
--- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
+++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
@@ -772,10 +772,10 @@ These predicates describe properties of the ambient Riemannian metric
 explicit argument because the underlying notations (`Riem`, `Ric_g`)
 already consume the metric through the typeclass. -/
 
-/-- **Math.** The ambient Riemannian metric is **flat** if its Riemann
+/-- **Math.** A Riemannian metric `g` is **flat** if its Riemann
 curvature tensor vanishes pointwise. -/
-def IsFlat : Prop :=
-  ∀ (X Y Z : VectorFieldSection I M) (x : M), riemannCurvature HasMetric.metric X Y Z x = 0
+def IsFlat (g : RiemannianMetric I M) : Prop :=
+  ∀ (X Y Z : VectorFieldSection I M) (x : M), riemannCurvature g X Y Z x = 0
 
 /-! ## Killing vector fields -/
 

From 8c2d27e6112e73fd268d976122edbb7454a6ef8b Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 18:18:43 -0400
Subject: [PATCH 3/6] 9h: lift IsKilling +
 second_covDeriv_(inner_skew|commutator|eq_curvature) to explicit g

- IsKilling predicate now takes (g : RiemannianMetric I M)
- IsKilling.second_covDeriv_inner_skew lifted; local scalar var g renamed to kw_g to avoid shadowing the section g
- second_covDeriv_commutator lifted
- IsKilling.second_covDeriv_eq_curvature lifted

All HasMetric.metric body refs replaced with g; metricInner abbrev calls with g.metricInner; metricInner_X lemma calls with g.metricInner_X. Internal callers within RiemannCurvature.lean updated to pass g.
---
 .../Curvature/RiemannCurvature.lean           | 262 +++++++++---------
 1 file changed, 133 insertions(+), 129 deletions(-)

diff --git a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
index 56e2650..cebf78e 100644
--- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
+++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
@@ -786,9 +786,10 @@ Equivalent to the Lie derivative $\mathcal{L}_X g = 0$ (the flow of $X$
 is by isometries).
 
 Reference: do Carmo §3 Ex. 5; Petersen Ch. 8. -/
-def IsKilling (X : SmoothVectorField I M) : Prop :=
+def IsKilling (g : RiemannianMetric I M) (X : SmoothVectorField I M) : Prop :=
   ∀ (U W : SmoothVectorField I M) (y : M),
-    metricInner y ((covDeriv HasMetric.metric U X) y) (W y) + metricInner y ((covDeriv HasMetric.metric W X) y) (U y) = 0
+    g.metricInner y ((covDeriv g U X) y) (W y)
+      + g.metricInner y ((covDeriv g W X) y) (U y) = 0
 
 /-- **Math.** Covariantly differentiating the Killing equation.
 
@@ -797,107 +798,108 @@ For a Killing field `X`, the tensor
 This is the textbook "differentiate the Killing equation and subtract the
 connection terms" step. -/
 private lemma IsKilling.second_covDeriv_inner_skew
-    (X : SmoothVectorField I M) (hX : IsKilling X)
+    (g : RiemannianMetric I M)
+    (X : SmoothVectorField I M) (hX : IsKilling g X)
     (U V W : SmoothVectorField I M) (x : M) :
-    metricInner x
-        (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)
-      + metricInner x
-        (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric W.toFun X.toFun y) x
-          - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric U.toFun W.toFun y) X.toFun x) (V x)
+    g.metricInner x
+        (covDeriv g U.toFun (fun y => covDeriv g V.toFun X.toFun y) x
+          - covDeriv g (fun y => covDeriv g U.toFun V.toFun y) X.toFun x) (W x)
+      + g.metricInner x
+        (covDeriv g U.toFun (fun y => covDeriv g W.toFun X.toFun y) x
+          - covDeriv g (fun y => covDeriv g U.toFun W.toFun y) X.toFun x) (V x)
       = 0 := by
   classical
   let f : M → ℝ := fun y =>
-    metricInner y (covDeriv HasMetric.metric V.toFun X.toFun y) (W y)
-  let g : M → ℝ := fun y =>
-    metricInner y (covDeriv HasMetric.metric W.toFun X.toFun y) (V y)
-  have h_kill_fun : (fun y : M => f y + g y) = fun _ => 0 := by
+    g.metricInner y (covDeriv g V.toFun X.toFun y) (W y)
+  let kw_g : M → ℝ := fun y =>
+    g.metricInner y (covDeriv g W.toFun X.toFun y) (V y)
+  have h_kill_fun : (fun y : M => f y + kw_g y) = fun _ => 0 := by
     funext y
     exact hX V W y
-  have h_deriv_zero : mDirDeriv (fun y : M => f y + g y) x (U x) = 0 := by
+  have h_deriv_zero : mDirDeriv (fun y : M => f y + kw_g y) x (U x) = 0 := by
     rw [h_kill_fun]
     rw [mDirDeriv, mfderiv_const]
     rfl
-  have h_dVX : TangentSmoothAt (fun y : M => covDeriv HasMetric.metric V.toFun X.toFun y) x :=
-    covDeriv_smoothVF_smoothAt HasMetric.metric V X x
-  have h_dWX : TangentSmoothAt (fun y : M => covDeriv HasMetric.metric W.toFun X.toFun y) x :=
-    covDeriv_smoothVF_smoothAt HasMetric.metric W X x
+  have h_dVX : TangentSmoothAt (fun y : M => covDeriv g V.toFun X.toFun y) x :=
+    covDeriv_smoothVF_smoothAt g V X x
+  have h_dWX : TangentSmoothAt (fun y : M => covDeriv g W.toFun X.toFun y) x :=
+    covDeriv_smoothVF_smoothAt g W X x
   have hf_mdiff : MDifferentiableAt I 𝓘(ℝ, ℝ) f x := by
-    exact metricInner_mdifferentiableAt_of_tangentSmoothAt h_dVX (W.smoothAt x)
-  have hg_mdiff : MDifferentiableAt I 𝓘(ℝ, ℝ) g x := by
-    exact metricInner_mdifferentiableAt_of_tangentSmoothAt h_dWX (V.smoothAt x)
+    exact g.metricInner_mdifferentiableAt_of_tangentSmoothAt h_dVX (W.smoothAt x)
+  have hkw_mdiff : MDifferentiableAt I 𝓘(ℝ, ℝ) kw_g x := by
+    exact g.metricInner_mdifferentiableAt_of_tangentSmoothAt h_dWX (V.smoothAt x)
   have h_deriv_add :
-      mDirDeriv (fun y : M => f y + g y) x (U x)
-        = mDirDeriv f x (U x) + mDirDeriv g x (U x) := by
+      mDirDeriv (fun y : M => f y + kw_g y) x (U x)
+        = mDirDeriv f x (U x) + mDirDeriv kw_g x (U x) := by
     unfold mDirDeriv
-    rw [show (fun y : M => f y + g y) = f + g from rfl,
-      mfderiv_add hf_mdiff hg_mdiff]
+    rw [show (fun y : M => f y + kw_g y) = f + kw_g from rfl,
+      mfderiv_add hf_mdiff hkw_mdiff]
     rfl
-  have h_compat_f := leviCivitaConnection_metric_compatible HasMetric.metric
-    U.toFun (fun y : M => covDeriv HasMetric.metric V.toFun X.toFun y) W.toFun x
+  have h_compat_f := leviCivitaConnection_metric_compatible g
+    U.toFun (fun y : M => covDeriv g V.toFun X.toFun y) W.toFun x
     (U.smoothAt x) h_dVX (W.smoothAt x)
-  have h_compat_g := leviCivitaConnection_metric_compatible HasMetric.metric
-    U.toFun (fun y : M => covDeriv HasMetric.metric W.toFun X.toFun y) V.toFun x
+  have h_compat_g := leviCivitaConnection_metric_compatible g
+    U.toFun (fun y : M => covDeriv g W.toFun X.toFun y) V.toFun x
     (U.smoothAt x) h_dWX (V.smoothAt x)
   change mDirDeriv f x (U x)
-      = metricInner x (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric V.toFun X.toFun y) x) (W x)
-        + metricInner x (covDeriv HasMetric.metric V.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun W.toFun x)
+      = g.metricInner x (covDeriv g U.toFun (fun y => covDeriv g V.toFun X.toFun y) x) (W x)
+        + g.metricInner x (covDeriv g V.toFun X.toFun x) (covDeriv g U.toFun W.toFun x)
     at h_compat_f
-  change mDirDeriv g x (U x)
-      = metricInner x (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric W.toFun X.toFun y) x) (V x)
-        + metricInner x (covDeriv HasMetric.metric W.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun V.toFun x)
+  change mDirDeriv kw_g x (U x)
+      = g.metricInner x (covDeriv g U.toFun (fun y => covDeriv g W.toFun X.toFun y) x) (V x)
+        + g.metricInner x (covDeriv g W.toFun X.toFun x) (covDeriv g U.toFun V.toFun x)
     at h_compat_g
   have h_expanded :
-      metricInner x (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric V.toFun X.toFun y) x) (W x)
-        + metricInner x (covDeriv HasMetric.metric V.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun W.toFun x)
-        + (metricInner x
-            (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric W.toFun X.toFun y) x) (V x)
-          + metricInner x (covDeriv HasMetric.metric W.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun V.toFun x))
+      g.metricInner x (covDeriv g U.toFun (fun y => covDeriv g V.toFun X.toFun y) x) (W x)
+        + g.metricInner x (covDeriv g V.toFun X.toFun x) (covDeriv g U.toFun W.toFun x)
+        + (g.metricInner x
+            (covDeriv g U.toFun (fun y => covDeriv g W.toFun X.toFun y) x) (V x)
+          + g.metricInner x (covDeriv g W.toFun X.toFun x) (covDeriv g U.toFun V.toFun x))
         = 0 := by
     linarith [h_deriv_zero, h_deriv_add, h_compat_f, h_compat_g]
   have h_cross_W :
-      metricInner x (covDeriv HasMetric.metric V.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun W.toFun x)
-        = -metricInner x
-            (covDeriv HasMetric.metric (fun y : M => covDeriv HasMetric.metric U.toFun W.toFun y) X.toFun x) (V x) := by
+      g.metricInner x (covDeriv g V.toFun X.toFun x) (covDeriv g U.toFun W.toFun x)
+        = -g.metricInner x
+            (covDeriv g (fun y : M => covDeriv g U.toFun W.toFun y) X.toFun x) (V x) := by
     have h := hX (SmoothVectorField.const (I := I) (M := M)
-        (covDeriv HasMetric.metric U.toFun W.toFun x)) V x
+        (covDeriv g U.toFun W.toFun x)) V x
     change
-      metricInner x
-          ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun X.toFun x ((fun y : M => covDeriv HasMetric.metric U.toFun W.toFun y) x))
+      g.metricInner x
+          ((leviCivitaConnection (I := I) (M := M) g).toFun X.toFun x ((fun y : M => covDeriv g U.toFun W.toFun y) x))
           (V x)
-        + metricInner x (covDeriv HasMetric.metric V.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun W.toFun x) = 0 at h
+        + g.metricInner x (covDeriv g V.toFun X.toFun x) (covDeriv g U.toFun W.toFun x) = 0 at h
     have h_comm :
-        metricInner x (covDeriv HasMetric.metric V.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun W.toFun x)
-          + metricInner x
-            ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun X.toFun x ((fun y : M => covDeriv HasMetric.metric U.toFun W.toFun y) x))
+        g.metricInner x (covDeriv g V.toFun X.toFun x) (covDeriv g U.toFun W.toFun x)
+          + g.metricInner x
+            ((leviCivitaConnection (I := I) (M := M) g).toFun X.toFun x ((fun y : M => covDeriv g U.toFun W.toFun y) x))
             (V x) = 0 := by
       rw [add_comm]
       exact h
     exact eq_neg_of_add_eq_zero_left h_comm
   have h_cross_V :
-      metricInner x (covDeriv HasMetric.metric W.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun V.toFun x)
-        = -metricInner x
-            (covDeriv HasMetric.metric (fun y : M => covDeriv HasMetric.metric U.toFun V.toFun y) X.toFun x) (W x) := by
+      g.metricInner x (covDeriv g W.toFun X.toFun x) (covDeriv g U.toFun V.toFun x)
+        = -g.metricInner x
+            (covDeriv g (fun y : M => covDeriv g U.toFun V.toFun y) X.toFun x) (W x) := by
     have h := hX (SmoothVectorField.const (I := I) (M := M)
-        (covDeriv HasMetric.metric U.toFun V.toFun x)) W x
+        (covDeriv g U.toFun V.toFun x)) W x
     change
-      metricInner x
-          ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun X.toFun x ((fun y : M => covDeriv HasMetric.metric U.toFun V.toFun y) x))
+      g.metricInner x
+          ((leviCivitaConnection (I := I) (M := M) g).toFun X.toFun x ((fun y : M => covDeriv g U.toFun V.toFun y) x))
           (W x)
-        + metricInner x (covDeriv HasMetric.metric W.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun V.toFun x) = 0 at h
+        + g.metricInner x (covDeriv g W.toFun X.toFun x) (covDeriv g U.toFun V.toFun x) = 0 at h
     have h_comm :
-        metricInner x (covDeriv HasMetric.metric W.toFun X.toFun x) (covDeriv HasMetric.metric U.toFun V.toFun x)
-          + metricInner x
-            ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun X.toFun x ((fun y : M => covDeriv HasMetric.metric U.toFun V.toFun y) x))
+        g.metricInner x (covDeriv g W.toFun X.toFun x) (covDeriv g U.toFun V.toFun x)
+          + g.metricInner x
+            ((leviCivitaConnection (I := I) (M := M) g).toFun X.toFun x ((fun y : M => covDeriv g U.toFun V.toFun y) x))
             (W x) = 0 := by
       rw [add_comm]
       exact h
     exact eq_neg_of_add_eq_zero_left h_comm
-  rw [metricInner_sub_left, metricInner_sub_left]
-  show metricInner x (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric V.toFun X.toFun y) x) (W x)
-      - metricInner x (covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric U.toFun V.toFun y) X.toFun x) (W x)
-      + (metricInner x (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric W.toFun X.toFun y) x) (V x)
-        - metricInner x (covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric U.toFun W.toFun y) X.toFun x) (V x))
+  rw [g.metricInner_sub_left, g.metricInner_sub_left]
+  show g.metricInner x (covDeriv g U.toFun (fun y => covDeriv g V.toFun X.toFun y) x) (W x)
+      - g.metricInner x (covDeriv g (fun y => covDeriv g U.toFun V.toFun y) X.toFun x) (W x)
+      + (g.metricInner x (covDeriv g U.toFun (fun y => covDeriv g W.toFun X.toFun y) x) (V x)
+        - g.metricInner x (covDeriv g (fun y => covDeriv g U.toFun W.toFun y) X.toFun x) (V x))
       = 0
   linarith [h_expanded, h_cross_W, h_cross_V]
 
@@ -905,16 +907,17 @@ private lemma IsKilling.second_covDeriv_inner_skew
 `H(U,V)X - H(V,U)X = R(U,V)X`, where
 `H(U,V)X = ∇_U∇_V X - ∇_{∇_U V}X`. -/
 private lemma second_covDeriv_commutator
+    (g : RiemannianMetric I M)
     (X U V : SmoothVectorField I M) (x : M) :
-    (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)
-      - (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)
-      = riemannCurvature HasMetric.metric U V X x := by
+    (covDeriv g U.toFun (fun y => covDeriv g V.toFun X.toFun y) x
+        - covDeriv g (fun y => covDeriv g U.toFun V.toFun y) X.toFun x)
+      - (covDeriv g V.toFun (fun y => covDeriv g U.toFun X.toFun y) x
+        - covDeriv g (fun y => covDeriv g V.toFun U.toFun y) X.toFun x)
+      = riemannCurvature g U V X x := by
   rw [riemannCurvature_commutator_form]
-  have h_torsion := covDeriv_sub_swap_eq_mlieBracket HasMetric.metric U.toFun V.toFun x
+  have h_torsion := covDeriv_sub_swap_eq_mlieBracket g U.toFun V.toFun x
     (U.smoothAt x) (V.smoothAt x)
-  unfold covDeriv HasMetric.metric at h_torsion ⊢
+  unfold covDeriv at h_torsion ⊢
   rw [← h_torsion]
   simp only [map_sub]
   abel_nf
@@ -931,88 +934,89 @@ 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
-`riemannCurvature HasMetric.metric Y X Z`, equivalently `-riemannCurvature HasMetric.metric X Y Z`.
+`riemannCurvature g Y X Z`, equivalently `-riemannCurvature g X Y Z`.
 
 Reference: do Carmo, *Riemannian Geometry*, §3 Ex. 5; Petersen, Ch. 8 §2;
 Cheeger–Ebin §1.84. -/
 theorem IsKilling.second_covDeriv_eq_curvature
-    (X : SmoothVectorField I M) (hX : IsKilling X)
+    (g : RiemannianMetric I M)
+    (X : SmoothVectorField I M) (hX : IsKilling g X)
     (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
-      = riemannCurvature HasMetric.metric Y X Z x := by
+    covDeriv g Y.toFun (covDeriv g Z X) x
+      - covDeriv g (covDeriv g Y Z) X.toFun x
+      = riemannCurvature g Y X Z x := by
   classical
-  apply (metricInner_eq_iff_eq x _ _).mp
+  apply (g.metricInner_eq_iff_eq x _ _).mp
   intro w
   set W : SmoothVectorField I M := SmoothVectorField.const (I := I) (M := M) w with hW_def
   let A (U V W : SmoothVectorField I M) : ℝ :=
-    metricInner x
-      (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)
+    g.metricInner x
+      (covDeriv g U.toFun (fun y => covDeriv g V.toFun X.toFun y) x
+        - covDeriv g (fun y => covDeriv g U.toFun V.toFun y) X.toFun x) (W x)
   let C (U V W : SmoothVectorField I M) : ℝ :=
-    metricInner x (riemannCurvature HasMetric.metric U V X x) (W x)
+    g.metricInner x (riemannCurvature g 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
+    simpa [A] using IsKilling.second_covDeriv_inner_skew g X hX Y Z W x
   have h_skew_Z : A Z W Y + A Z Y W = 0 := by
-    simpa [A] using IsKilling.second_covDeriv_inner_skew X hX Z W Y x
+    simpa [A] using IsKilling.second_covDeriv_inner_skew g X hX Z W Y x
   have h_skew_W : A W Y Z + A W Z Y = 0 := by
-    simpa [A] using IsKilling.second_covDeriv_inner_skew X hX W Y Z x
+    simpa [A] using IsKilling.second_covDeriv_inner_skew g X hX W Y Z x
   have h_comm_YZ : A Y Z W - A Z Y W = C Y Z W := by
-    have h := congrArg (fun v => metricInner x v (W x))
-      (second_covDeriv_commutator X Y Z x)
-    change metricInner x
-        ((covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric Z.toFun X.toFun y) x
-            - 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 (riemannCurvature HasMetric.metric Y Z X x) (W x) at h
-    rw [metricInner_sub_left] at h
+    have h := congrArg (fun v => g.metricInner x v (W x))
+      (second_covDeriv_commutator g X Y Z x)
+    change g.metricInner x
+        ((covDeriv g Y.toFun (fun y => covDeriv g Z.toFun X.toFun y) x
+            - covDeriv g (fun y => covDeriv g Y.toFun Z.toFun y) X.toFun x)
+          - (covDeriv g Z.toFun (fun y => covDeriv g Y.toFun X.toFun y) x
+            - covDeriv g (fun y => covDeriv g Z.toFun Y.toFun y) X.toFun x)) (W x)
+        = g.metricInner x (riemannCurvature g Y Z X x) (W x) at h
+    rw [g.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
-    have h := congrArg (fun v => metricInner x v (Y x))
-      (second_covDeriv_commutator X Z W x)
-    change metricInner x
-        ((covDeriv HasMetric.metric Z.toFun (fun y => covDeriv HasMetric.metric W.toFun X.toFun y) x
-            - 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 (riemannCurvature HasMetric.metric Z W X x) (Y x) at h
-    rw [metricInner_sub_left] at h
+    have h := congrArg (fun v => g.metricInner x v (Y x))
+      (second_covDeriv_commutator g X Z W x)
+    change g.metricInner x
+        ((covDeriv g Z.toFun (fun y => covDeriv g W.toFun X.toFun y) x
+            - covDeriv g (fun y => covDeriv g Z.toFun W.toFun y) X.toFun x)
+          - (covDeriv g W.toFun (fun y => covDeriv g Z.toFun X.toFun y) x
+            - covDeriv g (fun y => covDeriv g W.toFun Z.toFun y) X.toFun x)) (Y x)
+        = g.metricInner x (riemannCurvature g Z W X x) (Y x) at h
+    rw [g.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
-    have h := congrArg (fun v => metricInner x v (Z x))
-      (second_covDeriv_commutator X W Y x)
-    change metricInner x
-        ((covDeriv HasMetric.metric W.toFun (fun y => covDeriv HasMetric.metric Y.toFun X.toFun y) x
-            - 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 (riemannCurvature HasMetric.metric W Y X x) (Z x) at h
-    rw [metricInner_sub_left] at h
+    have h := congrArg (fun v => g.metricInner x v (Z x))
+      (second_covDeriv_commutator g X W Y x)
+    change g.metricInner x
+        ((covDeriv g W.toFun (fun y => covDeriv g Y.toFun X.toFun y) x
+            - covDeriv g (fun y => covDeriv g W.toFun Y.toFun y) X.toFun x)
+          - (covDeriv g Y.toFun (fun y => covDeriv g W.toFun X.toFun y) x
+            - covDeriv g (fun y => covDeriv g Y.toFun W.toFun y) X.toFun x)) (Z x)
+        = g.metricInner x (riemannCurvature g W Y X x) (Z x) at h
+    rw [g.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 (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
-    have h_bianchi := bianchi_first HasMetric.metric X W Y x
+      = 2 * g.metricInner x (riemannCurvature g Y X Z x) (W x) := by
+    have h_bianchi := bianchi_first g X W Y x
     have h_inner :
-        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)
+        g.metricInner x (riemannCurvature g X W Y x + riemannCurvature g W Y X x + riemannCurvature g 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 (riemannCurvature HasMetric.metric X W Y x) (Z x) := by
-      simpa [C] using riemannCurvature_pair_symm HasMetric.metric Y Z X W x
-    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 HasMetric.metric Z W X Y x
-    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 HasMetric.metric W Y X Z x
+      exact g.metricInner_zero_left x (Z x)
+    rw [g.metricInner_add_left, g.metricInner_add_left] at h_inner
+    have h_pair₁ : C Y Z W = g.metricInner x (riemannCurvature g X W Y x) (Z x) := by
+      simpa [C] using riemannCurvature_pair_symm g Y Z X W x
+    have h_pair₂ : C Z W Y = g.metricInner x (riemannCurvature g X Y Z x) (W x) := by
+      simpa [C] using riemannCurvature_pair_symm g Z W X Y x
+    have h_pair₃ : C W Y Z = g.metricInner x (riemannCurvature g X Z W x) (Y x) := by
+      simpa [C] using riemannCurvature_pair_symm g W Y X Z x
     have h_antisym12 :
-        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]
+        g.metricInner x (riemannCurvature g X Y Z x) (W x)
+          = -g.metricInner x (riemannCurvature g Y X Z x) (W x) := by
+      rw [riemannCurvature_antisymm g X.toFun Y.toFun Z.toFun x, g.metricInner_neg_left]
     have h_antisym34 :
-        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 HasMetric.metric Y X W Z x (by
+        g.metricInner x (riemannCurvature g Y X W x) (Z x)
+          = -g.metricInner x (riemannCurvature g Y X Z x) (W x) := by
+      have h := riemannCurvature_metric_skew g Y X W Z x (by
         rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
         exact Set.mem_univ _)
       linarith
@@ -1020,7 +1024,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 (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
+  have h_target : A Y Z W = g.metricInner x (riemannCurvature g Y X Z x) (W x) := by
     linarith [h_A, h_curv]
   simpa [A, hW_def] using h_target
 

From 7cea282c01496111e6ca0d110054238a5dcc9d25 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 18:22:53 -0400
Subject: [PATCH 4/6] 9h: lift ricci_symm to explicit g via (hg : g =
 hm.metric) hypothesis
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The proof routes through ⟪·,·⟫_ℝ = hm.metric.inner via the InnerProductSpace
instance derived from [HasMetric I M], so ricci_symm cannot be lifted for
arbitrary g without InnerProductSpace restructure. Use subst hg pattern:
caller passes g and proof of g = hm.metric, body works in hm.metric form.

BochnerExpansion caller updated to pass (HasMetric.metric, rfl).

RiemannCurvature.lean is now fully explicit-g for all theorems with at most
this trivial hg sidecar.
---
 .../Curvature/RiemannCurvature.lean           | 26 ++++++++-----------
 .../Operators/Bochner/BochnerExpansion.lean   |  2 +-
 2 files changed, 12 insertions(+), 16 deletions(-)

diff --git a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
index cebf78e..2d77e49 100644
--- a/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
+++ b/OpenGALib/Riemannian/Curvature/RiemannCurvature.lean
@@ -734,34 +734,30 @@ The hypothesis `h_interior` is required by `riemannCurvature_inner_self_zero`
 (via the Hessian-Lie identity on boundary-aware models). -/
 theorem ricci_symm
     [IsManifold I 2 M]
+    (g : RiemannianMetric I M) (hg : g = hm.metric)
     (X Y : SmoothVectorField I M) (x : M)
     (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) :
-    ricci HasMetric.metric X Y x = ricci HasMetric.metric Y X x := by
+    ricci g X Y x = ricci g Y X x := by
+  subst hg
   classical
   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 : ricci HasMetric.metric X Y x =
-      ∑ i, ⟪b i, riemannCurvature HasMetric.metric (fun _ : M => (b i : E)) X.toFun Y.toFun x⟫_ℝ := by
+  have h_RXY : ricci hm.metric X Y x =
+      ∑ i, ⟪b i, riemannCurvature hm.metric (fun _ : M => (b i : E)) X.toFun Y.toFun x⟫_ℝ := by
     show LinearMap.trace ℝ (TangentSpace I x)
-          (curvatureEndo (HasMetric.metric) X Y x) = _
+          (curvatureEndo hm.metric X Y x) = _
     exact LinearMap.trace_eq_sum_inner _ b
-  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
+  have h_RYX : ricci hm.metric Y X x =
+      ∑ i, ⟪b i, riemannCurvature hm.metric (fun _ : M => (b i : E)) Y.toFun X.toFun x⟫_ℝ := by
     show LinearMap.trace ℝ (TangentSpace I x)
-          (curvatureEndo (HasMetric.metric) Y X x) = _
+          (curvatureEndo hm.metric Y X x) = _
     exact LinearMap.trace_eq_sum_inner _ b
   rw [h_RXY, h_RYX]
   refine Finset.sum_congr rfl (fun i _ => ?_)
   rw [← sub_eq_zero, ← inner_sub_right,
-      riemannCurvature_const_first_swap_eq_neg (I := I) (M := M) HasMetric.metric (b i : E) X Y x]
-  -- Goal: ⟪b i, -R(X, Y) (const b i) x⟫_ℝ = 0
+      riemannCurvature_const_first_swap_eq_neg (I := I) (M := M) hm.metric (b i : E) X Y x]
   rw [inner_neg_right, neg_eq_zero]
-  -- Goal: ⟪b i, R(X, Y) (const b i) x⟫_ℝ = 0
-  -- Use real_inner_comm + riemannCurvature_inner_self_zero (with Z = cF[b i]).
   rw [real_inner_comm]
-  -- Goal: ⟪R(X, Y) (const b i) x, b i⟫_ℝ = 0 (def-eq g.metricInner via g).
-  exact riemannCurvature_inner_self_zero HasMetric.metric X Y
+  exact riemannCurvature_inner_self_zero hm.metric X Y
     (SmoothVectorField.const (I := I) (M := M) (b i : E)) x h_interior
 
 
diff --git a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
index 8b2011c..5f1e7f6 100644
--- a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
@@ -418,7 +418,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
           = ricciTensor (HasMetric.metric) x (gradF.toFun x) (W.toFun x)
         show ricci (HasMetric.metric) WV GV x
             = ricci (HasMetric.metric) GV WV x
-        exact ricci_symm WV GV x h_interior
+        exact ricci_symm HasMetric.metric rfl WV GV x h_interior
 
 /-- **Math.** Hessian-frame trace equals Laplacian locally: on a
 neighbourhood of $x$,

From bcd212d0a8c749d2a84df29b14144648cadde6f4 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 18:58:36 -0400
Subject: [PATCH 5/6] 9i: lift BochnerExpansion.lean to explicit g (via subst
 hg pattern)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Section variable adds (g : RiemannianMetric I M) (hg : g = hm.metric) + include g hg
- Each theorem signature uses g.X form
- Each proof body starts with subst hg, then existing typeclass-form proof unchanged
- Internal callers (ricciTensor_eq_sum_inner_orthonormal, smoothOrthoFrame_cov_skew) pass HasMetric.metric rfl
- PerSummand callers updated to pass HasMetric.metric rfl

Bochner stack body retains typeclass-bound infrastructure (smoothOrthoFrame
+ LinearMap.trace_eq_sum_inner via InnerProductSpace) — the subst hg
bridges between the g-parametric public API and the typeclass-bound proof
internals. Caller passes g = hm.metric and rfl to consume.
---
 .../Operators/Bochner/BochnerExpansion.lean   | 134 ++++++++++--------
 .../Operators/Bochner/PerSummand.lean         |   8 +-
 2 files changed, 78 insertions(+), 64 deletions(-)

diff --git a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
index 5f1e7f6..6d1ee05 100644
--- a/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
@@ -49,6 +49,9 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [T2Space M]
   [IsLocallyConstantChartedSpace H M]
   [hm : HasMetric I M]
+  (g : RiemannianMetric I M) (hg : g = hm.metric)
+
+include g hg
 
 /-! ## Building block: Ricci as g-orthonormal trace -/
 
@@ -61,12 +64,13 @@ endomorphism. -/
 theorem ricciTensor_eq_sum_inner_orthonormal
     [IsManifold I 2 M]
     (x : M) (V W : TangentSpace I x) :
-    ricciTensor HasMetric.metric x V W =
+    ricciTensor g x V W =
       ∑ i, ⟪(stdOrthonormalBasis ℝ (TangentSpace I x)) i,
-            curvatureEndo (HasMetric.metric)
+            curvatureEndo (g)
               (SmoothVectorField.const (I := I) (M := M) V)
               (SmoothVectorField.const (I := I) (M := M) W) x
               ((stdOrthonormalBasis ℝ (TangentSpace I x)) i)⟫_ℝ := by
+  subst hg
   show ricci (HasMetric.metric)
         (SmoothVectorField.const (I := I) (M := M) V)
         (SmoothVectorField.const (I := I) (M := M) W) x = _
@@ -101,17 +105,18 @@ theorem metricInner_secondCovDerivAt_grad_swap_of_hess_eventual_sym
     (f : M → ℝ) (x : M) (v w z : TangentSpace I x)
     (h_interior : extChartAt I x x ∈ closure (interior (Set.range I)))
     (hf_2 : ContMDiffAt I 𝓘(ℝ, ℝ) 2 f x)
-    (h_grad : TangentSmoothAt (manifoldGradient (I := I) HasMetric.metric f) x)
+    (h_grad : TangentSmoothAt (manifoldGradient (I := I) g f) x)
     (h_grad_const_w : TangentSmoothAt
-        (fun y : M => covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y w) x)
+        (fun y : M => covDerivAt g (manifoldGradient (I := I) g f) y w) x)
     (h_grad_const_z : TangentSmoothAt
-        (fun y : M => covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) y z) x)
-    (h_eventual_sym : (fun y : M => hessianBilin (I := I) HasMetric.metric f y w z)
-        =ᶠ[𝓝 x] (fun y : M => hessianBilin (I := I) HasMetric.metric f y z w)) :
-    metricInner x (secondCovDerivAt (I := I) (M := M) HasMetric.metric
-        (manifoldGradient (I := I) HasMetric.metric f) x v w) z =
-      metricInner x (secondCovDerivAt (I := I) (M := M) HasMetric.metric
-        (manifoldGradient (I := I) HasMetric.metric f) x v z) w := by
+        (fun y : M => covDerivAt g (manifoldGradient (I := I) g f) y z) x)
+    (h_eventual_sym : (fun y : M => hessianBilin (I := I) g f y w z)
+        =ᶠ[𝓝 x] (fun y : M => hessianBilin (I := I) g f y z w)) :
+    g.metricInner x (secondCovDerivAt (I := I) (M := M) g
+        (manifoldGradient (I := I) g f) x v w) z =
+      g.metricInner x (secondCovDerivAt (I := I) (M := M) g
+        (manifoldGradient (I := I) g f) x v z) w := by
+  subst hg
   classical
   -- Constant lifts of v, w, z at x.
   set V : VectorFieldSection I M := fun _ => (v : TangentSpace I x) with hV_def
@@ -235,8 +240,9 @@ theorem hessianBilin_eventually_symm_of_strict_interior
     [IsManifold I 2 M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M)
     (w z : TangentSpace I x) :
-    (fun y : M => hessianBilin (I := I) HasMetric.metric f y w z)
-      =ᶠ[𝓝 x] (fun y : M => hessianBilin (I := I) HasMetric.metric f y z w) := by
+    (fun y : M => hessianBilin (I := I) g f y w z)
+      =ᶠ[𝓝 x] (fun y : M => hessianBilin (I := I) g f y z w) := by
+  subst hg
   have h_strict : extChartAt I x x ∈ interior (Set.range I) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ]; exact Set.mem_univ _
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
@@ -263,8 +269,9 @@ theorem hessianBilin_section_eventually_symm_of_strict_interior
     [IsManifold I 2 M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f)
     (X Y : VectorFieldSection I M) (x : M) :
-    (fun y : M => hessianBilin (I := I) HasMetric.metric f y (X y) (Y y))
-      =ᶠ[𝓝 x] (fun y : M => hessianBilin (I := I) HasMetric.metric f y (Y y) (X y)) := by
+    (fun y : M => hessianBilin (I := I) g f y (X y) (Y y))
+      =ᶠ[𝓝 x] (fun y : M => hessianBilin (I := I) g f y (Y y) (X y)) := by
+  subst hg
   have h_strict : extChartAt I x x ∈ interior (Set.range I) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ]; exact Set.mem_univ _
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
@@ -286,14 +293,15 @@ $$\langle (\nabla^2 \nabla f)(v, w),\, z\rangle_g(x)
     + \langle R(\mathrm{const}\,v,\,\mathrm{const}\,w)\,\nabla f,\, z\rangle_g(x).$$ -/
 theorem metricInner_secondCovDerivAt_grad_eq_swap_add_curvature
     (f : M → ℝ) (x : M) (v w z : TangentSpace I x) :
-    metricInner x (secondCovDerivAt (I := I) (M := M) HasMetric.metric
-        (manifoldGradient (I := I) HasMetric.metric f) x v w) z
-      = metricInner x (secondCovDerivAt (I := I) (M := M) HasMetric.metric
-          (manifoldGradient (I := I) HasMetric.metric f) x w v) z
-        + metricInner x
-            (riemannCurvature HasMetric.metric (fun _ : M => (v : TangentSpace I x))
+    g.metricInner x (secondCovDerivAt (I := I) (M := M) g
+        (manifoldGradient (I := I) g f) x v w) z
+      = g.metricInner x (secondCovDerivAt (I := I) (M := M) g
+          (manifoldGradient (I := I) g f) x w v) z
+        + g.metricInner x
+            (riemannCurvature g (fun _ : M => (v : TangentSpace I x))
               (fun _ : M => (w : TangentSpace I x))
-              (manifoldGradient (I := I) HasMetric.metric f) x) z := by
+              (manifoldGradient (I := I) g f) x) z := by
+  subst hg
   have h := secondCovDerivAt_sub_swap_eq_riemannCurvature HasMetric.metric    (I := I) (M := M) (manifoldGradient (I := I) HasMetric.metric f) x v w
   -- h : secondCovDerivAt ∇f x v w - secondCovDerivAt ∇f x w v
   --       = riemannCurvature HasMetric.metric (const v) (const w) ∇f x
@@ -304,7 +312,7 @@ theorem metricInner_secondCovDerivAt_grad_eq_swap_add_curvature
             (fun _ : M => (w : TangentSpace I x))
             (manifoldGradient (I := I) HasMetric.metric f) x := by
     rw [← h]; abel
-  rw [h', metricInner_add_left]
+  rw [h', HasMetric.metric.metricInner_add_left]
 
 /-- **Math.** Curvature-term metric-skew packaging:
 given $g(R(B, w)\nabla f, B) + g(\nabla f, R(B, w) B) = 0$, the
@@ -315,14 +323,15 @@ The hypothesis is the polarisation of `riemannCurvature_inner_self_zero`. -/
 theorem heart_of_bochner_curvature_term
     (f : M → ℝ)
     {B w : VectorFieldSection I M} {x : M}
-    (h_metric_skew : metricInner x
-        (riemannCurvature HasMetric.metric B w (manifoldGradient (I := I) HasMetric.metric f) x) (B x)
-      + metricInner x (manifoldGradient (I := I) HasMetric.metric f x)
-          (riemannCurvature HasMetric.metric B w B x) = 0) :
-    metricInner x
-        (riemannCurvature HasMetric.metric B w (manifoldGradient (I := I) HasMetric.metric f) x) (B x) =
-      - metricInner x (manifoldGradient (I := I) HasMetric.metric f x)
-          (riemannCurvature HasMetric.metric B w B x) := by
+    (h_metric_skew : g.metricInner x
+        (riemannCurvature g B w (manifoldGradient (I := I) g f) x) (B x)
+      + g.metricInner x (manifoldGradient (I := I) g f x)
+          (riemannCurvature g B w B x) = 0) :
+    g.metricInner x
+        (riemannCurvature g B w (manifoldGradient (I := I) g f) x) (B x) =
+      - g.metricInner x (manifoldGradient (I := I) g f x)
+          (riemannCurvature g B w B x) := by
+  subst hg
   linarith
 
 /-- **Math.** **Ricci sum identity** (heart-of-Bochner Step 3): the
@@ -334,12 +343,13 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
     [IsManifold I 2 M] [T2Space M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f)
     (W : SmoothVectorField I M) (x : M) :
-    ∑ i, metricInner x
-        (riemannCurvature HasMetric.metric
+    ∑ i, g.metricInner x
+        (riemannCurvature g
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i)
-          W.toFun (manifoldGradient (I := I) HasMetric.metric f) x)
+          W.toFun (manifoldGradient (I := I) g f) x)
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
-      = ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x) (W.toFun x) := by
+      = ricciTensor g x (manifoldGradient (I := I) g f x) (W.toFun x) := by
+  subst hg
   classical
   have h_interior : extChartAt I x x ∈ closure (interior (Set.range I)) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
@@ -402,7 +412,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
                 ((stdOrthonormalBasis ℝ (TangentSpace I x)) i) :=
         Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x Φ
     _ = ricciTensor HasMetric.metric x (W.toFun x) (gradF.toFun x) := by
-        rw [ricciTensor_eq_sum_inner_orthonormal x (W.toFun x) (gradF.toFun x)]
+        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
@@ -428,10 +438,11 @@ with `sum_diagonal_smoothOrthoFrame_at_nbhd_eq_std` and the std-basis
 trace identification with `scalarLaplacian`. -/
 theorem sum_hessianBilin_smoothOrthoFrame_eventuallyEq_laplacian
     (f : M → ℝ) (x : M) :
-    (fun b => ∑ i, hessianBilin (I := I) HasMetric.metric f b
+    (fun b => ∑ i, hessianBilin (I := I) g f b
                     (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b)
                     (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b))
-      =ᶠ[𝓝 x] (Operators.scalarLaplacian (I := I) HasMetric.metric f : M → ℝ) := by
+      =ᶠ[𝓝 x] (Operators.scalarLaplacian (I := I) g f : M → ℝ) := by
+  subst hg
   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`.
@@ -454,15 +465,16 @@ and apply metric compatibility. -/
 theorem smoothOrthoFrame_cov_skew
     [T2Space M]
     (x : M) (i j : Fin (Module.finrank ℝ E)) (v : TangentSpace I x) :
-    metricInner x
-        ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
+    g.metricInner x
+        ((leviCivitaConnection (I := I) (M := M) g).toFun
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i) x v)
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j x) +
-    metricInner x
+    g.metricInner x
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
-        ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
+        ((leviCivitaConnection (I := I) (M := M) g).toFun
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j) x v)
       = 0 := by
+  subst hg
   classical
   -- Section-level smoothness of the smooth orthonormal frame.
   have hBi := Riemannian.Tensor.smoothOrthoFrame_smooth (I := I) hm.metric x i
@@ -521,11 +533,12 @@ theorem sum_hessianBilin_smoothOrthoFrame_cov_eq_zero
     [IsManifold I 2 M] [T2Space M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f)
     (W : SmoothVectorField I M) (x : M) :
-    ∑ i, hessianBilin (I := I) HasMetric.metric f x
+    ∑ i, hessianBilin (I := I) g f x
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
-        ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
+        ((leviCivitaConnection (I := I) (M := M) g).toFun
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i) x
           (W.toFun x)) = 0 := by
+  subst hg
   classical
   have h_interior : extChartAt I x x ∈ closure (interior (Set.range I)) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
@@ -598,14 +611,14 @@ theorem sum_hessianBilin_smoothOrthoFrame_cov_eq_zero
     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.
-    have h := smoothOrthoFrame_cov_skew x i j (W.toFun x)
-    have h_swap : metricInner x
+    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)
         ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x j) x (W.toFun x))
         = a j i := by
-      show metricInner x _ _ = metricInner x _ _
-      exact metricInner_comm x _ _
+      show HasMetric.metric.metricInner x _ _ = HasMetric.metric.metricInner x _ _
+      exact HasMetric.metric.metricInner_comm x _ _
     rw [h_swap] at h
     linarith
   have h_symm : ∀ i j, h_mat i j = h_mat j i := by
@@ -650,23 +663,24 @@ theorem sum_inner_secondCovDerivAt_grad_smoothOrthoFrame_of_inner_form
     [IsManifold I 2 M] [T2Space M]
     (f : M → ℝ) (x : M)
     (hInner : ∀ w : TangentSpace I x,
-      metricInner x
-          (∑ i, secondCovDerivAt (I := I) (M := M) HasMetric.metric
-            (manifoldGradient (I := I) HasMetric.metric f) x
+      g.metricInner x
+          (∑ i, secondCovDerivAt (I := I) (M := M) g
+            (manifoldGradient (I := I) g f) x
             (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 (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
+        = g.metricInner x (manifoldGradient (I := I) g (Operators.scalarLaplacian (I := I) g f) x) w
+          + ricciTensor g x (manifoldGradient (I := I) g f x) w) :
+    ∑ i, g.metricInner x
+        (secondCovDerivAt (I := I) (M := M) g (manifoldGradient (I := I) g 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 (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
+        (manifoldGradient (I := I) g f x)
+      = g.metricInner x (manifoldGradient (I := I) g f x)
+            (manifoldGradient (I := I) g (Operators.scalarLaplacian (I := I) g f) x)
+        + ricciTensor g x (manifoldGradient (I := I) g f x)
+                                          (manifoldGradient (I := I) g f x) := by
+  subst hg
   classical
   -- Specialise hInner at w = ∇f x.
   have h := hInner (manifoldGradient (I := I) HasMetric.metric f x)
diff --git a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
index 8705dee..b65d7b0 100644
--- a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
@@ -98,7 +98,7 @@ theorem bochner_per_summand_swap
       (fun y : M => metricInner y (Q y) (W.toFun y))
         =ᶠ[𝓝 x] (fun y : M => metricInner y (P y) (B.toFun y)) :=
     hessianBilin_section_eventually_symm_of_strict_interior
-      (I := I) f hf B.toFun W.toFun x
+      (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`.
   have h_compat_PB := leviCivitaConnection_metric_compatible HasMetric.metric
     B.toFun P B.toFun x (B.smoothAt x) (hP_smooth x) (B.smoothAt x)
@@ -537,10 +537,10 @@ theorem bochner_connectionLaplacian_grad_decomposition
   -- (1) ∑ R-term = Ric(∇f, ∇f).
   have h_R_eq : (∑ i, Rterm i) =
       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
+    heart_curvature_orthonormal_sum_eq_ricci (I := I) HasMetric.metric rfl f hf gradF x
   -- (2) ∑ H-term = 0.
   have h_H_eq : (∑ i, Hterm i) = 0 :=
-    sum_hessianBilin_smoothOrthoFrame_cov_eq_zero (I := I) f hf gradF x
+    sum_hessianBilin_smoothOrthoFrame_cov_eq_zero (I := I) HasMetric.metric rfl f hf gradF x
   -- (3) ∑ M-term: factor mfderiv outside, identify inner sum as Δ_g f via Stage 7.
   have h_each_hess_smooth : ∀ i,
       MDifferentiableAt I 𝓘(ℝ, ℝ)
@@ -561,7 +561,7 @@ theorem bochner_connectionLaplacian_grad_decomposition
       (fun b : M => ∑ i, hessianBilin (I := I) HasMetric.metric f b ((Bi i).toFun b)
             ((Bi i).toFun b))
         =ᶠ[𝓝 x] (fun b : M => Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric f b) :=
-    sum_hessianBilin_smoothOrthoFrame_eventuallyEq_laplacian (I := I) f x
+    sum_hessianBilin_smoothOrthoFrame_eventuallyEq_laplacian (I := I) HasMetric.metric rfl f x
   have h_M_to_lap :
       (mfderiv I 𝓘(ℝ, ℝ)
           (fun b : M => ∑ i, hessianBilin (I := I) HasMetric.metric f b ((Bi i).toFun b)

From 535e9231a4f551695e6e5e96f8472ebfde6fffb7 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Mon, 18 May 2026 19:19:21 -0400
Subject: [PATCH 6/6] 9i: lift PerSummand.lean to explicit g (via subst hg
 pattern)

Same approach as BochnerExpansion: (g, hg : g = hm.metric) section variable
+ include g hg + subst hg at proof body start. Statement uses g.X; body
unchanged (typeclass form). Internal callers within PerSummand pass
HasMetric.metric rfl (since after subst hg, g and hg are gone from context).

Bochner.lean's bochner_weitzenboeck now passes HasMetric.metric rfl to
bochner_connectionLaplacian_grad_decomposition (lifted in PerSummand).

Fixed h_id_LCQW/_LCBW statements: HasMetric.metric.metricInner (dot form)
to match goal after subst hg.
---
 OpenGALib/Riemannian/Operators/Bochner.lean   |   2 +-
 .../Operators/Bochner/PerSummand.lean         | 123 +++++++++---------
 2 files changed, 66 insertions(+), 59 deletions(-)

diff --git a/OpenGALib/Riemannian/Operators/Bochner.lean b/OpenGALib/Riemannian/Operators/Bochner.lean
index 34eec55..ddeaf78 100644
--- a/OpenGALib/Riemannian/Operators/Bochner.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner.lean
@@ -247,7 +247,7 @@ theorem bochner_weitzenboeck
             ((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]
+      bochner_connectionLaplacian_grad_decomposition HasMetric.metric rfl f hf x]
   abel
 
 /-- **Math.** **Explicit-`g` form of the Bochner–Weitzenböck identity**.
diff --git a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
index b65d7b0..78df348 100644
--- a/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
+++ b/OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean
@@ -41,6 +41,9 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [T2Space M]
   [IsLocallyConstantChartedSpace H M]
   [hm : HasMetric I M]
+  (g : RiemannianMetric I M) (hg : g = hm.metric)
+
+include g hg
 
 /-- **Math.** **Per-summand swap form** (Hess-sym swap, step (d) of
 Petersen Ch 7 §1 Prop 33). At an interior point $x$:
@@ -55,22 +58,23 @@ theorem bochner_per_summand_swap
     [IsManifold I 2 M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f)
     (B W : SmoothVectorField I M) (x : M) :
-    metricInner x
-        (covDeriv HasMetric.metric B.toFun
-          (fun y => covDeriv HasMetric.metric B.toFun (manifoldGradient (I := I) HasMetric.metric f) y) x)
+    g.metricInner x
+        (covDeriv g B.toFun
+          (fun y => covDeriv g B.toFun (manifoldGradient (I := I) g f) y) x)
         (W.toFun x)
-      - metricInner x
-          (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
-            (covDeriv HasMetric.metric B.toFun B.toFun x))
+      - g.metricInner x
+          (covDerivAt g (manifoldGradient (I := I) g f) x
+            (covDeriv g B.toFun B.toFun x))
           (W.toFun x)
-    = metricInner x
-        (covDeriv HasMetric.metric B.toFun
-          (fun y => covDeriv HasMetric.metric W.toFun (manifoldGradient (I := I) HasMetric.metric f) y) x)
+    = g.metricInner x
+        (covDeriv g B.toFun
+          (fun y => covDeriv g W.toFun (manifoldGradient (I := I) g f) y) x)
         (B.toFun x)
-      - metricInner x
-          (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
-            (covDeriv HasMetric.metric B.toFun W.toFun x))
+      - g.metricInner x
+          (covDerivAt g (manifoldGradient (I := I) g f) x
+            (covDeriv g B.toFun W.toFun x))
           (B.toFun x) := by
+  subst hg
   classical
   have h_strict : extChartAt I x x ∈ interior (Set.range I) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ]; exact Set.mem_univ _
@@ -203,25 +207,26 @@ Unfolds `riemannCurvature HasMetric.metric`, applies torsion-freeness $[B, W] =
 - \nabla_W B$, and the direction-slot ℝ-linearity of $\nabla_\cdot \nabla f$. -/
 theorem bochner_per_summand_riemann_form
     (f : M → ℝ) (B W : SmoothVectorField I M) (x : M) :
-    metricInner x
-        (covDeriv HasMetric.metric B.toFun
-          (fun y => covDeriv HasMetric.metric W.toFun (manifoldGradient (I := I) HasMetric.metric f) y) x)
+    g.metricInner x
+        (covDeriv g B.toFun
+          (fun y => covDeriv g W.toFun (manifoldGradient (I := I) g f) y) x)
         (B.toFun x)
-      - metricInner x
-          (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
-            (covDeriv HasMetric.metric B.toFun W.toFun x))
+      - g.metricInner x
+          (covDerivAt g (manifoldGradient (I := I) g f) x
+            (covDeriv g B.toFun W.toFun x))
           (B.toFun x)
-    = metricInner x
-        (riemannCurvature HasMetric.metric B.toFun W.toFun (manifoldGradient (I := I) HasMetric.metric f) x)
+    = g.metricInner x
+        (riemannCurvature g B.toFun W.toFun (manifoldGradient (I := I) g f) x)
         (B.toFun x)
-      + metricInner x
-          (covDeriv HasMetric.metric W.toFun
-            (fun y => covDeriv HasMetric.metric B.toFun (manifoldGradient (I := I) HasMetric.metric f) y) x)
+      + g.metricInner x
+          (covDeriv g W.toFun
+            (fun y => covDeriv g B.toFun (manifoldGradient (I := I) g f) y) x)
           (B.toFun x)
-      - metricInner x
-          (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
-            (covDeriv HasMetric.metric W.toFun B.toFun x))
+      - g.metricInner x
+          (covDerivAt g (manifoldGradient (I := I) g f) x
+            (covDeriv g W.toFun B.toFun x))
           (B.toFun x) := by
+  subst hg
   classical
   -- Unfold `riemannCurvature HasMetric.metric` via def.
   -- riemannCurvature HasMetric.metric B W ∇f x = ∇_B (∇_W ∇f) x - ∇_W (∇_B ∇f) x - ∇_{[B,W]} ∇f x
@@ -271,7 +276,8 @@ theorem bochner_per_summand_riemann_form
   --     = 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 +).
   -- Goal becomes pure algebra; linarith with metricInner-sub distribution closes.
-  rw [metricInner_sub_left, metricInner_sub_left, metricInner_sub_left]
+  rw [HasMetric.metric.metricInner_sub_left, HasMetric.metric.metricInner_sub_left,
+      HasMetric.metric.metricInner_sub_left]
   linarith
 
 /-- **Math.** **Per-summand assembled form** (step (f) of Petersen Ch 7
@@ -289,22 +295,23 @@ theorem bochner_per_summand_assembled
     [IsManifold I 2 M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f)
     (B W : SmoothVectorField I M) (x : M) :
-    metricInner x
-        (covDeriv HasMetric.metric B.toFun
-          (fun y => covDeriv HasMetric.metric B.toFun (manifoldGradient (I := I) HasMetric.metric f) y) x)
+    g.metricInner x
+        (covDeriv g B.toFun
+          (fun y => covDeriv g B.toFun (manifoldGradient (I := I) g f) y) x)
         (W.toFun x)
-      - metricInner x
-          (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
-            (covDeriv HasMetric.metric B.toFun B.toFun x))
+      - g.metricInner x
+          (covDerivAt g (manifoldGradient (I := I) g f) x
+            (covDeriv g B.toFun B.toFun x))
           (W.toFun x)
-    = metricInner x
-        (riemannCurvature HasMetric.metric B.toFun W.toFun (manifoldGradient (I := I) HasMetric.metric f) x)
+    = g.metricInner x
+        (riemannCurvature g B.toFun W.toFun (manifoldGradient (I := I) g f) x)
         (B.toFun x)
       + (show ℝ from mfderiv I 𝓘(ℝ, ℝ)
-          (fun y : M => hessianBilin (I := I) HasMetric.metric f y (B.toFun y) (B.toFun y))
+          (fun y : M => hessianBilin (I := I) g f y (B.toFun y) (B.toFun y))
           x (W.toFun x))
-      - 2 * hessianBilin (I := I) HasMetric.metric f x (B.toFun x)
-              (covDeriv HasMetric.metric W.toFun B.toFun x) := by
+      - 2 * hessianBilin (I := I) g f x (B.toFun x)
+              (covDeriv g W.toFun B.toFun x) := by
+  subst hg
   classical
   have h_strict : extChartAt I x x ∈ interior (Set.range I) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ]; exact Set.mem_univ _
@@ -316,8 +323,8 @@ theorem bochner_per_summand_assembled
     fun y => covDeriv HasMetric.metric B.toFun gradF.toFun y with hQ_def
   -- Step 1: chain `bochner_per_summand_swap` + `bochner_per_summand_riemann_form`.
   -- Get LHS = R-term + g(LC Q x (W x), B x) - g(LC Gf x (LC B x (W x))) (B x).
-  have h_swap := bochner_per_summand_swap (I := I) f hf B W x
-  have h_riem := bochner_per_summand_riemann_form (I := I) f B W x
+  have h_swap := bochner_per_summand_swap (I := I) HasMetric.metric rfl f hf B W x
+  have h_riem := bochner_per_summand_riemann_form (I := I) HasMetric.metric rfl f B W x
   -- Step 2: third metric compat on (Q, B) along direction W x at x.
   have hQ_smooth : TangentSmoothAt Q x :=
     covDeriv_smoothVF_smoothAt HasMetric.metric B gradF x
@@ -389,21 +396,19 @@ theorem bochner_per_summand_assembled
               ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun B.toFun x (W.toFun x)) :=
     h_compat_QB
   have h_id_LCQW :
-      metricInner x
+      HasMetric.metric.metricInner x
           ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun Q x (W.toFun x))
           (B.toFun x)
         = mf_val - hessianBilin (I := I) HasMetric.metric f x (B.toFun x)
             (covDeriv HasMetric.metric W.toFun B.toFun x) := by
     have h_id_Q_LCBW :
-        metricInner x (Q x)
+        HasMetric.metric.metricInner x (Q x)
             ((leviCivitaConnection (I := I) (M := M) HasMetric.metric).toFun B.toFun x (W.toFun x))
           = hessianBilin (I := I) HasMetric.metric f x (B.toFun x)
               (covDeriv HasMetric.metric W.toFun B.toFun x) := rfl
     linarith [h_compat_QB', h_id_Q_LCBW]
-  -- Identification of the LHS's third term as `hessianBilin (... ) (B x)`,
-  -- folded via h_sym_WB into the `(B x) (...)` form.
   have h_id_LCBW :
-      metricInner x
+      HasMetric.metric.metricInner x
           (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
             (covDeriv HasMetric.metric W.toFun B.toFun x))
           (B.toFun x)
@@ -441,7 +446,8 @@ private lemma hessianBilin_smoothVF_diag_mdifferentiableAt
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f)
     (B : SmoothVectorField I M) (x : M) :
     MDifferentiableAt I 𝓘(ℝ, ℝ)
-      (fun y : M => hessianBilin (I := I) HasMetric.metric f y (B.toFun y) (B.toFun y)) x := by
+      (fun y : M => hessianBilin (I := I) g f y (B.toFun y) (B.toFun y)) x := by
+  subst hg
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
   let gradF : SmoothVectorField I M := ⟨manifoldGradient (I := I) HasMetric.metric f, h_grad⟩
   -- Smoothness of `b ↦ covDerivAt HasMetric.metric ∇f b (B b) = (lcc).toFun ∇f b (B b)`.
@@ -466,12 +472,13 @@ 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) :
-    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
+    g.metricInner x
+          (connectionLaplacian g (manifoldGradient (I := I) g f) x)
+          ((manifoldGradient (I := I) g f) x)
+      = g.metricInner x ((manifoldGradient (I := I) g f) x)
+            ((manifoldGradient (I := I) g (Operators.scalarLaplacian (I := I) g f)) x)
+        + ricciTensor g x ((manifoldGradient (I := I) g f) x) ((manifoldGradient (I := I) g f) x) := by
+  subst hg
   classical
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
   let gradF : SmoothVectorField I M :=
@@ -506,7 +513,7 @@ theorem bochner_connectionLaplacian_grad_decomposition
     rw [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) f hf (Bi i) gradF x
+    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
         (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
@@ -537,17 +544,17 @@ theorem bochner_connectionLaplacian_grad_decomposition
   -- (1) ∑ R-term = Ric(∇f, ∇f).
   have h_R_eq : (∑ i, Rterm i) =
       ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x) (gradF.toFun x) :=
-    heart_curvature_orthonormal_sum_eq_ricci (I := I) HasMetric.metric rfl f hf gradF x
+    heart_curvature_orthonormal_sum_eq_ricci (I := I) (g := HasMetric.metric) (hg := rfl) f hf gradF x
   -- (2) ∑ H-term = 0.
   have h_H_eq : (∑ i, Hterm i) = 0 :=
-    sum_hessianBilin_smoothOrthoFrame_cov_eq_zero (I := I) HasMetric.metric rfl f hf gradF x
+    sum_hessianBilin_smoothOrthoFrame_cov_eq_zero (I := I) (g := HasMetric.metric) (hg := rfl) f hf gradF x
   -- (3) ∑ M-term: factor mfderiv outside, identify inner sum as Δ_g f via Stage 7.
   have h_each_hess_smooth : ∀ i,
       MDifferentiableAt I 𝓘(ℝ, ℝ)
           (fun y : M => hessianBilin (I := I) HasMetric.metric f y ((Bi i).toFun y)
             ((Bi i).toFun y)) x := by
     intro i
-    exact hessianBilin_smoothVF_diag_mdifferentiableAt f hf (Bi i) x
+    exact hessianBilin_smoothVF_diag_mdifferentiableAt HasMetric.metric rfl f hf (Bi i) x
   have h_M_factor :
       (∑ i, Mterm i)
         = (mfderiv I 𝓘(ℝ, ℝ)
@@ -561,7 +568,7 @@ theorem bochner_connectionLaplacian_grad_decomposition
       (fun b : M => ∑ i, hessianBilin (I := I) HasMetric.metric f b ((Bi i).toFun b)
             ((Bi i).toFun b))
         =ᶠ[𝓝 x] (fun b : M => Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric f b) :=
-    sum_hessianBilin_smoothOrthoFrame_eventuallyEq_laplacian (I := I) HasMetric.metric rfl f x
+    sum_hessianBilin_smoothOrthoFrame_eventuallyEq_laplacian (I := I) (g := HasMetric.metric) (hg := rfl) f x
   have h_M_to_lap :
       (mfderiv I 𝓘(ℝ, ℝ)
           (fun b : M => ∑ i, hessianBilin (I := I) HasMetric.metric f b ((Bi i).toFun b)
@@ -594,7 +601,7 @@ theorem bochner_connectionLaplacian_grad_decomposition_g
         + ricciTensor g x (manifoldGradient (I := I) g f x)
                           (manifoldGradient (I := I) g f x) := by
   subst hg
-  exact bochner_connectionLaplacian_grad_decomposition f hf x
+  exact bochner_connectionLaplacian_grad_decomposition HasMetric.metric rfl f hf x
 
 end Operators
 end Riemannian