ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Gram determinants and principal minors of the non-crystallographic types $H_{3}$ and $H_{4}$

Example

Let $Γ = H_{3}$ be the path $s_{1} - s_{2} - s_{3}$ with labels $m (s_{1}, s_{2}) = 3$ , $m (s_{2}, s_{3}) = 5$ , and let $Γ = H_{4}$ be the path $s_{1} - s_{2} - s_{3} - s_{4}$ with labels $3, 3, 5$ (Coxeter diagrams: edges, labels, components and finite type); let $B$ be the Coxeter form and $C$ the cosine matrix (The real Coxeter form, its radical, reflections, and form-preserving maps). Using $\cos (π / 5) = (1 + \sqrt{5}) / 4$ (derived in Verification 1.1):

(i) $H_{3}$ . The leading principal minors of $2 C$ are $2$ , $3$ and $\det (2 C) = 3 - \sqrt{5} > 0$ ; the $2 \times 2$ principal minor on the label- $5$ edge equals $4 \sin^{2} (π / 5) = (5 - \sqrt{5}) / 2 > 0$ ; the minor on ${s_{1}, s_{3}}$ equals $4$ . Hence $B$ is positive definite and the Coxeter group of type $H_{3}$ is finite.

(ii) $H_{4}$ . The leading principal minors of $2 C$ are $2, 3, 4$ (the first three vertices form type $A_{3}$ ) and $\det (2 C) = \frac{7 - 3 \sqrt{5}}{2} > 0$ . Hence $B$ is positive definite and the Coxeter group of type $H_{4}$ is finite.

(iii) Excluded neighbours. The overlong paths with labels $3, 5, 3$ and $3, 3, 5, 3$ have negative determinant, and the star with a degree- $3$ vertex whose three incident edges have labels $3, 3, 5$ has the negative witness value $1 - (\frac{1}{4} + \frac{1}{4} + \cos^{2} (π / 5)) < 0$ ; none of these diagrams is of finite type (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite, Exclusions for positive definite diagrams: trees, valency, labels, chains and arms (3),(4)).

Facts & Assumptions

Given: The paths $H_{3}$ , $H_{4}$ and the three excluded diagrams above, with the Coxeter form $B$ and its cosine matrix $C = (B (e_{s}, e_{t}))$ ; write $d_{k}$ for the determinant of the leading $k \times k$ principal submatrix of $C$ .

[F1]

$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$ , without any positivity assumption; non-adjacent distinct vertices have $m (s, t) = 2$ and hence matrix entry $0$ (The real Coxeter form, its radical, reflections, and form-preserving maps, Coxeter diagrams: edges, labels, components and finite type).

[F2]

