ExampleConstruction: Literature-sourcedVerification: 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 cycle and an overlong arm: explicit non-positive witnesses

Example

Throughout, $S$ is finite, $m$ is a Coxeter matrix with diagram $Γ$ and Coxeter form $B$ on $V = R^{S}$ (Coxeter diagrams: edges, labels, components and finite type, The real Coxeter form, its radical, reflections, and form-preserving maps), and one is asked whether $B$ can be positive definite.

(i) Cycles. Let $Γ$ be the cycle on $r \geq 3$ vertices $s_{1}, \dots, s_{r}$ with all labels $3$ , so that $B (e_{s_{i}}, e_{s_{i + 1}}) = - \frac{1}{2}$ for consecutive pairs (indices modulo $r$ ) and all other off-diagonal entries are $0$ . Then $u = e_{s_{1}} + \dots + e_{s_{r}}$ satisfies $B (u, u) = r - 2 \cdot r \cdot \frac{1}{2} = 0$ , so the cycle is not positive definite; more generally, if the labels on the cycle are $\geq 3$ then $B (u, u) \leq 0$ .

(ii) An overlong arm. Let $Γ = E_{9}$ be the star with central vertex $c$ and arms of $1, 2, 5$ vertices, all edges labelled $3$ , with arm vertices $a$ (length $1$ ), $b_{1} - b_{2}$ (length $2$ , $b_{1}$ adjacent to $c$ ) and $d_{1} - \dots - d_{5}$ (length $5$ , $d_{5}$ adjacent to $c$ ). Then $u = e_{c} + \frac{1}{2} e_{a} + \frac{1}{3} (2 e_{b_{1}} + e_{b_{2}}) + \frac{1}{6} (e_{d_{1}} + 2 e_{d_{2}} + 3 e_{d_{3}} + 4 e_{d_{4}} + 5 e_{d_{5}})$ satisfies $B (u, u) = 0$ ; hence the star $(1, 2, 5)$ , the one-vertex extension of $E_{8}$ , is not positive definite, in agreement with the arm inequality of Exclusions for positive definite diagrams: trees, valency, labels, chains and arms (6), which the triple $(1, 2, 5)$ fails with equality.

(iii) Two large labels. The three-vertex path with both edges labelled $4$ has the witness $u = e_{s_{1}} + \sqrt{2} e_{s_{2}} + e_{s_{3}}$ with $B (u, u) = 0$ , and the four-vertex path with labels $4, 3, 4$ has the witness $u = e_{s_{1}} + \sqrt{2} e_{s_{2}} + \sqrt{2} e_{s_{3}} + e_{s_{4}}$ with $B (u, u) = 0$ ; these are the first members of the family excluded in Exclusions for positive definite diagrams: trees, valency, labels, chains and arms (4)(ii).

Facts & Assumptions

Given: A finite set $S$ with Coxeter matrix $m$ and diagram $Γ$ , the space $V = R^{S}$ with the Coxeter form $B$ , and the specific diagrams of (i), (ii) and (iii).

[F1]

Distinct vertices $s \neq t$ of $Γ$ are joined exactly when $m (s, t) \geq 3$ and carry the label $m (s, t)$ ; the subdiagram $Γ_{T}$ is the induced labelled graph on $T$ , so deleting vertices deletes exactly the incident edges; the neighbours of $s$ are $N (s) = {t \neq s : m (s, t) \geq 3}$ (Coxeter diagrams: edges, labels, components and finite type).

[F2]

$B$ is the unique symmetric bilinear form on $V$ with $B (e_{s}, e_{s}) = 1$ , $B (e_{s}, e_{t}) = - \cos (π / m (s, t))$ for finite $m (s, t)$ and $B (e_{s}, e_{t}) = - 1$ for $m (s, t) = \infty$ (The real Coxeter form, its radical, reflections, and form-preserving maps).

[F3]

If $0 \neq u \in V_{T}$ for some $T \subseteq S$ and $B (u, u) \leq 0$ , then $B$ is not positive definite; and if all coordinates of $u$ are $\geq 0$ while a labelled graph $Γ_{0}$ on $T$ has all labels at most the labels of $Γ_{T}$ , then $B_{T} (u, u) \leq B_{0} (u, u)$ (Exclusions for positive definite diagrams: trees, valency, labels, chains and arms (1)).

[F4]

