[9a-pre] Explicit-g foundation: Koszul + RieszExtraction

[Xinze-Li-Moqian]

Part of umbrella #9. Bottom-up foundation sub-issue, prepended before #15 (9b LeviCivita).

Motivation

While starting work on #15 (LeviCivita explicit-g), it became clear that Koszul is the true foundation of the dependency stack:

LeviCivita (covDeriv, riemannCurvature) ← #15 (target)
 ↑
RieszExtraction (koszulCovDeriv)
 ↑
Koszul (koszulFunctional, koszul_* theorems) ← this issue
 ↑
Metric (metricInner) ← already explicit-g (commit 6312583)

The letI : HasMetric I M := ⟨g⟩ bridge that worked for #14 (Curvature core, which sits above LeviCivita) does not work for #15. Concretely: covDeriv_inner_eq_half_koszul has koszulFunctional X Y Z x in its statement RHS. Under any letI-bridge attempt, the lemma's letI-bound HasMetric instance and the caller's letI-bound instance are not definitionally equal (different let-bound local variables), so rw fails. The only clean fix is for koszulFunctional itself to take (g : RiemannianMetric I M) explicitly. The same applies to koszulCovDeriv.

The original #9 cascade ordered sub-issues by API-surface visibility, not dependency depth. This issue restores bottom-up order.

Scope

Files:

• OpenGALib/Riemannian/Connection/Koszul.lean (585 LOC, 12 koszul_* theorems)
• OpenGALib/Riemannian/Connection/RieszExtraction.lean (95 LOC, koszulCovDeriv + 2 helper theorems)

Changes (Phase 1)

1. Keep [hm : HasMetric I M] in section variable blocks (typeclass retention deferred to [9f] Explicit-g: Drop typeclass-dispatch _g notations entirely #19).
2. Add (g : RiemannianMetric I M) as explicit parameter to:
   • koszulFunctional
   • koszul_antisymm, koszul_metric_compat_sum
   • koszul_smul_right, koszul_add_right, koszul_add_left, koszul_add_middle, koszul_smul_left, koszul_smul_middle
   • koszulFunctional_local, koszulFunctional_tensorialAt
   • koszulLinearFunctional_exists, koszulCovDeriv_exists, koszulCovDeriv, koszulCovDeriv_inner_eq
3. Replace internal typeclass-dispatched metricInner y V W with explicit g.metricInner y V W (the alternative form metricInner from SmoothManifold.lean aliases to hm.metric.metricInner, but here we want the caller's g).
4. Add letI : HasMetric I M := ⟨g⟩ in proof bodies where they call deeper typeclass-dispatched primitives (e.g., metricInner_comm, metricInner_neg_left, metricInner_eq_iff_eq from the metric layer if they remain typeclass-dispatched).

Invariant

No public API behavior change. After this PR:

• koszulFunctional g X Y Z x exists with explicit g.
• No internal consumer outside Koszul/RieszExtraction calls these directly today (verified: they're only used inside LeviCivita.lean via the typeclass-dispatched form, which becomes explicit-g in [9b] Explicit-g: Levi-Civita connection #15).

Acceptance

• Build clean.
• Sorry / shake / linter baselines unchanged (sorry=36, shake=36, MathTag/AnchorPurity/Naming=0).
• All listed defs / theorems take (g : RiemannianMetric I M) as an explicit parameter.

Why now (not deferred)

#15 (LeviCivita) cannot proceed cleanly without this foundation. We discovered the gap mid-work on #15. Splitting out this prep PR keeps each PR focused and reviewable, rather than bundling a 2000-line megachange.

See also

#9 umbrella · next: #15 (9b Levi-Civita) — depends on this · prev: #14 (9a Curvature core, already done)