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.

The exceptional spectra for E_6 and H_3 computed exactly: characteristic polynomials, cyclotomic factorisations and the resulting degree tables

Statement

Assume the Axiom of Choice. Take the exceptional types $E_{6}$ and $H_{3}$ with the node numberings of the recorded certificate: $E_{6}$ is the path $0 - 1 - 2 - 3 - 4$ with a leaf $5$ attached to node $2$ , all edges labelled $3$ ; $H_{3}$ is the path $0 - 1 - 2$ with edges labelled $5$ and $3$ . Let $c$ be the bipartite Coxeter element, applied in the recorded orders $[0, 2, 4, 1, 3, 5]$ and $[0, 2, 1]$ , and let $ρ$ be the canonical reflection representation on $V = R^{S}$ with $B (e_{s}, e_{t}) = - \cos (π / m_{s t})$ and $r_{t} (v) = v - 2 B (v, e_{t}) e_{t}$ . Put $h : = ord (c)$ and $ζ_{h} : = e^{2 π i / h}$ . Then:

(1) $E_{6}$ . Here $h = 12$ , and the Coxeter element in the simple-root basis has characteristic polynomial $\det (X I - ρ (c)) = X^{6} + X^{5} - X^{3} + X + 1 = Φ_{3} (X) Φ_{12} (X),$ spectral exponents $1, 4, 5, 7, 8, 11$ , and basic degrees $2, 5, 6, 8, 9, 12$ , whose product is $51840 = ∣ W (E_{6}) ∣$ .

(2) $H_{3}$ . Here $h = 10$ . Put $φ : = 2 \cos (π / 5)$ , so $φ^{2} = φ + 1$ and $φ = 1 + ζ_{10}^{2} + ζ_{10}^{- 2}$ . The Coxeter element has characteristic polynomial $\det (X I - ρ (c)) = X^{3} + (1 - φ) X^{2} + (1 - φ) X + 1 = (X + 1) (X^{2} - φ X + 1),$ spectral exponents $1, 5, 9$ , and basic degrees $2, 6, 10$ , whose product is $120 = ∣ W (H_{3}) ∣$ .

(3) The residue sums are $36 = 6 \cdot 12 / 2$ and $15 = 3 \cdot 10 / 2$ , matching $∣ Φ_{+} ∣$ in each type. The operator orders are exactly $12$ and $10$ ; the characteristic polynomials have the primitive roots $ζ_{12}$ and $ζ_{10}$ , respectively.

Facts & Assumptions

Given: AC; one of the two finite Coxeter systems and the recorded bipartite reflection order from the Statement.

[F1]

The canonical representation is a homomorphism with $ρ (s) = r_{e_{s}}$ , and its complexification is faithful; for a finite Coxeter group these matrices have finite order. The simple-root Gram form and reflection formula are the ones in the Statement (The canonical reflection homomorphism, roots, reflections, and the positive cone, Complexifying a finite Coxeter reflection representation: faithfulness, complex reflections, and the hypotheses of the invariant-theory suppliers (1), The real Coxeter form, its radical, reflections, and form-preserving maps).

[F2]

The diagrams are finite type; the bipartite element is the product of the two commuting color-class products, and reversing class order gives a conjugate. The diagram lists, finite group property and Coxeter conventions are as stated in the classification (The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a, Coxeter diagrams: edges, labels, components and finite type, Classification of finite Coxeter systems, including the H and dihedral families (1)).

[F3]

For a square matrix $M$ , $\det (X I - M)$ is its characteristic polynomial; $A adj (A) = \det (A) I$ ; formal differentiation gives $\frac{d}{d t} \det (I - t M) = - tr (adj (I - t M) M)$ ; trace is the diagonal sum, so it is linear and $tr (A B) = \sum_{i, j} a_{i j} b_{j i} = \sum_{j, i} b_{j i} a_{i j} = tr (B A)$ ; and a finite-order operator over $C$ is diagonalisable (For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix, For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring, For every positive-sized square matrix over a commutative ring, $A adj (A) = adj (A) A = \det (A) I$ , $\frac{d}{d x} \det (I - x A) = - tr (adj (I - x A) A)$ , The formal derivative of a polynomial, The trace of a square matrix over a commutative ring, Over an algebraically closed field of characteristic $0$ , every element of finite order acts diagonalisably in a finite-dimensional representation). Over a field, a positive-sized square matrix is invertible exactly when its determinant is nonzero (A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit); hence $\det (λ I - M) = 0$ exactly when $λ$ is an eigenvalue.

