ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

A spherical simplex from a Gram matrix and its vertex-link Schur complement

Example

Let $c = \frac{1}{2}$ and let $C$ be the $4 \times 4$ real symmetric matrix with diagonal entries $1$ and off-diagonal entries $c$ . Then:

(i) $C$ is positive definite: for every $x \in R^{4}$ , $x^{T} C x = (1 - c) ∥ x ∥^{2} + c (\sum_{i} x_{i})^{2}$ , which is $> 0$ for $x \neq 0$ because $1 - c = \frac{1}{2} > 0$ and $c > 0$ .

(ii) By Spherical Gram simplices and angular links of Euclidean faces and Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(i), the Cholesky realisation gives four unit vectors $u_{0}, u_{1}, u_{2}, u_{3} \in R^{4}$ with $u_{i} \cdot u_{j} = \frac{1}{2}$ for $i \neq j$ ; the pairwise angular distances in the spherical simplex $Σ (C)$ are all $\arccos \frac{1}{2}$ , and the barycentric ray coordinates of every point of $Σ (C)$ are unique. The functional with $φ (u_{i}) = 1$ is the pairing with the vector $w = \frac{2}{5} (u_{0} + u_{1} + u_{2} + u_{3})$ (from $C \cdot 1 = \frac{5}{2} \cdot 1$ ), and $φ \equiv 1$ on $Δ (C)$ ; hence $Σ (C)$ lies in the open hemisphere ${φ > 0}$ .

(iii) The vertex link of $u_{0}$ computed by the Schur formula of Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(iv) has Gram matrix with off-diagonal entries $\frac{c - c^{2}}{1 - c^{2}} = \frac{c}{1 + c} = \frac{1}{3}$ ; explicitly $C^{l k} = (\begin{array}{ccc} 1 & \frac{1}{3} & \frac{1}{3} \\ \frac{1}{3} & 1 & \frac{1}{3} \\ \frac{1}{3} & \frac{1}{3} & 1 \end{array}), y^{T} C^{l k} y = \frac{2}{3} ∥ y ∥^{2} + \frac{1}{3} (\sum_{i} y_{i})^{2} > 0 (y \neq 0),$ so the link is the spherical triangle with all vertex-to-vertex angular distances $\arccos \frac{1}{3}$ , and its positivity is exactly the Schur-complement positivity of Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(iv).

(iv) Iterating the formula once more gives the link of the face spanned by $u_{0}, u_{1}$ as the arc of angular length $\arccos \frac{1}{4}$ between the unit directions of the orthogonal projections of $u_{2}, u_{3}$ onto $span (u_{0}, u_{1})^{⊥}$ : the projected squared norms are $\frac{2}{3}$ and the projected inner product is $\frac{1}{6}$ , so the projected cosine is $\frac{1}{4}$ , the same value that the two-step Schur computation $\frac{1 / 3 - (1 / 3)^{2}}{1 - (1 / 3)^{2}} = \frac{1}{4}$ produces; the formula and the positivity check are otherwise the same, so the face-link computation is order-independent for this matrix.

Facts & Assumptions

Given: The real symmetric $4 \times 4$ matrix $C$ with diagonal entries $1$ and off-diagonal entries $c = \frac{1}{2}$ , and its Cholesky realisation $u_{0}, u_{1}, u_{2}, u_{3}$ of Spherical Gram simplices and angular links of Euclidean faces.

[F1]

A real symmetric positive-definite matrix has a unique Cholesky factorisation with lower triangular factor and positive diagonal, and the bijection between positive-definite matrices and their Cholesky data (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).

[F2]

In a real inner-product space, $∣ v ∣ = \sqrt{⟨ v, v ⟩}$ is a norm, $∣ ⟨ u, v ⟩ ∣ \leq ∣ u ∣ ∣ v ∣$ , orthogonal projections onto finite-dimensional subspaces exist with $∣ x ∣^{2} = ∣ P x ∣^{2} + ∣ x - P x ∣^{2}$ , and for a subspace with basis $b_{1}, \dots, b_{k}$ the projection is $P x = \sum_{i, j} g^{i j} ⟨ x, b_{j} ⟩ b_{i}$ for the inverse Gram matrix $(g^{i j})$ (Real and complex inner-product spaces and their induced length, The induced length is a norm, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas).

[F3]

The Cholesky rows $u_{i}$ are unit vectors with $u_{i} \cdot u_{j} = c_{i j}$ ; the angular distance is $d_{a n g} (ξ, η) = \arccos ⟨ ξ, η ⟩$ ; the functional $φ$ with $φ (u_{i}) = 1$ satisfies $φ (\sum_{i} λ_{i} u_{i}) = \sum_{i} λ_{i}$ and $φ \equiv 1$ on $Δ (C)$ ; the link of the face spanned by a set of vertices has the Schur-complement Gram matrix of Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(i), (ii) and (iv) (Spherical Gram simplices and angular links of Euclidean faces, Principal inverse sine and inverse cosine).

Verification

1.1givenF1algebra

The quadratic form. Since $C$ has diagonal $1$ and off-diagonal $c$ , expanding gives $x^{T} C x = \sum_{i} x_{i}^{2} + 2 c \sum_{i < j} x_{i} x_{j} = (1 - c) ∥ x ∥^{2} + c (\sum_{i} x_{i})^{2}$ ; with $c = \frac{1}{2}$ both coefficients are positive, so $x^{T} C x > 0$ for $x \neq 0$ and $C$ is positive definite.

2.1step 1.1F3

