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.

Toponogov comparison on a round sphere

Example

Assume the inherited Axiom of Countable Choice ${A C}_{ω}$ . Fix $k > 0$ , put $R : = 1 / \sqrt{k}$ , let $n \geq 2$ , and give the round sphere $S_{R}^{n} : = {x \in R^{n + 1} : ⟨ x, x ⟩ = R^{2}}$ the Riemannian metric $g$ induced by the Euclidean inner product (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). By Round sphere model geometry and The round sphere has positive constant sectional curvature, the manifold $(S_{R}^{n}, g)$ is complete, connected and boundaryless with constant sectional curvature $k = 1 / R^{2}$ ; realize the model surface $M_{k}^{2}$ of Comparison triangle in the two dimensional space form as a round two-sphere of radius $R$ . Then, for data satisfying the hypotheses of the comparison theorems of Toponogov hinge comparison and Toponogov triangle comparison:

Hinge equality. If $σ_{1}, σ_{2}$ are unit-speed minimizing geodesics of lengths $a, b > 0$ starting at a common point $p$ , with included angle $θ \in [0, π]$ , endpoints $x, y$ and $c : = d_{g} (x, y)$ , and if the hinge datum is admissible, then $c = c_{k} (a, b, θ)$ : the hinge comparison is an equality.
Self-comparison and angle equality. If $x, y, z \in S_{R}^{n}$ are joined by minimizing geodesic segments with admissible side lengths $(a, b, c)$ , then each actual vertex angle equals the corresponding comparison angle, and the triangle is its own comparison triangle: its vertices lie in a round two-sphere of radius $R$ inside $S_{R}^{n}$ , and an isometry of that two-sphere onto the model $M_{k}^{2}$ carries the triangle, together with its three minimizing sides, to a comparison triangle with side lengths $(a, b, c)$ .
Side-point equality (diagnostic). For admissible hinge data and the points $u = σ_{1} (s)$ , $v = σ_{2} (t)$ with $s \in [0, a]$ , $t \in [0, b]$ , one has $d_{g} (u, v) = d_{k} (\overset{ˉ}{u}, \overset{ˉ}{v})$ for the corresponding points $\overset{ˉ}{u}, \overset{ˉ}{v}$ of a model hinge with the same lengths and included angle: the model attains equality in the corresponding-side-point comparison. This is a direct computation for the model and is not used as a proof of the general comparison theorem.

Here admissible means that the hypotheses of the respective comparison theorem are satisfied: for a hinge, $σ_{1}, σ_{2}$ are unit-speed minimizing geodesics with positive lengths and, since $k > 0$ , $a, b, c < π R, a + b + c < 2 π R;$ for a triangle, the three positive side lengths satisfy the strict triangle inequalities and the same two displayed bounds, so that a comparison triangle in $M_{k}^{2}$ exists. In general the two theorems give only the inequality $c \leq c_{k} (a, b, θ)$ and the angle inequality; the example shows that on the round sphere both are equalities, and it identifies the actual triangle with a comparison triangle through the standard isometry between a great two-sphere and the model.

Facts & Assumptions

Given: The inherited ${A C}_{ω}$ of [A1]; the curvature $k > 0$ and the radius $R = 1 / \sqrt{k}$ ; the dimension $n \geq 2$ ; the round sphere $S_{R}^{n}$ with its induced metric $g$ ; the model $M_{k}^{2}$ realized as a round two-sphere of radius $R$ ; and, for the three claims, the data: hinge geodesics $σ_{1}, σ_{2}$ with common initial point $p$ , lengths $a, b > 0$ , unit initial directions $v_{1}, v_{2}$ , included angle $θ \in [0, π]$ and endpoints $x, y$ at distance $c$ ; triangle vertices $x, y, z$ joined by minimizing geodesic segments with side lengths $a, b, c > 0$ ; and the side points $u = σ_{1} (s)$ , $v = σ_{2} (t)$ , $s \in [0, a]$ , $t \in [0, b]$ , all data assumed admissible in the sense of the Example.

[A1]

The countable-choice premise is the inherited ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), carried here by the exponential-map, cut-locus and comparison interfaces cited below. The example selects no family of objects: the only selections below are single selections from the nonempty finite-dimensional sets specified in step 3.1.

[F1]

