locating the roots of Lehmer's polynomial via its trace quintic.

L is reciprocal, so with y = x + 1/x it factors through a degree-5 polynomial: L(x) = x⁵ · q(x + 1/x), q(y) = y⁵ + y⁴ − 5y³ − 5y² + 4y + 3, and a root of L lies on |z| = 1 iff its trace y = x + 1/x lies in [−2, 2] (x = e^{iθ}, y = 2 cos θ). Salem's picture — 8 roots on the unit circle, one reciprocal pair {λ, 1/λ} off it — therefore reduces to "q has 4 real roots in (−2, 2) and one root in (2, 21/10)": five intermediate-value sign checks, carried out here. Axiom footprint: propext, Classical.choice, Quot.sound only.

noncomputable def LehmerE10.lehmerC (z : ℂ) : ℂ

Lehmer's polynomial as a function on ℂ.

Equations

• LehmerE10.lehmerC z = z ^ 10 + z ^ 9 - z ^ 7 - z ^ 6 - z ^ 5 - z ^ 4 - z ^ 3 + z + 1

def LehmerE10.traceQ (y : ℝ) : ℝ

The degree-5 TRACE polynomial over ℝ (for root location).

Equations

• LehmerE10.traceQ y = y ^ 5 + y ^ 4 - 5 * y ^ 3 - 5 * y ^ 2 + 4 * y + 3

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

Trace polynomial over ℂ.

Equations

• LehmerE10.traceQC y = y ^ 5 + y ^ 4 - 5 * y ^ 3 - 5 * y ^ 2 + 4 * y + 3

@[simp]

theorem LehmerE10.traceQC_ofReal (y : ℝ) : traceQC ↑y = ↑(traceQ y)

theorem LehmerE10.lehmer_trace_reduction (z : ℂ) (hz : z ≠ 0) : lehmerC z = z ^ 5 * traceQC (z + 1 / z)

THE RECIPROCAL → TRACE REDUCTION: L(x) = x⁵ · q(x + 1/x), PROVEN.

The five real roots of the trace polynomial (IVT).

theorem LehmerE10.traceQ_root_1 : ∃ y ∈ Set.Ioo (-2) (-3 / 2), traceQ y = 0

A trace root in (−2, −3/2) (endpoints: q(−2)=−1 < 0 < 3/32 = q(−3/2)).

theorem LehmerE10.traceQ_root_2 : ∃ y ∈ Set.Ioo (-3 / 2) (-1), traceQ y = 0

A trace root in (−3/2, −1).

theorem LehmerE10.traceQ_root_3 : ∃ y ∈ Set.Ioo (-1) 0, traceQ y = 0

A trace root in (−1, 0).

theorem LehmerE10.traceQ_root_4 : ∃ y ∈ Set.Ioo 0 1, traceQ y = 0

A trace root in (0, 1).

theorem LehmerE10.traceQ_root_salem : ∃ y ∈ Set.Ioo 2 (21 / 10), traceQ y = 0

The Salem trace root in (2, 21/10) — y_L = λ_L + 1/λ_L > 2, the off-circle reciprocal pair.

On-circle Lehmer roots from trace roots in (−2,2).

theorem LehmerE10.lehmer_root_on_circle (y₀ : ℝ) (h0 : traceQ y₀ = 0) (hmem : y₀ ∈ Set.Ioo (-2) 2) : ∃ (z : ℂ), ‖z‖ = 1 ∧ lehmerC z = 0

Each trace root in (−2,2) gives a root of L on |z| = 1: for y₀ ∈ (−2,2) with q(y₀) = 0, the explicit z = (y₀ + i√(4−y₀²))/2 has ‖z‖ = 1 and z + 1/z = y₀, so by the trace reduction L(z) = z⁵ · q(y₀) = 0.

theorem LehmerE10.elliptic_root_on_circle : ∃ (z : ℂ), ‖z‖ = 1 ∧ lehmerC z = 0

L has a root on the unit circle (combining the trace root in (−1,0) with lehmer_root_on_circle).