the finite contrast: the E₈ Coxeter element has order 30.

The E-series Coxeter elements cross a phase boundary at rank 10. For the finite root system E₈ the Coxeter element is torsion — its order is the Coxeter number h = 30, and its spectrum consists of the primitive 30th roots of unity (the exponents of E₈ are exactly the totatives of 30). Two ranks later, at the hyperbolic E₁₀, the Coxeter element is a Salem matrix of infinite order (coxeterE10_infinite_order) whose spectral radius is Lehmer's number. This file pins the finite side by kernel computation, in the same simple-reflection convention as Defs.lean:

• coxeterE8_pow_thirty : coxeterE8 ^ 30 = 1;
• orderOf_coxeterE8 : the order is exactly 30 (no proper power at 30/2, 30/3, 30/5 is the identity). So the pair (E₈, E₁₀) realizes both sides of Kronecker's dichotomy for integer matrices: spectrum on the unit circle ⟹ roots of unity ⟹ finite order, versus one eigenvalue off the circle ⟹ infinite order — with Lehmer's number as the first exit.

def LehmerE10.cartanE8 : Matrix (Fin 8) (Fin 8) ℤ

The Cartan matrix of E₈: nodes 0–6 form an A₇ chain and node 7 is attached to node 2 — the same labelling convention as cartanE10, truncated to the finite diagram (arm lengths 2, 1, 4 off the branch node 2).

Equations

• One or more equations did not get rendered due to their size.

def LehmerE10.simpleReflectionE8 (i : Fin 8) : Matrix (Fin 8) (Fin 8) ℤ

The simple reflection sᵢ of the E₈ Weyl group on the root lattice: (sᵢ)ⱼₖ = δⱼₖ − δⱼᵢ aᵢₖ.

Equations

• LehmerE10.simpleReflectionE8 i = Matrix.of fun (j k : Fin 8) => (if j = k then 1 else 0) - if j = i then LehmerE10.cartanE8 i k else 0

def LehmerE10.coxeterE8 : Matrix (Fin 8) (Fin 8) ℤ

A Coxeter element of the E₈ Weyl group: the product s₀ s₁ ⋯ s₇.

Equations

• LehmerE10.coxeterE8 = (List.map LehmerE10.simpleReflectionE8 (List.finRange 8)).prod

def LehmerE10.coxeterE8Mat : Matrix (Fin 8) (Fin 8) ℤ

The Coxeter element s₀ s₁ ⋯ s₇, evaluated (kernel computation below).

Equations

• One or more equations did not get rendered due to their size.

theorem LehmerE10.coxeterE8_eq : coxeterE8 = coxeterE8Mat

theorem LehmerE10.coxeterE8_pow_thirty : coxeterE8 ^ 30 = 1

coxeterE8 ^ 30 = 1: the E₈ Coxeter element is torsion, of order dividing the Coxeter number h = 30. Kernel computation, staged as ((c⁵)³)².

theorem LehmerE10.orderOf_coxeterE8 : orderOf coxeterE8 = 30

The order of the E₈ Coxeter element is exactly the Coxeter number 30: the powers 30/2 = 15, 30/3 = 10, 30/5 = 6 are not the identity (kernel computations), so no proper divisor of 30 kills it.