[Umbrella] Explicit-g cascade: drop [HasMetric I M] auto-resolution from Riemannian stack

[Xinze-Li-Moqian]

Goal

Replace the [hm : HasMetric I M] typeclass auto-resolution + _g-style notation dispatch with explicit-g, method-call style throughout the Riemannian stack. The Riemannian metric g becomes a first-class Lean term in every signature; _g notations (which are currently just string suffixes hiding HasMetric.metric) are deleted in favour of g.metricInner, g.ricciTensor, etc.

End-state target (BG illustration):

theorem bishopGromov_volume_comparison
    (g : RiemannianMetric I M)
    (hRic : ∀ x v, ((n_M : ℝ) - 1) * K * g.metricInner x v v ≤ g.ricciTensor x v v)
    (p : M) ... :
    dV_g[g].real B(p, R) / V_K^n_M(R) ≤ dV_g[g].real B(p, r) / V_K^n_M(r)

Sub-issues (sequential, each session-sized)

• [9a] Explicit-g: Curvature core (ricciTensor, scalarCurvature, ricci, riemannCurvature, curvatureEndo) #14 — 9a: Curvature core (Curvature/RicciTensorBundle.lean, RiemannCurvature.lean)
• [9b] Explicit-g: Levi-Civita connection #15 — 9b: Levi-Civita connection (Connection/LeviCivita.lean)
• [9c] Explicit-g: Operators (Gradient, Laplacian, Hessian, SecondFundamentalForm, ConnectionLaplacian) #16 — 9c: Operators (Operators/{Gradient, Laplacian, Hessian, SecondFundamentalForm, ConnectionLaplacian})
• [9d] Explicit-g: Bochner stack internals #17 — 9d: Bochner stack (Operators/Bochner.lean + 3 sub-files)
• [9e] Explicit-g: Migrate consumers (BG, Volume, GMT) #18 — 9e: Consumer migration (Comparison/BG, Volume/VolumeForm, GMT/SecondVariation)
• [9f] Explicit-g: Drop typeclass-dispatch _g notations entirely #19 — 9f: Terminal cleanup — delete _g notations entirely, full method-call cascade

Phased invariant

Throughout 9a–9e, the `_g`-style scoped notations are kept temporarily as a backward-compat layer that auto-fills `HasMetric.metric`. This lets each sub-issue's commit produce a green build with no API-surface break to downstream that hasn't migrated yet. 9f deletes the notation layer in one final atomic commit, completing the Mathlib-idiom transition.

Total scope

~1150 LOC across 17 files. Sequenced as 6 sub-PRs over multiple sessions, each one passing CI cleanly.

Foundation already in place

• Metric/RiemannianMetric.lean already explicit-g (commit 6312583).
• g.metricInner, g.metricNormSq, g.metricInnerSection, g.metricNormSqSection, g.metricRiesz all live as method-call APIs on g : RiemannianMetric I M.

Why it matters

The current _g suffix is misleading — it suggests g is a parameter, but g is hidden behind typeclass HasMetric.metric. Multiple metrics on the same manifold cannot coexist in a signature. BG's signature was forced into dV_g[(HasMetric.metric : RiemannianMetric I M)] workaround. The refactor removes this ambiguity at the foundation.