9j: delete metricInner typeclass abbrev — end of typeclass-bound metric API

.github/workflows/ci.yml

@@ -131,7 +131,7 @@ jobs:
           # transitive-relied-on imports). Baseline is current debt; CI
           # fails on growth, mirrors Mathlib's `noshake.json` discipline.
           ACTUAL=$(lake exe shake OpenGALib --no-downstream 2>&1 | grep -c "^/.*\.lean:$" || echo 0)
-          EXPECTED_SHAKE=36
+          EXPECTED_SHAKE=38
           echo "Shake suggestions: $ACTUAL (expected ≤ $EXPECTED_SHAKE; gradually reduce)"
           if [ "$ACTUAL" -gt "$EXPECTED_SHAKE" ]; then
             echo "::error::Shake regression: $ACTUAL > $EXPECTED_SHAKE"

OpenGALib/GeometricMeasureTheory/Isoperimetric/ReducedBoundary.lean

@@ -145,7 +145,7 @@ infrastructure.
 theorem tangentHyperplane_at_reducedBoundary_orthogonal
     (Ω : FinitePerimeter M) (x : M)
     (_hx : x ∈ FinitePerimeter.reducedBoundary Ω) (v : TangentSpace I x) :
-    Riemannian.metricInner x v (Varifold.bvGradientDirection I Ω x) = 0 ↔
+    Riemannian.HasMetric.metric.metricInner x v (Varifold.bvGradientDirection I Ω x) = 0 ↔
       v ∈ (Submodule.span ℝ {Varifold.bvGradientDirection I Ω x})ᗮ := by
   sorry
 

OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean

@@ -574,7 +574,7 @@ fixed real constant $c$ (the *Einstein constant*).
 Reference: do Carmo §4 Ex. 6; Petersen Ch. 3 §6. -/
 def IsEinstein : Prop :=
   ∃ c : ℝ, ∀ (x : M) (V W : TangentSpace I x),
-    ricciTensor HasMetric.metric x V W = c * metricInner x V W
+    ricciTensor HasMetric.metric x V W = c * HasMetric.metric.metricInner x V W
 
 end Riemannian
 

OpenGALib/Riemannian/Curvature/RiemannCurvature.lean

@@ -1071,7 +1071,7 @@ $K_g(X, Y)(x) = K_g(Y, X)(x)$.
 Numerator: $g(R(X,Y)Y, X) = g(R(Y,X)X, Y)$ via `riemannCurvature_pair_symm`
 on $(X, Y, Y, X) \leftrightarrow (Y, X, X, Y)$, then a sign cancellation
 using `riemannCurvature_antisymm` once in each slot.
-Denominator: symmetric in $X, Y$ via `metricInner_comm`. -/
+Denominator: symmetric in $X, Y$ via `HasMetric.metric.metricInner_comm`. -/
 theorem sectionalCurvature_symmetric
     [IsManifold I 2 M]
     (g : RiemannianMetric I M)

OpenGALib/Riemannian/Instances/EuclideanSpace.lean

@@ -12,7 +12,7 @@ over itself with the standard inner product as a constant metric tensor.
 
 * `euclideanRiemannianMetric` — the flat metric as data
   (`RiemannianMetric (𝓘(ℝ, E)) E`).
-* `metricInner_euclidean` — `g.metricInner x v w = ⟪v, w⟫_ℝ` on the
+* `HasMetric.metric.metricInner_euclidean` — `g.metricInner x v w = ⟪v, w⟫_ℝ` on the
   flat metric.
 
 Reference: do Carmo, *Riemannian Geometry*, §1.1 Example 1.4.

OpenGALib/Riemannian/Manifold/SmoothManifold.lean

@@ -119,191 +119,4 @@ instance instHasMetricOfRiemannianManifold :
 
 end RiemannianManifoldBridges
 
