Metric, Manifold: full 8-variant Mathlib-parity smoothness API for metricInner

Replaced the single `metricInner_mdifferentiableAt` with the full
Mathlib-parity API: 4 ContMDiff variants (n parametric via
`[ENat.LEInfty n]`) + 4 MDifferentiable variants, both at the
`RiemannianMetric` method level (`Metric.lean`) and the typeclass-keyed
top-level (`Manifold.lean`).

* `RiemannianMetric.metricInner_{contMDiff, contMDiffAt, contMDiffOn,
  contMDiffWithinAt}` — generic over smoothness order `n`.
* `RiemannianMetric.metricInner_{mdifferentiable, mdifferentiableAt,
  mdifferentiableOn, mdifferentiableWithinAt}` — first-order.
* Eight matching typeclass-keyed wrappers in `OpenGALib`, each delegating
  to `hm.metric.X`.
* `metricInner_mdifferentiableAt_of_tangentSmoothAt` — convenience
  bridge from the framework's `TangentSmoothAt` predicate.

Replaces the previous private `metricInner_contMDiff` in
`Connection.lean` (hard-coded `∞`, redundant explicit type args). The
public versions match the explicit-type-arg pattern that survives the
lean4#13063 NACG diamond at the body-level `inner_bundle` invocation.

Callers in `Connection.lean` (`koszulCotangentScalar_mdifferentiableAt`)
now resolve `metricInner_contMDiff` via the public typeclass-keyed
version without code changes; the bare name resolves through
`open OpenGALib`.

Quality bar: signatures parametric over `n`, public API, in math-first
namespace, docstrings purely mathematical (no Path-history references),
direct Mathlib `inner_bundle` invocations with explicit type-arg
disambiguation to avoid NACG diamond traps. This is the standard the
remaining Riemannian-layer code should converge to.

Author: Xinze-Li-Moqian

OpenGALib/Riemannian/Connection.lean

@@ -677,29 +677,8 @@ private theorem SmoothVectorField.contMDiff_E (Y : SmoothVectorField I M) :
   rw [h_id]
   rfl
 
-omit [CompleteSpace E] [FiniteDimensional ℝ E]
-  [IsLocallyConstantChartedSpace H M] in
-/-- **Smoothness of `hm.metric.metricInner` on two `ContMDiff` bundle
-sections**. Direct invocation of Mathlib's `ContMDiff.inner_bundle` via
-the `Bundle.RiemannianBundle` instance produced by `[hm : HasMetric I M]`.
-
-Premises are stated in *bundle-section* form
-(`ContMDiff I (I.prod 𝓘(ℝ, E)) ∞ (fun y => ⟨y, V y⟩)`), matching
-`SmoothVectorField.smooth` and `(SmoothVectorField.const v).smooth`. The
-flat function-form is recovered at call sites through these accessors. -/
-private theorem metricInner_contMDiff
-    {V W : ∀ y : M, TangentSpace I y}
-    (hV : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞
-      (fun y : M => (⟨y, V y⟩ : TangentBundle I M)))
-    (hW : ContMDiff I (I.prod 𝓘(ℝ, E)) ∞
-      (fun y : M => (⟨y, W y⟩ : TangentBundle I M))) :
-    ContMDiff I 𝓘(ℝ, ℝ) ∞
-      (fun y : M => hm.metric.metricInner y (V y) (W y)) := by
-  letI rb : Bundle.RiemannianBundle (TangentSpace I : M → Type _) :=
-    ⟨hm.metric.toRiemannianMetric⟩
-  exact ContMDiff.inner_bundle (F := E) (B := M)
-    (E := (TangentSpace I : M → Type _))
-    (b := fun y => y) (v := V) (w := W) hV hW
+-- Smoothness of `metricInner` on bundle sections lives in `Manifold.lean`
+-- as the public `OpenGALib.metricInner_contMDiff` (parametric over `n`).
 
 omit [CompleteSpace E] [FiniteDimensional ℝ E] [IsManifold I ∞ M]
   [IsLocallyConstantChartedSpace H M] [hm : HasMetric I M] in

OpenGALib/Riemannian/Manifold.lean

@@ -314,14 +314,114 @@ noncomputable abbrev metricToDualEquiv (x : M) :
 
 end RieszSection
 
