ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Bishop gromov ratio is constant in the model space

Example

Assume the inherited Axiom of Countable Choice ${A C}_{ω}$ . Let $n \geq 2$ and $k \in R$ , and let $(M, g)$ be a complete, connected, simply connected Riemannian $n$ -manifold of constant sectional curvature $k$ ; when $k > 0$ take $(M, g)$ to be the round sphere $S_{1 / \sqrt{k}}^{n}$ , the simply connected space form of positive curvature $k$ . Then for every $p \in M$ and every radius $r > 0$ the open metric ball $B (p, r)$ has the saturated model volume ${vol}_{g} (B (p, r)) = V_{k}^{⋆} (r),$ and consequently the Bishop–Gromov ratio $R_{p} (r) = {vol}_{g} (B (p, r)) / V_{k}^{⋆} (r)$ is equal to $1$ at every positive radius. The ratio is thus constant in $r$ ; for $k > 0$ this constancy continues past the spherical endpoint $r = π / \sqrt{k}$ , where the numerator and the saturated denominator both saturate. The standard realizations are the round sphere for $k > 0$ , Euclidean $n$ -space for $k = 0$ and hyperbolic $n$ -space for $k < 0$ ; for $k \leq 0$ the computation below applies to every complete, connected, simply connected constant-curvature- $k$ manifold, not only to the named realization.

Facts & Assumptions

Given: The inherited ${A C}_{ω}$ of [A1]; the dimension $n \geq 2$ ; the curvature $k \in R$ ; a complete, connected, simply connected Riemannian $n$ -manifold $(M, g)$ of constant sectional curvature $k$ , equal to the round sphere $S_{1 / \sqrt{k}}^{n}$ when $k > 0$ ; a point $p \in M$ ; a radius $r > 0$ ; the unit sphere $S_{p} M = {v \in T_{p} M : ∣ v ∣_{g_{p}} = 1}$ ; the polar surface measure $σ_{p}$ ; the radial geodesics $γ_{v} (t) = \exp_{p} (t v)$ with cut times $c_{p} (v)$ ; the radial Jacobi tensor $A (t)$ of $γ_{v}$ and the radial volume Jacobian $J_{p} (t, v)$ ; and the model functions ${sn}_{k}$ , $A_{k}$ , $V_{k}$ and $V_{k}^{⋆}$ .

[A1]

The countable-choice premise is the inherited ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), carried by the cut-time, polar-integration, Cartan–Hadamard and Hopf–Rinow interfaces below; no further selection is made.

[F1]

Polar integration (Polar integration may discard the cut locus): $(M, g)$ is complete, connected and boundaryless, $σ_{p}$ is the finite Borel measure on $S_{p} M$ obtained by transporting the polar surface measure of the unit sphere, and for every Borel $f : M \to [0, \infty]$ , $\int_{M} f d {vol}_{g} = \int_{S_{p} M} \int_{0}^{c_{p} (v)} f (γ_{v} (t)) \det a_{v} (t) d t d σ_{p} (v),$ where $a_{v} (t)$ is the matrix of the radial Jacobi fields in a parallel orthonormal frame, with $\det a_{v} (t) > 0$ for $0 < t < c_{p} (v)$ .

[F2]

Radial Jacobi tensor and radial volume Jacobian (Radial Jacobi tensor, Radial volume jacobian): for $w$ in the normal space $N_{0} = {X \in T_{p} M : g_{p} (X, v) = 0}$ the map $t \mapsto A (t) w$ is the unique Jacobi field along $γ_{v}$ with $A (0) w = 0$ and $D_{t} (A w) (0) = w$ ; in the parallel identification ${\overset{ˉ}{A}}_{v} (t) = P_{t}^{- 1} \circ A (t)$ one has $J_{p} (t, v) = \det {\overset{ˉ}{A}}_{v} (t) > 0$ for $0 < t < c_{p} (v)$ , and $\det a_{v} (t) = J_{p} (t, v)$ in the notation of [F1]. Moreover $\dim N_{0} = n - 1$ .

[F3]

