the Mahler measure of Lehmer's polynomial, in Mathlib's own API.

Mathlib now has the Mahler measure (Polynomial.mahlerMeasure, Jensen-formula definition, with mahlerMeasure_eq_leadingCoeff_mul_prod_roots), Kronecker's theorem in Mahler form, and Northcott's theorem. This file connects the repository to that API:

• lehmer_mahlerMeasure : M(L) = μ — the Mahler measure of Lehmer's polynomial is exactly the Salem root, computed (not estimated) from the root classification: eight roots on the unit circle contribute 1, ν = 1/μ lies inside, and μ alone lies outside.
• one_lt_lehmer_mahlerMeasure, lehmer_mahlerMeasure_lt : 1 < M(L) < 7/5, from the interval y₅ ∈ (2, 21/10) already isolated by the trace-quintic sign changes.
• LehmerConjecture, LehmerMinimal : Lehmer's 1933 question, stated in Mathlib's vocabulary (a hypothesis Prop, not claimed, not assumed): Mahler measures of integer polynomials do not accumulate at 1; strongly, L attains the minimum. lehmerConjecture_of_minimal : the strong form implies the gap form, with the gap witnessed by M(L) itself — which is > 1 by this file.
• coxeterE10_infinite_order : the E₁₀ Coxeter element has infinite order in GL(10, ℤ). If Cox^n = 1 then, since its characteristic polynomial L is irreducible, L would be the minimal polynomial and would divide Xⁿ − 1; but μ is a root of L with μ > 1, and every root of Xⁿ − 1 has norm 1. Together with coxeterE8_* facts (finite case) this locates E₁₀ precisely: the Coxeter series crosses from torsion (spectrum on the unit circle) to a Salem element exactly at rank 10, and the crossing value is Lehmer's number.

The Mahler measure of L is the Salem root μ.

theorem LehmerE10.classified_prod_max (S : Multiset ℂ) (hS : ∀ z ∈ S, ‖z‖ = 1 ∨ z = ↑mu ∨ z = ↑nu) : (Multiset.map (fun (z : ℂ) => max 1 ‖z‖) S).prod = mu ^ Multiset.count (↑mu) S

The classified product with max 1 ‖·‖ weights: unit-circle roots contribute 1, ν < 1 contributes 1, and each occurrence of μ contributes μ.

theorem LehmerE10.lehmer_mahlerMeasure : LC.mahlerMeasure = mu

The Mahler measure of Lehmer's polynomial is the Salem root: M(L) = μ. Computed exactly from mahlerMeasure_eq_leadingCoeff_mul_prod_roots and the root classification — this is the number ≈ 1.17628, the smallest known Mahler measure > 1 of an integer polynomial.

theorem LehmerE10.one_lt_lehmer_mahlerMeasure : 1 < LC.mahlerMeasure

M(L) > 1: Lehmer's polynomial is not a product of cyclotomics, quantitatively.

theorem LehmerE10.s5_lt : s5 < 7 / 10

The Salem square root is below 7/10: s₅² = y₅² − 4 < (21/10)² − 4 < (7/10)².

theorem LehmerE10.lehmer_mahlerMeasure_lt : LC.mahlerMeasure < 7 / 5

M(L) < 7/5: an unconditional upper bound from the trace-root interval. (The true value is 1.17628…; sharper bounds need only a tighter sign-change interval for y₅.)

Lehmer's question, stated in Mathlib's vocabulary.

Both are hypothesis Props: stated, never claimed, never assumed.

def LehmerE10.LehmerConjecture : Prop

Lehmer's conjecture (Lehmer 1933, gap form): Mahler measures of integer polynomials do not accumulate at 1 — there is a uniform gap c > 1 below which the only Mahler measure is 1 itself.

Equations

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

def LehmerE10.LehmerMinimal : Prop

The strong form: Lehmer's polynomial attains the minimal Mahler measure > 1.

Equations

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

theorem LehmerE10.lehmerConjecture_of_minimal (h : LehmerMinimal) : LehmerConjecture

The strong form implies the gap form, with the gap witnessed by M(L) itself — legitimate because M(L) > 1 is proven above.

The Coxeter element has infinite order.

theorem LehmerE10.coxeterE10_infinite_order {n : ℕ} (hn : 0 < n) : coxeterE10 ^ n ≠ 1

The E₁₀ Coxeter element has infinite order. If Cox^n = 1, then since its characteristic polynomial is the irreducible L, the minimal polynomial is L and divides Xⁿ − 1; evaluating at the Salem root μ > 1 gives μⁿ = 1, impossible.

Contrast: the Coxeter element of a finite Weyl group has order h (the Coxeter number — 30 for E₈); at E₁₀ the spectrum has left the unit circle and no power returns.