$T_{5} (\cos θ) = \cos (5 θ)$ for every real $θ$ , and the Chebyshev polynomials of the first kind satisfy $T_{0} = 1$ , $T_{1} = t$ , $T_{n + 2} = 2 t T_{n + 1} - T_{n}$ ; $\cos (x + π) = - \cos x$ , $\cos π = - 1$ ; $\cos (2 x) = 2 \cos^{2} x - 1$ ; $1 - \cos^{2} x = \sin^{2} x$ and $\sin x > 0$ for $0 < x < π$ ; cosine is strictly decreasing on $[0, π]$ ; and $2 < \sqrt{5} < 3$ , $3 \sqrt{5} < 7$ ( $T_{n} (\cos θ) = \cos (n θ)$ and $U_{n} (\cos θ) \sin θ = \sin ((n + 1) θ)$ for every $n \in N$ , Chebyshev polynomials of the first and second kinds by their three-term recurrences, Quarter-turn values and shifts by pi/2 and pi, Double-angle and quadratic power-reduction identities, Signs, monotonicity intervals, and ranges of sine and cosine, Pi as twice the smallest positive zero of cosine, Parity and the Pythagorean identity for sine and cosine, Squaring is monotone on the nonnegatives, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[F3]

A symmetric real matrix is positive definite if and only if its leading principal minors are positive; the form $B$ is positive definite when $B (u, u) > 0$ for every $u \neq 0$ , and $W$ is finite if and only if $B$ is positive definite (Sylvester's criterion: a real symmetric $n \times n$ matrix with $n \geq 1$ is positive definite if and only if all leading principal minors are positive, Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form, Finiteness criterion: W is finite exactly when the Coxeter form is positive definite).

[F4]

Scaling an $n \times n$ matrix by $2$ multiplies its determinant by $2^{n}$ , and $d_{k}$ is the determinant of the leading $k \times k$ principal submatrix (Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring, The determinant is the unique normalized alternating multilinear function on the columns).

[F5]

$H_{3}$ and $H_{4}$ are among the standard diagrams of the classification, and every proper principal submatrix of a listed diagram is a block diagonal matrix whose blocks are listed diagrams of smaller rank (Classification of finite Coxeter systems, including the H and dihedral families (3)).

[F6]

Laplace expansion along any row or column expresses the determinant as the sum of entries times their cofactors; the cofactor sign is $(- 1)^{i + j}$ and the determinant of the empty deleted matrix is $1$ (Laplace expansion computes the determinant along every row and every column over a commutative ring, Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring).

Verification

1.1F2algebra

(The three trigonometric values and the small determinants.) $\cos (π / 3) = 1 / 2$ follows from the double-angle formula $\cos (2 x) = 2 \cos^{2} x - 1$ at $x = π / 3$ together with $\cos (2 π / 3) = \cos (π - π / 3) = - \cos (π / 3)$ , which gives $2 c^{2} - 1 = - c$ , i.e. $(2 c - 1) (c + 1) = 0$ , and $c = \cos (π / 3) > - 1$ because $π / 3 \in (0, π)$ and cosine is strictly decreasing on $[0, π]$ with $\cos π = - 1$ [F2]; thus $c = 1 / 2$ . Also $\cos (π / 5) = (1 + \sqrt{5}) / 4$ : with $c_{5} = \cos (π / 5)$ , iterating the recurrence of [F2] gives $T_{5} (t) = 16 t^{5} - 20 t^{3} + 5 t$ , so $T_{5} (c_{5}) = \cos π = - 1$ , i.e. $16 c_{5}^{5} - 20 c_{5}^{3} + 5 c_{5} + 1 = (c_{5} + 1) (4 c_{5}^{2} - 2 c_{5} - 1)^{2} = 0$ by expansion, while $0 < π / 5 < π / 2$ gives $0 < c_{5} < 1$ [F2], so $c_{5} \neq - 1$ , $4 c_{5}^{2} - 2 c_{5} - 1 = 0$ and $(c_{5} - \frac{1}{4})^{2} = \frac{5}{16}$ ; by uniqueness of nonnegative square roots $c_{5} = \frac{1}{4} \pm \frac{\sqrt{5}}{4}$ , and the positive value is $(1 + \sqrt{5}) / 4$ because the other is negative as $2 < \sqrt{5}$ [F2]. Thus $\sin^{2} (π / 5) = 1 - \cos^{2} (π / 5) = (5 - \sqrt{5}) / 8 > 0$ [F2]; also $\sqrt{5} < 3$ and $3 \sqrt{5} < 7$ [F2], by squaring the positive quantities ( $5 < 9$ and $45 < 49$ ).

1.2F1F6algebra

(The recurrence without positivity.) For any of the paths in the Example, let $C_{k}$ be its leading $k \times k$ cosine matrix and set $d_{0} : = 1$ , $d_{1} = 1$ . For $k \geq 2$ put $a : = \cos (π / m_{k - 1})$ . By [F1] the last row has only the potentially nonzero entries $- a$ in column $k - 1$ and $1$ in column $k$ . In the deleted matrix for the first entry, the last column has only the bottom entry $- a$ , whose cofactor is $d_{k - 2}$ ; its determinant is therefore $- a d_{k - 2}$ by [F6]. The last-row cofactor sign at $(k, k - 1)$ is $- 1$ , while the diagonal cofactor is $d_{k - 1}$ . Thus Laplace expansion yields $d_{k} = d_{k - 1} - a^{2} d_{k - 2}$ [F6]. This identity uses no definiteness assumption and applies equally to the excluded paths.

2.1F1F2F3F4step 1.1step 1.2algebra

(The $H_{3}$ minors and positive definiteness.) With $d_{0} = 1$ , $d_{1} = 1$ and $d_{k} = d_{k - 1} - \cos^{2} (π / m_{k - 1}) d_{k - 2}$ by 1.2 [step 1.2]: $d_{2} = 1 - \cos^{2} (π / 3) = \frac{3}{4}$ , $d_{3} = \frac{3}{4} - \cos^{2} (π / 5) \cdot 1 = \frac{3}{4} - \frac{3 + \sqrt{5}}{8} = \frac{3 - \sqrt{5}}{8} > 0$ by 1.1 [step 1.1]. Multiplying by $2^{k}$ [F4] gives for $2 C$ the leading minors $2 d_{1} = 2$ , $4 d_{2} = 3$ , $8 d_{3} = 3 - \sqrt{5} > 0$ , and $\det (2 C) = 3 - \sqrt{5}$ ; the principal submatrix of $C$ on the label- $5$ edge ${s_{2}, s_{3}}$ is $(\begin{array}{cc} 1 & - \cos (π / 5) \\ - \cos (π / 5) & 1 \end{array})$ with determinant $\sin^{2} (π / 5)$ , so the determinant of the corresponding submatrix of $2 C$ is $4 \sin^{2} (π / 5) = (5 - \sqrt{5}) / 2 > 0$ [F1, F2]. The submatrix of $2 C$ on ${s_{1}, s_{3}}$ is $diag (2, 2)$ with determinant $4$ . All leading principal minors of $2 C$ are positive, so $2 C$ and hence $C$ is positive definite by [F3], and $H_{3}$ has finite Coxeter group.

2.2F1F2F3F4step 1.1step 1.2algebra

(The $H_{4}$ minors and positive definiteness.) Using the recurrence of 1.2 [step 1.2] for the path with labels $3, 3, 5$ : $d_{1} = 1$ , $d_{2} = \frac{3}{4}$ , $d_{3} = \frac{3}{4} - \frac{1}{4} \cdot 1 = \frac{1}{2}$ , $d_{4} = \frac{1}{2} - \cos^{2} (π / 5) \cdot \frac{3}{4} = \frac{1}{2} - \frac{3 + \sqrt{5}}{8} \cdot \frac{3}{4} = \frac{16 - 9 - 3 \sqrt{5}}{32} = \frac{7 - 3 \sqrt{5}}{32} > 0$ by 1.1 [step 1.1]. The first three vertices carry the all- $3$ path $A_{3}$ with the computed doubled leading minors $2, 3, 4$ [F4], and $\det (2 C) = 16 d_{4} = (7 - 3 \sqrt{5}) / 2 > 0$ because $3 \sqrt{5} < 7$ [F2]; all leading principal minors of $2 C$ are positive, so $C$ is positive definite by [F3] and $H_{4}$ has finite Coxeter group.

2.3F1F2F3step 1.1step 1.2algebra

(The excluded neighbours.) The unconditional recurrence of 1.2 [step 1.2] for the path with labels $3, 5, 3$ gives $d_{4} = d_{3} - \cos^{2} (π / 3) d_{2} = \frac{3 - \sqrt{5}}{8} - \frac{1}{4} \cdot \frac{3}{4} = \frac{3 - 2 \sqrt{5}}{16} < 0$ because $2 \sqrt{5} > 3$ , i.e. $\sqrt{5} > 3 / 2$ , follows from $\sqrt{5} > 2$ [F2]; for the path with labels $3, 3, 5, 3$ it gives $d_{5} = d_{4} - \cos^{2} (π / 3) d_{3} = \frac{7 - 3 \sqrt{5}}{32} - \frac{1}{4} \cdot \frac{1}{2} = \frac{3 - 3 \sqrt{5}}{32} < 0$ because $\sqrt{5} > 1$ [F2]; a negative leading minor excludes positive definiteness by [F3]. For the star with centre $c$ and neighbours $a, b, d$ , edges $c a, c b$ labelled $3$ and $c d$ labelled $5$ , the vector $u = e_{c} + \frac{1}{2} (e_{a} + e_{b}) + \cos (π / 5) e_{d} \neq 0$ has non-negative coordinates and satisfies $B (u, u) = 1 + \frac{1}{4} + \frac{1}{4} + \cos^{2} (π / 5) + 2 (- \frac{1}{4} - \frac{1}{4} - \cos^{2} (π / 5)) = 1 - (\frac{1}{4} + \frac{1}{4} + \cos^{2} (π / 5)) = \frac{1 - \sqrt{5}}{8} < 0$ because $\cos^{2} (π / 5) = (3 + \sqrt{5}) / 8$ [F2]; by [F3] this star is not positive definite either.

3.1F3F5step 2.1step 2.2step 2.3algebra∎

(Conclusion.) The leading principal minors of $2 C$ computed in 2.1 and 2.2 [step 2.1, step 2.2] are all positive, so $B$ is positive definite for $H_{3}$ and for $H_{4}$ by Sylvester's criterion [F3]; by the finiteness criterion [F3] the Coxeter groups of types $H_{3}$ and $H_{4}$ are finite, agreeing with their appearance in the classification [F5]. The three diagrams of 2.3 [step 2.3] either have a negative leading principal minor or a nonzero non-negative vector with non-positive value, so none of them is positive definite and none of their Coxeter groups is finite [F3], which is (iii).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

116 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

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

Gram determinants and principal minors of the non-crystallographic types H3H3​ and H4H4​