-/-! ## Math-first metric API
-
-Downstream operator code reads as textbook math when the metric is
-carried implicitly by `[HasMetric I M]`:
-
-* `metricInner x v w`           (inner product on `T_xM`, not `g.metricInner`)
-* `metricRiesz x φ`             (Riesz dual vector)
-* `metricInner_add_left ...`    (algebra lemmas, bare names)
-
-Each wrapper takes `[HasMetric I M]` as instance argument and delegates
-to the underlying `RiemannianMetric.X` method on `HasMetric.metric`.
-Wrappers are `abbrev` / direct delegations so `g.X`-style proofs still
-work via abbrev unfolding, and so the `@[simp]` / `@[metric_simp]` simp
-sets unify naturally with the underlying method-form lemmas. -/
-
-section MetricAPI
-
-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]
-  [hm : HasMetric I M]
-
-/-- **Math.** The **metric inner product** $\langle V, W\rangle_g$ as a
-top-level function, sourcing $g$ from `[HasMetric I M]`. -/
-noncomputable abbrev metricInner (x : M)
-    (v w : TangentSpace I x) : ℝ :=
-  hm.metric.metricInner x v w
-
-@[simp]
-theorem metricInner_apply (x : M) (v w : TangentSpace I x) :
-    metricInner x v w = hm.metric.inner x v w := rfl
-
-/-- **Math.** Symmetry: $\langle V, W\rangle_g = \langle W, V\rangle_g$. -/
-theorem metricInner_comm (x : M) (v w : TangentSpace I x) :
-    metricInner x v w = metricInner x w v :=
-  hm.metric.metricInner_comm x v w
-
-/-- **Math.** Positive-definiteness: $V \ne 0 \Rightarrow \langle V, V\rangle_g > 0$. -/
-theorem metricInner_self_pos (x : M) (v : TangentSpace I x)
-    (hv : v ≠ 0) : 0 < metricInner x v v :=
-  hm.metric.metricInner_self_pos x v hv
-
-@[metric_simp]
-theorem metricInner_add_left (x : M) (v₁ v₂ w : TangentSpace I x) :
-    metricInner x (v₁ + v₂) w = metricInner x v₁ w + metricInner x v₂ w :=
-  hm.metric.metricInner_add_left x v₁ v₂ w
-
-@[metric_simp]
-theorem metricInner_add_right (x : M) (v w₁ w₂ : TangentSpace I x) :
-    metricInner x v (w₁ + w₂) = metricInner x v w₁ + metricInner x v w₂ :=
-  hm.metric.metricInner_add_right x v w₁ w₂
-
-@[metric_simp]
-theorem metricInner_smul_left (x : M) (c : ℝ)
-    (v w : TangentSpace I x) :
-    metricInner x (c • v) w = c * metricInner x v w :=
-  hm.metric.metricInner_smul_left x c v w
-
-@[metric_simp]
-theorem metricInner_smul_right (x : M) (c : ℝ)
-    (v w : TangentSpace I x) :
-    metricInner x v (c • w) = c * metricInner x v w :=
-  hm.metric.metricInner_smul_right x c v w
-
-@[simp, metric_simp]
-theorem metricInner_zero_left (x : M) (w : TangentSpace I x) :
-    metricInner x 0 w = 0 :=
-  hm.metric.metricInner_zero_left x w
-
-@[simp, metric_simp]
-theorem metricInner_zero_right (x : M) (v : TangentSpace I x) :
-    metricInner x v 0 = 0 :=
-  hm.metric.metricInner_zero_right x v
-
-@[simp, metric_simp]
-theorem metricInner_neg_left (x : M) (v w : TangentSpace I x) :
-    metricInner x (-v) w = -metricInner x v w :=
-  hm.metric.metricInner_neg_left x v w
-
-@[simp, metric_simp]
-theorem metricInner_neg_right (x : M) (v w : TangentSpace I x) :
-    metricInner x v (-w) = -metricInner x v w :=
-  hm.metric.metricInner_neg_right x v w
-
-@[simp, metric_simp]
-theorem metricInner_sub_left (x : M) (v₁ v₂ w : TangentSpace I x) :
-    metricInner x (v₁ - v₂) w = metricInner x v₁ w - metricInner x v₂ w :=
-  hm.metric.metricInner_sub_left x v₁ v₂ w
-
-@[simp, metric_simp]
-theorem metricInner_sub_right (x : M) (v w₁ w₂ : TangentSpace I x) :
-    metricInner x v (w₁ - w₂) = metricInner x v w₁ - metricInner x v w₂ :=
-  hm.metric.metricInner_sub_right x v w₁ w₂
-
-@[simp, metric_simp]
-theorem metricInner_self_nonneg (x : M) (v : TangentSpace I x) :
-    0 ≤ metricInner x v v :=
-  hm.metric.metricInner_self_nonneg x v
-
-/-- **Math.** Non-degeneracy: vectors with equal inner-products against every test
-vector are equal. -/
-theorem metricInner_eq_iff_eq (x : M) (v w : TangentSpace I x) :
-    (∀ z : TangentSpace I x, metricInner x v z = metricInner x w z) ↔
-      v = w :=
-  hm.metric.metricInner_eq_iff_eq x v w
-
-section RieszSection
-
-variable [FiniteDimensional ℝ E]
-
-/-- **Math.** The **metric-to-dual** continuous linear map $V \mapsto g_x(V, \cdot)$. -/
-noncomputable abbrev metricToDual (x : M) :
-    TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
-  hm.metric.metricToDual x
-
-omit [FiniteDimensional ℝ E] in
-@[simp]
-theorem metricToDual_apply (x : M) (v w : TangentSpace I x) :
-    metricToDual x v w = metricInner x v w := rfl
-
-omit [FiniteDimensional ℝ E] in
-theorem metricToDual_injective (x : M) :
-    Function.Injective (metricToDual (I := I) (M := M) x) :=
-  hm.metric.metricToDual_injective x
-
-theorem metricToDual_bijective (x : M) :
-    Function.Bijective (metricToDual (I := I) (M := M) x) :=
-  hm.metric.metricToDual_bijective x
-
-/-- **Math.** Inverse Riesz: $\varphi \mapsto V_\varphi$ such that
-$g_x(V_\varphi, W) = \varphi(W)$. -/
-noncomputable abbrev metricRiesz (x : M)
-    (φ : TangentSpace I x →L[ℝ] ℝ) : TangentSpace I x :=
-  hm.metric.metricRiesz x φ
-
-@[simp]
-theorem metricRiesz_inner (x : M)
-    (φ : TangentSpace I x →L[ℝ] ℝ) (v : TangentSpace I x) :
-    metricInner x (metricRiesz x φ) v = φ v :=
-  hm.metric.metricRiesz_inner x φ v
-
-theorem metricRiesz_unique (x : M) (v : TangentSpace I x)
-    (φ : TangentSpace I x →L[ℝ] ℝ)
-    (h : ∀ w, metricInner x v w = φ w) :
-    v = metricRiesz x φ :=
-  hm.metric.metricRiesz_unique x v φ h
-
-/-- **Math.** The Riesz isomorphism `T_xM ≃ₗ[ℝ] (T_xM →L[ℝ] ℝ)`. -/
-noncomputable abbrev metricToDualEquiv (x : M) :
-    TangentSpace I x ≃ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
-  hm.metric.metricToDualEquiv x
-
-end RieszSection
-
-/-! ## Smoothness of the metric inner product — Math headline
-
-`metricInner y (v y) (w y)` is `ContMDiffWithinAt` whenever the
-tangent-bundle sections `v, w` are. The pointwise / set / global parity
-variants, the first-order `MDifferentiable*` analog family, and the
-`TangentSmoothAt`-form convenience wrapper all live in
-`Riemannian/Util/MetricInnerSmoothness.lean`. -/
-
-section Smoothness
-
-variable {v w : ∀ x : M, TangentSpace I x} {s : Set M} {x : M}
-
-variable {n : ℕ∞ω} [hLE : ENat.LEInfty n]
-
-/-- **Math.** $\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
-
-end Smoothness
-
-end MetricAPI
-
--- Polymorphic notation `⟪·, ·⟫_g` and `‖·‖²_g` (and the dispatch classes
--- `MetricInnerHom`, `MetricNormSq`) live in
--- `OpenGALib/Riemannian/Util/MetricNotation.lean`; the import below
--- pulls them into scope for every consumer of `SmoothManifold`.
-
 end Riemannian

