[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

• [9a] Explicit-g: Curvature core (ricciTensor, scalarCurvature, ricci, riemannCurvature, curvatureEndo) #14 — 9a: Curvature core — merged via [9a Phase 1] Explicit g on Ricci/scalarCurvature core (closes #14) #31 + [9a-pre Phase 1] Explicit-g foundation: Koszul + Riesz (closes #32) #33
• [9b] Explicit-g: Levi-Civita connection #15 — 9b: Levi-Civita connection — merged via [WIP 9b Phase 1] LeviCivita explicit-g — in-file done, consumer bridging pending #34; cleanup Koszul: omit unused [hm] in 10 explicit-g theorems #35
• [9c] Explicit-g: Operators (Gradient, Laplacian, Hessian, SecondFundamentalForm, ConnectionLaplacian) #16 — 9c: Operators (Gradient, Laplacian, Hessian, SecondFundamentalForm, Divergence, ConnectionLaplacian) — merged via Operators 9c: explicit g on Gradient/Hessian/Laplacian/Divergence/SFF/ConnectionLaplacian #36
• [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 (subsumes [9d] Explicit-g: Bochner stack internals #17)
• [9d] Explicit-g: Bochner stack internals #17 — 9d: Bochner stack internals — deferred: attempted 2026-05-18 and rolled back; Bochner proof bodies depend on ~10+ typeclass-form metricInner_* helpers in Util/MetricInnerSmoothness.lean that need lifting first. Resume as part of 9f.

Phased invariant

Throughout 9a–9e, the _g-style scoped notations are kept temporarily as a backward-compat layer that auto-fills HasMetric.metric. 9f deletes the notation layer in one final atomic commit, completing the Mathlib-idiom transition.

The Bochner stack remains typeclass-form internally through 9e. It pipes HasMetric.metric to the 9c-lifted operators, so it still produces a green build for all consumers — but the internals are not yet first-class explicit-g. 9f rewires the Bochner stack along with the notation drop.

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.

Status note (2026-05-18)

9a (#14), 9b (#15), 9c (#16) all merged. 9d (#17) deferred to 9f. Next: 9e (#18) consumer migration.