Bishop–Gromov Route B (Jacobi/Riccati, CH21) — full tracking: Level 1 (assemble leg ①) + Level 2 (cited facts)

[Xinze-Li-Moqian]

Bishop–Gromov, Route B (Jacobi / Riccati, Kapovitch CH21) — full tracking

Single tracking issue for the whole Route-B proof on feat/bishop-gromov-jacobi.
(Route A / Bochner is #85.) bishopGromov_volume_comparison is already 0-sorry
modulo BishopGromovVolumeData; this issue tracks discharging that interface.

Two levels:

• Level 1 (notes-rigor): prove leg ① (the Jacobi/Riccati monotonicity — the
  notes' actual argument) and assemble it into BishopGromovVolumeData, taking the
  standard geometry facts as a clean interface. This is the bulk of the math and is
  nearly done.
• Level 2 (fully-unconditional): also prove the standard facts the notes merely
  cite (parallel transport, Jacobi-field existence, conjugate points, S~I/t,
  cut-locus measure-0, polar volume).

Books: Lee, Intro to Riemannian Manifolds 2e (Ch 4, 6, 10); do Carmo Ch 13.

---

✅ DONE — all 0-sorry on feat/bishop-gromov-jacobi (the notes' math)

• Spine A''+R̃A=0 → a'+a²+κ≤0 / m-form (JacobiMatrixRiccati, JacobiRiccatiOperator; uses RB5 MatrixRiccati, RB4 RiccatiComparison).
• Liouville (det A)' = det A · tr(A⁻¹A'), i.e. j'/j = tr S (JacobiDeterminant).
• Parallel-frame D_t = component derivative + Jacobi matrix-ODE row + curvature self-adjoint + Wronskian ⟹ S symmetric (JacobiFrame).
• Ratio monotonicity j'/j ≤ j̄'/j̄ ⟹ j/j̄ antitone (RatioMonotone).
• Scalar assembly ratio_antitone_of_riccati_subsolution (JacobiRatioMonotone): m-Riccati subsol + asymptotics + j'/j=m + j>0 ⟹ j/s_K^{n-1} AntitoneOn. = CH21 L216–233 per-direction ratio_antitone.
• Base-bundle chart-transition ParallelTransportMovingFoot, IsParallelAlong+isometry ParallelTransport, chart-coord linear ODE ParallelTransportODE, coordinate characterization ParallelTransportBridge (parallel-transport groundwork; feeds Level-2 T1).

---

❌ LEVEL 1 — remaining glue (our work; finishes notes-rigor BG)

L1 — operator↔matrix inner-product bridge

Feed a single Jacobi matrix A to both the spine (operators on an inner-product
space with an orthonormal basis, for RB5's refined Cauchy–Schwarz → m = tr S) and
Liouville (Matrix, for j = det A, j'/j = tr S). Plan: V = EuclideanSpace ℝ (Fin n); bridge Matrix.trace/det/Ring.inverse ↔ operator via
toEuclideanCLM/toEuclideanLin (trace via Matrix.trace_toLin'_eq); RB5 kernel/dim
u = γ̇ ∈ ker S, tr R = Ric. ⚠ toEuclideanCLM-side API is thin in Mathlib
(mostly under CStar) — needs care.

L2 — per-direction assembly

From the geometric Jacobi interface (matrix A + A''+R̃A=0 + invertibility + S
symmetric [proven generically for Jacobi fields in JacobiFrame] + Ric bound +
S~I/t) produce m, j and apply ratio_antitone_of_riccati_subsolution ⟹
per-direction ratio_antitone.

L3 — construct BishopGromovVolumeData + discharge headline

Sphere-integrate the per-direction ratio into area/vol_eq/area_integrable
(polar volume = T6 below) ⟹ BishopGromovVolumeData ⟹
bishopGromov_volume_comparison unconditional.

---

❌ LEVEL 2 — discharge the cited standard facts (was #86 + #87)

• T1 Parallel transport existence along a curve: tangentCoordChange I.tangent
  (double tangent bundle) block structure ⟹ RB3a-2 piece ii-b. Groundwork done
  (see DONE list); remaining = the T(TM) block-structure lemma + assembly. Lee Ch 4.
• T2 Jacobi-field existence with J(0)=0, D_tJ(0)=eᵢ (2nd-order linear ODE in
  covDerivAlongCurve; mirror exists_hasDerivAt_linear_ode_Ioo). Lee Ch 10.
• T3 Parallel orthonormal normal frame existence (T1 + Gram–Schmidt;
  IsParallelAlong.norm_sq_const done). CH21 L121.
• T4 Conjugate points / A invertibility on (0,T]. Lee Ch 10.
• T5 Asymptotics S(t) ~ (1/t) I (a ~ (n-1)/r as r→0⁺; supplies
  riccati_le_model's Tendsto). CH21 L168.
• T6 Cut-locus measure-zero + geodesic-polar volume formula (vol B(p,R) = ∫_{S^{n-1}}∫₀ j; discharges vol_eq/area/area_integrable; shared with Route A
  Bishop–Gromov: complete via Route A (Bochner) — discharge the two interfaces #85). CH21 L248–293 ("Fact"); do Carmo Ch 13.

L2 consumes T1–T5 (geometric interface for A) and T6 (polar volume); T6/T1 are also
useful to Route A (#85).

[Xinze-Li-Moqian]

Method (verified against the books). This is Method ① — Jacobi fields / shape operator / matrix Riccati: the shape operator S of geodesic spheres satisfies the operator Riccati S' + S² + R = 0, the Jacobi density j = det A (A = Jacobi matrix) satisfies ∂_t log j = tr S, and tracing the Riccati gives the scalar a' + a² + κ ≤ 0. Works along radial geodesics (ODE in t); avoids needing r = dist smooth or the eikonal.

= our notes Kapovitch CH21 (which draw the Jacobi-field machinery from Lee, Introduction to Riemannian Manifolds 2e, Ch 10: Jacobi/variational fields Thm 10.1, ODE existence Prop 10.2, conjugate points), and = Lee Ch 11 (comparison theory built on the matrix Riccati for Jacobi fields).

The complementary Method ② (Laplacian-of-distance Δr) is Route A / #85 = Petersen, Riemannian Geometry §7.1 (∂_r Δr + (Δr)²/(n-1) ≤ -Ric, polar volume ∂_r λ = λ Δr), verified directly from the book.