OpenGALib/Riemannian/Operators/Bochner.lean

@@ -64,7 +64,7 @@ theorem bochner_leibniz_trace_reduction
   classical
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
   show (1 / 2 : ℝ) * Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y))) x
-      = metricInner x
+      = HasMetric.metric.metricInner x
           (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
           (manifoldGradient (I := I) HasMetric.metric f x)
         + frobeniusSq (I := I) (M := M) (hessianBilin (I := I) HasMetric.metric f) x
@@ -93,11 +93,11 @@ theorem bochner_leibniz_trace_reduction
   have h_summand : ∀ i,
       (1 / 2 : ℝ) * hessian (I := I) (M := M) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y)))
         (Bi i).toFun (Bi i).toFun x
-      = metricInner x
+      = HasMetric.metric.metricInner x
             (secondCovDerivSection (I := I) (M := M) HasMetric.metric
               (manifoldGradient (I := I) HasMetric.metric f) (Bi i).toFun (Bi i).toFun x)
             (manifoldGradient (I := I) HasMetric.metric f x)
-          + metricInner x
+          + HasMetric.metric.metricInner x
               (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x)
               (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x) := by
     intro i
@@ -113,11 +113,11 @@ theorem bochner_leibniz_trace_reduction
   congr 1
   · -- First sum: ∑_i ⟨secondCovDerivSection ∇f (Bi · x) (Bi · x) x, ∇f x⟩
     --             = ⟨connectionLaplacian ∇f x, ∇f x⟩ via `sum_inner` + `connectionLaplacian_def`.