[F4]

The cyclotomic polynomial $Φ_{m}$ has precisely the primitive $m$ th roots of unity as its roots; $ζ_{h}$ has order $h$ , and Euler's formula gives $e^{i θ} + e^{- i θ} = 2 \cos θ$ (The cyclotomic polynomials $Φ_{n} \in Z [t]$ , defined by $\prod_{d ∣ n} Φ_{d} = t^{n} - 1$ , Over a field whose characteristic does not divide $n$ , the roots of $Φ_{n}$ are exactly the primitive roots of unity, The $n$ -th roots of a complex number and the $n$ distinct roots of unity for every $n \geq 1$ , The group $μ_{n} (K)$ of $n$ -th roots of unity in a field, and primitive $n$ -th roots of unity, The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ , Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ ).

[F5]

The exact E6 and H3 reflection matrices in the recorded root orders, their exact power-sum lists, the H3 identity $φ^{2} = φ + 1$ , the embeddings of $φ$ in the corresponding cyclotomic fields, and the positive-root counts $∣ Φ_{+} ∣ = n h / 2$ are the outputs established in the preceding exceptional-spectrum item (The six exceptional Coxeter spectra: characteristic polynomials, orders and spectral exponents from exact matrices (2.1),(4.1),(5.1)-(5.2)).

[F6]

Under AC, the general theorem identifies basic degrees with one plus the spectral exponents, gives $h = \max_{i} d_{i}$ , and gives $\prod_{i} d_{i} = ∣ W ∣$ (Basic degrees, exponents, and the graded coinvariant algebra of a finite Coxeter system, A regular Coxeter eigenvector determines the basic degrees: the exponent-residue identification and the complete degree tables for all finite Coxeter types (1)-(2), The Axiom of Choice).

Proof

technique · Construct the two matrices from the reflection formula, derive the exact trace recurrence for the characteristic polynomial, and identify their roots with roots of unity

1.1F1F2algebra

For either diagram, let $R_{t}$ denote the matrix of $r_{t}$ . Its $j$ th column is $e_{j} - 2 B (e_{j}, e_{t}) e_{t}$ by [F1]. If the recorded application order is $i_{1}, \dots, i_{n}$ , then $M = R_{i_{n}} \dots R_{i_{1}}$ is the matrix of the corresponding bipartite Coxeter element. The Gram entries are $- 1 / 2$ on each label- $3$ edge, $- φ / 2$ on the label- $5$ edge of $H_{3}$ , and $0$ off the diagram. Applying the column rule gives $M_{E_{6}} = (\begin{array}{cccccc} - 1 & 1 & 0 & 0 & 0 & 0 \\ - 1 & 1 & - 1 & 1 & 0 & 1 \\ 0 & 1 & - 1 & 1 & 0 & 1 \\ 0 & 1 & - 1 & 1 & - 1 & 1 \\ 0 & 0 & 0 & 1 & - 1 & 0 \\ 0 & 1 & - 1 & 1 & 0 & 0 \end{array}), M_{H_{3}} = (\begin{array}{ccc} - 1 & φ & 0 \\ - φ & 1 + φ & - 1 \\ 0 & 1 & - 1 \end{array}) .$ These are the matrices for the stated application orders; the reflections preserve $B$ , so the products are finite-order matrices of the corresponding Coxeter elements [F1, F2].

1.2F3

For either matrix $M$ , write $\det (I - t M) = \sum_{k = 0}^{n} q_{k} t^{k}$ , with $q_{0} = 1$ , and $adj (I - t M) = \sum_{k = 0}^{n - 1} B_{k} t^{k}$ . The adjugate identity gives $B_{0} = I$ and, by comparing the coefficient of $t^{k}$ , $B_{k} = M B_{k - 1} + q_{k} I$ for $1 \leq k < n$ . The derivative identity in [F3] gives $k q_{k} = - tr (B_{k - 1} M) = - tr (M B_{k - 1})$ for $1 \leq k \leq n$ , using trace cyclicity. Thus the exact recurrence is $q_{k} = - tr (M B_{k - 1}) / k$ , $B_{k} = M B_{k - 1} + q_{k} I$ ; for $k = n$ , only $q_{n}$ is needed [F3, algebra]. Since $\det (X I - M) = X^{n} \det (I - X^{- 1} M)$ , the same $q_{k}$ are the coefficients of $X^{n - k}$ in the characteristic polynomial [F3, algebra].

