Pipeline-generated

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.

✓ 2 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 2 also cleared it.

Spherical Simplex Metrics, Angular Links, and Cones

1 · Prerequisites

2 · Summary

Combinatorial links already exist in the library. Here they receive angular metrics, and tangent neighbourhoods become cones over those links. Their spherical geometry must be proved before a link criterion can be used: every construction below is a named supplier contract, and the definitions are justified by the separately named existence, descent or uniqueness proofs before any application consumes their properties.

Spherical Gram simplices and angular links of Euclidean faces constructs the spherical simplex $Σ (C) = K (C) \cap S^{n}$ from the Cholesky factor of a real symmetric positive-definite Gram matrix $C$ with diagonal $1$ , and defines the tangent cone $T_{F} C$ , the normal cone $N_{F} C = T_{F} C \cap U (F)^{⊥}$ along the direction space of a face, the angular link ${Lk}_{C} (F) = N_{F} C \cap S (V)$ of a Euclidean face and the angular distance $d_{a n g} (ξ, η) = \arccos ⟨ ξ, η ⟩$ ; the normal direction sets of the cells of an isometric polyhedral gluing glue to ${Lk}_{X} (F)$ with the componentwise intrinsic path distance, extended by auxiliary infinity between components, and the link of a point of a relative interior is the join $S^{k - 1} * {Lk}_{C} (F)$ . No combinatorial link is redefined: in a simplicial complex the cells of the face link are those of its combinatorial link; general polyhedral gluings instead have polyhedral face links with cells indexed by the cofaces.

Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas proves that the Cholesky realisation realises the prescribed inner products, uniquely up to a linear isometry, and that the vertices lie in an open hemisphere: a linear functional $φ$ with $φ (u_{i}) = 1$ is positive on $K (C) ∖ {0}$ , radial normalisation is a bijection $Δ (C) \to Σ (C)$ with unique barycentric ray coordinates, and both maps satisfy explicit Lipschitz estimates, so the round metric of $Σ (C)$ is bi-Lipschitz equivalent to the Euclidean metric of $Δ (C)$ with explicit constants. Finite spherical complexes $∣ K ∣_{C}$ have compact proper complete length-space components with minimizing geodesics (the Axiom of Choice selects near-minimizing chains and supplies the proper-target Ascoli hypothesis), and the link of a vertex $u_{0}$ is the spherical simplex with Schur-complement Gram matrix $c_{i j}^{l k} = (c_{i j} - c_{i 0} c_{j 0}) / \sqrt{(1 - c_{i 0}^{2}) (1 - c_{j 0}^{2})}$ , positive definite and compatible with iterated faces. Clause (v) identifies the tangent cone with the intersection of the inward half-spaces of the active defining inequalities and proves that $d_{a n g}$ is the intrinsic path metric of the link; only in the cone formulas is the componentwise value $+ \infty$ used, as auxiliary notation.

The angular path metric, the Euclidean cone and spherical joins fixes the conventions: the componentwise intrinsic path distance $d_{p a t h}$ (with $+ \infty$ between components), its finite-valued truncation $d_{π} = \min {π, d_{p a t h}}$ , the $D_{π}$ -geodesic angular CAT(1) convention for triangles of perimeter $< 2 π$ , the Euclidean cone $C (L) = {o} ⊔ (0, \infty) \times L$ with $d_{C} (o, (r, x)) = r$ and $d_{C}^{2} = r^{2} + s^{2} - 2 r s \cos d_{π} (x, y)$ (so $C (\emptyset) = {o}$ ), and the spherical join $L_{1} * L_{2}$ as the quotient of $L_{1} \times L_{2} \times [0, π / 2]$ by the endpoint identifications, with its cosine formula and the conventions $L * \emptyset = L$ , $\emptyset * \emptyset = \emptyset$ . No metric axiom, geodesic or associativity statement is asserted here; all of them are conclusions of the justifying theorem.

The cone and join metrics and the local product chart of a polyhedral gluing proves them. The truncation is a metric of diameter at most $π$ agreeing with $d_{p a t h}$ below $π$ , and every triangle of perimeter $< 2 π$ has at most one side $π$ and lies in one intrinsic component. The cone formula defines a metric including angle $π$ , vanishing radii and disconnected links; the through-apex path is minimizing when $d_{π} (x, y) = π$ , a minimizing angular segment develops into its planar sector otherwise, and a $D_{π}$ -geodesic link gives a geodesic cone whose minimizing geodesics stay in the ball of radius $\max {r, s}$ . The join is a metric of diameter at most $π$ — the triangle inequality is read off from the product-cone isometry $C (L_{1}) \times C (L_{2}) ≅ C (L_{1} * L_{2})$ , which also gives associativity, the face metrics and $S^{m - 1} * S^{n - 1} ≅ S^{m + n - 1}$ — and at a point $p$ in the relative interior of a $k$ -cell $F$ of an isometric polyhedral gluing with local finiteness and finitely many shapes the angular link is the join ${Lk}_{X} (p) ≅ S^{k - 1} * {Lk}_{X} (F)$ and a small metric ball about $p$ in its connected component is isometric to the ball of the same radius about $(0, o)$ in $R^{k} \times C ({Lk}_{X} (F))$ and to the cone ball over ${Lk}_{X} (p)$ , preserving intrinsic lengths. The auxiliary value $+ \infty$ is never an ordinary distance value.

Required earlier pages: coxeter-polyhedral-gluings-and-intrinsic-metrics, real-forms-and-reflection-geometry, direct-matrix-factorisations-lu-cholesky-and-qr, simplicial-complexes-and-simplicial-homology, further-trigonometric-identities-and-inverses and hilbert-space-geometry-and-riesz-representation. The companion spherical-simplex-metrics-angular-links-and-cones-examples computes the Schur complement of a spherical simplex, compares link edge lengths with dihedral mirror angles and tests the truncation convention on a disconnected universal-Coxeter nerve. This page is a draft: its proofs are local, and the link criterion that consumes them is developed on cat-comparison-link-criteria-and-local-globalization.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Spherical Gram simplices and angular links of Euclidean faces

Definition

Spherical Gram simplices. Let $n \geq 0$ and let $C = (c_{i j})_{0 \leq i, j \leq n}$ be a real symmetric positive-definite $(n + 1) \times (n + 1)$ matrix with $c_{i i} = 1$ for every $i$ (Hermitian positive-definite matrices and Cholesky factorisation A = LL* with positive diagonal, A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique). Let $C = L L^{T}$ be its unique Cholesky factorisation with lower triangular $L$ and positive diagonal, and let $u_{i} \in R^{n + 1}$ be the $i$ -th row of $L$ , regarded as a column vector. Define the positive cone on the vertices and the spherical simplex $K (C) : = {\sum_{i} λ_{i} u_{i} : λ_{i} \geq 0}, Σ (C) : = K (C) \cap S^{n},$ where $S^{n} = {x \in R^{n + 1} : ∣ x ∣ = 1}$ is the unit sphere (Real and complex inner-product spaces and their induced length, The induced length is a norm, Euclidean spheres and closed balls as subspaces of $R^{n}$ ); the vertices of $Σ (C)$ are $u_{0}, \dots, u_{n}$ . The definition asserts neither that the $u_{i}$ are unit vectors with the prescribed inner products, nor that $Σ (C)$ lies in a hemisphere, nor any metric statement about it: all of that is proved in Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas ↗.

Angular link of a Euclidean face. Let $C$ be a compact convex polyhedral cell in its Euclidean affine hull with direction space $V$ , given by finitely many affine inequalities $ℓ_{j} \geq 0$ , and let $F$ be a nonempty face (Finite convex cell complex and linear subdivision). Discard inequalities constant on the affine hull: their constants are nonnegative since $C$ is nonempty, so this does not change $C$ . The remaining gradients are nonzero; in dimension zero no inequalities remain. Write $I (F)$ for the set of remaining $j$ with $ℓ_{j}$ vanishing on $F$ , $n_{j} : = \nabla ℓ_{j} / ∣ \nabla ℓ_{j} ∣$ for the inward unit normal of the defining hyperplane $ℓ_{j} = 0$ (a facet normal when that hyperplane cuts out a facet), and $U (F) : = span {x - y : x, y \in F} \subseteq V$ for the direction space of $F$ , the linear span of the differences of points of $F$ , which is ${0}$ exactly when $F$ is a vertex. The tangent cone of $C$ at $F$ is $T_{F} C : = {ξ \in V : ⟨ ξ, n_{j} ⟩ \geq 0 for all j \in I (F)},$ equivalently the closure of ${λ (x - p) : x \in C, λ \geq 0}$ for any (hence every) $p$ in the relative interior of $F$ , and the normal cone of $F$ in $C$ is $N_{F} C : = T_{F} C \cap U (F)^{⊥}, U (F)^{⊥} = {ξ \in V : ⟨ ξ, u ⟩ = 0 for all u \in U (F)};$ the angular link of $F$ in $C$ is the set of unit inward directions normal to $F$ , ${Lk}_{C} (F) : = N_{F} C \cap S (V), S (V) = {ξ \in V : ∣ ξ ∣ = 1},$ and the angular distance of $ξ, η \in {Lk}_{C} (F)$ is $d_{a n g} (ξ, η) : = \arccos ⟨ ξ, η ⟩$ , the principal inverse cosine (Principal inverse sine and inverse cosine); equivalently it is the intrinsic path metric of the round unit sphere restricted to the link, a metric of diameter at most $π$ (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric; proved in Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas ↗(v), using that $N_{F} C$ is a convex cone). For a point $p$ in the relative interior of $F$ the set of all unit inward directions at $p$ is ${Lk}_{C} (p) : = T_{F} C \cap S (V)$ ; when $\dim F = k$ it is the spherical join $S^{k - 1} * {Lk}_{C} (F)$ of the round unit sphere of $U (F)$ with the link of $F$ , and for a vertex $F$ it coincides with ${Lk}_{C} (F)$ (proved in The cone and join metrics and the local product chart of a polyhedral gluing(4)).

For an isometric polyhedral gluing $X$ with cells $C_{p}$ (Abstract isometric polyhedral gluings and the chain metric) the links ${Lk}_{C_{p}} (F)$ of the cells containing a face $F$ are identified along the isometries induced by the gluing maps $h_{p, q}$ , giving the angular link ${Lk}_{X} (F)$ with the componentwise intrinsic path distance of the cells, extended by the auxiliary value $+ \infty$ between components (The angular path metric, the Euclidean cone and spherical joins(1)); the links ${Lk}_{C_{p}} (p)$ of the point $p$ glue in the same way to ${Lk}_{X} (p)$ . Its link cells are the unit normal direction sets in the cofaces $G > F$ , with the induced face incidences. When $X$ is simplicial, the correspondence $G \mapsto G ∖ F$ identifies these cells with the nonempty simplices of the existing combinatorial link (Subcomplexes, closures, stars, and links in a simplicial complex); for general polyhedral cells this is a polyhedral face link, not an abstract simplicial link without subdivision.

Remarks