Model fields and comparison functions (Model jacobi fields in positive zero and negative curvature, Model functions solve the constant curvature jacobi equation, Comparison sine, cosine and cotangent functions, Constant sectional curvature and space form): on a Riemannian manifold of constant sectional curvature $k$ , the Jacobi field with $J (0) = 0$ , $D_{t} J (0) = E \in N_{0}$ satisfies $J (t) = {sn}_{k} (t) P_{t} E$ for every $t$ , so the radial Jacobi tensor is $A (t) = {sn}_{k} (t) P_{t}$ and its parallel-frame matrix is ${\overset{ˉ}{A}}_{v} (t) = {sn}_{k} (t) \cdot {i d}_{N_{0}}$ . The comparison sine is given by ${sn}_{0} (t) = t$ , ${sn}_{- a^{2}} (t) = \sinh (a t) / a$ for $a > 0$ and ${sn}_{k} (t) = \sin (\sqrt{k} t) / \sqrt{k}$ for $k > 0$ , it is positive on its positive domain $(0, π / \sqrt{k})$ for $k > 0$ and $(0, \infty)$ for $k \leq 0$ , and it satisfies ${sn}_{k}^{''} + k {sn}_{k} = 0$ .

[F4]

Cut time and minimizing initial intervals (Cut time in a unit tangent direction, Minimizing along a geodesic is an initial interval property): $c_{p} (v) = \sup {t > 0 : d_{g} (p, γ_{v} (t)) = t} \in (0, + \infty]$ , the set $A_{p} (v) = {t \geq 0 : d_{g} (p, γ_{v} (t)) = t}$ is an initial interval, and if $c_{p} (v)$ is finite then $c_{p} (v) \in A_{p} (v)$ . Hence $d_{g} (p, γ_{v} (t)) = t$ for every $0 < t < c_{p} (v)$ : if $t < c_{p} (v) = \sup A_{p} (v)$ there is $t^{'} \in A_{p} (v)$ with $t^{'} > t$ , and the initial-interval property gives $t \in A_{p} (v)$ .

[F5]

Cartan–Hadamard (Cartan hadamard): a connected, boundaryless, finite-dimensional Riemannian manifold that is complete and has sectional curvature $K \leq 0$ everywhere has $\exp_{p} : T_{p} M \to M$ a smooth covering map, and if it is in addition simply connected then $\exp_{p}$ is a diffeomorphism for every $p$ ; in particular $\exp_{p}$ is then injective.

[F6]

Hopf–Rinow (Hopf–Rinow theorem): for a nonempty, connected, boundaryless Riemannian manifold, metric completeness, geodesic completeness and $E_{p} = T_{p} M$ are equivalent, and then every $x, y \in M$ are joined by a minimizing geodesic: there is $w \in T_{x} M$ with $\exp_{x} (w) = y$ and $∣ w ∣_{g_{x}} = d_{g} (x, y)$ .

[F7]

The round sphere (The round sphere has positive constant sectional curvature, Round sphere model geometry): for $k > 0$ and $R = 1 / \sqrt{k}$ , the round sphere $S_{R}^{n}$ with its induced metric is complete, has constant sectional curvature $1 / R^{2} = k$ , and for every $p \in S_{R}^{n}$ and every unit $v \in T_{p} S_{R}^{n}$ the cut time is $c_{p} (v) = π R = π / \sqrt{k}$ .

[F8]

Model volumes and the sphere measure (Model space radial area and ball volume, The polar surface set function on the unit sphere): with $ω_{n - 1}$ the total surface measure of the unit sphere $S^{n - 1} \subseteq R^{n}$ , the model radial area is $A_{k} (s) = ω_{n - 1} {sn}_{k} (s)^{n - 1}$ , the model ball volume is $V_{k} (r) = \int_{0}^{r} A_{k} (t) d t$ , and the saturated model volume is $V_{k}^{⋆} (r) = V_{k} (\min {r, π / \sqrt{k}})$ for $k > 0$ and $V_{k}^{⋆} (r) = V_{k} (r)$ for $k \leq 0$ . The measure $σ_{p}$ of [F1] is the transport of the polar surface measure of $S^{n - 1}$ by a linear isometry, hence $σ_{p} (S_{p} M) = ω_{n - 1}$ , the total surface measure being preserved by the bijection.

[F9]

Borel indicator (The Borel sigma-algebra of a topological space): the open ball $B (p, r)$ is an open subset of $M$ , hence a Borel set, and the indicator of a Borel set is a Borel function: the preimage of an open subset of $R$ under $1_{B (p, r)}$ is one of $\emptyset$ , $B (p, r)$ , $M ∖ B (p, r)$ or $M$ , according to whether the open set contains neither, only $1$ , only $0$ , or both of the values $0, 1$ . All four sets are Borel.

[F10]

Ricci curvature of a space form of curvature $k$ (Distance hessian and laplacian in space forms): such a manifold satisfies $Ric = (n - 1) k g$ ; in particular the Ricci lower bound $Ric \geq (n - 1) k g$ holds with equality.

