no factor of Lehmer's polynomial lives on the unit circle.

Contents: • no_unit_circle_factor — a monic ℤ-factor of L of positive degree cannot have all its complex roots on the unit circle: such a factor would carry a root of unity (kronecker_roots), whose cyclotomic minimal polynomial would descend to a cyclotomic ℤ-divisor of L (Gauss's lemma), refuted by no_cyclotomic_divisor. So every proper factor must touch the off-circle Salem pair. • norm_eq_one_of_trace_in_ball — the on-circle half of the root dichotomy: z + 1/z real in (−2, 2) forces ‖z‖ = 1 (real z is excluded by AM–GM; the conjugate is then the reciprocal). • two_le_self_add_inv — the AM–GM inequality used above. Axiom footprint: propext, Classical.choice, Quot.sound only.

AM–GM face: a positive real plus its inverse is at least 2.

theorem LehmerE10.two_le_self_add_inv {t : ℝ} (ht : 0 < t) : 2 ≤ t + 1 / t

The on-circle half of the root dichotomy.

theorem LehmerE10.norm_eq_one_of_trace_in_ball {z : ℂ} {y : ℝ} (hz : z ≠ 0) (htr : z + 1 / z = ↑y) (hy : -2 < y) (hy' : y < 2) : ‖z‖ = 1

If z + 1/z is a real number strictly inside (−2, 2), then ‖z‖ = 1: z cannot be real (AM–GM), and the conjugate — a root of the same real quadratic — must then be the reciprocal, giving ‖z‖² = z·conj z = 1.

THE CIRCLE IS CLOSED: no all-on-circle factor.

theorem LehmerE10.no_unit_circle_factor {F : Polynomial ℤ} (hFm : F.Monic) (hdeg : 0 < F.natDegree) (hFdvd : F ∣ lehmerPolynomial) (hcirc : ∀ z ∈ (Polynomial.map (Int.castRingHom ℂ) F).roots, ‖z‖ = 1) : False

NO UNIT-CIRCLE FACTOR (proven): a monic factor of Lehmer with positive degree and all complex roots on the unit circle is impossible — its root of unity would give a cyclotomic ℤ-divisor of Lehmer, refuted by no_cyclotomic_divisor.