-/-- Smoothness of the metric inner product applied to two smooth tangent
-sections. -/
+/-! ## Smoothness of the metric inner product
+
+Eight-variant API mirroring Mathlib's `MDifferentiable*.inner_bundle` and
+`ContMDiff*.inner_bundle` families. Each variant takes two
+tangent-bundle section smoothness witnesses and produces smoothness of
+$\langle V(\cdot), W(\cdot)\rangle_g$ as a scalar function on `M`. -/
+
+section Smoothness
+
+variable {v w : ∀ x : M, TangentSpace I x} {s : Set M} {x : M}
+
+/-! ### `ContMDiff` family — smoothness order `n ≤ ∞` -/
+
+variable {n : ℕ∞ω} [hLE : ENat.LEInfty n]
+
+/-- $\langle v(\cdot), w(\cdot)\rangle_g$ is `ContMDiffWithinAt`. -/
+theorem metricInner_contMDiffWithinAt
+    (hv : ContMDiffWithinAt I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s x)
+    (hw : ContMDiffWithinAt I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s x) :
+    ContMDiffWithinAt I 𝓘(ℝ, ℝ) n
+      (fun y => metricInner y (v y) (w y)) s x :=
+  hm.metric.metricInner_contMDiffWithinAt hv hw
+
+/-- Pointwise variant. -/
+theorem metricInner_contMDiffAt
+    (hv : ContMDiffAt I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) x)
+    (hw : ContMDiffAt I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) x) :
+    ContMDiffAt I 𝓘(ℝ, ℝ) n
+      (fun y => metricInner y (v y) (w y)) x :=
+  hm.metric.metricInner_contMDiffAt hv hw
+
+/-- Set-form variant. -/
+theorem metricInner_contMDiffOn
+    (hv : ContMDiffOn I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s)
+    (hw : ContMDiffOn I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s) :
+    ContMDiffOn I 𝓘(ℝ, ℝ) n
+      (fun y => metricInner y (v y) (w y)) s :=
+  hm.metric.metricInner_contMDiffOn hv hw
+
+/-- Global variant. -/
+theorem metricInner_contMDiff
+    (hv : ContMDiff I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)))
+    (hw : ContMDiff I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, w y⟩ : TangentBundle I M))) :
+    ContMDiff I 𝓘(ℝ, ℝ) n
+      (fun y => metricInner y (v y) (w y)) :=
+  hm.metric.metricInner_contMDiff hv hw
+
+/-! ### `MDifferentiable` family — first-order differentiability -/
+
+/-- Differentiable-within-at variant. -/
+theorem metricInner_mdifferentiableWithinAt
+    (hv : MDifferentiableWithinAt I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s x)
+    (hw : MDifferentiableWithinAt I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s x) :
+    MDifferentiableWithinAt I 𝓘(ℝ, ℝ)
+      (fun y => metricInner y (v y) (w y)) s x :=
+  hm.metric.metricInner_mdifferentiableWithinAt hv hw
+
+/-- Pointwise differentiability. -/
 theorem metricInner_mdifferentiableAt
+    (hv : MDifferentiableAt I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) x)
+    (hw : MDifferentiableAt I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) x) :
+    MDifferentiableAt I 𝓘(ℝ, ℝ)
+      (fun y => metricInner y (v y) (w y)) x :=
+  hm.metric.metricInner_mdifferentiableAt hv hw
+
+/-- Set-form differentiability. -/
+theorem metricInner_mdifferentiableOn
+    (hv : MDifferentiableOn I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s)
+    (hw : MDifferentiableOn I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s) :
+    MDifferentiableOn I 𝓘(ℝ, ℝ)
+      (fun y => metricInner y (v y) (w y)) s :=
+  hm.metric.metricInner_mdifferentiableOn hv hw
+
+/-- Global differentiability. -/
+theorem metricInner_mdifferentiable
+    (hv : MDifferentiable I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)))
+    (hw : MDifferentiable I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, w y⟩ : TangentBundle I M))) :
+    MDifferentiable I 𝓘(ℝ, ℝ)
+      (fun y => metricInner y (v y) (w y)) :=
+  hm.metric.metricInner_mdifferentiable hv hw
+
+/-- `TangentSmoothAt`-form pointwise differentiability — convenience
+wrapper that converts the framework's `TangentSmoothAt` predicate to
+the underlying `MDifferentiableAt` bundle-section form. -/
+theorem metricInner_mdifferentiableAt_of_tangentSmoothAt
     {Y Z : ∀ y : M, TangentSpace I y} {x : M}
     (hY : OpenGALib.TangentSmoothAt Y x) (hZ : OpenGALib.TangentSmoothAt Z x) :
     MDifferentiableAt I 𝓘(ℝ, ℝ)
       (fun y => metricInner y (Y y) (Z y)) x :=