The Gram realisation. By step 1.1 and [F1] the Cholesky factorisation $C = L L^{T}$ exists with $L$ invertible, and [F3] gives that its rows $u_{0}, \dots, u_{3}$ are unit vectors with $u_{i} \cdot u_{j} = c_{i j}$ ; thus $u_{i} \cdot u_{j} = \frac{1}{2}$ for $i \neq j$ , the pairwise angular distances are $\arccos \frac{1}{2}$ , and every point of $Σ (C)$ has unique barycentric ray coordinates.

3.1step 2.1F3algebra

The hemisphere functional. Let $w : = \frac{2}{5} (u_{0} + u_{1} + u_{2} + u_{3})$ and $φ (x) : = ⟨ w, x ⟩$ . Since every row of $C$ sums to $1 + 3 c = \frac{5}{2}$ , for each fixed $j$ one has $⟨ w, u_{j} ⟩ = \frac{2}{5} \sum_{i} ⟨ u_{i}, u_{j} ⟩ = \frac{2}{5} \cdot \frac{5}{2} = 1$ ; hence $φ (u_{i}) = 1$ for all $i$ , so by [F3] $φ (\sum_{i} λ_{i} u_{i}) = \sum_{i} λ_{i}$ and $φ \equiv 1$ on $Δ (C)$ . Therefore $Σ (C) \subseteq {x : φ (x) > 0}$ , the open hemisphere.

3.2step 2.1F3algebra

The vertex link. By [F3] and the Schur formula with $c = \frac{1}{2}$ , the link of $u_{0}$ has Gram matrix $C^{l k}$ whose diagonal entries are $1$ and whose off-diagonal entries are $\frac{c - c^{2}}{1 - c^{2}} = \frac{1 / 2 - 1 / 4}{3 / 4} = \frac{1}{3}$ . Its quadratic form is $y^{T} C^{l k} y = \frac{2}{3} ∥ y ∥^{2} + \frac{1}{3} (\sum_{i} y_{i})^{2}$ , which is positive for $y \neq 0$ ; so the link is the spherical triangle whose three angular distances are $\arccos \frac{1}{3}$ .

3.3step 2.1F2algebra

The face link by projection. Let $G$ be the Gram matrix of $u_{0}, u_{1}$ , so $G = (\begin{array}{cc} 1 & 1 / 2 \\ 1 / 2 & 1 \end{array})$ and $G^{- 1} = \frac{4}{3} (\begin{array}{cc} 1 & - 1 / 2 \\ - 1 / 2 & 1 \end{array})$ ; the orthogonal projection onto $span (u_{0}, u_{1})$ is $P x = \sum_{i, j} g^{i j} ⟨ x, u_{j} ⟩ u_{i}$ by [F2], so $P u_{2} = \frac{1}{3} (u_{0} + u_{1}) = P u_{3}$ and $∣ P u_{2} ∣^{2} = \frac{1}{3}$ ; hence $∣ proj u_{2} ∣^{2} = ∣ proj u_{3} ∣^{2} = 1 - \frac{1}{3} = \frac{2}{3}$ and $⟨ proj u_{2}, proj u_{3} ⟩ = ⟨ u_{2}, u_{3} ⟩ - ⟨ P u_{2}, P u_{3} ⟩ = \frac{1}{2} - \frac{1}{3} = \frac{1}{6}$ , so the projected cosine is $\frac{1 / 6}{2 / 3} = \frac{1}{4}$ and the link of the face is an arc of angular length $\arccos \frac{1}{4}$ .

4.1step 3.2step 3.3F3algebra

The two-step Schur value. Iterating the Schur formula of [F3] over the vertices $u_{0}, u_{1}$ means applying it first to the Gram matrix of the link of $u_{0}$ , whose off-diagonal entries are $\frac{1}{3}$ by step 3.2, and then to a $2 \times 2$ block; the resulting off-diagonal entry is $\frac{1 / 3 - (1 / 3)^{2}}{1 - (1 / 3)^{2}} = \frac{2 / 9}{8 / 9} = \frac{1}{4}$ , the same value as the projected cosine of step 3.3.

5.1step 3.3step 4.1F3∎

Order independence and conclusion. By [F3] the link of the face spanned by $u_{0}, u_{1}$ equals the Gram matrix of the normalised orthogonal projections of the remaining vertices onto $span (u_{0}, u_{1})^{⊥}$ , so the projection computation of step 3.3 and the iterated Schur computation of step 4.1 are two descriptions of the same matrix; they agree at the value $\frac{1}{4}$ , the face link is an arc of angular length $\arccos \frac{1}{4}$ , and the positivity check is the one of step 3.2 applied to this $2 \times 2$ block, whose determinant $1 - \frac{1}{16}$ is positive.

Remarks

What the example checks. The example instantiates the definition and the four clauses of the Schur formula: positivity of the Gram matrix by an explicit quadratic form, the Cholesky realisation, the hemisphere functional $φ = ⟨ \frac{2}{5} (u_{0} + u_{1} + u_{2} + u_{3}), \cdot ⟩$ , the vertex-link Schur complement with value $\frac{1}{3}$ , and the iterated two-step computation with value $\frac{1}{4}$ matching an independent projection computation.
The hemisphere functional is written with the vertices. The vector representing $φ$ is $\frac{2}{5} (u_{0} + u_{1} + u_{2} + u_{3})$ , which uses the eigen-identity $C \cdot 1 = \frac{5}{2} \cdot 1$ ; it is not the vector $\frac{2}{5} (1, 1, 1, 1)$ of ambient coordinates, because the Cholesky rows $u_{i}$ are not the standard basis.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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