the assembly:

`Irreducible lehmerPolynomial`   and   `coxeterE10.charpoly = lehmerPolynomial`.

Route: (1) TRACE CENSUS: the trace quintic q (with L(x) = x⁵·q(x + 1/x), TraceQuintic) has EXACTLY the five IVT-located real roots y₁<y₂<y₃<y₄ ∈ (−2,2), y₅ ∈ (2,21/10): five distinct roots of a degree-5 polynomial exhaust its complex roots, and q = ∏(X − yᵢ) — so q'(y₅) = ∏_{i<5}(y₅ − yᵢ) ≠ 0: the Salem trace root is simple. (2) ROOT CLASSIFICATION: every complex root z of L has trace z + 1/z ∈ {y₁..y₅}; the four ball traces force ‖z‖ = 1 (norm_eq_one_of_trace_in_ball), the Salem trace forces z ∈ {μ, ν} with μν = 1, ν < 1 < μ (the off-circle Salem pair). (3) SALEM PAIR SIMPLE: a double root of L at t ∈ {μ,ν} would kill L' there; the derivative–trace identity z²·L'(z) = 5z⁶·q(y) + (z⁷ − z⁵)·q'(y) then forces q'(y₅) = 0 (since t ∉ {0, ±1}) — refuted by (1). count μ = count ν = 1 in L. (4) THE FACTOR ARGUMENT: L = F·G proper monic ⟹ F(0)·G(0) = L(0) = 1 ⟹ ‖F(0)‖ = 1; but ‖F(0)‖ = ∏‖roots F‖ = μ^a·ν^b with (a,b) ∈ {0,1}² by (3). (1,0) gives μ = 1, (0,1) gives ν = 1 — both refuted; (0,0) makes F all-on-circle, (1,1) makes G all-on-circle — both killed by no_unit_circle_factor (Kronecker + the uniform-1291 cyclotomic kill). No proper factor exists. (5) ASSEMBLY: lehmer_irreducible (ℤ, then ℚ by Gauss); the Coxeter element of E₁₀ is annihilated by L (kernel computation), so by charpoly_eq_lehmer_of_irreducible its characteristic polynomial is L — first over ℚ, then over ℤ by injectivity of the coefficient map. SCOPE: Lehmer's 1933 conjecture (a positive lower bound for Mahler measures > 1) is NOT claimed anywhere in this repository. Axiom footprint: propext, Classical.choice, Quot.sound only.

The five trace roots, pinned from the RHLehmerTrace IVT witnesses.

noncomputable def LehmerE10.y1 : ℝ

The first trace root of the quintic q, in (−2, −1).

Equations

• LehmerE10.y1 = LehmerE10.traceQ_root_1.choose

noncomputable def LehmerE10.y2 : ℝ

The second trace root of the quintic q, in (−1, 0).

Equations

• LehmerE10.y2 = LehmerE10.traceQ_root_2.choose

noncomputable def LehmerE10.y3 : ℝ

The third trace root of the quintic q, in (0, 1).

Equations

• LehmerE10.y3 = LehmerE10.traceQ_root_3.choose

noncomputable def LehmerE10.y4 : ℝ

The fourth trace root of the quintic q, in (1, 2).

Equations

• LehmerE10.y4 = LehmerE10.traceQ_root_4.choose

noncomputable def LehmerE10.y5 : ℝ

The Salem trace root of the quintic q, in (2, 21/10) — the one root off [−2, 2], giving the reciprocal pair {μ, 1/μ}.

Equations

• LehmerE10.y5 = LehmerE10.traceQ_root_salem.choose

theorem LehmerE10.y1_mem : y1 ∈ Set.Ioo (-2) (-3 / 2)

theorem LehmerE10.y2_mem : y2 ∈ Set.Ioo (-3 / 2) (-1)

theorem LehmerE10.y3_mem : y3 ∈ Set.Ioo (-1) 0

theorem LehmerE10.y4_mem : y4 ∈ Set.Ioo 0 1

theorem LehmerE10.y5_mem : y5 ∈ Set.Ioo 2 (21 / 10)

theorem LehmerE10.y1_root : traceQ y1 = 0

theorem LehmerE10.y2_root : traceQ y2 = 0

theorem LehmerE10.y3_root : traceQ y3 = 0

theorem LehmerE10.y4_root : traceQ y4 = 0