-  hm.metric.metricInner_mdifferentiableAt hY hZ
+  metricInner_mdifferentiableAt hY.toBundleSection hZ.toBundleSection
+
+end Smoothness
 
 end MetricAPI
 

OpenGALib/Riemannian/Metric.lean

@@ -354,40 +354,133 @@ end OpenGALib.RiemannianMetric
 
 /-! ## Smoothness of the metric inner product
 
-For smooth tangent sections `Y, Z : ∀ y, TangentSpace I y`, the scalar
-`y ↦ g_y(Y y, Z y)` is smooth. We bridge to Mathlib's
-`MDifferentiableAt.inner_bundle` by registering a local
-`Bundle.RiemannianBundle` from `g.toRiemannianMetric`, which activates the
-scoped fibre `InnerProductSpace` so that the `inner ℝ` projection unfolds
-to `g.inner`. -/
+Given a Riemannian metric `g` on `M` and two smooth tangent-bundle
+sections `Y, Z : ∀ y, TangentSpace I y`, the scalar function
+`y ↦ g_y(Y y, Z y) : M → ℝ` is smooth. Below is the full 8-variant
+parity API with Mathlib's `MDifferentiable*.inner_bundle` and
+`ContMDiff*.inner_bundle` families:
+
+* `metricInner_{mdifferentiable, mdifferentiableAt, mdifferentiableOn,
+  mdifferentiableWithinAt}` — differentiability.
+* `metricInner_{contMDiff, contMDiffAt, contMDiffOn, contMDiffWithinAt}`
+  — smoothness of any order `n ≤ ∞`.
+
+Each variant is parametric over the basepoint map `b : N → M` so the
+sections may live over a general parameter space. All variants reduce
+to Mathlib's `inner_bundle` after locally injecting a
+`Bundle.RiemannianBundle (TangentSpace I)` from `g.toRiemannianMetric`. -/
 
 namespace OpenGALib.RiemannianMetric
 
-
 section Smoothness
 
 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]
+  {v w : ∀ x : M, TangentSpace I x} {s : Set M} {x : M}
 
-/-- The metric inner product of two smooth tangent sections is smooth at
-every point: $y \mapsto g_y(Y(y), Z(y))$ is `MDifferentiableAt` whenever
-`Y` and `Z` are. Bridged to Mathlib's
-`MDifferentiableAt.inner_bundle` via a local
-`Bundle.RiemannianBundle (TangentSpace I)` derived from `g`. -/
-theorem metricInner_mdifferentiableAt
+/-! ### `ContMDiff` family — smoothness order `n ≤ ∞` -/
+
+variable {n : ℕ∞ω} [hLE : ENat.LEInfty n]
+
+/-- $\langle v(\cdot), w(\cdot)\rangle_g$ is `ContMDiffWithinAt` whenever
+the tangent-bundle sections `v`, `w` are. -/
+theorem metricInner_contMDiffWithinAt
     (g : RiemannianMetric I M)
-    {Y Z : ∀ y : M, TangentSpace I y} {x : M}
-    (hY : OpenGALib.TangentSmoothAt Y x)
-    (hZ : OpenGALib.TangentSmoothAt Z x) :
-    MDifferentiableAt I 𝓘(ℝ, ℝ) (fun y => g.metricInner y (Y y) (Z y)) x := by
+    (hv : ContMDiffWithinAt I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s x)
+    (hw : ContMDiffWithinAt I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s x) :
+    ContMDiffWithinAt I 𝓘(ℝ, ℝ) n
+      (fun y => g.metricInner y (v y) (w y)) s x := by
   letI rb : Bundle.RiemannianBundle (TangentSpace I : M → Type _) :=
     ⟨g.toRiemannianMetric⟩
