[9a] Explicit-g: Curvature core (ricciTensor, scalarCurvature, ricci, riemannCurvature, curvatureEndo)

[Xinze-Li-Moqian]

Part of umbrella #9. Sub-task 9a — Curvature core.

Scope

Files:

• OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean
• OpenGALib/Riemannian/Curvature/RiemannCurvature.lean

Changes

1. Drop [hm : HasMetric I M] from the section variable block.
2. Add (g : RiemannianMetric I M) as explicit parameter to:
   • ricci, curvatureEndo, riemannCurvature (RiemannCurvature.lean)
   • ricciTensor, scalarCurvature, ricciSharp (RicciTensorBundle.lean)
3. Update internal call sites (the proof bodies) to pass g explicitly.
4. Notation backward-compat: update the scoped notations to pass HasMetric.metric automatically, so downstream code using Ric_g(v, w) x, Ric(X, Y), Riem(X, Y) Z, scal_g[I] still works unchanged. Example:

   scoped[Riemannian] notation:max "Ric_g(" v ", " w ") " x:max =>
     ricciTensor (Riemannian.HasMetric.metric) x v w

Invariant

External notation behaviour unchanged. Downstream Bochner / BG / consumers see no API change yet — they pick up HasMetric.metric via notation expansion. Their explicit-g migration happens in later sub-issues.

Acceptance

• Build clean.
• Sorry count unchanged (38).
• All linters at baselines.
• [HasMetric I M] typeclass no longer appears in the section variable blocks of RicciTensorBundle.lean or RiemannCurvature.lean.

See also

#9 umbrella · next: 9b (Levi-Civita)