Round-sphere geometry (Round sphere model geometry, The round sphere has positive constant sectional curvature, Constant sectional curvature and space form, Riemannian distance on a connected manifold): $S_{R}^{n}$ is a nonempty, connected, boundaryless embedded $n$ -manifold in $R^{n + 1}$ with $T_{x} S_{R}^{n} = x^{⊥}$ , the induced metric is the restriction of the Euclidean inner product, it makes $S_{R}^{n}$ geodesically complete and hence metrically complete, and the Riemannian distance is the metric distance on this connected manifold. Its sectional curvature is constantly $1 / R^{2} = k$ , so $(S_{R}^{n}, g)$ is a complete, connected, boundaryless manifold with $K \geq k$ , and the two-dimensional model $M_{k}^{2}$ is the round two-sphere of radius $R$ .

[F2]

Explicit geodesics and the distance formula (Round sphere model geometry, Existence uniqueness and smooth dependence of geodesics, Principal inverse sine and inverse cosine): for $p \in S_{R}^{n}$ and a unit vector $v \in T_{p} S_{R}^{n}$ , the maximal geodesic with $γ (0) = p$ , $γ^{'} (0) = v$ is $γ_{p, v} (t) = \cos (t / R) p + R \sin (t / R) v, t \in R,$ and it has unit speed. For all $p, q \in S_{R}^{n}$ , $d_{g} (p, q) = R \arccos ⁣ (\frac{⟨ p, q ⟩}{R^{2}}),$ the argument lying in $[- 1, 1]$ by Cauchy–Schwarz (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs); in particular $d_{g} (p, γ_{p, v} (t)) = t$ for $0 \leq t \leq π R$ , and for every real $δ$ with $0 < δ < 2 π$ one has $\arccos (\cos δ) = \min {δ, 2 π - δ}$ , because for $δ \in (0, π]$ this is the inverse property of the principal inverse cosine and for $δ \in [π, 2 π)$ one uses $\cos (2 π - δ) = \cos δ$ with $2 π - δ \in (0, π]$ .

[F3]

Unique maximal geodesics (Existence uniqueness and smooth dependence of geodesics): for every $(p, v) \in T S_{R}^{n}$ there is exactly one maximal geodesic with initial data $(p, v)$ , and every geodesic segment with those initial data is its restriction.

[F4]

Model comparison data (Comparison triangle in the two dimensional space form, Toponogov hinge comparison, Toponogov triangle comparison): $c_{k} (A, B, θ)$ denotes the distance in $M_{k}^{2}$ between the endpoints of unit-speed geodesics of lengths $A, B > 0$ issuing from a common point with included angle $θ$ ; the number is independent of the choices made. For fixed $A, B > 0$ with $A, B < π R$ the map $c_{k} (A, B, \cdot)$ is continuous and strictly increasing on $[0, π]$ , it is the inverse of the comparison-angle function, $c_{k} (A, B, Φ_{A, B} (C)) = C for ∣ A - B ∣ < C < m (A, B),$ where $m (A, B) : = \min {A + B, 2 π R - A - B}$ , and its endpoint values are $c_{k} (A, B, 0) = ∣ A - B ∣$ and $c_{k} (A, B, π) = m (A, B)$ . The comparison angle at the vertex opposite the side $C$ between the sides $A$ and $B$ is the unique $\overset{ˉ}{α} \in (0, π)$ with $\cos \overset{ˉ}{α} = F_{A, B} (C) : = \frac{\cos (C / R) - \cos (A / R) \cos (B / R)}{\sin (A / R) \sin (B / R)},$ and a comparison triangle with side lengths $(A, B, C)$ exists, uniquely up to the isometries of $M_{k}^{2}$ , exactly when the positive side lengths satisfy the strict triangle inequalities and $A, B, C < π R$ , $A + B + C < 2 π R$ . Under their stated hypotheses the hinge comparison gives $C \leq c_{k} (A, B, θ)$ and the triangle comparison gives that each actual vertex angle is at least the corresponding comparison angle.

[F5]

Angles (Pointwise norm and angle from a riemannian metric): for nonzero tangent vectors in one tangent space, the angle is the unique $θ \in [0, π]$ with $\cos θ = g (u, w) / (∣ u ∣_{g} ∣ w ∣_{g})$ ; in particular for unit vectors $\cos θ = g (u, w)$ .

[F6]

Euclidean bilinearity, Cauchy–Schwarz and addition formulas (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, The addition formulas for sine and cosine): the Euclidean inner product is bilinear and symmetric, $∣ ⟨ u, w ⟩ ∣ \leq ∣ u ∣ ∣ w ∣$ with equality only for linearly dependent $u, w$ , and $\cos (x \pm y) = \cos x \cos y \mp \sin x \sin y$ .

[F7]

Isometries and orthonormal bases (Every finite-dimensional real or complex inner product space has an orthonormal basis, Riemannian isometry and local isometry, Riemannian isometries preserve length and distance): every finite-dimensional real inner product space has an orthonormal basis. A Riemannian isometry $F$ is a diffeomorphism with $F^{*} h = g$ , hence for tangent vectors $ξ, η$ one has $g_{x} (ξ, η) = h_{F (x)} (d F_{x} ξ, d F_{x} η)$ , so isometries preserve angles as defined in [F5]; they also preserve the lengths of curves and the distances between points. A linear isometry $L : V \to R^{3}$ of a three-dimensional subspace $V \subseteq R^{n + 1}$ satisfies $⟨ L u, L v ⟩ = ⟨ u, v ⟩$ , so its restriction $L ∣_{V \cap S_{R}^{n}}$ is a Riemannian isometry onto the round sphere $S_{R}^{2}$ .

Verification

technique · direct: the round sphere has explicit geodesics and an explicit distance formula, so each comparison quantity is computed on both sides from the same two formulas and the values are identified; an explicit linear isometry between a great two-sphere containing the triangle and the model realizes the triangle as its own comparison triangle

1.1A1F1F2F3F4given

Setup and explicit sides. By [F1] the sphere $(S_{R}^{n}, g)$ is complete, connected and boundaryless with constant curvature $k$ , so it satisfies the curvature hypothesis $K \geq k$ of both comparison theorems of [F4]. The two hinge legs and the three triangle sides have positive lengths below $π R$ by admissibility; the hinge endpoint distance $c$ may be zero. Let $σ$ be such a segment, with starting point $p : = σ (0)$ and initial unit vector $v : = σ^{'} (0)$ ; by [F3] it is the restriction to its interval of the maximal geodesic $γ_{p, v}$ , so [F2] gives $σ (t) = \cos (t / R) p + R \sin (t / R) v, 0 \leq t \leq L,$ where $L$ is the length of $σ$ , and $⟨ p, p ⟩ = R^{2}$ , $⟨ p, v ⟩ = 0$ , $⟨ v, v ⟩ = 1$ . In particular every endpoint of the given hinge and triangle data is of this form, and, for two points $x, y$ obtained this way from a common base point, the distance $d_{g} (x, y)$ is computed from the Euclidean inner product $⟨ x, y ⟩$ by the distance formula of [F2].

2.1F2F3F4F5F6step 1.1given

Hinge equality. Write $v_{1} : = σ_{1}^{'} (0)$ and $v_{2} : = σ_{2}^{'} (0)$ . By [F5] the included angle satisfies $\cos θ = ⟨ v_{1}, v_{2} ⟩$ , since $g$ is the Euclidean inner product. Step 1.1 gives $x = \cos (a / R) p + R \sin (a / R) v_{1}, y = \cos (b / R) p + R \sin (b / R) v_{2},$ so bilinearity and $⟨ p, p ⟩ = R^{2}$ , $⟨ p, v_{i} ⟩ = 0$ , $⟨ v_{i}, v_{i} ⟩ = 1$ give $⟨ x, y ⟩ = R^{2} (\cos (a / R) \cos (b / R) + \sin (a / R) \sin (b / R) \cos θ) .$ The distance formula of [F2] therefore yields $c = d_{g} (x, y) = R \arccos (\cos (a / R) \cos (b / R) + \sin (a / R) \sin (b / R) \cos θ) .$ On the model side, [F4] says that $c_{k} (a, b, θ)$ is independent of the choices made; choose a model hinge in the realization $M_{k}^{2} = S_{R}^{2}$ , i.e. a point $\overset{ˉ}{p} \in S_{R}^{2}$ and unit-speed geodesics ${\overset{ˉ}{σ}}_{1}, {\overset{ˉ}{σ}}_{2}$ from $\overset{ˉ}{p}$ of lengths $a, b$ with included angle $θ$ , and write ${\overset{ˉ}{v}}_{i} : = {\overset{ˉ}{σ}}_{i}^{'} (0)$ , so that $⟨ {\overset{ˉ}{v}}_{1}, {\overset{ˉ}{v}}_{2} ⟩ = \cos θ$ by [F5]. The formulas of [F2] hold on $S_{R}^{2}$ as well (they are stated for every $n \geq 2$ ), so the same computation with $\overset{ˉ}{p}, {\overset{ˉ}{v}}_{1}, {\overset{ˉ}{v}}_{2}$ in place of $p, v_{1}, v_{2}$ gives $c_{k} (a, b, θ) = R \arccos (\cos (a / R) \cos (b / R) + \sin (a / R) \sin (b / R) \cos θ) .$ The two displayed values are equal, so $c = c_{k} (a, b, θ)$ : the hinge comparison of [F4], which asserts $c \leq c_{k} (a, b, θ)$ for these data, is an equality. The computation makes no use of the strictness of the inequalities $a, b, c < π R$ and $a + b + c < 2 π R$ beyond the well-definedness of the model hinge, which [F4] supplies.

2.2F2F3step 1.1given

Minimizing segments below the diameter are unique. Let $σ, τ$ be unit-speed minimizing geodesics in $S_{R}^{n}$ from a point $p$ to a point $q$ with $0 < L : = d_{g} (p, q) < π R$ . By [F3] and the explicit formula of [F2], $σ (t) = \cos (t / R) p + R \sin (t / R) σ^{'} (0)$ and $τ (t) = \cos (t / R) p + R \sin (t / R) τ^{'} (0)$ for $0 \leq t \leq L$ . Evaluating at $t = L$ , where both curves meet $q$ , gives $\cos (L / R) p + R \sin (L / R) σ^{'} (0) = \cos (L / R) p + R \sin (L / R) τ^{'} (0) .$ Since $0 < L / R < π$ , one has $\sin (L / R) > 0$ , so $σ^{'} (0) = τ^{'} (0)$ and hence $σ = τ$ . Consequently, in admissible triangle data the minimizing geodesic segment between two vertices at distance $< π R$ is unique, and the actual angles of the Example are independent of the choice of minimizing sides.

2.3F2F4F5step 1.1given

Angle equality by the spherical law of cosines. At the vertex $x$ of the triangle let the sides to $y$ and $z$ have lengths $c$ and $b$ , so that the opposite side is $a = d_{g} (y, z)$ , and let $α \in [0, π]$ be the angle at $x$ , between the unit directions $v : = σ_{x y}^{'} (0)$ and $w : = σ_{x z}^{'} (0)$ . By [F5], $\cos α = ⟨ v, w ⟩$ , and step 1.1 gives $y = \cos (c / R) x + R \sin (c / R) v, z = \cos (b / R) x + R \sin (b / R) w .$ Bilinearity and $⟨ x, x ⟩ = R^{2}$ , $⟨ x, v ⟩ = ⟨ x, w ⟩ = 0$ , $⟨ v, v ⟩ = ⟨ w, w ⟩ = 1$ yield $⟨ y, z ⟩ = R^{2} (\cos (b / R) \cos (c / R) + \sin (b / R) \sin (c / R) \cos α) .$ On the other hand $a = d_{g} (y, z) < π R$ , so the distance formula of [F2] gives $⟨ y, z ⟩ = R^{2} \cos (a / R)$ . Equating the two expressions and dividing by $\sin (b / R) \sin (c / R)$ , which is nonzero because $0 < b, c < π R$ , gives $\cos α = \frac{\cos (a / R) - \cos (b / R) \cos (c / R)}{\sin (b / R) \sin (c / R)} = F_{b, c} (a),$ the model expression of [F4] with $(A, B, C) = (b, c, a)$ . By [F4] the comparison angle $\overset{ˉ}{α} \in (0, π)$ opposite the side $a$ is the unique element of $(0, π)$ with $\cos \overset{ˉ}{α} = F_{b, c} (a)$ , while $α \in [0, π]$ by [F5]; cosine is injective on $[0, π]$ , so $α = \overset{ˉ}{α}$ . Cycling the roles of the vertices gives the equality at $y$ and at $z$ as well, with $β = \overset{ˉ}{β}$ and $γ = \overset{ˉ}{γ}$ .

3.1F1F2F4F7step 1.1step 2.3given

The triangle is its own comparison triangle. Let $W : = span {x, y, z} \subseteq R^{n + 1}$ . The distinct vertices $x, y$ are not antipodal because $0 < d_{g} (x, y) < π R$ , so they are linearly independent; hence $2 \leq \dim W \leq 3$ . There is a three-dimensional subspace $V$ with $W \subseteq V$ : if $\dim W = 3$ take $V = W$ ; otherwise $W^{⊥}$ is nonzero because $\dim W^{⊥} = n + 1 - \dim W \geq 3 - 2 > 0$ , and we take $V = W \oplus R u$ for one nonzero $u \in W^{⊥}$ . Then $x, y, z \in V$ , and each of the three minimizing sides lies in $V$ : by step 1.1 the side from a vertex $r$ to the other endpoint with unit direction $v$ is $t \mapsto \cos (t / R) r + R \sin (t / R) v$ , and this lies in $span {r, v} \subseteq V$ , since $v$ is determined by the two endpoints. By [F7] choose an orthonormal basis $(e_{1}, e_{2}, e_{3})$ of $V$ and define $L : V \to R^{3}$ by $L (α_{1} e_{1} + α_{2} e_{2} + α_{3} e_{3}) = (α_{1}, α_{2}, α_{3})$ ; then $L$ is a linear isometry, $⟨ L u, L w ⟩ = ⟨ u, w ⟩$ for $u, w \in V$ . Its restriction $Φ : = L ∣_{V \cap S_{R}^{n}}$ maps the round two-sphere $V \cap S_{R}^{n}$ of radius $R$ bijectively onto $S_{R}^{2}$ and is a Riemannian isometry by [F7], because on both spheres the metric is the restriction of the ambient Euclidean inner product. Hence $Φ$ preserves distances, lengths and angles. For a minimizing side $σ$ of the triangle, with unit direction $v$ at its startpoint $r$ and length $L_{0}$ , the curve $Φ \circ σ$ satisfies $Φ \circ σ (t) = \cos (t / R) Φ (r) + R \sin (t / R) L (v), 0 \leq t \leq L_{0},$ where $L (v)$ is a unit tangent vector of $S_{R}^{2}$ at $Φ (r)$ . By [F2] applied to $S_{R}^{2}$ , this is the unit-speed geodesic of the model with those initial data, so its length is $L_{0}$ ; and its endpoints have model distance $L_{0}$ because $Φ$ preserves distances. It is therefore a minimizing geodesic segment of the model. Applying this to the three sides, the triple $(Φ (x), Φ (y), Φ (z))$ , together with their image segments, has pairwise model distances $a, b, c$ and is thus a comparison triangle with side lengths $(a, b, c)$ in the model $M_{k}^{2}$ . Since $Φ$ preserves angles, its angles are the actual angles $α, β, γ$ , which by step 2.3 are the comparison angles; and comparison triangles with these side lengths are unique up to isometries of $M_{k}^{2}$ by [F4]. Hence, under the identification of the great two-sphere $V \cap S_{R}^{n}$ with the model by the isometry $Φ$ , the actual triangle is its own comparison triangle.

3.2F2F4step 1.1step 2.1given

Side-point equality. Write $u = σ_{1} (s) = \cos (s / R) p + R \sin (s / R) v_{1}$ and $v = σ_{2} (t) = \cos (t / R) p + R \sin (t / R) v_{2}$ by step 1.1, with $v_{1}, v_{2}$ unit and $⟨ v_{1}, v_{2} ⟩ = \cos θ$ . The bilinear computation of step 2.1 with $s, t$ in place of $a, b$ gives $⟨ u, v ⟩ = R^{2} (\cos (s / R) \cos (t / R) + \sin (s / R) \sin (t / R) \cos θ),$ so the distance formula of [F2] gives $d_{g} (u, v) = R \arccos (\cos (s / R) \cos (t / R) + \sin (s / R) \sin (t / R) \cos θ) .$ On the model side choose any point $\overset{ˉ}{p} \in S_{R}^{2} = M_{k}^{2}$ and unit vectors ${\overset{ˉ}{v}}_{1}, {\overset{ˉ}{v}}_{2} \in T_{\overset{ˉ}{p}} S_{R}^{2}$ with $⟨ {\overset{ˉ}{v}}_{1}, {\overset{ˉ}{v}}_{2} ⟩ = \cos θ$ ; such vectors exist because the tangent plane is two-dimensional. Put $\overset{ˉ}{u} : = \cos (s / R) \overset{ˉ}{p} + R \sin (s / R) {\overset{ˉ}{v}}_{1}$ and $\overset{ˉ}{v} : = \cos (t / R) \overset{ˉ}{p} + R \sin (t / R) {\overset{ˉ}{v}}_{2}$ , the model points at distances $s$ and $t$ along model geodesics of lengths $a$ and $b$ enclosing the angle $θ$ . The same computation in $S_{R}^{2}$ gives $d_{k} (\overset{ˉ}{u}, \overset{ˉ}{v}) = R \arccos (\cos (s / R) \cos (t / R) + \sin (s / R) \sin (t / R) \cos θ),$ an expression depending only on $s, t, θ$ and hence independent of the choices made. Therefore $d_{g} (u, v) = d_{k} (\overset{ˉ}{u}, \overset{ˉ}{v})$ for every $s \in [0, a]$ and $t \in [0, b]$ , including the endpoint choices $s = 0$ , $t = 0$ , $s = a$ and $t = b$ ; the case $s = a$ , $t = b$ reduces to step 2.1. This is the equality case of the corresponding-side-point comparison in the model, verified by direct computation; it is recorded as a diagnostic of the model geometry and is not used to prove the general corresponding-side-point comparison.

4.1A1F2F4F6step 1.1step 2.1step 2.2step 2.3step 3.1step 3.2given∎

Conclusion and boundary cases. [A1, F2, F4, F6, step 1.1, step 2.1, step 2.2, step 2.3, step 3.1, step 3.2, given] Steps 2.1, 2.3 and 3.2 show that on the round sphere of curvature $k$ the hinge, angle and side-point comparisons are equalities whenever their data are admissible, and step 3.1 exhibits the admissible triangle as its own comparison triangle under the isometry $Φ$ ; step 2.2 shows that the minimizing sides used are unique. The endpoint angles are covered by the same formula: if $θ = 0$ then $v_{2} = v_{1}$ by [F5] and [F6], and step 2.1 gives $c = R \arccos (\cos ((a - b) / R)) = ∣ a - b ∣ = c_{k} (a, b, 0)$ by [F2] and the endpoint value of [F4]; if $θ = π$ then $v_{2} = - v_{1}$ and step 2.1 gives $c = R \arccos (\cos ((a + b) / R)) = \min {a + b, 2 π R - a - b} = c_{k} (a, b, π)$ , because $0 < a + b < 2 π R$ and by the arccos identity of [F2] and the addition formulas of [F6]. The endpoint parameters $s, t \in {0, a} \times {0, b}$ were included in step 3.2. Triangle admissibility includes strict triangle inequalities and excludes collinear configurations. Hinge admissibility permits $θ = 0$ or $θ = π$ and hence collinear model hinges; these are covered by the endpoint formulas above, including $c = 0$ when $a = b$ and $θ = 0$ . Both kinds of data exclude sides equal to $π R$ and perimeter equal to $2 π R$ . No compactness of anything is assumed and no iff statement is made. On choice: the only selections are the single vector $u \in W^{⊥}$ and the single orthonormal basis of the three-dimensional space $V$ in step 3.1, each a selection from one nonempty set and not from a family; the inherited ${A C}_{ω}$ of [A1] suffices, and no full choice principle is used. Thus every admissible minimizing triangle of the round sphere is its own constant- $k$ comparison triangle, and all hinge, angle and side-point inequalities of the two comparison theorems become equalities.

Source locator

Lang, Riemannian and Metric Geometry, Chapter 5, Lemmas 5.1–5.2 and Theorem 5.15 (printed pp.64–70, PDF pp.67–73), gives the model cosine law, hinge monotonicity and Toponogov comparison whose equality case is exhibited here; Eschenburg, Comparison Theorems in Riemannian Geometry, §6, Theorem 6.1 and its Corollary 6.3, printed pp.21–25, proves the distance and angle comparisons for $K \geq k$ , the inequality directions used above. The computations are local: the geodesics and the distance formula are those of Round sphere model geometry, the model comparison data are those of Comparison triangle in the two dimensional space form, and the equality statements are verified on the explicit formulas rather than imported from the sources.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

103 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

U. Lang, Riemannian and Metric Geometry (lecture notes) (standard reference, not scraped)
J.-H. Eschenburg, Comparison Theorems in Riemannian Geometry (standard reference, not scraped)