Sign convention of the normals. The normals are inward: each $n_{j}$ points into $C$ along the increasing direction of $ℓ_{j}$ , so the tangent cone at a face is cut out by $⟨ ξ, n_{j} ⟩ \geq 0$ . With outward normals every inequality would be reversed. The two descriptions of $T_{F} C$ displayed above are proved to agree in Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas ↗(v), together with the facts that $T_{F} C$ is independent of the chosen point in the relative interior of $F$ and that the angular distance is the intrinsic metric of the link.
What is deferred to the justifier. The unit-norm and inner-product properties of the $u_{i}$ and the uniqueness of $Σ (C)$ up to an isometry of $S^{n}$ (clause (i)), the hemisphere and radial coordinates (clause (ii)), the metric axioms and intrinsic description of $d_{a n g}$ (clause (v)) and the Schur-complement formula for vertex links (clause (iv)) are all conclusions of Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas ↗; nothing beyond the construction is asserted here.
Why the vertices are not assumed to be unit vectors. The Cholesky factor of $C$ is used only as a convenient ambient realisation; that its rows are unit vectors with inner products $c_{i j}$ is the content of clause (i) of the justifier, not part of the construction.
Face link versus point link. The angular link ${Lk}_{C} (F)$ of a face collects only the directions normal to $F$ and has dimension ${codim}_{C} F - 1$ , with the empty link in codimension zero. In the simplicial case its cells are those of the combinatorial link of $F$ . The larger set ${Lk}_{C} (p) = T_{F} C \cap S (V)$ of all inward directions at a point $p$ in the relative interior of $F$ is the join $S^{k - 1} * {Lk}_{C} (F)$ , and the two notions coincide exactly when $F$ is a vertex. The cone charts of The cone and join metrics and the local product chart of a polyhedral gluing(4) use ${Lk}_{X} (p)$ , while the Schur-complement and metric-flag computations use the face link ${Lk}_{X} (F)$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas

Statement

Let $C = (c_{i j})$ be a real symmetric positive-definite $(n + 1) \times (n + 1)$ matrix with diagonal $1$ , and let $L$ , $u_{0}, \dots, u_{n}$ , $K (C)$ , $Σ (C)$ be as in Spherical Gram simplices and angular links of Euclidean faces.

(i) Existence and uniqueness of the Gram realisation. The vectors $u_{i}$ are unit vectors with $u_{i} \cdot u_{j} = c_{i j}$ , they are linearly independent and span $R^{n + 1}$ , and every other family $u_{i}^{'}$ of unit vectors in a Euclidean space with $u_{i}^{'} \cdot u_{j}^{'} = c_{i j}$ is the image of $(u_{0}, \dots, u_{n})$ under a linear isometry of $R^{n + 1}$ onto the span of the $u_{i}^{'}$ . Hence $Σ (C)$ is well-defined up to an isometry of $S^{n}$ mapping vertices to vertices.

(ii) Hemisphere, radial coordinates and bi-Lipschitz comparison. The linear functional $φ$ determined by $φ (u_{i}) = 1$ for all $i$ satisfies $φ (\sum_{i} λ_{i} u_{i}) = \sum_{i} λ_{i}$ ; consequently $φ > 0$ on $K (C) ∖ {0}$ and $Σ (C)$ is contained in the open hemisphere ${x \in S^{n} : φ (x) > 0}$ . Radial normalisation $ρ (x) : = x / ∣ x ∣$ restricts to a bijection $Δ (C) \to Σ (C)$ , where $Δ (C) : = {\sum_{i} λ_{i} u_{i} : λ_{i} \geq 0, \sum_{i} λ_{i} = 1}$ , with inverse $y \mapsto y / φ (y)$ ; every point of $Σ (C)$ therefore has unique barycentric ray coordinates $λ_{i} \geq 0$ with $\sum_{i} λ_{i} = 1$ . Moreover $ρ$ and $ρ^{- 1}$ satisfy the explicit Lipschitz estimates $∣ ρ (x) - ρ (y) ∣ \leq \frac{2}{\min_{z \in Δ (C)} ∣ z ∣} ∣ x - y ∣$ and $∣ ρ^{- 1} (y) - ρ^{- 1} (y^{'}) ∣ \leq (1 + ∥ φ ∥) ∣ y - y^{'} ∣$ , proved directly from the formulas without differentiability; here $∥ φ ∥ = ∣ w ∣$ for the unique coordinate vector $w$ with $φ (x) = w \cdot x$ . Hence the round metric $d_{a n g} (ξ, η) = \arccos ⟨ ξ, η ⟩$ on $Σ (C)$ is bi-Lipschitz equivalent to the Euclidean metric of the compact convex cell $Δ (C)$ carried by $ρ$ (on a subset of the unit sphere the round distance and the chord distance satisfy $chord \leq round \leq \frac{π}{2} chord$ ).

(iii) Finite spherical complexes. Let $K$ be a finite abstract simplicial complex (An abstract simplicial complex) whose nonempty simplices $σ$ carry positive-definite Gram matrices $C_{σ}$ of diagonal $1$ , compatible with faces. Form $X : = ∣ K ∣_{C}$ by gluing the spherical simplices $Σ (C_{σ})$ along their vertex-wise face identifications. On each component define the chain metric $d$ as the infimum of $\sum_{i} d_{p_{i}} (x_{i - 1}, x_{i})$ over finite chains in common cells, with $d_{p}$ the angular metric of that cell; equivalently it is the infimum of lengths of continuous paths. Between different components this infimum is $+ \infty$ , auxiliary notation rather than a metric value (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric). The inverse cellwise radial maps descend to a homeomorphism $X \to Y$ , where $Y$ is the Euclidean gluing with cells $Δ (C_{σ})$ ; it is bi-Lipschitz on every component. Each component of $X$ is a compact proper complete length space whose metric topology is the weak topology, and $X$ is a finite disjoint union of these components. For the empty complex, $X = Y = \emptyset$ . Under the Axiom of Choice (The Axiom of Choice), every two points in a component are joined by a minimizing geodesic of length $d (x, y)$ , in particular every pair at distance $< π$ . The proper-target argument is written locally below, using Length in a metric target: lower semicontinuity and arc-length reparametrization and Under the Axiom of Choice, a pointwise bounded equicontinuous sequence on a nonempty compact metric domain into a proper metric target has a uniformly convergent subsequence; compare Under the Axiom of Choice, proper polyhedral spaces admit minimizing geodesics.

(iv) Vertex and face links by Schur complements. The normal link of a nonempty spherical face spanned by vertices indexed by $A$ consists of the unit tangent directions perpendicular to $P_{A} : = span {u_{a} : a \in A}$ that point into $Σ (C)$ at a relative interior point of the face. For $n \geq 1$ and $1 \leq i \leq n$ put $v_{i} : = (u_{i} - c_{i 0} u_{0}) / \sqrt{1 - c_{i 0}^{2}} \in u_{0}^{⊥} \cap S^{n}$ . The link of the vertex $u_{0}$ in $Σ (C)$ is the spherical simplex with vertices $v_{1}, \dots, v_{n}$ , and its Gram matrix is $c_{i j}^{l k} = \frac{c_{i j} - c_{i 0} c_{j 0}}{\sqrt{(1 - c_{i 0}^{2}) (1 - c_{j 0}^{2})}} (1 \leq i, j \leq n),$ which is positive definite: the projection formula follows by expanding $v_{i} \cdot v_{j}$ , and positivity follows from the positive definiteness of the unnormalised Schur complement $(c_{i j} - c_{i 0} c_{j 0})_{i, j \geq 1}$ , whose quadratic form is $w^{T} C w > 0$ for the nonzero vector $w = (- x_{1} c_{10} - \dots - x_{n} c_{n 0}, x_{1}, \dots, x_{n})$ . Iterating the formula over the vertices of a face of $Σ (C)$ gives the link of that face; the result is independent of the order of iteration, and the link of a face of a link is the link of a higher face. If no vertices remain, the link is empty; in particular the vertex link for $n = 0$ is empty. More generally, for a nonempty proper vertex set $A$ , let $C_{A} = (c_{a b})_{a, b \in A}$ , $b_{i} = (c_{a i})_{a \in A}$ and $w_{i} : = u_{i} - \sum_{a \in A} (C_{A}^{- 1} b_{i})_{a} u_{a}$ for $i \notin A$ . These are the orthogonal projections onto $P_{A}^{⊥}$ , with $z_{i j} : = ⟨ w_{i}, w_{j} ⟩ = c_{i j} - b_{i}^{T} C_{A}^{- 1} b_{j}$ ; the face-link Gram matrix is $z_{i j} / \sqrt{z_{i i} z_{j j}}$ .

(v) Angular links of Euclidean faces. For a compact convex polyhedral cell $C$ and a face $F$ as in Spherical Gram simplices and angular links of Euclidean faces, with direction space $U (F)$ and normal cone $N_{F} C = T_{F} C \cap U (F)^{⊥}$ , after constant defining inequalities are discarded, the two descriptions of the tangent cone agree: $T_{F} C = \overline{{λ (x - p) : x \in C, λ \geq 0}}$ for every $p$ in the relative interior of $F$ , and $T_{F} C = {ξ : ⟨ ξ, n_{j} ⟩ \geq 0 (j \in I (F))}$ for the inward unit normals of the active defining hyperplanes; the tangent cone and the normal cone depend only on $F$ . The cone $N_{F} C$ is pointed, and is closed under nonnegative combinations, so for $ξ, η \in N_{F} C \cap S (V)$ the shorter great-circle arc between them stays in $N_{F} C \cap S (V)$ and realises $\arccos ⟨ ξ, η ⟩$ as an intrinsic path in the link; conversely every path in $N_{F} C \cap S (V)$ has length at least the round distance of its endpoints. Hence the angular distance of Spherical Gram simplices and angular links of Euclidean faces is the intrinsic path metric of the round sphere restricted to ${Lk}_{C} (F)$ , it is a metric of diameter at most $π$ , and the links ${Lk}_{C_{p}} (F)$ of the cells containing a face $F$ of an isometric polyhedral gluing depend only on $F$ , so their quotient ${Lk}_{X} (F)$ is well defined up to canonical isometry.

(vi) Disconnected components. If the angular link of a face of a complex is disconnected, the componentwise path distance is $+ \infty$ between distinct components; this value is auxiliary notation only and is truncated in the cone formulas of The angular path metric, the Euclidean cone and spherical joins.

Facts & Assumptions

Given: A real symmetric positive-definite $(n + 1) \times (n + 1)$ matrix $C$ with diagonal $1$ , its Cholesky factor $L$ , the vectors $u_{i}$ , the cone $K (C)$ and simplex $Σ (C)$ of Spherical Gram simplices and angular links of Euclidean faces; in clauses (iii) and (vi) additionally a finite abstract simplicial complex $K$ with compatible Gram matrices $C_{σ}$ as in the Statement.

[F1]

A real symmetric positive-definite matrix has a unique Cholesky factorisation $C = L L^{T}$ with lower triangular $L$ and positive diagonal; then $L$ is invertible and $C = L L^{T}$ is its own real case (A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique, Hermitian positive-definite matrices and Cholesky factorisation A = LL* with positive diagonal).

[F2]

In a real inner-product space, $⟨ \cdot, \cdot ⟩$ is bilinear and symmetric, $∣ v ∣ = \sqrt{⟨ v, v ⟩}$ is a norm, $∣ ⟨ u, v ⟩ ∣ \leq ∣ u ∣ ∣ v ∣$ with equality exactly for linearly dependent $u, v$ , every finite-dimensional subspace has an orthogonal complement and orthogonal projection by For a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$ and The orthogonal projection $P_{W} v$ is the $W$ -component in $V = W \oplus W^{⊥}$ , the unit sphere is $S^{n} = {x \in R^{n + 1} : ∣ x ∣ = 1}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ), and $\arccos : [- 1, 1] \to [0, π]$ is the inverse of the strictly decreasing restriction of $\cos$ to $[0, π]$ , continuous on $[- 1, 1]$ (Principal inverse sine and inverse cosine, The induced length is a norm, Real and complex inner-product spaces and their induced length, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[F3]

$\cos (x + y) = \cos x \cos y - \sin x \sin y$ and $\sin (x + y) = \sin x \cos y + \cos x \sin y$ for all real $x, y$ (The addition formulas for sine and cosine); $\sin^{'} = \cos$ and $\cos^{'} = - \sin$ (The derivatives of sine and cosine are cosine and minus sine); $\sin (π / 2) = 1$ , $\cos (π / 2) = 0$ , $\sin π = 0$ and $\cos π = - 1$ (Quarter-turn values and shifts by pi/2 and pi); $\cos^{2} t + \sin^{2} t = 1$ and $\sin (- t) = - \sin t$ (Parity and the Pythagorean identity for sine and cosine); $\cos$ is strictly decreasing on $[0, π]$ , and $\sin$ is strictly increasing on $[0, π / 2]$ (Signs, monotonicity intervals, and ranges of sine and cosine); for $0 < x \leq 2$ one has $\sin x \geq x - x^{3} / 6 \geq x / 3 > 0$ , and $\cos 2 \leq - 1 / 3$ , so $\cos$ is strictly decreasing on $[0, 2]$ and $π / 2 < 2$ (Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3); $\lim_{x \to 0} \sin x / x = 1$ (The limit of sin x divided by x at zero is one); and $\sin u \leq u$ for $u \geq 0$ , since for $u > 0$ the mean value theorem gives $\sin u = u \cos ξ$ for some $ξ \in (0, u)$ with $\cos ξ \leq 1$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F4]