2.1F3F5step 1.2algebra

Exact multiplication of the displayed matrices gives the following power traces and recurrence traces. For $E_{6}$ , $(tr M, \dots, tr M^{6}) = (- 1, 1, 2, - 3, - 1, - 2)$ and $(tr (M B_{0}), \dots, tr (M B_{5})) = (- 1, 0, 3, 0, - 5, - 6)$ , so $(q_{1}, \dots, q_{6}) = (1, 0, - 1, 0, 1, 1)$ . For $H_{3}$ , using $φ^{2} = φ + 1$ , $(tr M, tr M^{2}, tr M^{3}) = (φ - 1, φ, - φ)$ and $(tr (M B_{0}), tr (M B_{1}), tr (M B_{2})) = (φ - 1, 2 (φ - 1), - 3)$ , so $(q_{1}, q_{2}, q_{3}) = (1 - φ, 1 - φ, 1)$ . Substituting these coefficients into $\det (X I - M) = X^{n} + q_{1} X^{n - 1} + \dots + q_{n}$ yields the two displayed characteristic polynomials in (1) and (2).

3.1F4F5step 2.1algebra

Use the fixed integers $H = 12$ for E6 and $H = 10$ for H3 in this root calculation, independently of the unknown group order $h$ ; throughout this step $ζ_{H} = \exp (2 π i / H)$ . For E6, $Φ_{3} (X) = X^{2} + X + 1$ and $Φ_{12} (X) = X^{4} - X^{2} + 1$ ; multiplying gives $X^{6} + X^{5} - X^{3} + X + 1$ , the polynomial computed in 2.1. The roots of $Φ_{3}$ are $ζ_{12}^{4}, ζ_{12}^{8}$ , and the roots of $Φ_{12}$ are $ζ_{12}^{1}, ζ_{12}^{5}, ζ_{12}^{7}, ζ_{12}^{11}$ . Thus the E6 spectral exponents are $1, 4, 5, 7, 8, 11$ . All these eigenvalues are twelfth roots and $ζ_{12}$ occurs. For H3, the polynomial in 2.1 factors as $(X + 1) (X^{2} - φ X + 1)$ . By [F4]-[F5], $ζ_{10} + ζ_{10}^{- 1} = 2 \cos (π / 5) = φ$ , so the quadratic roots are $ζ_{10}, ζ_{10}^{- 1}$ ; the linear root is $- 1 = ζ_{10}^{5}$ . Thus its spectral exponents are $1, 5, 9$ , all tenth roots with $ζ_{10}$ occurring.

4.1F1F3F5F6step 3.1algebra∎

By [F1]-[F3], each matrix is finite order and diagonalisable. Step 3.1 shows that in E6 all eigenvalues are twelfth roots of unity and $ζ_{12}$ occurs, so $M^{12} = I$ while $M^{k} \neq I$ for every positive $k < 12$ ; in H3 all eigenvalues are tenth roots and $ζ_{10}$ occurs, so $M^{10} = I$ while $M^{k} \neq I$ for every positive $k < 10$ . Thus the matrix orders are exactly $12$ and $10$ . Faithfulness in [F1] implies the orders of $c$ and $M = ρ_{C} (c)$ agree, so $h = 12$ and $h = 10$ , respectively. The residue sums are $1 + 4 + 5 + 7 + 8 + 11 = 36 = 6 \cdot 12 / 2$ and $1 + 5 + 9 = 15 = 3 \cdot 10 / 2$ , which equal $∣ Φ_{+} ∣$ by [F5]. Under AC, [F6] gives the degrees $e_{i} + 1$ : E6 has $2, 5, 6, 8, 9, 12$ , and H3 has $2, 6, 10$ . Their products are $51840$ and $120$ , respectively, so [F6] gives the stated group orders. The Axiom of Choice is used only for this basic-degree transfer; all matrix, trace and root calculations are finite and exact.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

160 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

Bill Casselman, Essays on Coxeter groups: Coxeter elements in finite Coxeter groups (author-hosted PDF, 12 pages) (standard reference, not scraped)
Josh Swanson, On eigenvalues of representations of reflection groups and wreath products (University of Washington CAT seminar notes, 7-page PDF) (standard reference, not scraped)