Prove bishopGromov_volume_comparison via exponential chart + Jacobi field comparison

[Xinze-Li-Moqian]

Current state

bishopGromov_volume_comparison (in OpenGALib/Comparison/BishopGromov/VolumeComparison.lean) has its final signature in place (commit 9fd1435):

```lean
theorem bishopGromov_volume_comparison
(hRic : ∀ x v, ((n_M : ℝ) - 1) * K * ⟪v, v⟫_g ≤ Ric_g(v, v) x)
(p : M) {r R : ℝ} (hr : r ∈ 𝒟_K) (hR : R ∈ 𝒟_K) (hrR : r ≤ R) :
dV_g[(HasMetric.metric : RiemannianMetric I M)].real B(p, R) / V_K^n_M(R) ≤
dV_g[(HasMetric.metric : RiemannianMetric I M)].real B(p, r) / V_K^n_M(r) := by
sorry
```

The sorry is the only thing remaining. After #9 (explicit-g refactor) the signature becomes cleaner.

Proof outline (do Carmo Ch.10 §2 / Petersen Ch.9 §27)

1. Exponential chart polar decomposition: in normal coordinates centered at p,
   ```
   vol_g(B(p, r)) = ∫_0^r ∫_{S_p^{n-1}} J_g(s, v) ds dσ(v)
   ```
   where J_g(s, v) = det(d_{sv} exp_p) is the Jacobian of the exponential map and dσ is the round measure on the unit sphere.

2. Jacobi field equation: J_g(s, v) = ‖J_1 ∧ ... ∧ J_{n-1}‖ where J_i are Jacobi fields along t ↦ exp_p(tv).

3. Comparison via Riccati: the Ricci lower bound Ric ≥ (n-1)K implies J_g(s, v) ≤ J_K(s) where J_K is the constant-curvature reference Jacobian. By Rauch comparison.

4. Integrate to get monotonicity:
   ```
   vol_g(B(p, R)) / V_K^n(R) ≤ vol_g(B(p, r)) / V_K^n(r)
   ```
   via the integral comparison: if f/F is monotone in s for s ≤ s', s' ≤ s'', then ratio of integrals is monotone.

Dependencies

• Blocked-upstream / framework-self-build: Mathlib's Riemannian.expMap is gappy (Phase 4 of riemannian-volume). For OpenGA to prove BG, either:
  • Mathlib expMap matures, OR
  • OpenGA self-builds an exponential-chart polar-coordinate decomposition lemma.
• Jacobi field infrastructure: OpenGA doesn't have Jacobi field machinery yet. Needs to be built (or imported from Mathlib if available).
• Rauch comparison: Mathlib status unknown.

Estimated scope

~500 LOC for the proof itself if all prerequisites are in place. Probably 2-3x that with prerequisites.

Acceptance

• bishopGromov_volume_comparison 0 sorries.
• docs/SORRY_CATALOG.md updated.
• CI EXPECTED decreased by 1.

See also

• Issue [Umbrella] Explicit-g cascade: drop [HasMetric I M] auto-resolution from Riemannian stack #9 (explicit-g refactor) — should land first to clean up signature.
• OpenGALib/Riemannian/Volume/Exponential.lean — Phase 4 of riemannian-volume, sorry'd, related.