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.

Bonnet-Myers for the round sphere

Example

Assume the inherited Axiom of Countable Choice ${A C}_{ω}$ . Let $k > 0$ , let $R = 1 / \sqrt{k}$ , let $n \geq 2$ , and let $S_{R}^{n} = {x \in R^{n + 1} : ∣ x ∣ = R}$ carry the Riemannian metric induced from Euclidean $R^{n + 1}$ . Then:

$S_{R}^{n}$ has constant sectional curvature $K = 1 / R^{2} = k$ , hence Ricci curvature $Ric = (n - 1) k g$ ;
$S_{R}^{n}$ is complete and has diameter $diam (S_{R}^{n}, g) = π R = \frac{π}{\sqrt{k}};$
it therefore attains the equality case of the Bonnet–Myers bound $diam \leq π / \sqrt{k}$ : both the Ric lower bound $Ric \geq (n - 1) k g$ and the diameter bound are equalities.

Facts & Assumptions

Given: The inherited ${A C}_{ω}$ of [A1], a real number $k > 0$ , the radius $R = 1 / \sqrt{k}$ , an integer $n \geq 2$ , the round sphere $S_{R}^{n}$ with its induced Riemannian metric $g$ , and the metric diameter $diam (S_{R}^{n}, g) = \sup_{p, q} d_{g} (p, q)$ .

[A1]

The countable-choice premise is the inherited ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), carried by the sectional-curvature, cut-locus and Hopf–Rinow interfaces cited below; every point and curve below is explicit.

[F1]

The round sphere $S_{R}^{n}$ with the induced metric has constant sectional curvature $1 / R^{2}$ for $n \geq 2$ (The round sphere has positive constant sectional curvature); this is the constant-curvature predicate of Constant sectional curvature and space form.

[F2]

Constant curvature: a manifold of constant sectional curvature $k$ has curvature tensor $R (X, Y) Z = k (g (Y, Z) X - g (X, Z) Y)$ (Curvature tensor of constant sectional curvature); the Ricci tensor is $Ric (X, Y) = tr (Z \mapsto R (Z, X) Y)$ (Ricci curvature) and equals $\sum_{i} Rm (e_{i}, X, Y, e_{i})$ in an orthonormal basis (Ricci curvature is symmetric and basis independent), with $Rm (A, B, C, D) = g (R (A, B) C, D)$ and $K = Rm (u, v, v, u)$ for an orthonormal pair (Riemann curvature four-tensor, Sectional curvature).

[F3]

Cut locus of the round sphere: 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$ and the cut locus is the antipodal singleton $Cut (p) = {- p}$ (Round sphere model geometry); the radial geodesics are the great circles of Great circles as round-sphere geodesics, and for $0 < t < c_{p} (v)$ the radial geodesic is minimizing, $d_{g} (p, \exp_{p} (t v)) = t$ , by the definition of the cut time (Cut time in a unit tangent direction).

[F4]

A compact boundaryless Riemannian manifold is geodesically complete, and each connected component is metrically complete (Compact Riemannian manifolds are geodesically complete), and geodesic completeness gives metric completeness by Hopf–Rinow; the Riemannian distance makes a connected Riemannian manifold a metric space (Riemannian distance on a connected manifold).

[F5]

Bonnet–Myers: a nonempty, complete, connected, boundaryless Riemannian manifold of dimension $n \geq 2$ with $Ric \geq (n - 1) k g$ , $k > 0$ , has $diam \leq π / \sqrt{k}$ (Bonnet myers, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

Verification

Proof technique: direct: the round sphere has constant curvature $k$ , its Ricci tensor is traced from the constant-curvature tensor identity, and the diameter is read off from the cut locus, where the antipode lies at distance $π R$ .

1.1F1given

The round sphere has $K = k$ . [F1, given] By [F1] the sectional curvature is everywhere $1 / R^{2}$ , and $R = 1 / \sqrt{k}$ gives $1 / R^{2} = k$ ; in particular $K = k > 0$ and the space is a space form in the sense of [F1].

2.1F2step 1.1

The Ricci curvature is $Ric = (n - 1) k g$ . [F2, step 1.1] Let $p \in S_{R}^{n}$ and let $(e_{1}, \dots, e_{n})$ be an orthonormal basis of $T_{p} S_{R}^{n}$ . By step 1.1 the manifold has constant sectional curvature $k$ , so [F2] gives $R (A, B) C = k (g (B, C) A - g (A, C) B)$ for all tangent vectors. Substituting into the orthonormal-basis formula of [F2], $Ric (X, Y) = \sum_{i = 1}^{n} Rm (e_{i}, X, Y, e_{i}) = \sum_{i = 1}^{n} k (g (X, Y) g (e_{i}, e_{i}) - g (e_{i}, Y) g (X, e_{i})) = k (n g (X, Y) - g (X, Y)) = (n - 1) k g (X, Y) .$ Hence $Ric = (n - 1) k g$ , and in particular the Bonnet–Myers lower bound holds with equality at every point and every tangent vector.

3.1F3F4givenstep 2.1

The sphere is complete and its diameter is $π / \sqrt{k}$ . [F3, F4, given, step 2.1] The sphere $S_{R}^{n}$ is a closed and bounded subset of $R^{n + 1}$ , hence compact. It is connected and boundaryless by the round-sphere geometry of [F3], so [F4] makes it complete. Diameter: fix $p \in S_{R}^{n}$ . Every point $q \in S_{R}^{n}$ either is the antipode $q = - p$ or lies outside the cut locus ${- p}$ of [F3]. In the second case the distance formula of Round sphere model geometry gives $d_{g} (p, q) < π R$ , including $q = p$ with distance zero; in the first case the radial geodesic in the direction of $v$ with $\exp_{p} (π R v) = - p$ has length $π R$ and is minimizing, because the cut time is exactly $π R$ , so $d_{g} (p, - p) = π R$ . Therefore $\sup_{q} d_{g} (p, q) = π R$ , and since $p$ was arbitrary, $diam (S_{R}^{n}, g) = π R = \frac{π}{\sqrt{k}}$ by the definition of the diameter in [F5].

4.1F5step 2.1step 3.1∎

Equality in Bonnet–Myers, and the boundary cases. [F5, step 2.1, step 3.1] By step 2.1 the sphere satisfies $Ric \geq (n - 1) k g$ with equality everywhere, and it is complete, connected, boundaryless and of dimension $n \geq 2$ ; [F5] gives $diam \leq π / \sqrt{k}$ , and step 3.1 gives $diam = π / \sqrt{k}$ : the diameter bound is attained, so the example is an equality case of Bonnet–Myers. The case $n = 2$ is included and is the minimal dimension for which the statement and Bonnet–Myers are formulated; the parameter $k > 0$ is essential, since for $k = 0$ the Euclidean space has unbounded pairwise distances and Ricci curvature $0$ ; its diameter is undefined under Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space. The radius is normalized to $R = 1 / \sqrt{k}$ so that the curvature is exactly $k$ ; for a general radius $r$ the same computation gives $K = 1 / r^{2}$ and diameter $π r$ . No choice beyond the inherited [A1] is used: the sphere, its antipodal point and the great circles are explicit.

Source locator

Datar §27.1 and §28.2, pp.199–200 and 210–212, and Eschenburg §12, pp.59–62, present the round sphere of curvature $k$ as the equality case of Myers' diameter bound. The curvature and cut-locus computations are those of the published round-sphere items cited in [F1]–[F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

98 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)