[9d] Explicit-g: Bochner stack internals

[Xinze-Li-Moqian]

Part of umbrella #9. Sub-task 9d — Bochner stack.

Scope

Files (4):

• OpenGALib/Riemannian/Operators/Bochner.lean
• OpenGALib/Riemannian/Operators/Bochner/HessianExpansion.lean
• OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean
• OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean

Heaviest file in the cascade — Bochner stack has 67 `_g` notation uses total. After #14–#16, the underlying definitions take explicit `g`; this sub-issue migrates the Bochner stack itself.

Changes

For each Bochner file:

1. Drop `[hm : HasMetric I M]` from section variables.
2. Add `(g : RiemannianMetric I M)` as explicit section parameter — auto-included in all theorems / lemmas.
3. Update all internal call sites of curvature / operator functions to pass `g` explicitly: `g.ricciTensor x v w`, `g.manifoldLaplacian f`, etc.
4. `_g`-style notations still work in proof bodies (via `HasMetric.metric` resolution from outer scope, or no longer needed if all switched to method calls). The pragmatic choice: in this sub-issue, keep using `⟪⟫_g` etc. via the notation infrastructure (it auto-routes to `HasMetric.metric` per the notation update in 9a/9b/9c). The final `_g` deletion happens in 9f.

Risk

This is the highest-friction file cluster — 67 notation uses, many internal lemmas. Build may take iterations to settle.

Invariant

Bochner stack 0-sorry maintained. `bochner_weitzenboeck` headline + `manifoldGradient_smooth_of_smooth` unconditional preserved.

Acceptance

• Build clean.
• Sorry count unchanged (38).
• Bochner stack 0-sorry preserved.
• All 4 Bochner files have explicit `g` as section parameter.

Dependencies

Requires #14 (9a), #15 (9b), #16 (9c) merged first.

See also

#9 umbrella · prev: 9c (#16) · next: 9e (consumers)

[Xinze-Li-Moqian]

Deferred to 9f (2026-05-18)

Attempted in a session today and rolled back. The Bochner stack proof bodies use ~10+ typeclass-form helpers from Util/MetricInnerSmoothness.lean (lines 138–217: metricInner_contMDiff, metricInner_mdifferentiableAt_of_tangentSmoothAt, etc.) that don't unify under arbitrary g. Lifting them is mechanical but larger than the umbrella estimated.

The cascade plan now runs #18 (9e) and #19 (9f) before returning here. 9f's "drop _g notations entirely" cleanup will likely subsume the notation-unfold work anyway, so this issue may close naturally as part of 9f rather than as a standalone PR.

Resume checklist:

1. Lift Util/MetricInnerSmoothness.lean typeclass-form helpers (lines 138–217) to explicit-g, or have consumers call the existing explicit-g forms (lines 37–109) directly via dot notation (g.metricInner_contMDiff hv hw).
2. Add explicit-g variant of metricInner_mdifferentiableAt_of_tangentSmoothAt (currently typeclass-only).
3. Per Bochner file: variable (g : RiemannianMetric I M) at section, HasMetric.metric → g everywhere, replace bare metricInner → g.metricInner (leave dot-method calls alone), unfold ‖grad_g[I] f‖²_g notation in theorem statements to fun y => g.metricInner y (manifoldGradient g f y) (manifoldGradient g f y) (since ‖·‖²_g is hardcoded to HasMetric.metric in MetricNotation.lean).

Status: Bochner stack remains typeclass-form internally. It pipes HasMetric.metric to the 9c-lifted operators, so it still produces a green build for all consumers.