9g (part 2): drop Riem, ‖·‖²_g, II, (∇R)— last typeclass-dispatch notations

[Xinze-Li-Moqian]

Summary

9g (part 2) — completes the _g notation drop started in #39.

Notations dropped

Notation	Expansion	Callsites
Riem(X, Y) Z	riemannCurvature HasMetric.metric X Y Z	41
‖V‖²_g	section: fun y => HasMetric.metric.metricInner y (V y) (V y); Bilin: frobeniusSq B	9
II(X, Y)	(no callsites)	0
(∇R)[X](Y, Z) W	covDerivRiemann X Y Z W	1 (in bianchi_second sorry)

Also removed MetricNormSq typeclass + 3 instances (Tangent, Section, Bilin).

After this PR, the only scoped notation left in OpenGALib's Riemannian namespace is ⟦X, Y⟧ for VectorField.mlieBracket _ X Y — which is metric-independent and stays.

Why

All _g notations dispatched via typeclass to HasMetric.metric, hardcoding a single metric per manifold. Dropping them is the precursor to 9h, which will replace HasMetric.metric with explicit (g : RiemannianMetric I M) parameters file-by-file (enabling Ricci flow / conformal change / comparison geometry where multiple metrics naturally appear).

Vol_g

vol_g (28 grep hits) is only docstring/comment usage — no Lean notation exists. No action needed; left as math prose.

Test plan

• lake build clean per commit
• CI green
• Sorry / shake / MathTag baselines unchanged