[9e] Explicit-g: Migrate consumers (BG, Volume, GMT)

[Xinze-Li-Moqian]

Part of umbrella #9. Sub-task 9e — consumer migration.

Scope

Files (3):

• OpenGALib/Comparison/BishopGromov/VolumeComparison.lean
• OpenGALib/Riemannian/Volume/VolumeForm.lean
• OpenGALib/GeometricMeasureTheory/Variation/SecondVariation.lean

After 9a–9d, the entire Riemannian-side stack has explicit `g`. The final consumer-facing surfaces still depend on `[HasMetric I M]` typeclass — this sub-issue migrates them.

Changes

For each consumer file:

1. Drop `[HasMetric I M]` from section variables.
2. Add `(g : RiemannianMetric I M)` as explicit theorem parameter (or section parameter, depending on convention).
3. Replace `dV_g[(HasMetric.metric : RiemannianMetric I M)]` style with `dV_g[g]` (clean once `g` is explicit).
4. Bishop–Gromov signature becomes:

   theorem bishopGromov_volume_comparison
       (g : RiemannianMetric I M) (hRic : ...)
       (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)

   — `g` is finally a first-class term in the most important Comparison theorem.

Acceptance

• Build clean.
• Sorry count unchanged.
• BG / VolumeForm / SecondVariation signatures show `g` as explicit parameter.
• No verbose (HasMetric.metric : RiemannianMetric I M)\ workaround anywhere in the three files.

Dependencies

Requires #17 (9d) merged first.

See also

#9 umbrella · prev: 9d (#17) · next: 9f (notation infrastructure removal)