Close Federer bridge: vol_g = α(n) · μH[n] (Hausdorff measure characterization)

[Xinze-Li-Moqian]

Current state

Two PRE-PAPER / CITED-BLACK-BOX sorries in OpenGALib/Riemannian/Volume/Hausdorff.lean:

```lean
noncomputable def alphaFedererConstant (n : ℕ) : ℝ≥0∞ := sorry

theorem volumeMeasure_eq_alphaFederer_smul_hausdorffMeasure (g : RiemannianMetric I M) :
volumeMeasure g =
alphaFedererConstant (Module.finrank ℝ E) •
MeasureTheory.Measure.hausdorffMeasure ((Module.finrank ℝ E : ℕ) : ℝ) := by
sorry
```

This is Federer §3.2.46-50 — the n-dimensional Hausdorff measure of a smooth Riemannian manifold equals a constant multiple of the Riemannian volume measure. The constant α(n) = ω_n / 2^n (Federer normalization).

Why it matters

Once closed, BG's Hausdorff-form variants are automatic: any μ satisfying IsScalarMultipleOfHausdorff n becomes vol_g-equivalent. Also unlocks:

• "Hausdorff measure of a Riemannian manifold" identification in any future theorem.
• Removal of the IsScalarMultipleOfHausdorff stopgap predicate from OpenGALib/MetricGeometry/Util/.

Why it's hard

Proof requires:

1. Local Lipschitz approximation in charts — Riemannian distance and Euclidean chart distance differ by 1 + O(r) as ball radius r → 0.
2. Covering lemma — Besicovitch / Vitali in metric spaces. Mathlib has these.
3. Density estimates — Hausdorff density at every point of a smooth manifold is α(n).
4. Differentiation of measures — Lebesgue / Radon-Nikodym style.

OpenGA's GeometricMeasureTheory/ layer is currently shape-complete but proof-shallow (per memory project_gmt_depth_gap). The infrastructure for steps 1-4 needs to be built. Closing this issue = the GMT depth fill.

Estimated scope

~500-1000 LOC including all prerequisites. Multi-week.

Architecture choice

Two equivalent terminal states:

• Federer normalization: α(n) = ω_n / 2^n, identity vol_g = α(n) · μH[n]_{d_g}.
• Mathlib normalization: μH[n] already gives volume on ℝⁿ (no α-factor); identity becomes vol_g = μH[n]_{d_g}.

Either works. Pick once and document.

Acceptance

• Both sorries in Volume/Hausdorff.lean closed.
• IsScalarMultipleOfHausdorff predicate becomes a derivable corollary.
• docs/SORRY_CATALOG.md updated.

Out of scope for this issue

BG proof itself — see #10. BG no longer depends on this bridge (signature uses vol_g directly).