theorem LehmerE10.y5_root : traceQ y5 = 0

theorem LehmerE10.y_chain : y1 < y2 ∧ y2 < y3 ∧ y3 < y4 ∧ y4 < y5

The trace quintic as a polynomial over ℂ, and its root census.

noncomputable def LehmerE10.tracePoly : Polynomial ℂ

The trace quintic over ℂ: q(y) = y⁵ + y⁴ − 5y³ − 5y² + 4y + 3, with L(x) = x⁵·q(x + 1/x).

Equations

• LehmerE10.tracePoly = Polynomial.X ^ 5 + Polynomial.X ^ 4 - Polynomial.C 5 * Polynomial.X ^ 3 - Polynomial.C 5 * Polynomial.X ^ 2 + Polynomial.C 4 * Polynomial.X + Polynomial.C 3

theorem LehmerE10.tracePoly_monic : tracePoly.Monic

theorem LehmerE10.tracePoly_natDegree : tracePoly.natDegree = 5

theorem LehmerE10.tracePoly_eval (z : ℂ) : Polynomial.eval z tracePoly = traceQC z

theorem LehmerE10.trace_root_mem {y : ℝ} (hy : traceQ y = 0) : ↑y ∈ tracePoly.roots

noncomputable def LehmerE10.T5 : Multiset ℂ

The five trace roots as a multiset over ℂ.

Equations

• LehmerE10.T5 = {↑LehmerE10.y1, ↑LehmerE10.y2, ↑LehmerE10.y3, ↑LehmerE10.y4, ↑LehmerE10.y5}

theorem LehmerE10.T5_nodup : T5.Nodup

theorem LehmerE10.trace_roots_eq : tracePoly.roots = T5

theorem LehmerE10.trace_root_cases {w : ℂ} (hw : traceQC w = 0) : w = ↑y1 ∨ w = ↑y2 ∨ w = ↑y3 ∨ w = ↑y4 ∨ w = ↑y5

Trace exhaustion: every complex root of the trace quintic is one of the five.

theorem LehmerE10.trace_factor : tracePoly = (Polynomial.X - Polynomial.C ↑y1) * (Polynomial.X - Polynomial.C ↑y2) * (Polynomial.X - Polynomial.C ↑y3) * (Polynomial.X - Polynomial.C ↑y4) * (Polynomial.X - Polynomial.C ↑y5)

The spectral factorization of the trace quintic: q = ∏ (X − yᵢ).

The derivative of the trace quintic; the Salem trace root is simple.

noncomputable def LehmerE10.dtraceQC (y : ℂ) : ℂ

The derivative of the trace quintic, evaluated over ℂ (used to show the trace roots are simple).

Equations

• LehmerE10.dtraceQC y = 5 * y ^ 4 + 4 * y ^ 3 - 15 * y ^ 2 - 10 * y + 4

theorem LehmerE10.tracePoly_derivative_eval (w : ℂ) : Polynomial.eval w (Polynomial.derivative tracePoly) = dtraceQC w

theorem LehmerE10.dtrace_y5_ne_zero : dtraceQC ↑y5 ≠ 0

THE SALEM TRACE ROOT IS SIMPLE: q'(y₅) = ∏_{i<5}(y₅ − yᵢ) ≠ 0.

Lehmer over ℂ: evaluation bridge, derivative, and the derivative–trace identity.

noncomputable def LehmerE10.LC : Polynomial ℂ

Lehmer's polynomial over ℂ.

Equations

• LehmerE10.LC = Polynomial.map (Int.castRingHom ℂ) lehmerPolynomial

theorem LehmerE10.LC_poly : LC = Polynomial.X ^ 10 + Polynomial.X ^ 9 - Polynomial.X ^ 7 - Polynomial.X ^ 6 - Polynomial.X ^ 5 - Polynomial.X ^ 4 - Polynomial.X ^ 3 + Polynomial.X + 1

theorem LehmerE10.LC_eval (z : ℂ) : Polynomial.eval z LC = lehmerC z

theorem LehmerE10.LC_monic : LC.Monic

theorem LehmerE10.LC_ne_zero : LC ≠ 0

theorem LehmerE10.LC_eval_zero : Polynomial.eval 0 LC = 1

theorem LehmerE10.root_ne_zero {z : ℂ} (hz : z ∈ LC.roots) : z ≠ 0

