Bishop–Gromov leg [C]: cut-locus measure-zero + geodesic-polar volume formula (shared with Route A)

[Xinze-Li-Moqian]

Goal

Construct the geodesic-polar volume leg of BishopGromovVolumeData
(Comparison/BishopGromov/VolumeComparison.lean) — the measure-theoretic plumbing
that is shared with Route A and carries none of the Jacobi/Riccati mathematical
content. Concretely, discharge the two analytic fields:

• vol_eq — geodesic-polar volume formula
  (volumeMeasure g).real (B(p,R)) = ∫₀ᴿ area t (CH21 L248–293).
• area_integrable — interval-integrability of the area profile on each admissible
  window radius.

with area t = ∫_{S^{n-1}} j(t,v) dvol^{n-1} the geodesic-sphere area profile
(j(t,v) = the exp-polar Jacobian, supplied by the Jacobi/Riccati leg — separate
work, not part of this issue).

Books: Lee, Intro to Riemannian Manifolds 2e — Ch 10 Jacobi Fields &
Ch 6 Geodesics and Distance (cut locus, normal/cut domain); do Carmo,
Riemannian Geometry Ch 13 (cut locus, measure zero); Petersen,
Riemannian Geometry 3e §5.7 / §7.1.

---

The pieces

• C1 — cut locus has measure zero. cut(p) ⊆ M is Lebesgue/volumeMeasure-null,
  so vol B(p,R) = vol(B(p,R) \ cut(p)) = vol(exp(C_p ∩ B(0,R))). (CH21 Fact, L255.)
  Ref: do Carmo Ch 13; Lee Ch 10.
• C2 — exp_p is a diffeomorphism on the open star-shaped cut domain C_p
  onto M \ cut(p). (CH21 L254, L261.)
• C3 — polar change of variables. Push the volume measure through
  exp_p ∘ (polar coords); the Jacobian factorizes as r^{n-1} · (sphere factor),
  giving vol B(p,R) = ∫_{S^{n-1}} ∫₀^{min(R, cut(v))} j(v,t) dt dvol^{n-1}
  (CH21 L263). Mathlib entry: MeasureTheory.integral_comp_polar-style / the
  manifold change-of-variables on exp.
• C4 — assemble vol_eq + area_integrable with j redefined to 0 past
  cut(v) (CH21 L265–276), matching the BishopGromovVolumeData field shapes.

Relation to other work

• The Jacobi/Riccati leg (ratio_antitone, i.e. ∂_t log(j/j̄) ≤ 0) is built
  separately on feat/bishop-gromov-jacobi and is not part of this issue.
• This leg is also consumed by Route A (issue Bishop–Gromov: complete via Route A (Bochner) — discharge the two interfaces #85); building it once unblocks
  both routes.
• bishopGromov_volume_comparison itself is already 0-sorry modulo
  BishopGromovVolumeData; this issue + the Jacobi/Riccati leg together discharge
  the interface.

[Xinze-Li-Moqian]

Merged into #86 (now the unified Level-2 work-list for fully-unconditional Bishop–Gromov; T6 there is this issue's cut-locus/polar-volume content).