[9f] Explicit-g: Drop typeclass-dispatch _g notations entirely

[Xinze-Li-Moqian]

Part of umbrella #9. Sub-task 9f — final notation cleanup.

Scope

This is the terminal commit that completes the Mathlib-idiom transition. After 9a–9e, all definitions take explicit `g` and consumer signatures use explicit `g`. The `_g`-style scoped notations still exist as a backward-compat layer that auto-fills `HasMetric.metric`. This sub-issue deletes them and switches all usage to method-call style.

Files affected (every file with `_g` notation usage):

1. OpenGALib/Riemannian/Util/MetricNotation.lean — delete typeclass dispatch (MetricInnerHom, MetricNormSq) and the ⟪⟫_g, ‖²_g notations.
2. OpenGALib/Util/Notation.lean — remove notation-facade entries for deleted notations.
3. Every consumer of ⟪V, W⟫_g, ‖V‖²_g, Ric_g, Riem, Ric, Δ_g, grad_g, Hess_g, II, H_g, scal_g, ∇[X] — mechanical search-replace to method call:
   • ⟪v, w⟫_g → g.metricInner x v w (pointwise) or g.metricInnerSection v w (section form)
   • ‖V‖²_g x → g.metricNormSq x (V x) or g.metricNormSqSection V x
   • Ric_g(v, w) x → g.ricciTensor x v w
   • Δ_g[I] f → g.manifoldLaplacian f
   • grad_g[I] f → g.manifoldGradient f
   • Hess_g[I] f → g.manifoldHessian f
   • ∇[X] Y → g.covDeriv X Y
   • etc.

Estimated effort

~600 LOC of mechanical replacements across ~17 files. Per-file rough counts (from earlier inventory):

File	uses
Bochner/HessianExpansion.lean	26
Bochner/BochnerExpansion.lean	16
Operators/Bochner.lean	13
Bochner/PerSummand.lean	12
Curvature/RicciTensorBundle.lean	8
Operators/Gradient.lean	4
Operators/Hessian.lean	4
GMT/Variation/SecondVariation.lean	3
(others)	1–2 each

Invariant

Math statements identical. Bochner stack 0-sorry. All linters pass.

Acceptance

• Zero ⟪V, W⟫_g, ‖V‖²_g, Ric_g, Δ_g, grad_g, Hess_g, Ric, Riem, II, H_g, scal_g, ∇[X] occurrences remain in code (except possibly in doc strings as math notation).
• MetricInnerHom, MetricNormSq typeclass classes deleted.
• Build clean, sorry count unchanged.
• BG and other consumer signatures match the issue [Umbrella] Explicit-g cascade: drop [HasMetric I M] auto-resolution from Riemannian stack #9 vision:

  (hRic : ∀ x v, ((n-1)*K * g.metricInner x v v ≤ g.ricciTensor x v v))

Dependencies

Requires #18 (9e) merged first.

See also

#9 umbrella · prev: 9e (#18) · closes the umbrella