theorem LehmerE10.LC_derivative_eval (z : ℂ) : Polynomial.eval z (Polynomial.derivative LC) = 10 * z ^ 9 + 9 * z ^ 8 - 7 * z ^ 6 - 6 * z ^ 5 - 5 * z ^ 4 - 4 * z ^ 3 - 3 * z ^ 2 + 1

theorem LehmerE10.deriv_trace_identity {z : ℂ} (hz : z ≠ 0) : z ^ 2 * Polynomial.eval z (Polynomial.derivative LC) = 5 * z ^ 6 * traceQC (z + 1 / z) + (z ^ 7 - z ^ 5) * dtraceQC (z + 1 / z)

THE DERIVATIVE–TRACE IDENTITY: differentiating L(z) = z⁵ q(z + 1/z) and clearing denominators: z²·L'(z) = 5z⁶·q(y) + (z⁷ − z⁵)·q'(y) at y = z + 1/z.

The off-circle Salem pair {μ, ν}, μν = 1, ν < 1 < μ.

noncomputable def LehmerE10.s5 : ℝ

The square-root discriminant √(y₅² − 4) splitting the Salem trace root into the reciprocal pair.

Equations

• LehmerE10.s5 = √(LehmerE10.y5 ^ 2 - 4)

noncomputable def LehmerE10.mu : ℝ

Lehmer's number μ ≈ 1.17628: the larger root of x² − y₅·x + 1.

Equations

• LehmerE10.mu = (LehmerE10.y5 + LehmerE10.s5) / 2

noncomputable def LehmerE10.nu : ℝ

The reciprocal root 1/μ: the smaller root of x² − y₅·x + 1.

Equations

• LehmerE10.nu = (LehmerE10.y5 - LehmerE10.s5) / 2

theorem LehmerE10.y5_gt_two : 2 < y5

theorem LehmerE10.s5_sq : s5 ^ 2 = y5 ^ 2 - 4

theorem LehmerE10.s5_pos : 0 < s5

theorem LehmerE10.mu_nu_sum : mu + nu = y5

theorem LehmerE10.mu_nu_prod : mu * nu = 1

theorem LehmerE10.mu_gt_one : 1 < mu

theorem LehmerE10.nu_pos : 0 < nu

theorem LehmerE10.nu_lt_one : nu < 1

theorem LehmerE10.muC_prod : ↑mu * ↑nu = 1

theorem LehmerE10.muC_sum : ↑mu + ↑nu = ↑y5

theorem LehmerE10.muC_ne_zero : ↑mu ≠ 0

theorem LehmerE10.nuC_ne_zero : ↑nu ≠ 0

theorem LehmerE10.muC_ne_nuC : ↑mu ≠ ↑nu

theorem LehmerE10.mu_trace : ↑mu + 1 / ↑mu = ↑y5

theorem LehmerE10.nu_trace : ↑nu + 1 / ↑nu = ↑y5

theorem LehmerE10.traceQC_y5 : traceQC ↑y5 = 0

Root classification: on the circle, or in the Salem pair.

theorem LehmerE10.root_classification {z : ℂ} (hz : z ∈ LC.roots) : ‖z‖ = 1 ∨ z = ↑mu ∨ z = ↑nu

ROOT CLASSIFICATION (proven): every complex root of Lehmer is on the unit circle or equals μ or ν — the trace lands on one of the five census roots; ball traces pin the circle, the Salem trace pins the pair.

theorem LehmerE10.muC_mem : ↑mu ∈ LC.roots

theorem LehmerE10.nuC_mem : ↑nu ∈ LC.roots

The Salem pair is SIMPLE in L (multiplicity one).

theorem LehmerE10.salem_count_le_one {t : ℝ} (ht0 : 0 < t) (ht1 : t ≠ 1) (htr : ↑t + 1 / ↑t = ↑y5) : Multiset.count (↑t) LC.roots ≤ 1

A real positive trace-y₅ root of Lehmer other than 1 has multiplicity one: a double root kills L' there, and the derivative–trace identity then forces q'(y₅)·t⁵(t² − 1) = 0 — refuted by the simple Salem trace root and t ∉ {0, ±1}.

theorem LehmerE10.count_muC : Multiset.count (↑mu) LC.roots = 1

theorem LehmerE10.count_nuC : Multiset.count (↑nu) LC.roots = 1

Norm products over classified root multisets.

