LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

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.

Products of CAT(0) spaces, joins of CAT(1) spaces, and round spheres

Statement

Let $(X, d_{X})$ and $(Y, d_{Y})$ be metric spaces (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

(i) The $l^{2}$ -product. Give $X \times Y$ the $l^{2}$ -product metric $d ((x, y), (x^{'}, y^{'})) : = (d_{X} (x, x^{'})^{2} + d_{Y} (y, y^{'})^{2})^{1 / 2}$ ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs). If $X$ and $Y$ are geodesic spaces, then $X \times Y$ is geodesic: for endpoints with factor distances $a$ and $b$ , a geodesic is exactly a pair of factor geodesics traversed at constant proportional speeds $a / \sqrt{a^{2} + b^{2}}$ and $b / \sqrt{a^{2} + b^{2}}$ (with the constant path when $a = b = 0$ ). If $X$ and $Y$ are CAT(0) (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles(3)), then $X \times Y$ is CAT(0). The same conclusions hold with either factor replaced by a Euclidean space $E^{n}$ with its Euclidean metric.

(ii) Joins. Let $L_{1}, L_{2}$ be nonempty metric spaces of diameter at most $π$ , carrying their truncated metrics $d_{π} = \min {π, d}$ (The angular path metric, the Euclidean cone and spherical joins(2)). The construction and formula of The angular path metric, the Euclidean cone and spherical joins(5) — the quotient of $L_{1} \times L_{2} \times [0, π / 2]$ by the identifications at $θ = 0$ and $θ = π / 2$ , with $d (x, x^{'})$ the unique number in $[0, π]$ satisfying $\cos d (x, x^{'}) = \cos θ \cos θ^{'} \cos d_{π}^{1} (x_{1}, x_{1}^{'}) + \sin θ \sin θ^{'} \cos d_{π}^{2} (x_{2}, x_{2}^{'})$ — is a metric of diameter at most $π$ on the spherical join $L_{1} * L_{2}$ , still with the conventions $L * \emptyset = \emptyset * L = L$ . The natural radial map $C (L_{1}) \times C (L_{2}) \to C (L_{1} * L_{2})$ , sending $((r, x), (s, y))$ to the apex if $R = 0$ and otherwise to radius $R = \sqrt{r^{2} + s^{2}}$ in the join direction $(\cos θ) x + (\sin θ) y$ with $\cos θ = r / R$ and $\sin θ = s / R$ , is an isometry for the square-sum product metric of (i) (The angular path metric, the Euclidean cone and spherical joins(3)). Consequently, if $L_{1}$ and $L_{2}$ are CAT(1), then $L_{1} * L_{2}$ is CAT(1). In particular, for a one-point space ${p}$ the spherical cone ${p} * L$ is CAT(1) if and only if $L$ is CAT(1).

(iii) Round spheres, balls and convex subspaces. For every $k \geq 0$ the round sphere $S^{k}$ with the metric $d_{S} (x, y) = \arccos ⟨ x, y ⟩$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ , Principal inverse sine and inverse cosine, Pi is the first positive zero of sine) is CAT(1); every closed ball $\overset{ˉ}{B} (x, ρ) \subseteq S^{k}$ with $0 < ρ < π / 2$ (Open ball, closed ball and sphere in a metric space) is convex and CAT(1) for the induced metric; and every nonempty convex subset $Z$ of a CAT(1) space, with the induced metric, is CAT(1), where convex means that every pair of points of $Z$ at distance $< π$ is joined by a geodesic segment of the ambient space lying in $Z$ (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences(ii), (v)). Consequently, if $L$ is CAT(1) of diameter at most $π$ and $D$ is a nonempty closed ball of positive radius $< π / 2$ in some $S^{k}$ , then the join $D * L$ is CAT(1).

Facts & Assumptions

Given: Metric spaces $(X, d_{X})$ , $(Y, d_{Y})$ and, in (ii) and (iii), nonempty metric spaces $L_{1}, L_{2}, L$ of diameter at most $π$ carrying their truncations $d_{π} = \min {π, d}$ .

[F1]

A metric space is CAT(0) when it is geodesic and every geodesic triangle satisfies the Euclidean comparison inequality; it is CAT(1) when every pair of points at distance $< π$ is joined by a geodesic segment and every geodesic triangle of perimeter $< 2 π$ satisfies the spherical comparison inequality; the empty metric space satisfies both tests vacuously and a one-point space is CAT(0) and CAT(1). (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles)

[F2]

A continuous path has length the supremum of its polygonal sums, and a space is a length space when every pair of points is joined by paths of length arbitrarily close to their distance; geodesic segments are isometric parametrizations of intervals. (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles)

