9f: explicit-g cascade — Tensoriality/RiemannCurvature/bianchi_first + Bochner wrappers (#38)

* 9f Phase 1: lift HessianExpansion + Tensoriality to explicit-g

Lifts the explicit-g cascade through:
- Util/MetricInnerSmoothness: add Riemannian.RiemannianMetric.metricInner_mdifferentiableAt_of_tangentSmoothAt (explicit-g variant of typeclass helper)
- Operators/Bochner/HessianExpansion: full lift to (g : RiemannianMetric I M) section variable; body uses g.metricInner, manifoldGradient g, etc.; ‖grad_g[I] f‖²_g notation expanded inline
- Curvature/Tensoriality: full mass lift with include g; all riemannCurvature_eq_of_X/Y/Z_eq_at, _pointwise_eq, add_first, smul_third/first, eventuallyEq, zero_of_zero theorems now take explicit g; local g shadowing fixed via rename to c
- Curvature/RiemannCurvature: riemannCurvature_antisymm, riemannCurvature_add_third lifted to explicit g; internal callers updated

Consumer fixups:
- Operators/Bochner: pass HasMetric.metric to hessian_gradientNormSq_apply_section; add show cast to bridge ‖V‖²_g notation
- Operators/Bochner/BochnerExpansion: pass HasMetric.metric to riemannCurvature_eq_of_pointwise_eq

Defers to follow-up:
- BochnerExpansion/PerSummand/Bochner.lean full body lift requires lifting ricci_symm, riemannCurvature_inner_self_zero, bianchi_first, SmoothOrthoFrame wrappers (cascade depth ~10+ theorems); separate PR.
- Notation drop and metricInner typeclass abbrev deletion deferred.

* 9f Phase 2: lift bianchi_first + curvature_self chain to explicit-g

Continues the upstream cascade started in Phase 1:
- LeviCivita.bianchi_first lifted; ∇[X] Y / ⟦X, Y⟧ notations expanded inline in body
- RiemannCurvature.mDirDeriv_self_eq_two_metricInner_leviCivita_self lifted
- RiemannCurvature.fun_mDirDeriv_self_eq_two_metricInner_leviCivita_self lifted
- RiemannCurvature.half_mDirDeriv_iterate_eq_metricInner_iterCovDeriv lifted
- RiemannCurvature.riemannCurvature_inner_self_zero lifted (statement: g.metricInner ... = 0; body uses Riem notation in some places — kept where downstream typeclass-form needed)
- RiemannCurvature.riemannCurvature_const_first_swap_eq_neg lifted (uses lifted bianchi_first + antisymm)

ricci_symm intentionally NOT lifted: its proof routes through ⟪·,·⟫_ℝ (= hm.metric.inner via InnerProductSpace instance), so lifting requires either g = hm.metric hypothesis or instance restructuring. Consumers (Bochner) call ricci_symm with implicit typeclass form; works under typical use where g = hm.metric.

riemannCurvature_metric_skew internal callers pass HasMetric.metric to lifted riemannCurvature_inner_self_zero.

* 9f Phase 3: ricci_symm statement explicit, BochnerExpansion caller fix

- ricci_symm statement: Ric(X, Y) notation → explicit ricci HasMetric.metric form (kept typeclass since proof routes through ⟪·,·⟫_ℝ = hm.metric.inner via InnerProductSpace instance — lifting to arbitrary g requires either g = hm.metric hypothesis or trace-without-inner-product refactor)
- BochnerExpansion: riemannCurvature_eq_of_pointwise_eq caller updated to pass HasMetric.metric (matches Tensoriality lift)

* 9f Phase 4: explicit-g wrappers for headline Bochner theorems

Adds explicit-g wrappers for the three public-facing Bochner theorems via subst hg pattern:
- bochner_leibniz_trace_reduction_g (Operators/Bochner.lean)
- bochner_connectionLaplacian_grad_decomposition_g (Operators/Bochner/PerSummand.lean)
- bochner_weitzenboeck_g (Operators/Bochner.lean)

Each wrapper takes (g : RiemannianMetric I M) (hg : g = hm.metric) and discharges via subst hg + typeclass version. Provides explicit-g API surface without requiring lift of internal proof bodies (which depend on ricci_symm + smoothOrthoFrame chain still tied to ⟪·,·⟫_ℝ = hm.metric.inner via InnerProductSpace instance).

End users pass hm.metric for g and rfl for hg to consume.

Author: Xinze-Li-Moqian

OpenGALib/Riemannian/Connection/LeviCivita.lean

@@ -771,8 +771,11 @@ standard $C^2$ textbook setup but fire pointwise.
 
 **Ground truth**: do Carmo 1992 §4 Proposition 2.5 (ii). -/
 theorem bianchi_first
+    (g : RiemannianMetric I M)
     (X Y Z : SmoothVectorField I M) (x : M) :
-    Riem(X, Y) Z x + Riem(Y, Z) X x + Riem(Z, X) Y x = 0 := by
+    riemannCurvature g X.toFun Y.toFun Z.toFun x
+      + riemannCurvature g Y.toFun Z.toFun X.toFun x
+      + riemannCurvature g Z.toFun X.toFun Y.toFun x = 0 := by
   -- Jacobi identity via the `SmoothVectorField.mlieBracket_jacobi` framework
   -- primitive (wraps Mathlib's `leibniz_identity_mlieBracket_apply`).
   have h_jac : (⟦X, ⟦Y, Z⟧⟧) x = (⟦⟦X, Y⟧, Z⟧) x + (⟦Y, ⟦X, Z⟧⟧) x :=
@@ -782,12 +785,12 @@ theorem bianchi_first
   have hX : ∀ y, TangentSmoothAt X.toFun y := X.smoothAt
   have hY : ∀ y, TangentSmoothAt Y.toFun y := Y.smoothAt
   have hZ : ∀ y, TangentSmoothAt Z.toFun y := Z.smoothAt
-  have h_dXZ : ∀ y, TangentSmoothAt ∇[X] Z y :=
-    fun y => covDeriv_smoothVF_smoothAt HasMetric.metric X Z y
-  have h_dYX : ∀ y, TangentSmoothAt ∇[Y] X y :=
-    fun y => covDeriv_smoothVF_smoothAt HasMetric.metric Y X y
-  have h_dZY : ∀ y, TangentSmoothAt ∇[Z] Y y :=
-    fun y => covDeriv_smoothVF_smoothAt HasMetric.metric Z Y y
+  have h_dXZ : ∀ y, TangentSmoothAt (fun y => covDeriv g X.toFun Z.toFun y) y :=
+    fun y => covDeriv_smoothVF_smoothAt g X Z y
+  have h_dYX : ∀ y, TangentSmoothAt (fun y => covDeriv g Y.toFun X.toFun y) y :=
+    fun y => covDeriv_smoothVF_smoothAt g Y X y
+  have h_dZY : ∀ y, TangentSmoothAt (fun y => covDeriv g Z.toFun Y.toFun y) y :=
+    fun y => covDeriv_smoothVF_smoothAt g Z Y y
   have h_XY : ∀ y, TangentSmoothAt ⟦X, Y⟧ y :=
     fun _ => mlieBracket_tangentSmoothAt X.smooth Y.smooth
   have h_YX : ∀ y, TangentSmoothAt ⟦Y, X⟧ y :=
@@ -799,42 +802,45 @@ theorem bianchi_first
   have h_XZ : ∀ y, TangentSmoothAt ⟦X, Z⟧ y :=
     fun _ => mlieBracket_tangentSmoothAt X.smooth Z.smooth
   -- Step 1: section-level torsion-freeness (Π-equalities, via global smoothness).
-  have eq_YZ : (∇[Y] Z : VectorFieldSection I M) = ∇[Z] Y + ⟦Y, Z⟧ :=
-    covDeriv_section_eq_swap_add_mlieBracket HasMetric.metric Y Z hY hZ
-  have eq_ZX : (∇[Z] X : VectorFieldSection I M) = ∇[X] Z + ⟦Z, X⟧ :=
-    covDeriv_section_eq_swap_add_mlieBracket HasMetric.metric Z X hZ hX
-  have eq_XY : (∇[X] Y : VectorFieldSection I M) = ∇[Y] X + ⟦X, Y⟧ :=
-    covDeriv_section_eq_swap_add_mlieBracket HasMetric.metric X Y hX hY
+  have eq_YZ : ((fun y => covDeriv g Y.toFun Z.toFun y) : VectorFieldSection I M)
+      = (fun y => covDeriv g Z.toFun Y.toFun y) + ⟦Y, Z⟧ :=
+    covDeriv_section_eq_swap_add_mlieBracket g Y.toFun Z.toFun hY hZ
+  have eq_ZX : ((fun y => covDeriv g Z.toFun X.toFun y) : VectorFieldSection I M)
+      = (fun y => covDeriv g X.toFun Z.toFun y) + ⟦Z, X⟧ :=
+    covDeriv_section_eq_swap_add_mlieBracket g Z.toFun X.toFun hZ hX
+  have eq_XY : ((fun y => covDeriv g X.toFun Y.toFun y) : VectorFieldSection I M)
+      = (fun y => covDeriv g Y.toFun X.toFun y) + ⟦X, Y⟧ :=
+    covDeriv_section_eq_swap_add_mlieBracket g X.toFun Y.toFun hX hY
   -- Step 2: unfold riemannCurvature, substitute section equalities, split via add_field.
-  show (∇[X] (∇[Y] Z)) x
-        - (∇[Y] (∇[X] Z)) x
-        - (∇[⟦X, Y⟧] Z) x
-      + ((∇[Y] (∇[Z] X)) x
-        - (∇[Z] (∇[Y] X)) x
-        - (∇[⟦Y, Z⟧] X) x)
-      + ((∇[Z] (∇[X] Y)) x
-        - (∇[X] (∇[Z] Y)) x
-        - (∇[⟦Z, X⟧] Y) x) = 0
+  show (covDeriv g X.toFun (fun y => covDeriv g Y.toFun Z.toFun y) x
+        - covDeriv g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) x
+        - covDeriv g (VectorField.mlieBracket I X.toFun Y.toFun) Z.toFun x)
+      + (covDeriv g Y.toFun (fun y => covDeriv g Z.toFun X.toFun y) x
+        - covDeriv g Z.toFun (fun y => covDeriv g Y.toFun X.toFun y) x
+        - covDeriv g (VectorField.mlieBracket I Y.toFun Z.toFun) X.toFun x)
+      + (covDeriv g Z.toFun (fun y => covDeriv g X.toFun Y.toFun y) x
+        - covDeriv g X.toFun (fun y => covDeriv g Z.toFun Y.toFun y) x
+        - covDeriv g (VectorField.mlieBracket I Z.toFun X.toFun) Y.toFun x) = 0
   rw [eq_YZ, eq_ZX, eq_XY]
-  rw [covDeriv_add_field HasMetric.metric X ∇[Z] Y ⟦Y, Z⟧ x
+  rw [covDeriv_add_field g X.toFun (fun y => covDeriv g Z.toFun Y.toFun y) ⟦Y, Z⟧ x
         (h_dZY x) (h_YZ x),
-      covDeriv_add_field HasMetric.metric Y ∇[X] Z ⟦Z, X⟧ x
+      covDeriv_add_field g Y.toFun (fun y => covDeriv g X.toFun Z.toFun y) ⟦Z, X⟧ x
         (h_dXZ x) (h_ZX x),
-      covDeriv_add_field HasMetric.metric Z ∇[Y] X ⟦X, Y⟧ x
+      covDeriv_add_field g Z.toFun (fun y => covDeriv g Y.toFun X.toFun y) ⟦X, Y⟧ x
         (h_dYX x) (h_XY x)]
   -- Step 3: pointwise torsion-free pairings (∇_A B - ∇_B A = [A,B]):
-  have pair_X : (∇[X] ⟦Y, Z⟧) x
-                  - (∇[⟦Y, Z⟧] X) x
+  have pair_X : covDeriv g X.toFun ⟦Y, Z⟧ x
+                  - covDeriv g ⟦Y, Z⟧ X.toFun x
                 = (⟦X, ⟦Y, Z⟧⟧) x :=
-    covDeriv_sub_swap_eq_mlieBracket HasMetric.metric X ⟦Y, Z⟧ x (hX x) (h_YZ x)
-  have pair_Y : (∇[Y] ⟦Z, X⟧) x
-                  - (∇[⟦Z, X⟧] Y) x
+    covDeriv_sub_swap_eq_mlieBracket g X.toFun ⟦Y, Z⟧ x (hX x) (h_YZ x)
+  have pair_Y : covDeriv g Y.toFun ⟦Z, X⟧ x
+                  - covDeriv g ⟦Z, X⟧ Y.toFun x
                 = (⟦Y, ⟦Z, X⟧⟧) x :=
-    covDeriv_sub_swap_eq_mlieBracket HasMetric.metric Y ⟦Z, X⟧ x (hY x) (h_ZX x)
-  have pair_Z : (∇[Z] ⟦X, Y⟧) x
-                  - (∇[⟦X, Y⟧] Z) x
+    covDeriv_sub_swap_eq_mlieBracket g Y.toFun ⟦Z, X⟧ x (hY x) (h_ZX x)
+  have pair_Z : covDeriv g Z.toFun ⟦X, Y⟧ x
+                  - covDeriv g ⟦X, Y⟧ Z.toFun x
                 = (⟦Z, ⟦X, Y⟧⟧) x :=
-    covDeriv_sub_swap_eq_mlieBracket HasMetric.metric Z ⟦X, Y⟧ x (hZ x) (h_XY x)
+    covDeriv_sub_swap_eq_mlieBracket g Z.toFun ⟦X, Y⟧ x (hZ x) (h_XY x)
   -- Step 4: rearrange so abel collapses all 12 cov-terms via pair_X/Y/Z.
   -- The goal after rewrites is (with shorthand):
   --   (∇_X∇_Z Y + ∇_X[Y,Z]) - ∇_Y∇_X Z - ∇_{[X,Y]} Z
@@ -845,17 +851,17 @@ theorem bianchi_first
   -- We rewrite using pair_X/Y/Z by isolating the LHS shapes.
   -- pair_X gives ∇_X[Y,Z] = pair_X.lhs.lhs ↦ … — to use pair_X as a substitution,
   -- we set up the equations as A = mlie + B and rewrite ∇_X[Y,Z] = mlie + ∇_{[Y,Z]} X:
-  have h_subX : (∇[X] ⟦Y, Z⟧) x
+  have h_subX : covDeriv g X.toFun ⟦Y, Z⟧ x
                   = (⟦X, ⟦Y, Z⟧⟧) x
-                    + (∇[⟦Y, Z⟧] X) x := by
+                    + covDeriv g ⟦Y, Z⟧ X.toFun x := by
     rw [← pair_X]; abel
-  have h_subY : (∇[Y] ⟦Z, X⟧) x
+  have h_subY : covDeriv g Y.toFun ⟦Z, X⟧ x
                   = (⟦Y, ⟦Z, X⟧⟧) x
-                    + (∇[⟦Z, X⟧] Y) x := by
+                    + covDeriv g ⟦Z, X⟧ Y.toFun x := by
     rw [← pair_Y]; abel
-  have h_subZ : (∇[Z] ⟦X, Y⟧) x
+  have h_subZ : covDeriv g Z.toFun ⟦X, Y⟧ x
                   = (⟦Z, ⟦X, Y⟧⟧) x
-                    + (∇[⟦X, Y⟧] Z) x := by
+                    + covDeriv g ⟦X, Y⟧ Z.toFun x := by
     rw [← pair_Z]; abel
   rw [h_subX, h_subY, h_subZ]
   -- Goal now has 3 outer-bracket terms + 6 ∇_·_ terms; three pairs of ∇_{[·,·]} ·