9g (part 1): drop 9 _g typeclass-dispatch notations

[Xinze-Li-Moqian]

Summary

9g (part 1) — first wave of _g notation drops. Each notation is replaced inline with explicit HasMetric.metric-form expansions, then the notation definition is deleted.

Notations dropped (9 commits, each its own commit)

Notation	Expansion	Callsites
Ric_g(v, w) x	ricciTensor HasMetric.metric x v w	17
grad_g[I] f	manifoldGradient (I := I) HasMetric.metric f	18
Δ_g[I] f	Operators.scalarLaplacian (I := I) HasMetric.metric f	17
hess_g[I] f	Operators.hessianBilin (I := I) HasMetric.metric f	2
div_g[I]	(no callsites — notation only)	0
H_g[I]	(no callsites — notation only)	0
K_g[I](X, Y)	sectionalCurvature (I := I) X Y	1
scal_g[I]	(no callsites — notation only)	0
Ric(X, Y)	ricci HasMetric.metric X Y	2
⟪V, W⟫_g	HasMetric.metric.metricInner x V W (tangent) / fun y => ... (section)	4
∇[X] Y	covDeriv HasMetric.metric X Y	4

Also removed the MetricInnerHom dispatch class (only consumer was ⟪V, W⟫_g).

Deferred to follow-up

Larger notations not yet dropped:

• Riem(X, Y) Z (41 callsites)
• vol_g (28 callsites)
• ‖V‖²_g (20 callsites) — polymorphic, still needs MetricNormSq dispatch class
• (∇R)[X](Y, Z) W (covariant Riemann tensor notation)
• II(X, Y), ⟦X, Y⟧ (mlieBracket — metric-independent, may keep)

Why

Typeclass-dispatch notations conflate metric and operator at parse time, making multi-metric reasoning (Ricci flow, conformal change, comparison geometry) impossible. Explicit forms make HasMetric.metric / g visible at every site. Future PR (9h) can selectively re-introduce dot-method notations (e.g., g.gradient f, g.scalarLaplacian f) once typeclass abbrev is gone.

Test plan

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