With $c (s, t) : = - B (e_{s}, e_{t})$ for $s \neq t$ : $c (s, t) \in [0, 1]$ , $c (s, t) = 0$ exactly when $m (s, t) = 2$ , and $c (s, t) \geq \frac{1}{2}$ whenever $m (s, t) \geq 3$ (Exclusions for positive definite diagrams: trees, valency, labels, chains and arms).

[F5]

For a vertex $v$ of degree $3$ whose edges all have label $3$ and whose three arms have $p, q, r \geq 1$ vertices, $\frac{1}{p + 1} + \frac{1}{q + 1} + \frac{1}{r + 1} > 1$ is necessary for positive definiteness (Exclusions for positive definite diagrams: trees, valency, labels, chains and arms (6)).

[F6]

$\cos (2 x) = 2 \cos^{2} x - 1$ for every real $x$ (Double-angle and quadratic power-reduction identities).

[F7]

$\cos (x + π) = - \cos x$ and $\cos (- x) = \cos x$ for every real $x$ (Quarter-turn values and shifts by pi/2 and pi, Parity and the Pythagorean identity for sine and cosine).

[F8]

Cosine is strictly decreasing on $[0, π]$ , $π > 0$ and $\cos π = - 1$ (Signs, monotonicity intervals, and ranges of sine and cosine, Pi as twice the smallest positive zero of cosine, Quarter-turn values and shifts by pi/2 and pi).

[F9]

$\cos (π / 4) = \sqrt{2} / 2$ and this factor is positive (The finite Viete cosine product and its positive nested-radical factors).

[F10]

$\sqrt{2} \geq 0$ and ${\sqrt{2}}^{2} = 2$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

Verification

1.1F6F7F8F9algebra

(The two numerical values.) $\cos (π / 4) = \sqrt{2} / 2$ is [F9]. For $\cos (π / 3)$ , put $c = \cos (π / 3)$ : the shift formula gives $\cos (2 π / 3) = \cos (π - π / 3) = - \cos (- π / 3) = - c$ by [F7], while the double-angle formula gives $\cos (2 π / 3) = 2 c^{2} - 1$ by [F6]; hence $2 c^{2} - 1 = - c$ , i.e. $(2 c - 1) (c + 1) = 0$ . Since $0 < π / 3 < π$ and cosine is strictly decreasing on $[0, π]$ with $\cos π = - 1$ , one has $c > - 1$ [F8], so $c = \cos (π / 3) = 1 / 2$ .

2.1F2step 1.1algebra

(Weighted arms.) Let a path arm on vertices $s_{1}, \dots, s_{p}$ have all its edges labelled $3$ and let $s_{p}$ be the vertex adjacent to the centre $c$ ; put $u_{p} = \sum_{k = 1}^{p} k e_{s_{k}}$ . Every internal edge ${s_{k}, s_{k + 1}}$ contributes $k (k + 1) B (e_{s_{k}}, e_{s_{k + 1}}) = - k (k + 1) / 2$ twice, so $B (u_{p}, u_{p}) = \sum_{k = 1}^{p} k^{2} - \sum_{k = 1}^{p - 1} k (k + 1) = p^{2} - \sum_{k = 1}^{p - 1} k = p (p + 1) / 2$ , by [1.1] and [F2]; and $B (e_{c}, u_{p}) = - p / 2$ since among the pairs $(c, s_{k})$ only ${c, s_{p}}$ is an edge, with coefficient $p$ .

2.2F1F2F3F4step 1.1algebra

(The cycle witness (i).) For the cycle of (i) put $u = \sum_{i = 1}^{r} e_{s_{i}} \neq 0$ , a non-negative vector. Its diagonal contribution is $r$ ; each of the $r$ consecutive pairs contributes $2 B (e_{s_{i}}, e_{s_{i + 1}}) = - 2 c (s_{i}, s_{i + 1}) \leq - 1$ because $c \geq \frac{1}{2}$ on edges [F4], and every other pair is a non-edge, contributing $0$ [F2, F4]; hence $B (u, u) \leq r - r = 0$ , so $B$ is not positive definite by [F3]. If the labels on the cycle are any values $\geq 3$ , the same computation gives $B (u, u) \leq 0$ because each consecutive $c$ is still $\geq \frac{1}{2}$ while every other pair contributes $\leq 0$ (an edge of label $\geq 3$ gives $\leq - 1$ , a non-edge gives $0$ ), and the conclusion is unchanged.

