Bishop–Gromov: complete via Route A (Bochner) — discharge the two interfaces

[Xinze-Li-Moqian]

Goal

Make Bishop–Gromov unconditional by constructing the two interface structures the
headlines currently take as hypotheses, via Route A (Bochner).

• bishopGromov_volume_comparison (Comparison/BishopGromov/VolumeComparison.lean) takes
  BishopGromovVolumeData g K p ⇒ ratio $\dfrac{\mathrm{vol}M(B_p(R))}{\mathrm{vol}{\mathbb M_\kappa}(B(R))}$ non-increasing.
• laplacian_comparison (Comparison/BishopGromov/LaplacianComparison.lean) takes
  RadialLaplacianProfile g K p x ⇒ $\Delta_g r \le m_\kappa(r)$, $,m_\kappa(r)=(n-1)\dfrac{s_\kappa'(r)}{s_\kappa(r)}$.

The plan reaches the scalar Riccati $a'+a^2+\kappa\le 0$, $a=\dfrac{\Delta r}{n-1}$, via the Bochner
formula on $\tfrac12|\nabla r|^2$ together with the eikonal $|\nabla r|=1$, then applies the
proved comparison $a\le\mathrm{ct}_\kappa$. It keeps our already-0-sorry Bochner analytic core; its
only extra cost is B1 ($\exp$ $C^1!\to!C^\infty$) + B2 (eikonal $|\nabla r|=1$).

Book references are to Lee, Introduction to Riemannian Manifolds, 2nd ed.
(Springer PDF) and
Petersen, Riemannian Geometry, 3rd ed. (author PDF).
Section/page numbers verified against the actual TOCs. (NB Petersen 3e: §7.1 is volume
comparison / Bishop–Gromov; §9.4 is the Bochner technique.)

---

Leg [B] — Laplacian comparison ⇒ RadialLaplacianProfile

✅ done

• B3 Bochner radial Riccati bochner_radial_riccati (Comparison/BishopGromov/RadialRiccati.lean).
  Ref: Petersen §9.4 The Bochner Technique in General (p.296); Lee Ch 11 Jacobi Fields, Hessians, and Riccati Equations (p.320).
• B4 Riccati comparison riccati_le_model (Comparison/BishopGromov/RiccatiComparison.lean).
  Ref: Petersen §6.4 Basic Comparison Estimates (p.213); Lee Ch 11 (p.320).
• refined Cauchy–Schwarz $(\mathrm{tr}S)^2\le(n-1)|S|^2$ (Comparison/Util/RefinedCauchySchwarz.lean).

❌ B1 — lift $\exp_p$ from $C^1$ to $C^\infty$  ⚠

• Math. $\exp_p:T_pM\to M$ is $C^\infty$. Needed because bochner_radial_riccati requires
  $r=\mathrm{dist}(p,\cdot)\in\mathrm{ContMDiff}\infty$ (it differentiates $\mathrm{Hess}r$),
  and $r\in C^\infty$ on the normal ball iff $\exp_p$ is.
• Construct. Files: Exponential/Smoothness/* (AtZero, MatchDataReduction,
  ZeroSectionConstancy, UniformChartFlowBridge, ChartFlowVelocitySlice, MfderivZero) +
  Exponential/LocalDiffeomorphism.lean. Target: generalize expMap_contMDiffAt_zero from the
  hard-coded order $1$ to arbitrary order — i.e. ContMDiffAt 𝓘(ℝ,E) I n (expMap g p) 0 for all $n$
  (or $\top$). Principle: the geodesic ODE flow is already $C^\infty$
  (SmoothFlow.chartPhaseVFTime_uncurry_contDiffOn_univ_nat); thread an order parameter through the
  chain. Shortcut to assess (math): bochner_radial_riccati only assumes [IsManifold I 2 M],
  so its $\infty$-hypothesis on $r$ likely weakens to finite order $\approx C^3$ → only a finite-order
  lift needed.
• Lee: Ch 5 The Exponential Map (p.126), Normal Neighborhoods and Normal Coordinates (p.131).
• Petersen: §5.5 Riemannian Coordinates (p.155), §5.2 Geodesics (p.140).

🔶 B2 — eikonal $|\nabla r|^2 = 1$  (⚠ the $\ge 1$ half)

• Math. $|\nabla r|^2_g=1$ on the punctured normal ball. The full triple
  ($|\nabla r|^2=1,\ d|\nabla r|^2=0,\ \Delta|\nabla r|^2=0$) that bochner_radial_riccati consumes
  reduces to this single identity.
• $\le 1$ — mostly done: manifoldGradient_metricInner_self_le_one (Operators/Gradient.lean).
  • Still to construct: in Operators/Gradient.lean, the differential bound
    $(d(\mathrm{dist}(p,\cdot))(v))^2\le|v|_g^2$, from $\mathrm{dist}$ being $1$-Lipschitz
    w.r.t. riemannianEDist (the riemannianEDist$\leftrightarrow g$-norm infinitesimal bridge).
    Lee: Ch 6 Distance Functions (p.174). Petersen: §5.3 The Metric Structure of a Riemannian Manifold (p.145).
• $\ge 1$ — ❌ ⚠ HIGHEST RISK.
  • Math. $|\nabla r|\ge 1$ via the Gauss lemma + radial isometry $\mathrm{dist}(p,\exp_p v)=|v|$:
    along a unit radial geodesic $dr(\gamma')=1$, $|\gamma'|=1$, so Cauchy–Schwarz gives $|\nabla r|\ge1$.
  • Construct. New file Exponential/GaussLemma.lean: gaussLemma (radial $\perp$ spherical,
    $d\exp_p$ radial-isometric) and dist_expMap_eq_norm (radial isometry). Then in
    Operators/Gradient.lean: manifoldGradient_metricInner_self_ge_one; combine with $\le1$
    → …_self_eq_one. Build in our conventions; do not migrate external's variation cone.
  • Lee: Ch 6 Geodesics and Minimizing Curves (p.151) — the Gauss lemma + local minimizing.
  • Petersen: §5.4 First Variation of Energy (p.151).

❌ B5 — construct RadialLaplacianProfile (leg-[B] discharge)

• Math. The radial profile $m(s)=\Delta_g r$ satisfies the Riccati sub-equation
  $m'(s)+\dfrac{m(s)^2}{n-1}+(n-1)\kappa\le0$ and the asymptotic $m(s)-\dfrac{n-1}{s}\to0$ as $s\to0^+$.
• Construct. File: Comparison/BishopGromov/LaplacianComparison.lean (or new …/RadialProfile.lean).
  Target: radialLaplacianProfile_of_dist : RadialLaplacianProfile g K p x, fields profile$=m$,
  eval (vs scalarLaplacian, Operators/Laplacian.lean:99), riccati_sub ⇐ B3+B1+B2,
  asymptotic ⇐ $d\exp_p|_0=\mathrm{id}$.
• Lee: Ch 11 Comparisons Based on Ricci Curvature (p.336).
• Petersen: §7.1 Volume Comparison (p.233) — the mean-curvature / $\Delta r$ estimate.

---

Leg [C] — polar volume formula ⇒ BishopGromovVolumeData  (needs only $C^1$)

✅ done

• C1 exp-volume change of variables + volume substrate
  (Volume/ExpBridge.lean, Volume/ChartPullback*.lean, Volume/VolumeForm.lean).
• C5 monotone average integral: $q$ non-increasing ⇒ $\frac{1}{t}\int_0^t q$ non-increasing
  (Comparison/BishopGromov/VolumeMonotone.lean, PolarVolumeReduction.lean).
  Ref: Petersen §7.1 Volume Comparison (p.233).

🔶 C2 — polar Jacobian $\det d\exp_p(t\xi) = t^{n-1} J_\xi(t)$

• Math. In polar coordinates the Jacobian factors as $t^{n-1}J_\xi(t)$, where $J_\xi(t)$ is the
  determinant of the $(n-1)\times(n-1)$ Jacobi-field matrix along $\gamma_\xi(t)=\exp_p(t\xi)$.
• Construct. File: Volume/Exponential.lean (partial: det_dExpMap_jacobiField_decomp,
  det_dExpMap_pos present). Finish the $t^{n-1}$ extraction + the radial Jacobi-field density $J_\xi(t)$.
• Lee: Ch 10 The Jacobi Equation (p.284), Basic Computations with Jacobi Fields (p.287).
• Petersen: §6.1 The Connection Along Curves (p.193).

❌ C3 — radial log-derivative bridge $\partial_t\log J_\xi(t)=\Delta_g r$

• Math. $\partial_t\log J_\xi(t)=\mathrm{tr}S(t)=\Delta_g r(\gamma_\xi(t))$ (mean curvature of the
  geodesic sphere = Laplacian of $r$). Lets leg-[B]'s $\Delta r\le m_\kappa$ drive ratio_antitone.
• Construct. File: Volume/Exponential.lean (or new Volume/RadialJacobian.lean).
  Target: deriv_log_jacobian_eq_scalarLaplacian_dist. Principle: $J'=SJ$ ⇒
  $\partial_t\log\det J=\mathrm{tr}(J^{-1}J')=\mathrm{tr}S$; identify $\mathrm{tr}S=\Delta r$.
• Lee: Ch 11 Jacobi Fields, Hessians, and Riccati Equations (p.320); Ch 10 The Second Variation Formula (p.300).
• Petersen: §7.1 Volume Comparison (p.233).

❌ C4 — cut locus measure-zero + polar volume formula

• Math. $\exp_p:(B(0,r)\cap C_p)\to B(p,r)\setminus\mathrm{cut}(p)$ is a diffeomorphism,
  $\mathrm{cut}(p)$ has measure zero, hence
  $\mathrm{vol}(B(p,R))=\int_0^R!!\int_{S^{n-1}}J_\xi(t),d\xi,dt=\int_0^R A(t),dt$, $A(t)=\int_{S^{n-1}}J_\xi(t),d\xi$.
• Construct. New file Exponential/CutLocus.lean: cutLocus, measure_cutLocus_eq_zero
  (no cut-locus layer exists yet). Plus: Volume/Polar.lean (or extend Volume/Exponential.lean):
  volumeMeasure_ball_eq_intervalIntegral_area, combining C1 + C2.
• Lee: Ch 10 Cut Points (p.307).
• Petersen: §7.1 Volume Comparison (p.233) — segment domain; §5.7 Completeness (p.176).

❌ C6 — construct BishopGromovVolumeData (leg-[C] discharge)

• Math. area$=A(t)$, vol_eq $\mathrm{vol}g(B(p,R))=\int_0^R A$ ⇐ C4,
  ratio_antitone ($t\mapsto A(t)/\max(0,s\kappa(t))^{n-1}$ antitone) ⇐ C3 + leg-[B] $\Delta r\le m_\kappa$
  (so $\partial_t\log(A/\bar j)=\Delta r-m_\kappa\le0$).
• Construct. File: Comparison/BishopGromov/VolumeComparison.lean.
  Target: bishopGromovVolumeData_of_dist : BishopGromovVolumeData g K p.
• Lee: Ch 11 Comparisons Based on Ricci Curvature (p.336) — Günther + Bishop–Gromov.
• Petersen: §7.1 Volume Comparison (p.233).

---

Finish

• Drop the (data : …) arguments from both headline theorems (proof bodies already written
  against the interfaces) ⇒ BG unconditional.

---

Most concentrated single reference

Petersen §7.1 Volume Comparison (p.233) covers B5 + C3 + C4 + C6 (Laplacian/mean-curvature
comparison + relative volume + Bishop–Gromov) in one section; the Lee parallel is Ch 11 (pp.319–342).
Bochner formula proper: Petersen §9.4 (p.296). Cut locus: Lee Ch 10 Cut Points (p.307).

Owners

• Engineering (build the Lean on feat/bishop-gromov): @LehengChen, @imathwy
• Math (verify §/page against the PDFs, pin to each task, resolve B1 finite-order shortcut & B2 $\ge1$ Gauss route): @zhifeizhu92, @Spring-1211

[Xinze-Li-Moqian]

Method (verified against the book). This is Method ② — the Laplacian of the distance function Δr: distance function r, the Hess r Riccati (∇_∂r Hess r) + Hess²r = -R(·,∂r,∂r,·), traced to ∂_r Δr + (Δr)²/(n-1) ≤ -Ric(∂r,∂r) ≤ -(n-1)κ (via Cauchy–Schwarz |Hess r|² ≥ (Δr)²/(n-1)), polar volume ∂_r λ = λ Δr, model Δr = (n-1)·sn_κ'(r)/sn_κ(r). Needs r smooth (exp C^∞) + eikonal |∇r| = 1.

The Petersen references in this issue are correct — confirmed directly from Petersen, Riemannian Geometry, Ch 7 §7.1.1 "The Fundamental Equations" / Prop 7.1.1.

The complementary Method ① (Jacobi fields / matrix Riccati) is Route B / #86 = Kapovitch CH21 + Lee Ch 10–11; it works along geodesics and bypasses the exp C^∞ + eikonal interfaces (B1/B2 in this issue).