theorem LehmerE10.norm_multiset_prod (S : Multiset ℂ) : ‖S.prod‖ = (Multiset.map (fun (z : ℂ) => ‖z‖) S).prod

theorem LehmerE10.norm_muC : ‖↑mu‖ = mu

theorem LehmerE10.norm_nuC : ‖↑nu‖ = nu

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

theorem LehmerE10.norm_eval_zero_eq_prod {H : Polynomial ℤ} (hHm : H.Monic) : ‖Polynomial.eval 0 (Polynomial.map (Int.castRingHom ℂ) H)‖ = (Multiset.map (fun (z : ℂ) => ‖z‖) (Polynomial.map (Int.castRingHom ℂ) H).roots).prod

Norm of the constant term of a monic integer polynomial = product of root norms.

THE FACTOR KILL: no proper monic factor of Lehmer exists.

theorem LehmerE10.lehmer_no_proper_factor {F : Polynomial ℤ} (hFm : F.Monic) (hd1 : 1 ≤ F.natDegree) (hd9 : F.natDegree ≤ 9) (hdvd : F ∣ lehmerPolynomial) : False

STAGE 2, ASSEMBLED (proven): a monic factor of Lehmer of degree 1–9 is impossible. F(0)·G(0) = L(0) = 1 pins both constant terms at norm one; the classified norm product is μ^a·ν^b with the pair counts a, b ∈ {0,1} summing to one across the two factors; the split cases give μ = 1 or ν = 1 (refuted), and the non-split cases leave an all-on-circle factor — killed by no_unit_circle_factor (Kronecker + the uniform-1291 cyclotomic kill).

FIRE: irreducibility over ℤ and ℚ, and the unconditional charpoly.

theorem LehmerE10.lehmer_irreducible : Irreducible lehmerPolynomial

IRREDUCIBILITY OF LEHMER'S POLYNOMIAL (proven, over ℤ).

theorem LehmerE10.lehmer_irreducible_rat : Irreducible (Polynomial.map (Int.castRingHom ℚ) lehmerPolynomial)

IRREDUCIBILITY OVER ℚ (Gauss: primitivity transfers it from ℤ).

The Coxeter element of E₁₀.

theorem LehmerE10.coxeterE10_eq : coxeterE10 = !![0, 0, 1, 0, 0, 0, 0, 0, -1, -1; 1, 0, 1, 0, 0, 0, 0, 0, -1, -1; 0, 1, 1, 0, 0, 0, 0, 0, -1, -1; 0, 0, 1, 0, 0, 0, 0, 0, -1, 0; 0, 0, 0, 1, 0, 0, 0, 0, -1, 0; 0, 0, 0, 0, 1, 0, 0, 0, -1, 0; 0, 0, 0, 0, 0, 1, 0, 0, -1, 0; 0, 0, 0, 0, 0, 0, 1, 0, -1, 0; 0, 0, 0, 0, 0, 0, 0, 1, -1, 0; 0, 0, 1, 0, 0, 0, 0, 0, 0, -1]

The Coxeter element s₀ s₁ ⋯ s₉, evaluated to an explicit matrix (kernel computation).

theorem LehmerE10.coxeter_annihilation : coxeterE10 ^ 10 + coxeterE10 ^ 9 - coxeterE10 ^ 7 - coxeterE10 ^ 6 - coxeterE10 ^ 5 - coxeterE10 ^ 4 - coxeterE10 ^ 3 + coxeterE10 + 1 = 0

Lehmer's polynomial annihilates the Coxeter element (kernel computation).

theorem LehmerE10.aeval_coxeterE10_lehmer : (Polynomial.aeval coxeterE10) lehmerPolynomial = 0

The annihilation, restated through aeval.

theorem LehmerE10.coxeter_charpoly_rat : (coxeterE10.map ⇑(Int.castRingHom ℚ)).charpoly = Polynomial.map (Int.castRingHom ℚ) lehmerPolynomial

The characteristic polynomial of the E₁₀ Coxeter element is Lehmer's polynomial, over ℚ.

theorem LehmerE10.coxeter_charpoly_lehmer : coxeterE10.charpoly = lehmerPolynomial

The characteristic polynomial of a Coxeter element of E₁₀ is Lehmer's polynomial, over ℤ (McMullen, Coxeter groups, Salem numbers and the Hilbert metric, 2002 — here as a kernel-checked identity).