no cyclotomic polynomial divides Lehmer's polynomial, and the

characteristic-polynomial identity conditional on irreducibility. no_cyclotomic_divisor: no cyclotomic polynomial divides L. One uniform argument, using that 2 is a primitive root mod 1291 = L(2) (order 1290): Φ_k ∣ L ⟹ Φ_k(2) ∣ L(2) = 1291 (prime), and |Φ_k(2)| ≥ 2 (Mathlib's sub_one_lt_natAbs_cyclotomic_eval) ⟹ |Φ_k(2)| = 1291 ⟹ 1291 ∣ 2^k − 1 ⟹ 1290 = ord₁₂₉₁(2) ∣ k ⟹ 336 = φ(1290) ∣ φ(k) (totient_dvd_of_dvd) — but Φ_k ∣ L forces φ(k) = deg Φ_k ≤ 10. Contradiction. (k = 1: L(1) = −1.) charpoly_eq_lehmer_of_irreducible: if L is irreducible over ℚ, then any 10×10 integer matrix annihilated by L has characteristic polynomial L (over ℚ), via Cayley–Hamilton + minimal-polynomial divisibility + degree count. Axiom footprint: propext, Classical.choice, Quot.sound only.

The primitive-root certificate: ord₁₂₉₁(2) = 1290.

instance LehmerE10.instFactPrimeOfNatNat_leanPool : Fact (Nat.Prime 1291)

theorem LehmerE10.orderOf_two_mod_1291 : orderOf 2 = 1290

2 has order exactly 1290 = 2·3·5·43 in (ℤ/1291)ˣ — certified by Fermat plus the four maximal-divisor refusals (kernel bignum arithmetic).

LEG (a): the uniform cyclotomic kill.

theorem LehmerE10.no_cyclotomic_divisor {k : ℕ} (hk : 1 ≤ k) : ¬Polynomial.cyclotomic k ℤ ∣ lehmerPolynomial

NO CYCLOTOMIC DIVIDES LEHMER (proven) — the uniform 1291 argument.

The charpoly identity, conditional on irreducibility.

theorem LehmerE10.charpoly_eq_lehmer_of_irreducible {M : Matrix (Fin 10) (Fin 10) ℤ} (hann : (Polynomial.aeval M) lehmerPolynomial = 0) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) lehmerPolynomial)) : (M.map ⇑(Int.castRingHom ℚ)).charpoly = Polynomial.map (Int.castRingHom ℚ) lehmerPolynomial

If Lehmer's polynomial is irreducible over ℚ, then any 10×10 integer matrix it annihilates has characteristic polynomial L over ℚ. (Cayley–Hamilton gives minpoly ∣ charpoly; annihilation gives minpoly ∣ L; irreducibility forces minpoly = L; degree 10 monic on both sides closes it.)