the objects of the claim.

This file is intentionally byte-identical (after the header) to the definitions in Challenge.lean: it defines Lehmer's polynomial, the generalized Cartan matrix of the hyperbolic Kac–Moody root system E₁₀, its simple reflections acting on the root lattice in the basis of simple roots, and a Coxeter element as the product of the ten simple reflections.

noncomputable def lehmerPolynomial : Polynomial ℤ

Lehmer's polynomial (Lehmer, 1933): x¹⁰ + x⁹ − x⁷ − x⁶ − x⁵ − x⁴ − x³ + x + 1. Its Mahler measure λ ≈ 1.17628 is the smallest known Mahler measure > 1 of an integer polynomial.

Equations

• lehmerPolynomial = Polynomial.X ^ 10 + Polynomial.X ^ 9 - Polynomial.X ^ 7 - Polynomial.X ^ 6 - Polynomial.X ^ 5 - Polynomial.X ^ 4 - Polynomial.X ^ 3 + Polynomial.X + 1

def cartanE10 : Matrix (Fin 10) (Fin 10) ℤ

The generalized Cartan matrix of the rank-10 hyperbolic Kac–Moody root system E₁₀: nodes 0–8 form an A₉ chain and node 9 is attached to node 2 (Bourbaki-style E-series labelling, extended once more past E₉ = E₈⁽¹⁾).

Equations

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

def simpleReflection (i : Fin 10) : Matrix (Fin 10) (Fin 10) ℤ

The simple reflection sᵢ of the E₁₀ Weyl group acting on the root lattice, in the basis of simple roots: sᵢ(αⱼ) = αⱼ − aᵢⱼ αᵢ, so as a matrix (sᵢ)ⱼₖ = δⱼₖ − δⱼᵢ aᵢₖ.

Equations

• simpleReflection i = Matrix.of fun (j k : Fin 10) => (if j = k then 1 else 0) - if j = i then cartanE10 i k else 0

def coxeterE10 : Matrix (Fin 10) (Fin 10) ℤ

A Coxeter element of the E₁₀ Weyl group: the product s₀ s₁ ⋯ s₉ of the ten simple reflections, as a matrix acting on the root lattice.

Equations

• coxeterE10 = (List.map simpleReflection (List.finRange 10)).prod