[F11]

Bishop–Gromov comparison (Bishop gromov volume comparison): for a complete, connected, boundaryless $(M, g)$ of dimension $n \geq 2$ with $Ric \geq (n - 1) k g$ , the ratio $R_{p} (r) = {vol}_{g} (B (p, r)) / V_{k}^{⋆} (r)$ is nonincreasing on $(0, \infty)$ with $\lim_{r ↓ 0} R_{p} (r) = 1$ , it is constant on $[π / \sqrt{k}, \infty)$ when $k > 0$ , and ${vol}_{g} (B (p, r)) \leq V_{k}^{⋆} (r)$ for every $r > 0$ .

Verification

Proof technique: direct: the radial Jacobi tensor of a constant-curvature $k$ manifold is ${sn}_{k} (t)$ times parallel transport, so the polar integration formula writes the ball volume as $ω_{n - 1}$ times the integral of the model density cut off at the cut time; the cut time is $+ \infty$ for $k \leq 0$ by Cartan–Hadamard and $π / \sqrt{k}$ for the round sphere, and the saturated model volume reproduces exactly this cutoff.

1.1F2F3given

The radial density of the model. [F2, F3, given] Fix $v \in S_{p} M$ . By [F3], for every $w \in N_{0}$ the radial field is $A (t) w = {sn}_{k} (t) P_{t} w$ , so the parallel-frame matrix of $A (t)$ is the scalar matrix ${\overset{ˉ}{A}}_{v} (t) = {sn}_{k} (t) \cdot {i d}_{N_{0}}$ . Since $\dim N_{0} = n - 1$ by [F2], its determinant is $\det {\overset{ˉ}{A}}_{v} (t) = {sn}_{k} (t)^{n - 1}, 0 < t < c_{p} (v),$ and [F2] identifies this determinant with the radial volume Jacobian, $\det a_{v} (t) = J_{p} (t, v) = {sn}_{k} (t)^{n - 1}$ , in the notation of [F1].

1.2F4F5F6F7given

The cut time of the model in each curvature regime. [F4, F5, F6, F7, given] Let $v \in S_{p} M$ . Suppose first that $k \leq 0$ . Then $(M, g)$ is complete, connected, boundaryless and simply connected with constant sectional curvature $k \leq 0$ , so [F5] makes $\exp_{p} : T_{p} M \to M$ a diffeomorphism, in particular injective. Let $t > 0$ and $q : = γ_{v} (t) = \exp_{p} (t v)$ . By [F6] there is $w \in T_{p} M$ with $\exp_{p} (w) = q$ and $∣ w ∣_{g_{p}} = d_{g} (p, q)$ . Injectivity gives $w = t v$ , so $d_{g} (p, q) = ∣ w ∣_{g_{p}} = t$ ; since $t > 0$ was arbitrary, the set $A_{p} (v)$ of [F4] contains every positive time, hence $c_{p} (v) = + \infty$ . Suppose now that $k > 0$ , so that $(M, g) = S_{1 / \sqrt{k}}^{n}$ by the hypothesis of the example; then [F7] gives $c_{p} (v) = π / \sqrt{k}$ for every unit $v$ . Consequently $\min {c_{p} (v), r} = r$ when $k \leq 0$ and $\min {c_{p} (v), r} = \min {r, π / \sqrt{k}}$ when $k > 0$ , for every $r > 0$ .

2.1F1F4F8F9step 1.1step 1.2given

The ball volume as the model integral. [F1, F4, F8, F9, step 1.1, step 1.2, given] Fix the point $p$ and the radius $r > 0$ . By [F9] the ball $B (p, r)$ is Borel and $1_{B (p, r)}$ is a Borel function, so the polar formula [F1] applies to $f = 1_{B (p, r)}$ : ${vol}_{g} (B (p, r)) = \int_{S_{p} M} \int_{0}^{c_{p} (v)} 1_{B (p, r)} (γ_{v} (t)) \det a_{v} (t) d t d σ_{p} (v) .$ For $0 < t < c_{p} (v)$ the minimizing property of [F4] gives $d_{g} (p, γ_{v} (t)) = t$ , hence $1_{B (p, r)} (γ_{v} (t)) = 1_{{t < r}}$ , while step 1.1 gives $\det a_{v} (t) = {sn}_{k} (t)^{n - 1}$ . Therefore the inner integral equals the extended nonnegative integral $\int_{0}^{\min {c_{p} (v), r}} {sn}_{k} (t)^{n - 1} d t,$ a finite real number. By step 1.2 this number depends on $v$ only through the case distinction: it equals $\int_{0}^{r} {sn}_{k} (t)^{n - 1} d t$ when $k \leq 0$ and $\int_{0}^{\min {r, π / \sqrt{k}}} {sn}_{k} (t)^{n - 1} d t$ when $k > 0$ . Write $I (r)$ for this common value. The outer integrand of the polar formula is then the constant $I (r)$ , and $σ_{p}$ is a finite measure with $σ_{p} (S_{p} M) = ω_{n - 1}$ by [F8], so ${vol}_{g} (B (p, r)) = ω_{n - 1} I (r) .$

