basic facts about Lehmer's polynomial L, and Kronecker's theorem.

Contents: • degree/monicity of L and the evaluation witnesses L(1) = −1, L(−1) = 1, L(2) = 1291 (prime); • kronecker_roots — Kronecker's theorem (1857) in root form: every complex root of a monic integer polynomial, all of whose complex roots lie on the unit circle, is a root of unity. Proved from Mathlib's NumberField.Embeddings.pow_eq_one_of_norm_eq_one applied inside the number field ℚ⟮z⟯. • totient_le_of_lehmer_root — a primitive k-th root of unity that is a root of L has φ(k) ≤ 10 (cyclotomic = minimal polynomial + degree bound). Axiom footprint: propext, Classical.choice, Quot.sound only.

theorem LehmerE10.lehmerPolynomial_natDegree : lehmerPolynomial.natDegree = 10

theorem LehmerE10.lehmerPolynomial_monic : lehmerPolynomial.Monic

theorem LehmerE10.lehmerPolynomial_ne_zero : lehmerPolynomial ≠ 0

The eval-witness integers (the kill table's three points).

theorem LehmerE10.lehmer_eval_one : Polynomial.eval 1 lehmerPolynomial = -1

theorem LehmerE10.lehmer_eval_neg_one : Polynomial.eval (-1) lehmerPolynomial = 1

theorem LehmerE10.lehmer_eval_two : Polynomial.eval 2 lehmerPolynomial = 1291

theorem LehmerE10.witness_1291_prime : Nat.Prime 1291

1291 is prime: the x = 2 witness kills every remaining non-prime-power modulus (Φ₁₂(2)=13, Φ₁₅(2)=151, Φ₂₀(2)=205, Φ₂₄(2)=241, Φ₃₀(2)=331 — none divide 1291).

Kronecker's theorem: roots of unit-circle monic ℤ-polynomials are roots of unity.

theorem LehmerE10.kronecker_roots {p : Polynomial ℤ} (hm : p.Monic) (h1 : ∀ w ∈ (Polynomial.map (Int.castRingHom ℂ) p).roots, ‖w‖ = 1) {z : ℂ} (hz : z ∈ (Polynomial.map (Int.castRingHom ℂ) p).roots) : ∃ (n : ℕ), 0 < n ∧ z ^ n = 1

Kronecker's theorem, root form: every complex root of a monic integer polynomial, all of whose complex roots lie on the unit circle, is a root of unity. (The conclusion is stated root-wise: the p ∣ xⁿ − 1 form fails for non-squarefree p.)

The order bound: root-of-unity roots of L live in the eligible census.

theorem LehmerE10.totient_le_of_lehmer_root {z : ℂ} {k : ℕ} (hk : 0 < k) (hprim : IsPrimitiveRoot z k) (hroot : (Polynomial.aeval z) (Polynomial.map (Int.castRingHom ℚ) lehmerPolynomial) = 0) : k.totient ≤ 10

A primitive k-th root of unity that is a root of lehmerPolynomial (over ℚ) has φ(k) ≤ 10: cyclotomic k = minpoly, and the minpoly divides the degree-10 image.

theorem LehmerE10.eligible_totient_census : List.map (fun (x : ℕ) => x + 1) (List.filter (fun (n : ℕ) => decide ((n + 1).totient ≤ 10)) (List.range 66)) = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 18, 20, 22, 24, 30]

The moduli k ≤ 66 with φ(k) ≤ 10 — the only possible orders of root-of-unity roots of a degree-10 polynomial.