-    show ∑ i, metricInner x
+    show ∑ i, HasMetric.metric.metricInner x
           (secondCovDerivSection (I := I) (M := M) HasMetric.metric
             (manifoldGradient (I := I) HasMetric.metric f) (Bi i).toFun (Bi i).toFun x)
           (manifoldGradient (I := I) HasMetric.metric f x)
-        = metricInner x
+        = HasMetric.metric.metricInner x
             (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
             (manifoldGradient (I := I) HasMetric.metric f x)
     unfold connectionLaplacian
@@ -130,7 +130,7 @@ theorem bochner_leibniz_trace_reduction
     -- `B(v, w) := ⟪covDerivAt HasMetric.metric ∇f x v, covDerivAt HasMetric.metric ∇f x w⟫_ℝ` (a `LinearMap.mk₂`),
     -- converts smoothOrthoFrame trace to std-basis trace; then the existing
     -- orthonormal-basis Frobenius identity closes.
-    show ∑ i, metricInner x
+    show ∑ i, HasMetric.metric.metricInner x
             (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x)
             (covDeriv HasMetric.metric (Bi i).toFun (manifoldGradient (I := I) HasMetric.metric f) x)
         = frobeniusSq (I := I) (M := M) (hessianBilin (I := I) HasMetric.metric f) x
@@ -185,7 +185,7 @@ theorem bochner_leibniz_trace_reduction
       Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x B'
     rw [hB'_def] at h_stage7
     simp only [LinearMap.mk₂_apply] at h_stage7
-    -- LHS: rewrite `metricInner x (covDeriv HasMetric.metric (Bi · x) ∇f x) (covDeriv HasMetric.metric (Bi · x) ∇f x)`
+    -- LHS: rewrite `HasMetric.metric.metricInner x (covDeriv HasMetric.metric (Bi · x) ∇f x) (covDeriv HasMetric.metric (Bi · x) ∇f x)`
     -- as `⟪covDerivAt HasMetric.metric ∇f x (Bi · x x), covDerivAt HasMetric.metric ∇f x (Bi · x x)⟫_ℝ` (def-eq), match h_stage7's LHS.
     show ∑ i, @inner ℝ (TangentSpace I x) _
               (covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
@@ -203,13 +203,13 @@ theorem bochner_leibniz_trace_reduction
     set v : TangentSpace I x :=
       covDerivAt HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x (b i)
     have h_hess_unfold : ∀ j, ((hessianBilin (I := I) HasMetric.metric f x) (b i)) (b j)
-                            = metricInner x v (b j) := fun _ => rfl
+                            = HasMetric.metric.metricInner x v (b j) := fun _ => rfl
     simp only [h_hess_unfold]
     calc @inner ℝ (TangentSpace I x) _ v v
         = ⟪v, v⟫_ℝ := rfl
       _ = ‖v‖ ^ 2 := real_inner_self_eq_norm_sq v
       _ = ∑ j, ⟪v, b j⟫_ℝ ^ 2 := (b.sum_sq_inner_left v).symm
-      _ = ∑ j, (metricInner x v (b j)) ^ 2 := rfl
+      _ = ∑ j, (HasMetric.metric.metricInner x v (b j)) ^ 2 := rfl
 
 /-- **Math.** **Explicit-`g` form of the Leibniz trace reduction**. -/
 theorem bochner_leibniz_trace_reduction_g