2.3F2F3step 1.1F10algebra

(Two large labels (iii).) For the path with labels $4, 4$ and $u = e_{s_{1}} + \sqrt{2} e_{s_{2}} + e_{s_{3}}$ : the diagonal is $1 + 2 + 1 = 4$ [F2], and the two edges contribute $2 \cdot (- \cos (π / 4)) \cdot \sqrt{2} = - 2 \sqrt{2} \cos (π / 4) = - 2$ each by [F10] and [1.1]; hence $B (u, u) = 4 - 4 = 0$ . For the path with labels $4, 3, 4$ and $u = e_{s_{1}} + \sqrt{2} e_{s_{2}} + \sqrt{2} e_{s_{3}} + e_{s_{4}}$ : the diagonal is $1 + 2 + 2 + 1 = 6$ , the two label- $4$ edges contribute $- 2$ each, and the middle label- $3$ edge contributes $2 \cdot (- \frac{1}{2}) \cdot \sqrt{2} \cdot \sqrt{2} = - 2$ by [1.1]; hence $B (u, u) = 6 - 6 = 0$ . In both cases $u \neq 0$ has non-negative coordinates, so $B$ is not positive definite by [F3].

3.1F1F2F3step 2.1algebra

(The star witness (ii).) In the star of (ii) the three arms meet only at $c$ [F1], so the three arm vectors $u_{1} = \frac{1}{2} e_{a}$ , $u_{2} = \frac{1}{3} (2 e_{b_{1}} + e_{b_{2}})$ and $u_{3} = \frac{1}{6} (e_{d_{1}} + 2 e_{d_{2}} + 3 e_{d_{3}} + 4 e_{d_{4}} + 5 e_{d_{5}})$ , in which the centre-adjacent vertices $a, b_{1}, d_{5}$ carry the weights $1, 2, 5$ , are pairwise $B$ -orthogonal; step 2.1 with $p = 1, 2, 5$ gives $B (u_{1}, u_{1}) = \frac{1}{4}$ , $B (u_{2}, u_{2}) = \frac{1}{9} \cdot 3 = \frac{1}{3}$ , $B (u_{3}, u_{3}) = \frac{1}{36} \cdot 15 = \frac{5}{12}$ , and $B (e_{c}, u_{1}) = - \frac{1}{2} \cdot \frac{1}{2} = - \frac{1}{4}$ , $B (e_{c}, u_{2}) = - \frac{1}{3} \cdot \frac{2}{2} = - \frac{1}{3}$ , $B (e_{c}, u_{3}) = - \frac{1}{6} \cdot \frac{5}{2} = - \frac{5}{12}$ . Therefore $u = e_{c} + u_{1} + u_{2} + u_{3}$ satisfies $B (u, u) = 1 + \frac{1}{4} + \frac{1}{3} + \frac{5}{12} + 2 (- \frac{1}{4} - \frac{1}{3} - \frac{5}{12}) = 1 - (\frac{1}{4} + \frac{1}{3} + \frac{5}{12}) = 0$ , and $u \neq 0$ with all coordinates $\geq 0$ , so $B$ is not positive definite by [F3].

4.1F5step 3.1step 2.3algebra∎

(Agreement with the general exclusions.) The triple $(1, 2, 5)$ of arm lengths in (ii) gives $\frac{1}{1 + 1} + \frac{1}{2 + 1} + \frac{1}{5 + 1} = \frac{1}{2} + \frac{1}{3} + \frac{1}{6} = 1$ , so it fails the necessary inequality [F5] with equality, and the star of (ii) is the first diagram at which the arm inequality becomes non-strict; the equality in the computation of [3.1] is the same equality. The paths of (iii) are the two shortest diagrams with two edges of label $\geq 4$ , so they are the first members of the family excluded in Exclusions for positive definite diagrams: trees, valency, labels, chains and arms (4)(ii), whose witness vector is $\sqrt{2}$ -weighted on the interior of the chain, exactly as in [2.3].

Depends on

Used by

Path determinants dₖ=dₖ₋₁-cos²(π/m)dₖ₋₂ and the three-arm inequality Example

Dependency tree · two levels

58 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

Jean Michel, Lectures on Coxeter groups (Beijing lecture notes, April-May 2014) (standard reference, not scraped)
Michael W. Davis, The Geometry and Topology of Coxeter Groups (first-edition author manuscript, 2007-2008) (standard reference, not scraped)