A continuous real function on an interval assumes every value between its endpoint values (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ).

[F5]

A compact convex polyhedral cell is given by finitely many affine inequalities $ℓ_{j} \geq 0$ ; its nonempty faces arise by turning some of them into equalities, and each nonempty face is the cell itself or its intersection with a supporting hyperplane (Finite convex cell complex and linear subdivision).

[F6]

A finite abstract simplicial complex has a compact Hausdorff geometric realization, and a closed subspace of a compact space is compact (A finite simplicial complex has a compact Hausdorff realization, A closed subset of a compact metric space is compact, An abstract simplicial complex).

[F7]

For an isometric polyhedral gluing: the cells are compact convex polyhedral cells, the face relation and gluing isometries $h_{p, q}$ satisfy the cocycle and intersection conditions, the topology is the weak topology, and the chain metric is the infimum of chain lengths over points lying in common cells; its metric axioms, the agreement of its topology with the weak topology and properness and completeness under (H1)-(H3) are the conclusions of The chain metric is a metric, its topology is the weak topology, and the space is proper and complete, the proper-target geodesic argument is recorded in Under the Axiom of Choice, proper polyhedral spaces admit minimizing geodesics, and arc-length reparametrisation together with lower semicontinuity of length under uniform convergence is Length in a metric target: lower semicontinuity and arc-length reparametrization (Abstract isometric polyhedral gluings and the chain metric).

[F8]

Assume the Axiom of Choice; the proper-target Ascoli theorem states that a pointwise bounded equicontinuous sequence of continuous maps from a nonempty compact metric space into a proper metric space has a uniformly convergent subsequence, and a compact metric space is proper because its closed balls are closed, hence compact (The Axiom of Choice, Under the Axiom of Choice, a pointwise bounded equicontinuous sequence on a nonempty compact metric domain into a proper metric target has a uniformly convergent subsequence, Open cover, subcover, compact metric space, and compact subset of a metric space, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions, Bilipschitz embeddings and bilipschitz equivalences of metric spaces, Complete metric space: every Cauchy sequence converges in the space, Geodesics and geodesic metric spaces, Upper bound, least upper bound, and strict upper bound, $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it).

[F9]