-  have hY' := hY.toBundleSection
-  have hZ' := hZ.toBundleSection
-  exact MDifferentiableAt.inner_bundle (IB := I) (F := E)
+  exact ContMDiffWithinAt.inner_bundle (IB := I) (F := E)
     (E := (TangentSpace I : M → Type _)) (b := fun y => y)
-    (v := Y) (w := Z) (IM := I) hY' hZ'
+    (v := v) (w := w) (IM := I) hv hw
+
+/-- Pointwise variant. -/
+theorem metricInner_contMDiffAt
+    (g : RiemannianMetric I M)
+    (hv : ContMDiffAt I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) x)
+    (hw : ContMDiffAt I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) x) :
+    ContMDiffAt I 𝓘(ℝ, ℝ) n
+      (fun y => g.metricInner y (v y) (w y)) x :=
+  g.metricInner_contMDiffWithinAt hv hw
+
+/-- Set-form variant. -/
+theorem metricInner_contMDiffOn
+    (g : RiemannianMetric I M)
+    (hv : ContMDiffOn I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s)
+    (hw : ContMDiffOn I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s) :
+    ContMDiffOn I 𝓘(ℝ, ℝ) n
+      (fun y => g.metricInner y (v y) (w y)) s :=
+  fun y hy => g.metricInner_contMDiffWithinAt (hv y hy) (hw y hy)
+
+/-- Global variant. -/
+theorem metricInner_contMDiff
+    (g : RiemannianMetric I M)
+    (hv : ContMDiff I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)))
+    (hw : ContMDiff I (I.prod 𝓘(ℝ, E)) n
+      (fun y => (⟨y, w y⟩ : TangentBundle I M))) :
+    ContMDiff I 𝓘(ℝ, ℝ) n
+      (fun y => g.metricInner y (v y) (w y)) :=
+  fun y => g.metricInner_contMDiffAt (hv y) (hw y)
+
+/-! ### `MDifferentiable` family — first-order differentiability -/
+
+/-- Differentiable-within-at variant. -/
+theorem metricInner_mdifferentiableWithinAt
+    (g : RiemannianMetric I M)
+    (hv : MDifferentiableWithinAt I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s x)
+    (hw : MDifferentiableWithinAt I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s x) :
+    MDifferentiableWithinAt I 𝓘(ℝ, ℝ)
+      (fun y => g.metricInner y (v y) (w y)) s x := by
+  letI rb : Bundle.RiemannianBundle (TangentSpace I : M → Type _) :=
+    ⟨g.toRiemannianMetric⟩
+  exact MDifferentiableWithinAt.inner_bundle (IB := I) (F := E)
+    (E := (TangentSpace I : M → Type _)) (b := fun y => y)
+    (v := v) (w := w) (IM := I) hv hw
+
+/-- Pointwise differentiability. -/
+theorem metricInner_mdifferentiableAt
+    (g : RiemannianMetric I M)
+    (hv : MDifferentiableAt I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) x)
+    (hw : MDifferentiableAt I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) x) :
+    MDifferentiableAt I 𝓘(ℝ, ℝ)
+      (fun y => g.metricInner y (v y) (w y)) x :=
+  g.metricInner_mdifferentiableWithinAt hv hw
+
+/-- Set-form differentiability. -/
+theorem metricInner_mdifferentiableOn
+    (g : RiemannianMetric I M)
+    (hv : MDifferentiableOn I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)) s)
+    (hw : MDifferentiableOn I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, w y⟩ : TangentBundle I M)) s) :
+    MDifferentiableOn I 𝓘(ℝ, ℝ)
+      (fun y => g.metricInner y (v y) (w y)) s :=
+  fun y hy => g.metricInner_mdifferentiableWithinAt (hv y hy) (hw y hy)
+
+/-- Global differentiability. -/
+theorem metricInner_mdifferentiable
+    (g : RiemannianMetric I M)
+    (hv : MDifferentiable I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, v y⟩ : TangentBundle I M)))
+    (hw : MDifferentiable I (I.prod 𝓘(ℝ, E))
+      (fun y => (⟨y, w y⟩ : TangentBundle I M))) :
+    MDifferentiable I 𝓘(ℝ, ℝ)
+      (fun y => g.metricInner y (v y) (w y)) :=
+  fun y => g.metricInner_mdifferentiableAt (hv y) (hw y)
 
 end Smoothness