3.1F8step 1.2step 2.1given

The volume is the saturated model volume. [F8, step 1.2, step 2.1, given] Put $m : = {\begin{cases} r, & k \leq 0, \\ \min {r, π / \sqrt{k}}, & k > 0. \end{cases}$ By step 2.1 the ball volume is $ω_{n - 1} I (r)$ , and by step 1.2 the inner integral $I (r)$ is exactly $\int_{0}^{m} {sn}_{k} (t)^{n - 1} d t$ in both cases. Since $A_{k} (t) = ω_{n - 1} {sn}_{k} (t)^{n - 1}$ by [F8], ${vol}_{g} (B (p, r)) = \int_{0}^{m} A_{k} (t) d t = V_{k} (m) = V_{k}^{⋆} (r),$ the last equality being the case distinction defining the saturated model volume in [F8]. Moreover $V_{k}^{⋆} (r) > 0$ : the integrand $A_{k}$ is continuous and positive on the nondegenerate interval $(0, m)$ , by the positivity of ${sn}_{k}$ on its positive domain. The value $r = π / \sqrt{k}$ for $k > 0$ is included, since the definition of $V_{k}^{⋆}$ cuts off at that endpoint.

4.1F8F10F11step 1.2step 3.1given∎

Unit ratio, saturation and sharpness of the comparison. [F8, F10, F11, step 1.2, step 3.1, given] By step 3.1, ${vol}_{g} (B (p, r)) = V_{k}^{⋆} (r) > 0$ for every $p \in M$ and every $r > 0$ , so the Bishop–Gromov ratio is $R_{p} (r) = 1$ at every positive radius: it is a constant function of $r$ . When $k > 0$ and $r \geq π / \sqrt{k}$ , step 1.2 makes the cutoff $m = π / \sqrt{k}$ independent of $r$ , so both ${vol}_{g} (B (p, r))$ and $V_{k}^{⋆} (r) = V_{k} (π / \sqrt{k})$ are constant there; this is the saturation clause of [F8] and of the comparison [F11]. Finally, by [F10] the model space satisfies $Ric = (n - 1) k g$ , so the hypotheses of the Bishop–Gromov comparison [F11] hold, and its general conclusion $R_{p} (r) \leq 1$ with limit $1$ at the origin is attained with equality at every radius: the model space is an equality case of the comparison, and the comparison is sharp. The cases $n = 2$ , where $A_{k} = 2 π {sn}_{k}$ , and $r$ below, equal to, or above $π / \sqrt{k}$ (for $k > 0$ ) are all covered by the single cutoff $m$ ; the value $r = 0$ is excluded, as in the definition of $R_{p}$ . No choice beyond the inherited [A1] is used: the point, the radial direction $v$ , the minimizing geodesic of [F6] and the sphere realization of [F7] are fixed or explicit, and the polar, cut-time, Jacobi, Cartan–Hadamard and Hopf–Rinow interfaces carry exactly ${A C}_{ω}$ .

Source locator

Datar §§27.2 and 28.1, pp.200–209, computes the polar volume element with the model radial density ${sn}_{k}^{n - 1}$ and the model ball volume that the Bishop–Gromov quotient compares with; Eschenburg §§4–5, pp.15–20, introduces the model radial density and its integral. The computation above is carried out on the model space itself: the radial Jacobi tensor is ${sn}_{k} (t)$ times parallel transport, the cut time is $+ \infty$ in nonpositive curvature by Cartan–Hadamard and $π / \sqrt{k}$ on the round sphere, and the polar formula turns the ball volume into the saturated model volume $V_{k}^{⋆} (r)$ .

Depends on

Used by

Equality cases as diagnostics for all comparison signs Example

Dependency tree · two levels

183 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ved Datar, Lectures on Riemannian Geometry (2025) (standard reference, not scraped)
J.-H. Eschenburg, Comparison Theorems in Riemannian Geometry (standard reference, not scraped)