A continuous real-valued function on a nonempty compact metric space attains its minimum and maximum, without Choice (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

1.1givenF1F2algebra

Gram realisation. By [F1], $C = L L^{T}$ with $L$ invertible, so the rows $u_{i}$ of $L$ satisfy $u_{i} \cdot u_{j} = (L L^{T})_{i j} = c_{i j}$ , in particular $∣ u_{i} ∣^{2} = c_{i i} = 1$ , and they are linearly independent because $\det L \neq 0$ . If $(u_{i}^{'})$ is any family of unit vectors of a Euclidean space with $u_{i}^{'} \cdot u_{j}^{'} = c_{i j}$ and $\sum_{i} λ_{i} u_{i} = 0$ , then $∣ \sum_{i} λ_{i} u_{i}^{'} ∣^{2} = λ^{T} C λ = ∣ \sum_{i} λ_{i} u_{i} ∣^{2} = 0$ , so $\sum_{i} λ_{i} u_{i}^{'} = 0$ ; the two families therefore obey the same linear relations, the map $T$ sending $u_{i}$ to $u_{i}^{'}$ is a well-defined linear isomorphism of their spans, and it preserves inner products because these are given by the Gram matrices on both sides; $T$ extends to a linear isometry of $R^{n + 1}$ onto the span of the $u_{i}^{'}$ , which carries $K (C)$ onto the cone generated by the $u_{i}^{'}$ and $Σ (C)$ onto its unit section.

1.2givenF5F2algebra

The two tangent-cone descriptions. Let $C$ be given by the nonconstant inequalities $ℓ_{j} \geq 0$ after the discarding prescribed in the definition, and let $p$ lie in the relative interior of the face $F$ , with $I (F)$ the set of $j$ with $ℓ_{j} (p) = 0$ and $n_{j} = \nabla ℓ_{j} / ∣ \nabla ℓ_{j} ∣$ inward. If $ξ$ satisfies $⟨ ξ, n_{j} ⟩ \geq 0$ for all $j \in I (F)$ , then for small $ε > 0$ the point $p + ε ξ$ satisfies $ℓ_{j} (p + ε ξ) = ℓ_{j} (p) + ε ⟨ \nabla ℓ_{j}, ξ ⟩ = ε ∣ \nabla ℓ_{j} ∣ ⟨ n_{j}, ξ ⟩ \geq 0$ for $j \in I (F)$ and $ℓ_{j} (p + ε ξ) > 0$ for $j \notin I (F)$ by continuity and $ℓ_{j} (p) > 0$ , so $p + ε ξ \in C$ and $ξ$ is a limit of vectors $λ (x - p)$ with $x \in C$ . Conversely, for $x \in C$ and $j \in I (F)$ the affine identity $ℓ_{j} (x) = ℓ_{j} (p) + ⟨ x - p, \nabla ℓ_{j} ⟩$ gives $⟨ x - p, n_{j} ⟩ = ℓ_{j} (x) / ∣ \nabla ℓ_{j} ∣ \geq 0$ , so every $λ (x - p)$ with $λ \geq 0$ lies in the closed cone ${ξ : ⟨ ξ, n_{j} ⟩ \geq 0 (j \in I (F))}$ ; the two cones agree, and since an affine function nonnegative on $F$ vanishes at a relative interior point exactly when it vanishes throughout $F$ , the active set does not depend on $p$ , and the tangent cone $T_{F} C$ does not depend on the chosen point of the relative interior. The common kernel of the active gradients is $U (F)$ : it contains $U (F)$ because the active functions vanish on $F$ ; conversely, for a vector in that kernel, sufficiently small displacements $p \pm ε ξ$ remain in $C$ and satisfy all active equalities, hence belong to $F$ by [F5], so $ξ \in U (F)$ .

1.3givenF2F3algebra

The angular distance is a metric. For unit vectors $ξ, η$ the number $d_{a n g} (ξ, η) = \arccos ⟨ ξ, η ⟩ \in [0, π]$ is well defined by [F2], is symmetric, vanishes exactly when $⟨ ξ, η ⟩ = 1$ , i.e. $ξ = η$ , and is at most $π$ . If $ξ, ζ, η$ are unit, $α : = d_{a n g} (ξ, ζ)$ and $β : = d_{a n g} (ζ, η)$ satisfy $α + β \leq π$ , write (trivially if $α = 0$ or $β = 0$ ) $ξ = \cos α ζ + \sin α a$ and $η = \cos β ζ + \sin β b$ with $a, b$ unit and orthogonal to $ζ$ by [F2]; then $⟨ ξ, η ⟩ = \cos α \cos β + \sin α \sin β ⟨ a, b ⟩ \geq \cos α \cos β - \sin α \sin β = \cos (α + β)$ by [F2] and [F3], so $d_{a n g} (ξ, η) \leq α + β$ because $\arccos$ is the inverse of the strictly decreasing $\cos$ on $[0, π]$ ; if $α + β > π$ the same inequality is trivial. So $d_{a n g}$ is a metric of diameter at most $π$ on every set of unit vectors.

2.1step 1.1F2algebra

The hemisphere functional. Since $(u_{i})$ is a basis of $R^{n + 1}$ by step 1.1, there is a unique linear functional $φ$ with $φ (u_{i}) = 1$ for all $i$ , and $φ (\sum_{i} λ_{i} u_{i}) = \sum_{i} λ_{i}$ for all $λ$ . If $x = \sum_{i} λ_{i} u_{i} \in K (C) ∖ {0}$ with $λ_{i} \geq 0$ , then some $λ_{i} > 0$ , so $φ (x) = \sum_{i} λ_{i} > 0$ ; hence $Σ (C) \subseteq {x \in S^{n} : φ (x) > 0}$ and $0 \notin Δ (C) : = {x \in K (C) : φ (x) = 1}$ , which is the set of convex combinations $\sum_{i} λ_{i} u_{i}$ with $λ_{i} \geq 0$ , $\sum_{i} λ_{i} = 1$ . In standard coordinates $φ (x) = w \cdot x$ for a unique nonzero vector $w$ ; [F2] gives $∣ φ (x) ∣ \leq ∣ w ∣ ∣ x ∣$ , with equality at $x = w / ∣ w ∣$ , so $∥ φ ∥ : = ∣ w ∣$ is the finite operator norm.

2.2step 1.1F2algebra

Schur complements. Since $∣ c_{i 0} ∣ < 1$ for $i \geq 1$ by [F2] and the linear independence of $u_{i}, u_{0}$ of step 1.1, the vectors $v_{i} : = (u_{i} - c_{i 0} u_{0}) / \sqrt{1 - c_{i 0}^{2}}$ are well defined; they satisfy $v_{i} \cdot u_{0} = 0$ and $∣ v_{i} ∣ = 1$ , and expanding $v_{i} \cdot v_{j}$ gives $v_{i} \cdot v_{j} = (c_{i j} - c_{i 0} c_{j 0}) / \sqrt{(1 - c_{i 0}^{2}) (1 - c_{j 0}^{2})} = c_{i j}^{l k}$ , in particular $c_{i i}^{l k} = 1$ . Writing $w : = (- \sum_{j} c_{0 j} x_{j}, x_{1}, \dots, x_{n})$ for $x \in R^{n} ∖ {0}$ , the vector $w$ is nonzero and, with $c_{00} = 1$ , $w^{T} C w = \sum_{i, j \geq 1} c_{i j} x_{i} x_{j} - (\sum_{j} c_{0 j} x_{j})^{2} > 0$ ; the quadratic form on the right is that of the unnormalised Schur complement $Z : = (c_{i j} - c_{i 0} c_{j 0})_{i, j \geq 1}$ , so $Z$ is positive definite, and $C^{l k} = S^{- 1 / 2} Z S^{- 1 / 2}$ with the positive diagonal $S = diag (1 - c_{i 0}^{2})$ is positive definite as well.

2.3step 1.2step 1.3F2F3F4algebra

The intrinsic path metric of a link. For a continuous path $γ$ in $V$ write $ℓ (γ)$ for the supremum of $\sum_{i} ∣ γ (t_{i + 1}) - γ (t_{i}) ∣$ over finite partitions of its parameter interval, and for $ξ, η \in {Lk}_{C} (F)$ let $d_{i n t} (ξ, η)$ be the infimum of $ℓ (γ)$ over continuous paths in ${Lk}_{C} (F)$ from $ξ$ to $η$ . Let $θ = d_{a n g} (ξ, η)$ . The cone $N_{F} C$ is pointed: a vector and its negative lying in it satisfy every active facet equality, hence lie in the direction space of the affine hull of $F$ , namely $U (F)$ ; orthogonality to $U (F)$ then forces the vector to be zero. Thus distinct unit directions are never antipodal and $0 < θ < π$ . If $θ > 0$ , pick a unit $w \in ξ^{⊥}$ with $η = \cos θ ξ + \sin θ w$ and put $γ (t) : = \cos t ξ + \sin t w$ for $t \in [0, θ]$ ; then $γ ([0, θ]) \subseteq N_{F} C \cap S (V)$ because $γ (t) = \frac{\sin (θ - t)}{\sin θ} ξ + \frac{\sin t}{\sin θ} η$ is a nonnegative combination of $ξ, η \in N_{F} C$ for $0 \leq t \leq θ$ , and for every partition $\sum_{i} ∣ γ (t_{i + 1}) - γ (t_{i}) ∣ = \sum_{i} 2 \sin \frac{t_{i + 1} - t_{i}}{2} \leq \sum_{i} (t_{i + 1} - t_{i}) = θ$ while the uniform partition into $m$ parts has sum $2 m \sin \frac{θ}{2 m} \to θ$ as $m \to \infty$ by [F3]; hence $ℓ (γ) = θ$ and $d_{i n t} (ξ, η) \leq θ$ . Conversely let $γ : [a, b] \to N_{F} C \cap S (V)$ be any continuous path from $ξ$ to $η$ and let $f (t) : = d_{a n g} (ξ, γ (t))$ , a continuous function with $f (a) = 0$ and $f (b) = θ$ ; for each $m \geq 1$ successively applying [F4] on $[t_{i - 1}, b]$ gives $a = t_{0} \leq t_{1} \leq \dots \leq t_{m} = b$ with $f (t_{i}) = i θ / m$ , and then $\sum_{i} ∣ γ (t_{i}) - γ (t_{i - 1}) ∣ = \sum_{i} 2 \sin \frac{φ_{i}}{2}$ with $φ_{i} : = d_{a n g} (γ (t_{i - 1}), γ (t_{i})) \geq ∣ f (t_{i}) - f (t_{i - 1}) ∣ = θ / m$ by step 1.3 and [F2]; since $φ_{i} \in [0, π]$ and $\sin$ is strictly increasing on $[0, π / 2]$ , each term is at least $2 \sin \frac{θ}{2 m}$ , so $ℓ (γ) \geq 2 m \sin \frac{θ}{2 m} \to θ$ and $d_{i n t} (ξ, η) \geq θ$ ; for $θ = 0$ both numbers are $0$ . Hence $d_{i n t} = d_{a n g}$ on ${Lk}_{C} (F)$ , the link has diameter at most $π$ , and $d_{a n g}$ is the intrinsic path metric of the round unit sphere restricted to the link.

2.4step 1.2F7

Links of gluings. Let $X$ be an isometric polyhedral gluing with cells $C_{p}$ and let $F$ be a face. By step 1.2 the tangent cone $T_{F} C_{p}$ and the angular link ${Lk}_{C_{p}} (F)$ depend only on $F$ , and for $p \leq q$ the isometry $h_{p, q} : C_{p} \to C_{q}$ maps $F$ onto $F$ , so its linear part maps $T_{F} C_{p}$ isometrically into $T_{F} C_{q}$ and maps its normal section onto the corresponding link face that is compatible with the cocycle condition; the intersection condition makes the intersections of the resulting images correspond to the common faces, so the cell links glue to a well-defined quotient ${Lk}_{X} (F)$ , and replacing the point of $F$ changes nothing by step 1.2. The normal sections in cofaces $G > F$ inherit their polyhedral face incidences; when $X$ is simplicial these correspond to the simplices $G ∖ F$ of its combinatorial link. A general polyhedral face link need not itself be simplicial.

3.1step 1.1step 2.1F2algebra

Radial coordinates. For $x \in Δ (C)$ the vector $ρ (x) = x / ∣ x ∣$ lies in $K (C) \cap S^{n} = Σ (C)$ , and for $y \in Σ (C)$ , written $y = \sum_{i} λ_{i} u_{i}$ with $λ_{i} \geq 0$ , the number $φ (y) = \sum_{i} λ_{i} > 0$ is positive, the point $y / φ (y) = \sum_{i} (λ_{i} / φ (y)) u_{i}$ lies in $Δ (C)$ and normalises back to $y$ ; so $y \mapsto y / φ (y)$ is an inverse of $ρ$ and $ρ$ is a bijection $Δ (C) \to Σ (C)$ . It is injective because $x / ∣ x ∣ = x^{'} / ∣ x^{'} ∣$ gives $x = a x^{'}$ with $a = ∣ x ∣ / ∣ x^{'} ∣ = φ (x) / φ (x^{'}) = 1$ . The coefficients $λ_{i}$ of a point of $Δ (C)$ in the basis $(u_{i})$ are unique, so every point of $Σ (C)$ has unique barycentric ray coordinates $λ_{i} \geq 0$ with $\sum_{i} λ_{i} = 1$ .

3.2step 1.1step 2.2F2algebra

Iterated links and face compatibility. Let $A$ be a nonempty proper set of vertices (if it is the full set, the normal link is empty), put $P_{A} : = span {u_{a} : a \in A}$ , and write $b_{i} = (c_{a i})_{a \in A}$ . The orthogonal projection of $u_{i}$ onto $P_{A}^{⊥}$ is $w_{i} = u_{i} - \sum_{a \in A} (C_{A}^{- 1} b_{i})_{a} u_{a}$ : pairing with each $u_{a}$ gives zero, while the subtracted vector lies in $P_{A}$ . Consequently $⟨ w_{i}, w_{j} ⟩ = c_{i j} - b_{i}^{T} C_{A}^{- 1} b_{j}$ , the Schur complement $Z$ of $C_{A}$ , and $Z$ is positive definite since for nonzero $x$ on the complementary indices, $(- C_{A}^{- 1} B x, x)^{T} C (- C_{A}^{- 1} B x, x) = x^{T} Z x > 0$ , where $B = (c_{a i})$ . In particular all $w_{i}$ are nonzero; normalising them gives the diagonal- $1$ Gram matrix $z_{i j} / \sqrt{z_{i i} z_{j j}}$ . These projected rays describe the normal link: at an interior point of the face, coefficients of the face vertices can vary in both directions, whereas coefficients of the remaining vertices must be nonnegative; quotienting out the face span therefore leaves exactly the cone generated by the $w_{i}$ . For iteration, after removing a vertex, project the remaining vectors onto the perpendicular of its residual projected direction, not onto the perpendicular of the original vector. For a relative interior point $p$ of the spherical face, $p$ is a positive combination of its face vertices. A tangent vector $v$ with $v ⊥ p$ points into the simplex exactly when its coefficients outside $A$ are nonnegative: for small $ε > 0$ , the vector $p + ε v$ retains positive coefficients in $A$ , and its normalisation has initial direction $v$ , as $(p + ε v) / ∣ p + ε v ∣ = p + ε v + O (ε^{2})$ . Removing the tangent face directions $P_{A} \cap p^{⊥}$ leaves $P_{A}^{⊥}$ and the projected rays $w_{i}$ , proving the asserted geometric link identification. Those residual directions obtained from an ordering of $A$ are orthogonal and span $P_{A}$ (each new residual is orthogonal to the preceding span and is nonzero by independence); their successive perpendicular projections therefore equal the single orthogonal projection onto $P_{A}^{⊥}$ . Intermediate normalisations only rescale rays by positive factors, so the final normalised Gram matrix is the same in every order. Restricting to a subface retains the corresponding subset of remaining rays, while linking a further face enlarges $A$ and repeats this operation.

4.1step 2.1step 3.1F2F3F5F9algebra

Lipschitz estimates and the chord bound. $Δ (C)$ is a nonempty compact convex cell and avoids $0$ by step 2.1 and [F5]. The reverse norm triangle inequality makes $z \mapsto ∣ z ∣$ continuous, so [F9] gives an attained minimum $m_{0} : = \min_{z \in Δ (C)} ∣ z ∣ > 0$ , and for $x, y \in Δ (C)$ the estimate $∣ \frac{x}{∣ x ∣} - \frac{y}{∣ y ∣} ∣ \leq \frac{∣ x - y ∣}{∣ x ∣} + \frac{∣ ∣ x ∣ - ∣ y ∣ ∣}{∣ x ∣} \leq \frac{2 ∣ x - y ∣}{m_{0}}$ holds. On $Σ (C)$ one has $∣ y ∣ = 1$ and $φ (y) \geq 1$ (because $y = z / ∣ z ∣$ with $z \in Δ (C)$ and $∣ z ∣ \leq 1$ ), so writing $y / φ (y) - y^{'} / φ (y^{'}) = \frac{(y - y^{'})}{φ (y)} + \frac{y^{'} (φ (y^{'}) - φ (y))}{φ (y) φ (y^{'})}$ gives $∣ ρ^{- 1} (y) - ρ^{- 1} (y^{'}) ∣ \leq ∣ y - y^{'} ∣ + ∥ φ ∥ ∣ y - y^{'} ∣$ . For unit vectors $ξ, η$ put $θ : = d_{a n g} (ξ, η) = \arccos ⟨ ξ, η ⟩$ ; then $∣ ξ - η ∣^{2} = 2 - 2 ⟨ ξ, η ⟩ = 2 - 2 \cos θ = 4 \sin^{2} (θ / 2)$ by [F3], so the chord length is $chord = 2 \sin (θ / 2) \leq θ = round$ , the last step because $\sin u \leq u$ for $u \geq 0$ by [F3]. For the reverse comparison note first that $π > 2$ : for $0 < u \leq π / 2$ the mean value theorem gives $\sin u = u \cos ξ$ with $ξ \in (0, u)$ , and $\cos ξ < \cos 0 = 1$ because $\cos$ is strictly decreasing on $[0, π]$ [F3], so $\sin u < u$ and $1 = \sin (π / 2) < π / 2$ ; the restriction of $\cos$ to $[0, π]$ is strictly decreasing with $\cos 0 = 1$ and $\cos (π / 2) = 0$ by [F2] and [F3], so $2 / π \in (0, 1)$ and $u_{*} : = \arccos (2 / π)$ is the unique point of $[0, π]$ with $\cos u_{*} = 2 / π$ , lying in $(0, π / 2)$ ; the function $f (u) : = \sin u - 2 u / π$ therefore has $f^{'} (u) = \cos u - 2 / π$ by [F3], positive on $[0, u_{*})$ and negative on $(u_{*}, π / 2]$ . The mean value theorem [F3] gives $f (u) \geq f (0) = 0$ on $[0, u_{*}]$ and $f (u) \geq f (π / 2) = 0$ on $[u_{*}, π / 2]$ (with $f (π / 2) = \sin (π / 2) - 1 = 0$ ), that is, $\sin u \geq 2 u / π$ on $[0, π / 2]$ . Applied to $u = θ / 2 \leq π / 2$ this gives $θ \leq (π / 2) 2 \sin (θ / 2) = (π / 2) chord$ , so the chord and round distances satisfy $chord \leq round \leq \frac{π}{2} chord$ .

4.2step 1.1step 3.2

The finite spherical complex and the descent map. By steps 1.1 and 3.2 the identifications $Σ (C_{τ}) \to Σ (C_{σ})$ for $τ \subseteq σ$ are well-defined isometries onto faces, so $X = ∣ K ∣_{C}$ is a well-defined quotient of the finite disjoint union of the compact simplices $Σ (C_{σ})$ by finitely many face identifications. Let $Y$ be the corresponding isometric polyhedral gluing with cells $Δ (C_{σ})$ ; the cell maps $Φ_{σ} : Σ (C_{σ}) \to Δ (C_{σ})$ , $Φ_{σ} (y) : = y / φ_{σ} (y)$ , agree on identified faces, because $φ_{σ}$ takes the value $1$ on all vertices in $σ$ and hence restricts to $φ_{τ}$ ; so the $Φ_{σ}$ descend to a bijection $Φ : X \to Y$ .

4.3step 2.2step 3.2step 2.4

The link of a face of a finite spherical complex. Let $X = ∣ K ∣_{C}$ be a finite spherical complex and let $F$ be the face corresponding to a nonempty simplex $σ$ . The cells of ${Lk}_{X} (F)$ are the links ${Lk}_{C_{τ}} (F)$ of the spherical simplices containing $F$ ; by step 3.2 each is again a spherical simplex, with Gram matrix obtained by iterating the Schur complements of step 2.2 over the vertices of $σ$ , and these matrices are positive definite of diagonal $1$ and compatible with faces, because passing to a smaller coface retains a subset of the projected rays, while linking a further face enlarges the projected-out span; the identifications are those induced by $K$ and are isometric by step 2.4. Hence ${Lk}_{X} (F)$ is again presented as a finite spherical complex, and clauses (i)-(v) apply to it.

5.1step 3.1step 4.1F8

Bi-Lipschitz equivalence of the model and its spherical simplex. With $m_{0} = \min_{z \in Δ (C)} ∣ z ∣ > 0$ and the operator norm $∥ φ ∥$ , steps 3.1 and 4.1 give for $y = ρ (x)$ , $y^{'} = ρ (x^{'})$ the bounds $d_{a n g} (y, y^{'}) \leq \frac{π}{2} ∣ y - y^{'} ∣ \leq \frac{π}{m_{0}} ∣ x - x^{'} ∣$ and $∣ x - x^{'} ∣ \leq (1 + ∥ φ ∥) ∣ y - y^{'} ∣ \leq (1 + ∥ φ ∥) d_{a n g} (y, y^{'})$ , so $ρ$ is a bi-Lipschitz equivalence between the Euclidean metric of $Δ (C)$ and the round metric of $Σ (C)$ with the constant $L : = \max {π / m_{0}, 1 + ∥ φ ∥}$ .

6.1step 5.1step 4.2

The radial map is bi-Lipschitz for the chain metrics. If $K$ has no nonempty simplex then $X = Y = \emptyset$ and there are no distance estimates to check. Otherwise, by step 5.1 each $Φ_{σ}$ is bi-Lipschitz with constant $L_{σ} = \max {π / m_{0}^{σ}, 1 + ∥ φ_{σ} ∥}$ , and the finitely many simplices of $K$ give finite maxima $L^{'} : = \max_{σ} (1 + ∥ φ_{σ} ∥)$ and $L^{''} : = \max_{σ} π / m_{0}^{σ}$ . Every chain in $X$ maps under $Φ$ to a chain in $Y$ whose one-step Euclidean distances are at most $L^{'}$ times the angular distances of the original chain, so $d_{Y} (Φ x, Φ x^{'}) \leq L^{'} d_{X} (x, x^{'})$ ; likewise every chain in $Y$ is the image of a chain in $X$ with angular steps at most $L^{''}$ times the Euclidean steps, so $d_{X} (x, x^{'}) \leq L^{''} d_{Y} (Φ x, Φ x^{'})$ . Hence $Φ$ is a bi-Lipschitz equivalence of the chain metrics.

7.1step 4.2step 6.1F6F7

Component metrics and topology. The classes under being joined by a chain are finite in number. Each is a union of whole cells: any two points of one cell are joined by a single chain step. The trace of a class on every cell is therefore the entire cell or empty, so every class is weakly open and closed; each class is path connected by cell arcs, hence is a connected component. The corresponding component of $Y$ satisfies (H1)-(H3), so [F7] supplies its metric, weak topology, properness and completeness; step 6.1 transfers these properties to the component of $X$ . Each component is compact as a quotient of finitely many compact cells. Its chain metric is a length metric: a chain can be replaced by cell arcs, whose $d$ -length is at most its chain length because $d \leq d_{a n g}$ on a cell, while every path has length at least the distance of its endpoints. Cellwise radial homeomorphisms descend to a homeomorphism for the quotient (weak) topologies, and the components are open and closed, so $X$ and $Y$ are compact finite disjoint unions of the component metric spaces. Distances between distinct components remain auxiliary infinities; no real-valued global chain metric is asserted. The empty case is vacuous.

8.1step 2.3step 7.1F5F7F8

Minimizing geodesics (AC). Assume AC, fix $x, y$ in one component and put $R = d (x, y)$ . AC selects, for each $n \geq 1$ , a chain of length $L_{n} < R + 1 / n$ ; the infimum definition gives $R \leq L_{n}$ . Replace its steps by cell arcs, traversed at angular speed $L_{n}$ on $[0, 1]$ (use the constant path for $L_{n} = 0$ ). Each arc lies in its cell by the nonnegative-combination argument of step 2.3 applied to $K (C_{σ})$ , and the triangle inequality gives $d (γ_{n} (s), γ_{n} (t)) \leq L_{n} ∣ s - t ∣$ , hence $R \leq ℓ (γ_{n}) \leq L_{n}$ . The paths are equicontinuous and pointwise bounded in the compact proper component of step 7.1. The domain $[0, 1]$ is compact as a nonempty bounded one-dimensional polyhedral cell by [F5]; with AC it satisfies [F8], giving a uniformly convergent subsequence with continuous limit $γ$ and endpoints $x, y$ . Since $R \leq ℓ (γ_{n}) \leq L_{n} \to R$ , lower semicontinuity [F7] gives $ℓ (γ) \leq R$ , while the endpoint partition gives the reverse bound. Reparametrise by arc length using [F7]. For $0 \leq u \leq v \leq R$ , the resulting path $\overset{ˉ}{γ}$ is $1$ -Lipschitz, and $R = d (x, y) \leq u + d (\overset{ˉ}{γ} (u), \overset{ˉ}{γ} (v)) + R - v$ forces $d (\overset{ˉ}{γ} (u), \overset{ˉ}{γ} (v)) \geq v - u$ ; thus equality holds and $\overset{ˉ}{γ}$ is a minimizing geodesic. AC is used for the sequence selection and for Ascoli.

9.1step 4.3step 7.1∎

The $+ \infty$ convention. Let $F$ be a face of a finite spherical complex $X$ . By step 4.3 the angular link ${Lk}_{X} (F)$ is a finite spherical complex, so step 7.1 applies to it: being joined by a chain of directions inside common cells is reflexive (singleton chains), symmetric (reverse a chain) and transitive (concatenate chains), hence an equivalence relation on ${Lk}_{X} (F)$ ; the infimum $d_{p a t h} (x, y)$ is finite whenever a chain from $x$ to $y$ exists and is a metric on each class by step 7.1, while for $x, y$ in different classes no chain joins them and $d_{p a t h} (x, y) = + \infty$ . This infinite value is auxiliary notation, not an ordinary distance of the metric-space definition, and it is replaced by $π$ in the truncated metric of The angular path metric, the Euclidean cone and spherical joins.

Remarks

Choice. In step 8.1 the Axiom of Choice selects the sequence of near-minimizing chains and supplies the hypothesis of the proper-target Ascoli theorem; clauses (i), (ii), (iv), (v) and (vi), and the metric/topology conclusions of (iii), are choice-free; the geodesic conclusion of (iii) assumes AC.
The two model metrics. Steps 4.1 and 5.1 compare the round metric of $Σ (C)$ with the Euclidean metric of $Δ (C)$ through the chord metric; the constants are explicit ( $π / 2$ for round versus chord, $\max {π / m_{0}, 1 + ∥ φ ∥}$ in step 5.1) and are not asserted to be optimal.
No curvature claim. The link metric is proved to be a metric and the intrinsic metric of the round sphere; no CAT(1) assertion is made here, and the $D_{π}$ -geodesic convention remains a hypothesis of The angular path metric, the Euclidean cone and spherical joins and The cone and join metrics and the local product chart of a polyhedral gluing.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The angular path metric, the Euclidean cone and spherical joins

Definition

(1) Angular path metric. Let $L$ be a set with an extended metric $d_{p a t h} : L \times L \to [0, \infty]$ , symmetric, vanishing exactly on the diagonal and satisfying the triangle inequality in the extended reals. For the angular link ${Lk}_{X} (F)$ of a face of a finite spherical complex (Spherical Gram simplices and angular links of Euclidean faces, Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas) the metric $d_{p a t h}$ is the componentwise intrinsic path distance: the infimum of lengths of finite chains of directions inside a common cell, with $d_{p a t h} (x, y) = + \infty$ for $x, y$ in different components. The value $+ \infty$ is auxiliary notation only and is never passed to the published definition of a metric space (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

(2) Truncated angular metric. With the convention $\min {π, \infty} : = π$ , put $d_{π} (x, y) : = \min {π, d_{p a t h} (x, y)}$ . This finite-valued function on $L \times L$ is the angular metric; it has values in $[0, π]$ and its metric axioms are proved in The cone and join metrics and the local product chart of a polyhedral gluing ↗ (Sine and cosine defined by their real power series, Pi is the first positive zero of sine, Principal inverse sine and inverse cosine).

(3) The Euclidean cone. The Euclidean cone on the angular link $L$ is the set $C (L) : = {o} ⊔ ((0, \infty) \times L),$ where $o$ is the apex, with $d_{C} (o, o) : = 0, d_{C} (o, (r, x)) : = r, d_{C} ((r, x), (s, y))^{2} : = r^{2} + s^{2} - 2 r s \cos d_{π} (x, y) .$ In particular $C (\emptyset) = {o}$ is a one-point space, not the empty space; and if $d_{π} (x, y) = π$ — which happens in particular when $x, y$ lie in different components of $L$ — then $d_{C} ((r, x), (s, y)) = r + s$ , the length of the path through the apex. The infinite value of $d_{p a t h}$ is never an ordinary metric value, and the cone receives only $d_{π}$ .

(4) Angular CAT(1) convention. A link $L$ is $D_{π}$ -geodesic if every pair of points at distance $< π$ is joined by a minimizing segment. Angular CAT(1) statements about a link concern only triangles of perimeter $< 2 π$ and their comparison in the unit sphere $S^{2}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ); every such test lies in one intrinsic component and agrees with the componentwise intrinsic test of $d_{p a t h}$ whenever no side equals $π$ , while a side of length $π$ is realised in the model sphere by an antipodal pair; this is proved in The cone and join metrics and the local product chart of a polyhedral gluing ↗.

(5) Spherical join. Let $L_{1}, L_{2}$ be angular links with metrics $d_{π}^{1}, d_{π}^{2}$ . The spherical join $L_{1} * L_{2}$ is the quotient of $L_{1} \times L_{2} \times [0, π / 2]$ by the identifications $(x, y, 0) \sim (x, y^{'}, 0)$ and $(x, y, π / 2) \sim (x^{'}, y, π / 2)$ ; write $(\cos θ) x + (\sin θ) y$ for the class of $(x, y, θ)$ . The distance of $x = (\cos θ) x_{1} + (\sin θ) x_{2}$ and $x^{'} = (\cos θ^{'}) x_{1}^{'} + (\sin θ^{'}) x_{2}^{'}$ is the unique number in $[0, π]$ with $\cos d (x, x^{'}) = \cos θ \cos θ^{'} \cos d_{π}^{1} (x_{1}, x_{1}^{'}) + \sin θ \sin θ^{'} \cos d_{π}^{2} (x_{2}, x_{2}^{'}) .$ Conventions: $L * \emptyset : = L$ , $\emptyset * L : = L$ and $\emptyset * \emptyset : = \emptyset$ ; these are consistent with the product-cone isometry $C (L_{1}) \times C (L_{2}) ≅ C (L_{1} * L_{2})$ , under which $L_{1} * L_{2}$ is the unit link of the product cone. Quotient descent to the identified endpoints, the triangle inequality, associativity, the face metrics and the isometry with the unit link are conclusions of The cone and join metrics and the local product chart of a polyhedral gluing ↗; this item asserts only the construction, the formula and the conventions.

Remarks

What is construction and what is theorem. Clauses (1)–(5) fix notation and conventions only: the truncated metric, the cone with its apex and the join with its empty conventions are defined here, while the metric axioms of $d_{π}$ , the cone metric and its geodesics, the quotient descent and triangle inequality of the join, associativity and the product-cone isometry are all proved in The cone and join metrics and the local product chart of a polyhedral gluing ↗. This item is the justification target of that theorem and asserts none of its conclusions.
Why the truncation. The Euclidean cone formula requires a finite angular distance bounded by $π$ : the value $+ \infty$ of $d_{p a t h}$ across distinct components of a link is replaced by $π$ , and the geodesics between the corresponding rays then pass through the apex. The link of a finite spherical complex is the case in which $d_{p a t h}$ is the componentwise intrinsic path distance of Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(vi).
The square-sum convention. By the product-cone isometry, $C (L_{1}) \times C (L_{2})$ carries the square-sum product metric $d^{2} = d_{1}^{2} + d_{2}^{2}$ and $L_{1} * L_{2}$ is its unit link; the displayed cosine formula is the law of cosines of that cone, not an independent claim of the definition.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The cone and join metrics and the local product chart of a polyhedral gluing

Statement

Let $(L, d_{p a t h}, d_{π})$ be an angular link with its componentwise path metric and truncated metric as in The angular path metric, the Euclidean cone and spherical joins, and let $L_{1}, L_{2}$ be angular links. Then:

(1) Truncation agreement. $d_{π}$ is a metric on $L$ of diameter at most $π$ ; it agrees with $d_{p a t h}$ on every pair at distance $< π$ ; every triple with $d_{π}$ -perimeter $< 2 π$ has at most one side equal to $π$ , and if no side equals $π$ then the triple lies in a single component of $d_{p a t h}$ and its three sides are the intrinsic path distances. Consequently the angular CAT(1) conventions of The angular path metric, the Euclidean cone and spherical joins ( $D_{π}$ -geodesics and comparisons for perimeter $< 2 π$ ) coincide with the componentwise intrinsic tests whenever no side equals $π$ , and a side of length $π$ — which can arise only from a pair in different components or at intrinsic distance $\geq π$ — is realised in the model sphere by an antipodal pair.

(2) Cone metric and geodesics. Clause (3) of The angular path metric, the Euclidean cone and spherical joins defines a metric on $C (L)$ , including the cases where one radius is zero, where $d_{π} (x, y) = π$ and where $x, y$ lie in different components; the metric is finite-valued and $C (\emptyset) = {o}$ is a point. If $d_{π} (x, y) = π$ then the path through the apex has length $r + s = d_{C} ((r, x), (s, y))$ and is minimizing. If $d_{π} (x, y) < π$ and $x, y$ are joined in $L$ by a minimizing segment, then the development of that segment into the planar sector of angle $d_{π} (x, y)$ is a minimizing geodesic of $C (L)$ from $(r, x)$ to $(s, y)$ of length $d_{C} ((r, x), (s, y))$ ; if in addition $L$ is $D_{π}$ -geodesic, then $C (L)$ is a geodesic space and every minimizing geodesic joining two points of $C (L)$ is contained in the closed ball of radius $\max {r, s}$ about $o$ (Geodesics and geodesic metric spaces).

(3) Join, cone and product cone. Clause (5) of The angular path metric, the Euclidean cone and spherical joins defines a metric on $L_{1} * L_{2}$ (descent to the quotient, symmetry and the triangle inequality included) of diameter at most $π$ ; $L_{1}$ and $L_{2}$ sit in $L_{1} * L_{2}$ as the classes with $θ = 0$ and $θ = π / 2$ , and the conventions $L * \emptyset = L$ , $\emptyset * \emptyset = \emptyset$ are consistent with the construction. The map $((r, x), (s, y)) \mapsto ξ (R), R = \sqrt{r^{2} + s^{2}}, \cos θ = \frac{r}{R}, \sin θ = \frac{s}{R},$ where $ξ (R)$ is the point of $C (L_{1} * L_{2})$ at distance $R$ from the apex in the direction $(\cos θ) x + (\sin θ) y$ , is an isometry $C (L_{1}) \times C (L_{2}) \to C (L_{1} * L_{2})$ for the square-sum product metric; consequently $L_{1} * L_{2}$ is, up to isometry, the unit link of the product cone, and the join is associative up to canonical isometry. The face metrics of the join are the joins of the corresponding face metrics, and for round unit spheres $S^{m - 1} * S^{n - 1} ≅ S^{m + n - 1}$ .

(4) Local product chart. Let $X$ be an isometric polyhedral gluing satisfying the standing hypotheses (H2) local finiteness and (H3) finitely many shapes of Abstract isometric polyhedral gluings and the chain metric, and let $p \in X$ lie in the relative interior of a $k$ -dimensional cell $F$ (Finite convex cell complex and linear subdivision). Then the connected component $X_{p}$ of $p$ carries its chain metric, and the angular link of the point $p$ , that is the set ${Lk}_{X} (p)$ of unit directions of the tangent cone $T_{p} X$ (the finitely many sets $T_{F} C_{r} \cap S (V_{r})$ for the cells $C_{r}$ containing $p$ , identified by the gluing), is the spherical join ${Lk}_{X} (p) ≅ S^{k - 1} * {Lk}_{X} (F)$ , where $S^{k - 1}$ is the round unit sphere of the direction space of $F$ ; and there is $ε > 0$ such that the metric ball $B_{X_{p}} (p, ε)$ in $X_{p}$ is isometric to the ball of radius $ε$ about the cone point of $C ({Lk}_{X} (p))$ and to the ball of radius $ε$ about $(0, o)$ in $R^{k} \times C ({Lk}_{X} (F))$ , these charts preserving intrinsic lengths. In particular the cone receives only the truncated angular metric: the auxiliary value $+ \infty$ of $d_{p a t h}$ is never an ordinary distance value.

Facts & Assumptions

Given: Angular links $(L, d_{p a t h}, d_{π})$ , $L_{1}$ , $L_{2}$ as in The angular path metric, the Euclidean cone and spherical joins, with $C (L)$ , $C (L_{1})$ , $C (L_{2})$ their Euclidean cones; in clause (4) an isometric polyhedral gluing $X$ with (H2) and (H3), a point $p$ in the relative interior of a $k$ -dimensional cell $F$ , and its connected component $X_{p}$ with its chain metric.

[F1]

$d_{π} = \min {π, d_{p a t h}}$ with $\min {π, \infty} = π$ ; $d_{p a t h}$ is an extended metric, symmetric, vanishing exactly on the diagonal and satisfying the extended triangle inequality (The angular path metric, the Euclidean cone and spherical joins).

[F2]

$\cos$ is strictly decreasing on $[0, π]$ , $\sin$ is strictly increasing on $[0, π / 2]$ , $\cos (π) = - 1$ , $\cos 0 = 1$ , $\cos^{2} + \sin^{2} = 1$ , the addition formulas hold and $\arccos$ is the inverse of $\cos ∣_{[0, π]}$ (Principal inverse sine and inverse cosine, Sine and cosine defined by their real power series, The addition formulas for sine and cosine, Signs, monotonicity intervals, and ranges of sine and cosine, Pi is the first positive zero of sine).

[F3]

For unit vectors in a Euclidean space $∣ x - y ∣^{2} = 2 - 2 ⟨ x, y ⟩$ and the Euclidean plane with the standard norm is a metric space ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[F4]

In an isometric polyhedral gluing satisfying (H1)-(H3) the chain metric is a metric whose topology is the weak topology and the space is proper and complete; the uniform star radius and compatible triangulation of a face give a positive radius around every point in the relative interior of a cell (The chain metric is a metric, its topology is the weak topology, and the space is proper and complete, Face coherence, global hat coordinates and a uniform star radius, Finite convex cell complexes admit compatible triangulations, Abstract isometric polyhedral gluings and the chain metric).

[F5]

A geodesic segment is a distance-preserving parametrisation of an interval and a metric space is geodesic when every two points are joined by one; a product of two metric spaces with the square-sum metric is a metric space: the factor triangle inequalities bound its distance by the Euclidean norm of the sum of the two nonnegative distance-coordinate vectors, and the Euclidean triangle inequality bounds that norm by the sum of their norms (Geodesics and geodesic metric spaces, 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).

Proof

1.1givenF1algebra

Truncation. The function $d_{π} (x, y) = \min {π, d_{p a t h} (x, y)}$ is symmetric and vanishes exactly when $d_{p a t h} (x, y) = 0$ , i.e. when $x = y$ ; it has values in $[0, π]$ , so its diameter is at most $π$ ; and for real $a, b \geq 0$ one has $\min {π, a + b} \leq \min {π, a} + \min {π, b}$ , so the triangle inequality of $d_{p a t h}$ passes to $d_{π}$ . On a pair with $d_{p a t h} (x, y) < π$ clearly $d_{π} = d_{p a t h}$ .

1.2givenF2algebra

Cone basics. For points $(r, x), (s, y) \in C (L)$ the definition gives $d_{C} ((r, x), (s, y))^{2} = r^{2} + s^{2} - 2 r s \cos d_{π} (x, y)$ , so $d_{C} \geq 0$ and $d_{C}$ is symmetric, $d_{C}$ vanishes exactly when $r = s$ and $d_{π} (x, y) = 0$ , and $d_{C} (o, (r, x)) = r$ with $d_{C} (o, o) = 0$ ; moreover $(r - s)^{2} \leq d_{C}^{2} \leq (r + s)^{2}$ , that is $∣ r - s ∣ \leq d_{C} \leq r + s$ , and $d_{C} = r + s$ holds exactly when $\cos d_{π} (x, y) = - 1$ , i.e. $d_{π} (x, y) = π$ . In particular $d_{C} ((t, x), (t^{'}, x)) = ∣ t - t^{'} ∣$ for fixed $x$ , and $d_{C}$ is finite whenever $L$ is nonempty, while $C (\emptyset) = {o}$ is a point.

1.3assume-case smallgivenF2F3algebra

The cone triangle inequality, first case. Let $P = (r, x)$ , $Q = (t, z)$ , $T = (s, y)$ with $α : = d_{π} (x, z)$ , $β : = d_{π} (z, y)$ , $γ : = d_{π} (x, y)$ and suppose $α + β \leq π$ . In the Euclidean plane with origin $0$ put $A : = r e_{0}$ , $B : = t e_{α}$ , $C : = s e_{α + β}$ (if $A = 0$ or $C = 0$ read the point as the origin); then $∣ A - B ∣ = d_{C} (P, Q)$ and $∣ B - C ∣ = d_{C} (Q, T)$ by the law of cosines [F2], while $γ \leq α + β \leq π$ and $\cos$ decreasing on $[0, π]$ give $\cos γ \geq \cos (α + β)$ and hence $d_{C} (P, T)^{2} = r^{2} + s^{2} - 2 r s \cos γ \leq r^{2} + s^{2} - 2 r s \cos (α + β) = ∣ A - C ∣^{2}$ . So $d_{C} (P, T) \leq ∣ A - C ∣ \leq ∣ A - B ∣ + ∣ B - C ∣ = d_{C} (P, Q) + d_{C} (Q, T)$ .

1.4givenF2F3

Development of a minimizing segment. Let $x, y \in L$ have $d_{π} (x, y) = θ < π$ and let $γ : [0, θ] \to L$ be a minimizing segment with $d_{π} (γ (u), γ (w)) = ∣ u - w ∣$ . Let $S : = {t e_{u} \in R^{2} : t \geq 0, 0 \leq u \leq θ}$ be the planar sector of angle $θ$ and define $Ψ (t e_{u}) : = (t, γ (u))$ for $t > 0$ , $Ψ (0) : = o$ . Then for $t, t^{'} > 0$ the identity $d_{C} ((t, γ (u)), (t^{'}, γ (w)))^{2} = t^{2} + t^{' 2} - 2 t t^{'} \cos ∣ u - w ∣ = ∣ t e_{u} - t^{'} e_{w} ∣^{2}$ holds, so $Ψ$ is an isometry of $S$ onto its image and preserves lengths; the straight segment in $S$ from $r e_{0}$ to $s e_{θ}$ has Euclidean length $\sqrt{r^{2} + s^{2} - 2 r s \cos θ} = d_{C} ((r, x), (s, y))$ and its image is a path in $C (L)$ of the same length joining the two points, hence a minimizing geodesic.

1.5givenF1F2algebra

The join: descent and first properties. The relation on $L_{1} \times L_{2} \times [0, π / 2]$ generated by the stated endpoint identifications is an equivalence relation. Write $E : = \cos θ \cos θ^{'} \cos d_{π}^{1} (x_{1}, x_{1}^{'}) + \sin θ \sin θ^{'} \cos d_{π}^{2} (x_{2}, x_{2}^{'})$ and $a : = \cos θ \cos θ^{'}$ , $b : = \sin θ \sin θ^{'}$ ; then $a, b \geq 0$ and $a + b = \cos (θ - θ^{'}) \leq 1$ , so $E \leq a + b \leq 1$ and $E \geq - a - b \geq - 1$ by [F2], that is $E \in [- 1, 1]$ . If $θ = θ^{'} = 0$ then $E = \cos d_{π}^{1} (x_{1}, x_{1}^{'})$ depends only on the first coordinates, and if $θ = θ^{'} = π / 2$ then $E = \cos d_{π}^{2} (x_{2}, x_{2}^{'})$ depends only on the second, so $E$ is unchanged when a representative is replaced; the formula therefore descends to a symmetric function $G$ on pairs of classes, and $d$ is defined by $\cos d (x, x^{'}) = G (x, x^{'})$ with $d (x, x^{'}) \in [0, π]$ . Moreover $G (x, x^{'}) \leq 1$ with equality only for $x = x^{'}$ : equality forces $\cos (θ - θ^{'}) = 1$ , that is $θ = θ^{'}$ , and then forces $\cos d_{π}^{1} (x_{1}, x_{1}^{'}) = 1$ when $\cos θ > 0$ and $\cos d_{π}^{2} (x_{2}, x_{2}^{'}) = 1$ when $\sin θ > 0$ , so the two classes coincide, and conversely equal classes give $G = 1$ ; hence $d (x, x^{'}) = 0$ exactly for $x = x^{'}$ and $d$ has diameter at most $π$ . The classes with $θ = 0$ and $θ = π / 2$ are the images of $L_{1}$ and $L_{2}$ ; when $L_{1}$ or $L_{2}$ is empty the quotient of $L_{1} \times L_{2} \times [0, π / 2]$ is empty, and the stated conventions $L * \emptyset : = L$ , $\emptyset * L : = L$ , $\emptyset * \emptyset : = \emptyset$ together with $C (\emptyset) = {o}$ are exactly the cone formula at a one-point link.

1.6F4algebra

Localisation and radial coordinates. Work in the connected component $X_{p}$ of $p$ : chain classes are open and closed unions of cells and are path connected, so this subgluing satisfies (H1)-(H3) and [F4] applies. The union $A$ of all cells not containing $F$ is weakly closed: its trace on any cell is a union of some of that cell's finitely many closed faces, by the intersection condition. It omits $p$ , since a face containing a relative interior point of $F$ contains $F$ . Thus $B (p, a) \cap A = \emptyset$ for some $a > 0$ . There are finitely many incident cells by (H2). In each, the facet inequalities not active at $p$ have positive values at $p$ ; choosing $b > 0$ smaller than all their distances to their supporting hyperplanes ensures that, within Euclidean radius $b$ , the cell agrees exactly with $p + T_{F} C_{r}$ . Choose $h < \min {a, b}$ and let $Z$ be the gluing of the incident tangent cones, with Euclidean chain metric. On the radial subset $∣ v ∣ < h$ , the map $v \mapsto p_{r} + v$ into the incident cell, followed by its inclusion in $X$ , is well defined and injective: the common-face condition and the gluing cocycle identify exactly the same vectors in $Z$ and points in $X$ . For a chain of length $ℓ < h$ starting at $p$ , all its vertices lie in $B (p, h)$ , hence in incident cells, and radial norms along it are at most $ℓ$ by the Euclidean reverse triangle inequality. Its pullback into $Z$ has the same length. Conversely a radial segment of length $t < h$ maps to a path in $X$ of that length. Taking infima shows $d_{X} (p, Φ (v)) = ∣ v ∣$ for $∣ v ∣ < h$ , and every point of $B (p, h)$ has such coordinates by pulling back a chain from $p$ of length less than $h$ .

2.1step 1.1F1F2

Triples and antipodal pairs. If a triple has $d_{π} (x, y) = π$ , then $π \leq d_{π} (x, z) + d_{π} (z, y)$ by the triangle inequality of step 1.1, so its perimeter is at least $2 π$ ; hence a triple of perimeter $< 2 π$ has no side equal to $π$ , and a fortiori at most one. If no side equals $π$ then all three $d_{π}$ -distances are $< π$ , hence finite $d_{p a t h}$ -distances, hence all three points lie in one component and the sides are intrinsic path distances, because on a pair at distance $< π$ the truncated metric is the componentwise path distance. Finally, a pair of points of the model sphere $S^{2}$ at round distance $π$ is antipodal, since the round distance is $\arccos$ of the inner product.

2.2assume-case largestep 1.2F2algebra

The cone triangle inequality, second case. With the same notation assume $α + β > π$ ; then $\cos α + \cos β = 2 \cos \frac{α + β}{2} \cos \frac{α - β}{2} < 0$ because $\frac{α + β}{2} \in (π / 2, π]$ and $\frac{∣ α - β ∣}{2} < π / 2$ . The identity $d_{C} (P, Q)^{2} = r^{2} + t^{2} - 2 r t \cos α = (r - t \cos α)^{2} + t^{2} \sin^{2} α$ gives $d_{C} (P, Q) \geq r - t \cos α$ , and similarly $d_{C} (Q, T) \geq s - t \cos β$ ; hence $d_{C} (P, Q) + d_{C} (Q, T) \geq r + s - t (\cos α + \cos β) \geq r + s \geq d_{C} (P, T)$ , with strict inequality when $t > 0$ , where the last inequality is step 1.2.

2.3givenstep 1.2step 1.5F2algebra

The product-cone isometry. Let $R : = \sqrt{r^{2} + s^{2}}$ , $\cos θ : = r / R$ , $\sin θ : = s / R$ for $(r, x), (s, y) \in C (L_{1}) \times C (L_{2})$ with $R > 0$ , and map $((r, x), (s, y))$ to the point of $C (L_{1} * L_{2})$ at distance $R$ from the apex in the direction $(\cos θ) x + (\sin θ) y$ ; this map is a bijection onto $C (L_{1} * L_{2})$ (the collapsed cases $r = 0$ or $s = 0$ giving the points over $L_{2}$ or $L_{1}$ , and $R = 0$ the apex) and it carries the square-sum product distance of two points to the cone distance: expanding with $\cos^{2} + \sin^{2} = 1$ gives $d_{C} ((r, x_{1}), (r^{'}, x_{1}^{'}))^{2} + d_{C} ((s, x_{2}), (s^{'}, x_{2}^{'}))^{2} = R^{2} + R^{' 2} - 2 R R^{'} (\cos θ \cos θ^{'} \cos d_{π}^{1} (x_{1}, x_{1}^{'}) + \sin θ \sin θ^{'} \cos d_{π}^{2} (x_{2}, x_{2}^{'}))$ , which is the square of the cone distance of step 1.2 computed with the join formula.

3.1step 1.2step 1.3step 2.2

The cone is a metric. Steps 1.2, 1.3 and 2.2 cover all triples: those with a vanishing radius, those with $α + β \leq π$ and those with $α + β > π$ , so $d_{C}$ satisfies the triangle inequality; symmetry and positivity were noted in step 1.2, and $d_{C} (P, T) = 0$ forces $r = s$ and $d_{π} (x, y) = 0$ , i.e. $P = T$ . Hence $d_{C}$ is a metric on $C (L)$ in all cases, including $d_{π} (x, y) = π$ , different components and $C (\emptyset) = {o}$ , and it is finite-valued on nonempty $L$ .

4.1step 1.2step 3.1

The apex paths. If $d_{π} (x, y) = π$ then step 1.2 gives $d_{C} ((r, x), (s, y)) = r + s$ ; the two radial segments from $(r, x)$ to $o$ and from $o$ to $(s, y)$ have length $r$ and $s$ by step 1.2 and concatenate to a path of length $r + s$ , so it is minimizing, and for $r = 0$ or $s = 0$ the same argument with a single radial segment applies. Thus radial segments are geodesics from the apex and the through-apex path realizes the distance whenever $d_{π} (x, y) = π$ .

4.2step 1.5step 3.1step 2.3F2F5algebra

The join is a metric space. Let $Φ : C (L_{1}) \times C (L_{2}) \to C (L_{1} * L_{2})$ be the bijection of step 2.3 and let $D$ be the cone function on $C (L_{1} * L_{2})$ built by the cone formula of step 1.2 from the join function $d$ of step 1.5; the identity of step 2.3 says exactly that $D (X, X^{'}) = ρ (Φ^{- 1} X, Φ^{- 1} X^{'})$ for all $X, X^{'} \in C (L_{1} * L_{2})$ , where $ρ$ is the square-sum product metric of $C (L_{1}) \times C (L_{2})$ . The cone metrics on $C (L_{1})$ and $C (L_{2})$ are metrics by step 3.1, so $ρ$ is a metric by [F5] and $D$ , the pushforward of $ρ$ along $Φ$ , is a metric as well; in particular $D (X, X^{''}) \leq D (X, X^{'}) + D (X^{'}, X^{''})$ for all $X, X^{'}, X^{''} \in C (L_{1} * L_{2})$ . Now let $x, y, z \in L_{1} * L_{2}$ and put $A : = d (x, y)$ , $B : = d (y, z)$ , $C : = d (x, z)$ ; applying that inequality to the cone points of radii $1, s, 1$ over $x, y, z$ gives $\sqrt{2 - 2 \cos C} \leq \sqrt{1 + s^{2} - 2 s \cos A} + \sqrt{1 + s^{2} - 2 s \cos B}$ for every $s \geq 0$ , by the cone formula of step 1.2. If $A + B \geq π$ then $C \leq π \leq A + B$ by step 1.5; otherwise let $U : = (1, 0)$ and $W : = (\cos (A + B), \sin (A + B))$ in the plane. If $\sin A + \sin B > 0$ put $s_{*} : = \frac{\sin (A + B)}{\sin A + \sin B}$ and $λ : = \frac{\sin A}{\sin A + \sin B} \in [0, 1]$ ; then the point $V : = s_{*} (\cos A, \sin A)$ satisfies $(1 - λ) \cdot 0 + λ \sin (A + B) = s_{*} \sin A$ and $(1 - λ) \cdot 1 + λ \cos (A + B) = \frac{\sin B + \sin A \cos (A + B)}{\sin A + \sin B} = \frac{\sin (A + B) \cos A}{\sin A + \sin B} = s_{*} \cos A$ — the middle equality being the addition formulas, since $\sin B = \sin (A + B) \cos A - \sin A \cos (A + B)$ — so $V = (1 - λ) U + λ W$ lies on the segment $[U, W]$ ; if instead $\sin A + \sin B = 0$ then $A, B \in {0, π}$ with $A + B \leq π$ , the only cases being $(A, B) = (0, 0), (0, π), (π, 0)$ , and the choice $s_{*} : = 1$ gives $V = U$ or $V = W$ . Either way $V$ lies on $[U, W]$ , and expanding the three squares gives $∣ U - V ∣ = \sqrt{1 + s_{*}^{2} - 2 s_{*} \cos A}$ , $∣ V - W ∣ = \sqrt{1 + s_{*}^{2} - 2 s_{*} \cos B}$ and $∣ U - W ∣ = \sqrt{2 - 2 \cos (A + B)} = 2 \sin \frac{A + B}{2}$ ; hence $\sqrt{2 - 2 \cos C} \leq ∣ U - V ∣ + ∣ V - W ∣ = ∣ U - W ∣ = 2 \sin \frac{A + B}{2}$ at $s = s_{*}$ . Both $\frac{C}{2}$ and $\frac{A + B}{2}$ lie in $[0, \frac{π}{2}]$ , where $\sin$ is strictly increasing and $\sqrt{2 - 2 \cos t} = 2 \sin \frac{t}{2}$ for $t \in [0, π]$ by [F2], so $C \leq A + B$ . Hence the join function satisfies the triangle inequality and, with step 1.5, is a metric on $L_{1} * L_{2}$ of diameter at most $π$ .

4.3step 1.2step 3.1F2F3

The cone over a sphere. For $k \geq 1$ the map $C (S^{k - 1}) \to R^{k}$ , $(t, ξ) \mapsto t ξ$ and $o \mapsto 0$ , is a bijection, and for two points it preserves distances because $d_{C} ((t, ξ), (t^{'}, ξ^{'}))^{2} = t^{2} + t^{' 2} - 2 t t^{'} \cos d_{π} (ξ, ξ^{'}) = t^{2} + t^{' 2} - 2 t t^{'} ⟨ ξ, ξ^{'} ⟩ = ∣ t ξ - t^{'} ξ^{'} ∣^{2}$ ; hence $C (S^{k - 1}) ≅ R^{k}$ . For $k = 0$ the sphere $S^{- 1}$ is empty and $C (\emptyset) = {o} = R^{0}$ by the empty convention.

4.4step 3.1step 1.6F2F4algebra

The tangent-cone metric and the cone formula. Put $M = {Lk}_{X} (p)$ with its cellwise intrinsic angular chain distance. Initially this is an extended pseudometric: reversing and concatenating chains prove symmetry and the triangle inequality, but separation has not yet been proved. The following comparison uses the cosine cone function on the direction quotient $C (M)$ and does not assume separation. For the upper bound, if the truncated angular distance is $π$ , use the two radial segments through the origin. Otherwise take a link chain of total angle $Θ < π$ approaching that distance, and develop its successive sectors in a plane: the straight segment between the endpoint radii intersects the intermediate rays and yields a chain in $Z$ of length $\sqrt{t^{2} + t^{' 2} - 2 t t^{'} \cos Θ}$ . For the lower bound replace a chain in $Z$ by its straight cell segments. If any segment passes through the origin, its total length is at least $t + t^{'}$ . Otherwise its radial projections give a link chain; develop the segments with monotonically increasing polar angle, of total angle $Θ$ at least the intrinsic angular distance. If $Θ < π$ , the endpoint chord has length at least the cone distance. If $Θ \geq π$ , split at the first crossing of the opposite ray, at radius $s$ : the preceding polyline has length at least $t + s$ , and the remainder at least $∣ t^{'} - s ∣$ , so the total is at least $t + t^{'}$ . These bounds prove the equality, without passing an infinite value to the cosine. Let $ε = h / 4$ . Cone chains realizing the upper bound between radii below $ε$ remain at radii below $ε$ , so they map to $X$ . Conversely chains in $X$ of length below $h - ε$ between points of $B (p, ε)$ lie in $B (p, h)$ and pull back with unchanged length; chains longer than that already exceed the cone distance, which is at most $2 ε < h - ε$ . Hence $Φ$ preserves distances bijectively between these balls. Distinct directions with zero angular distance would give distinct points at the same radius $ε / 2$ with zero distance in $X$ , contradicting [F4]. Thus the angular chain distance separates directions; the cone function is a metric by step 3.1, and $Φ$ is an isometry $B (o, ε) \subset C (M) \to B (p, ε)$ . Scaling tangent vectors scales every Euclidean chain length, so the cone formula and separation also hold on all of $Z$ .

5.1step 1.4step 4.1F5

Geodesic space. Assume in addition that $L$ is $D_{π}$ -geodesic. For two points $P = (r, x)$ , $T = (s, y)$ : if $r = 0$ or $s = 0$ or $d_{π} (x, y) = π$ use the radial or the through-apex path of step 4.1; if $d_{π} (x, y) < π$ the hypothesis supplies a minimizing segment in $L$ and step 1.4 supplies a minimizing geodesic in $C (L)$ joining $P$ to $T$ . So every two points of $C (L)$ are joined by a geodesic segment and $C (L)$ is a geodesic metric space.

5.2step 2.3step 4.2F2

Associativity, faces and spheres. The unit link of a cone is recovered by $d_{π} (u, v) = \arccos ((2 - d_{C} ((1, u), (1, v))^{2}) / 2)$ , so step 2.3 identifies $L_{1} * L_{2}$ with the unit link of $C (L_{1}) \times C (L_{2})$ ; iterating gives $C ((L_{1} * L_{2}) * L_{3}) ≅ C (L_{1} * L_{2}) \times C (L_{3}) ≅ C (L_{1}) \times C (L_{2}) \times C (L_{3})$ , so the two bracketed joins are isometric up to a canonical isometry; when $L_{1}, L_{2}$ are round unit spheres the same computation with the round inner product gives $S^{m - 1} * S^{n - 1} ≅ S^{m + n - 1}$ , and the face metrics of the join are the joins of the face metrics because the formula restricts to sub-links.

6.1cases-exhaustivestep 1.2step 1.3step 2.2step 5.1F3

Containment in the ball. Let $c$ be a minimizing geodesic from $P = (r, x)$ to $T = (s, y)$ in $C (L)$ and let $Q = (t, z)$ be a point of its image with $α : = d_{π} (x, z)$ , $β : = d_{π} (z, y)$ , $γ : = d_{π} (x, y)$ , so that $d_{C} (P, Q) + d_{C} (Q, T) = d_{C} (P, T)$ . If $Q = o$ the claimed radius bound is immediate, so suppose $t > 0$ . If $α + β > π$ , the strict inequality of step 2.2 contradicts this equality; hence $α + β \leq π$ . Then, with $A, B, C$ as in step 1.3, the chain $d_{C} (P, Q) + d_{C} (Q, T) = ∣ A - B ∣ + ∣ B - C ∣ \geq ∣ A - C ∣ \geq d_{C} (P, T) = d_{C} (P, Q) + d_{C} (Q, T)$ is an equality throughout, so $A, B, C$ are collinear with $B$ between $A$ and $C$ ; since the norm is convex along the segment from $A$ to $C$ , one has $t = ∣ B ∣ \leq \max {∣ A ∣, ∣ C ∣} = \max {r, s}$ . This includes $Q = o$ and the endpoints, so every minimizing geodesic joining $P$ to $T$ is contained in the closed ball of radius $\max {r, s}$ about $o$ .

7.1step 2.3step 4.2step 4.3step 5.2step 4.4F3algebra∎

The face product and its angular link. Let $U = span (F - p)$ . Every active facet normal is perpendicular to $U$ , so each tangent cone splits orthogonally as $U \oplus N_{F} C_{r}$ , and the gluing maps respect the common $U$ and the normal sections. Thus $Z$ is the gluing of $U \times N_{F} C_{r}$ . The chain comparison of step 4.4 applied to the normal cones identifies their glued chain distance $d_{N}$ with the cosine cone function on their angular direction quotient; separation is checked below. The chain metric of $Z$ is the square-sum product metric: each chain has length at least $\sqrt{∣ u - u^{'} ∣^{2} + d_{N} (n, n^{'})^{2}}$ by the triangle inequality in $R^{2}$ , applied to its nonnegative coordinate lengths; conversely choose a piecewise straight normal path with length approaching $d_{N} (n, n^{'})$ , parametrise it proportionally to length, and move the $U$ coordinate linearly over the same interval. The resulting cellwise path has length $\sqrt{∣ u - u^{'} ∣^{2} + ℓ_{N}^{2}}$ , proving the reverse bound on taking infima (constant normal paths cover coincident endpoints; a zero infimum is handled by arbitrarily short chains). Since the chain distance on $Z$ is a metric by step 4.4, the product identity forces $d_{N}$ to separate points. The cone formula then forces the angular chain distance of distinct normal directions to be positive; reversal and concatenation give its extended metric axioms. Consequently $Z ≅ R^{k} \times C ({Lk}_{X} (F))$ , with the genuine cone metric of step 3.1. Steps 2.3, 4.2 and 4.3 identify this product with $C (S^{k - 1} * {Lk}_{X} (F))$ by a map preserving radial norm. Recovering the truncated angular distance from the distances of unit radial points as in step 5.2 gives $M ≅ S^{k - 1} * {Lk}_{X} (F)$ with its angular metric. The ball isometries and all charts preserve intrinsic lengths.

Remarks

Source of the route. Clauses (1)-(3) are Bridson-Haefliger I.5.6-I.5.16 (cone, truncation, geodesic characterisation, join and product-cone isometry) with Davis Appendix I.2 (Proposition I.2.17, Lemma I.2.18) for the cone and join; clause (4) is Bridson-Haefliger I.7.14-I.7.16 together with the facial identification $Lk (x, Σ) = S^{\dim F - 1} * Lk (F, Σ)$ used in the proof of Davis Theorem I.3.5.
Triangle inequality of the join. The proof replaces an earlier, false argument (embedding three points of each factor into the round circle) by the product-cone pullback of step 4.2: the join formula is the apex-angle formula of the cone over the join, whose cone function is a metric because it is the pushforward of the square-sum product of the two Euclidean cones, and the chord comparison $\sqrt{2 - 2 \cos t} = 2 \sin \frac{t}{2}$ at the radii $1, s_{*}, 1$ then transfers the triangle inequality to the three classes, uniformly in all cases including disconnected links and sides of length $π$ .

5 · Examples, counterexamples and false statements

None yet.

Spherical Simplex Metrics, Angular Links, and Cones

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Spherical Gram simplices and angular links of Euclidean faces

Definition

Remarks

Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas

Statement

Facts & Assumptions

Proof

Remarks

The angular path metric, the Euclidean cone and spherical joins

Definition

Remarks

The cone and join metrics and the local product chart of a polyhedral gluing

Statement

Facts & Assumptions

Proof

Remarks

5 · Examples, counterexamples and false statements

Sources