[F3]

The Euclidean plane is CAT(0); for $n \geq 2$ the round sphere $S^{n - 1}$ with $d_{S} (x, y) = \arccos (x \cdot y)$ is a geodesic space whose geodesic segments are the minimal great-circle arcs, pairs at distance $< π$ have a unique such segment, and every closed ball of positive radius $< π / 2$ is convex. (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences)

[F4]

A geodesic space is CAT(0) if and only if for every geodesic triangle with vertices $z, x, y$ and every point $p_{t}$ of a side $[x, y]$ at fraction $t$ one has $d (z, p_{t})^{2} \leq (1 - t) d (z, x)^{2} + t d (z, y)^{2} - t (1 - t) d (x, y)^{2}$ . (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences)

[F5]

In a CAT(1) space every closed ball of positive radius $< π / 2$ is convex, and the round circle $S_{ℓ}^{1}$ is CAT(1) if and only if $ℓ \geq 2 π$ . (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences)

[F6]

A metric space is CAT(1) exactly when its Euclidean cone is CAT(0), and the cone is formed with the truncation at $π$ . (Berestovskii's cone criterion and the polyhedral link criterion)

[F7]

The Euclidean cone $C (L)$ on a metric space $L$ with truncated metric $d_{π}$ is ${o} ⊔ ((0, \infty) \times L)$ with $d_{C} (o, (r, x)) = r$ and $d_{C} ((r, x), (s, y))^{2} = r^{2} + s^{2} - 2 r s \cos d_{π} (x, y)$ , and the spherical join $L_{1} * L_{2}$ is the quotient of $L_{1} \times L_{2} \times [0, π / 2]$ with $\cos d (x, x^{'}) = \cos θ \cos θ^{'} \cos d_{π}^{1} (x_{1}, x_{1}^{'}) + \sin θ \sin θ^{'} \cos d_{π}^{2} (x_{2}, x_{2}^{'})$ , with the conventions $L * \emptyset = L$ and $\emptyset * \emptyset = \emptyset$ . (The angular path metric, the Euclidean cone and spherical joins)

[F8]

The cone formula defines a metric, the join formula defines a metric of diameter at most $π$ , and the radial map $((r, x), (s, y)) \mapsto ξ (\sqrt{r^{2} + s^{2}})$ is an isometry $C (L_{1}) \times C (L_{2}) \to C (L_{1} * L_{2})$ for the square-sum product metric; for round spheres $S^{m - 1} * S^{n - 1} ≅ S^{m + n - 1}$ . (The cone and join metrics and the local product chart of a polyhedral gluing)

[F9]

A metric is a symmetric function vanishing exactly on the diagonal and satisfying the triangle inequality, and the Euclidean norm on $R^{n}$ satisfies the triangle inequality. (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it)

[F10]

In an inner product space, $∣ ⟨ u, v ⟩ ∣ \leq ∣ u ∣ ∣ v ∣$ , and $∣ u ∣ = ⟨ u, u ⟩^{1 / 2}$ is a norm. (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, The induced length is a norm)

[F11]

For a sphere $S^{n - 1} \subset R^{n}$ the round distance is $d_{S} (x, y) = \arccos (x \cdot y)$ with $\arccos$ the principal inverse cosine, and $\cos π = - 1$ . (Euclidean spheres and closed balls as subspaces of $R^{n}$ , Principal inverse sine and inverse cosine, Pi is the first positive zero of sine)

Proof

1.1F9F10algebra

The function $d ((x, y), (x^{'}, y^{'})) : = (d_{X} (x, x^{'})^{2} + d_{Y} (y, y^{'})^{2})^{1 / 2}$ is a metric on $X \times Y$ : symmetry and vanishing exactly on the diagonal are immediate from [F9], and the triangle inequality is the triangle inequality of the Euclidean norm on $R^{2}$ applied to the vectors $(d_{X} (x, x^{'}), d_{Y} (y, y^{'}))$ and $(d_{X} (x^{'}, x^{''}), d_{Y} (y^{'}, y^{''}))$ [F9, F10].

1.2F2F9F10algebra

Let $γ = (γ_{X}, γ_{Y})$ be a rectifiable path and put $A : = L (γ_{X})$ , $B : = L (γ_{Y})$ . For any $ε > 0$ , choose partitions whose coordinate polygonal sums exceed $A - ε$ and $B - ε$ , and take a common refinement. If $a_{i}, b_{i}$ are the two coordinate distances on its successive subintervals, then the product polygonal sum is $\sum_{i} \sqrt{a_{i}^{2} + b_{i}^{2}} \geq \sqrt{(\sum_{i} a_{i})^{2} + (\sum_{i} b_{i})^{2}}$ by the Euclidean triangle inequality [F9, F10]. Letting $ε ↓ 0$ gives $L (γ) \geq \sqrt{A^{2} + B^{2}}$ . For endpoints with factor distances $a, b$ , this is at least $D : = \sqrt{a^{2} + b^{2}}$ . If both factors are geodesic, pair constant-speed factor segments, parametrized on $[0, D]$ at speeds $a / D, b / D$ when $D > 0$ , give a product geodesic because their product distance between parameters $s, t$ is $∣ s - t ∣$ ; if $D = 0$ use the constant path. Conversely, if $γ : [0, D] \to X \times Y$ is a product geodesic, then $L (γ) = D$ and this bound forces $A = a$ and $B = b$ . For any $t \in [0, D]$ , apply the same bound to the two restrictions $[0, t]$ and $[t, D]$ . Their product distances are $t$ and $D - t$ , so equality must hold in the coordinate-length bounds and in the Euclidean triangle inequality for the two vectors of coordinate lengths. Thus those lengths are $(t a / D, t b / D)$ and $((D - t) a / D, (D - t) b / D)$ ; each coordinate distance equals its path length, so both coordinate paths are geodesics with constant proportional speeds. This proves the stated characterization when $D > 0$ ; when $D = 0$ both factors are constant.

1.3F7F8algebra

For a metric space $L$ of diameter at most $π$ , the formula of [F7] defines a metric on $C (L)$ : the case analysis of [F8] uses only that $d_{π}$ is a metric of diameter at most $π$ (the zero-radius case reduces to the triangle inequality, the case $α + β \leq π$ places three points in the plane and uses monotonicity of $\cos$ on $[0, π]$ , and the case $α + β > π$ uses the projection estimates $r - s \cos α$ , $t - s \cos β$ and $\cos α + \cos β \leq 0$ ), so it applies verbatim to the spaces $L_{1}$ and $L_{2}$ .

2.1F1F4step 1.2algebra

The product is CAT(0) if $X$ and $Y$ are: by 1.2 its geodesic triangles have componentwise geodesic sides, and for a triangle with vertices $z, x, y$ and the point $p_{t}$ of $[x, y]$ at fraction $t$ the hinged criterion [F4] applied in each factor and added gives $d (z, p_{t})^{2} \leq (1 - t) d (z, x)^{2} + t d (z, y)^{2} - t (1 - t) d (x, y)^{2}$ , because squared product distances add; by [F4] the product is CAT(0).

2.2F7F8step 1.1step 1.3algebra

Let $E$ be the cosine expression in the join formula [F7]. Its two coefficients are nonnegative and sum to $\cos (θ - θ^{'}) \leq 1$ , so $E \in [- 1, 1]$ ; the function $d_{J} = \arccos E$ descends to the endpoint quotient and separates its classes by the equality case $E = 1$ . The unit-radius map $Ψ$ into $C (L_{1}) \times C (L_{2})$ satisfies $D (Ψ x, Ψ y)^{2} = 2 - 2 \cos d_{J} (x, y)$ , where $D$ is the product metric: this is the chord distance, not $d_{J}$ . For arbitrary radii, the same expansion transports $D$ along the radial bijection to the cone function built from $d_{J}$ , so that cone function is a metric. The triangle inequality for $d_{J}$ follows from the radius- $1, s, 1$ argument in [F8], in its proof paragraph "The join is a metric space": if $A = d_{J} (x, y)$ , $B = d_{J} (y, z)$ and $A + B < π$ , choose $s = \sin (A + B) / (\sin A + \sin B)$ when $A + B > 0$ . The intermediate planar point $s (\cos A, \sin A)$ lies on the chord from $(1, 0)$ to $(\cos (A + B), \sin (A + B))$ , so the cone triangle inequality gives $2 \sin (d_{J} (x, z) / 2) \leq 2 \sin ((A + B) / 2)$ and hence $d_{J} (x, z) \leq A + B$ . The case $A + B = 0$ follows from separation, and $A + B \geq π$ follows from $d_{J} \leq π$ . Thus the join formula defines the required angular metric.

3.1F7step 2.2algebra

The radial map in (ii) is an isometry $C (L_{1}) \times C (L_{2}) \to C (L_{1} * L_{2})$ : for general radii the expansion of 2.2 gives $d_{C} (ξ (R), ξ (R^{'}))^{2} = R^{2} + R^{' 2} - 2 R R^{'} \cos d$ with $d$ the join distance, which equals the sum of the two squared cone distances, namely the square-sum product distance; the conventions $L * \emptyset = L$ and $\emptyset * \emptyset = \emptyset$ of [F7] cover the empty cases.

3.2F3step 1.2step 2.1algebra

A Euclidean space $E^{n}$ is CAT(0) [F3], so replacing either factor in 2.1 by $E^{n}$ is the special case in which that factor's hinged inequality is an equality; the componentwise description of geodesics of 1.2 and the CAT(0) conclusion of 2.1 therefore yield the clause as stated.

4.1F1F6F7step 2.1step 3.1discharge-construct

If $L_{1}$ and $L_{2}$ are CAT(1) then $L_{1} * L_{2}$ is CAT(1): by [F6] the cones $C (L_{1}), C (L_{2})$ are CAT(0), by 2.1 their $l^{2}$ -product is CAT(0), by 3.1 it is isometric to $C (L_{1} * L_{2})$ , and by [F6] again the join is CAT(1); if one factor is empty the join is the other factor [F7], which is CAT(1), and a point is CAT(1) [F1].

5.1F6step 1.2step 2.1step 4.1suffices

For a one-point space ${p}$ the spherical cone ${p} * L$ is CAT(1) exactly when $L$ is: if $L$ is CAT(1) then ${p} * L$ is CAT(1) by 4.1; conversely if ${p} * L$ is CAT(1) then $C ({p} * L)$ is CAT(0) [F6] and is isometric to $C ({p}) \times C (L)$ by the radial map of (ii), and $C (L)$ is CAT(0) because a geodesic of this product joining two points of a slice ${0} \times C (L)$ has constant first coordinate by 1.2, so triangles in the slice lift to the product with their side lengths unchanged and the product comparison inequality of 2.1 restricts to the CAT(0) inequality of $C (L)$ ; hence $L$ is CAT(1) [F6].

5.2F3F5F8F11step 4.1inductiondischarge-induction

The round sphere $S^{k}$ is CAT(1): $S^{0}$ is a two-point space at distance $π$ [F11], in which every triangle with two distinct vertices has a side of length $π$ and hence perimeter at least $2 π$ , so all admissible tests are degenerate; $S^{1} = S^{0} * S^{0}$ of circumference $2 π$ is CAT(1) [F5, F8]; and $S^{k} = S^{k - 1} * S^{0}$ for $k \geq 1$ [F8], so induction on $k$ with 4.1 gives the claim. Every closed ball $\overset{ˉ}{B} (x, ρ) \subseteq S^{k}$ with $0 < ρ < π / 2$ is convex (by [F3] for $k \geq 1$ , and because it is a singleton for $k = 0$ ) and hence CAT(1) for the induced metric: a triangle of perimeter $< 2 π$ in a convex subset has its sides, which are ambient geodesic segments of length $< π$ , contained in the subset, and its comparisons hold in the ambient CAT(1) space.

6.1F7step 4.1step 5.2algebra∎

If $L$ is CAT(1) of diameter at most $π$ and $D$ is a nonempty closed ball of positive radius $< π / 2$ in some $S^{k}$ , then $D * L$ is CAT(1): $D$ is nonempty, has diameter $< π$ and is CAT(1) with the induced metric by 5.2, so the join step 4.1 applies to the pair $(D, L)$ .

Remarks

Supplier decision recheck: proof steps 4.1 and 5.1 use both directions of Berestovskii's equivalence from Berestovskii's cone criterion and the polyhedral link criterion(i): step 4.1 transfers CAT(1) of the factors to CAT(0) of their cones and back to the join; step 5.1 uses the converse for the one-point join. The current supplier text contains explicit large-perimeter and antipodal comparison arguments in its proof steps 3.1 and 4.1, which were rechecked against Bridson–Haefliger II.3.14, printed pp. 189–190; the current part-(i) claim and these two uses agree. Its only item receipt has an older hash and remains escalated in the supplier's pair, so this batch records the current clause-(i) dependency as verified for these exact uses and reports the stale supplier decision for owner reconciliation.

Depends on

Used by

Dependency tree · two levels

75 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

Martin R. Bridson and Andre Haefliger, Metric Spaces of Non-Positive Curvature (Springer Grundlehren 319, 1999; author-hosted PDF) (standard reference, not scraped)
Michael W. Davis, The Geometry and Topology of Coxeter Groups (first-edition author manuscript, 2007-2008) (standard reference, not scraped)
Ruth Charney and Michael W. Davis, The Euler characteristic of a nonpositively curved, piecewise Euclidean manifold, Pacific J. Math. 171 (1995) (standard reference, not scraped)