PdtSalemArith — the arithmetic Salem-ness certificate

The arithmetic certificate for Salem's construction: a real root tau > 1 of the integer family, excluded from the two integer degeneracies, is a Salem number; the exclusions are discharged for the ladder sequence in the assembly (PdtSalemEndgame); Kronecker's theorem is not needed (the Gauss step covers all degenerate cases).

Setting: Pz : Polynomial ℤ monic whose complex image is the PdtSalemCircle product P alpha inside (one root alpha > 1, the rest strictly inside the unit circle, conjugation-closed), Qz : Polynomial ℤ whose complex image is the mirrored product Q alpha inside, and the family Rz = X^m·Pz + Qz. If tau > 1 is a real root of Rz with tau ∉ ℤ and tau + 1/tau ∉ ℤ (the two degeneracies), then (salem_certificate):

• tau is an algebraic integer (Rz is monic and kills it);
• every complex root of minpoly ℚ tau other than tau lies in the CLOSED unit disk (the trichotomy of PdtSalemCircle through the divisibility minpoly ∣ Rz over ℚ);
• some root lies ON the unit circle — otherwise the minimal polynomial has degree ≤ 2 and the Gauss step (minpoly ℚ = minpoly ℤ mapped, ℤ integrally closed) forces tau ∈ ℤ (degree 1) or tau + 1/tau ∈ ℤ (degree 2, Vieta on the X-coefficient);
• 1/tau is a root of minpoly ℚ tau — otherwise all conjugates except tau are unimodular and the constant term has absolute value tau ∉ ℤ (Vieta on the constant term, plus the Gauss step again).

Together: tau is a Salem number. Qz is data with only its complex image constrained, so the reverse-polynomial identification is decoupled (reverse_bridge below discharges it for the actual companion Qz = Pz.reverse).

Small helpers

theorem PDT.SalemArith.norm_multiset_prod_eq_one (s : Multiset ℂ) : (∀ w ∈ s, ‖w‖ = 1) → ‖s.prod‖ = 1

A multiset of unimodular numbers has unimodular product.

theorem PDT.SalemArith.castQC_triangle : (algebraMap ℚ ℂ).comp (Int.castRingHom ℚ) = Int.castRingHom ℂ

The ℤ-cast triangle through ℚ: ring homs out of ℤ are unique.

theorem PDT.SalemArith.aeval_eq_eval_map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Polynomial R) (x : S) : (Polynomial.aeval x) p = Polynomial.eval x (Polynomial.map (algebraMap R S) p)

aeval as evaluation of the mapped polynomial.

theorem PDT.SalemArith.aeval_ofReal {R : Type u_1} [CommRing R] [Algebra R ℝ] [Algebra R ℂ] [IsScalarTower R ℝ ℂ] (p : Polynomial R) (x : ℝ) : (Polynomial.aeval ↑x) p = ↑((Polynomial.aeval x) p)

Transport of scalar aeval along ℝ → ℂ.

The family is monic over ℤ, and its complex image is R

theorem PDT.SalemArith.Pz_natDegree (Pz : Polynomial ℤ) (hmonic : Pz.Monic) (alpha : ℝ) (inside : Multiset ℂ) (hfacC : Polynomial.map (Int.castRingHom ℂ) Pz = SalemCircle.P alpha inside) : Pz.natDegree = inside.card + 1

Degree transfer from the complex factorization: Pz has degree inside.card + 1.

theorem PDT.SalemArith.Qz_natDegree_le (alpha : ℝ) (inside : Multiset ℂ) (Qz : Polynomial ℤ) (hQmap : Polynomial.map (Int.castRingHom ℂ) Qz = SalemCircle.Q alpha inside) : Qz.natDegree ≤ inside.card + 1

Degree transfer for the companion: Qz has degree at most inside.card + 1.

theorem PDT.SalemArith.family_monic (Pz : Polynomial ℤ) (hmonic : Pz.Monic) (alpha : ℝ) (inside : Multiset ℂ) (hfacC : Polynomial.map (Int.castRingHom ℂ) Pz = SalemCircle.P alpha inside) (Qz : Polynomial ℤ) (hQmap : Polynomial.map (Int.castRingHom ℂ) Qz = SalemCircle.Q alpha inside) (m : ℕ) (hm : 1 ≤ m) : (Polynomial.X ^ m * Pz + Qz).Monic

The integer family X^m·Pz + Qz is monic (for m ≥ 1).

theorem PDT.SalemArith.family_map_C (Pz : Polynomial ℤ) (alpha : ℝ) (inside : Multiset ℂ) (hfacC : Polynomial.map (Int.castRingHom ℂ) Pz = SalemCircle.P alpha inside) (Qz : Polynomial ℤ) (hQmap : Polynomial.map (Int.castRingHom ℂ) Qz = SalemCircle.Q alpha inside) (m : ℕ) : Polynomial.map (Int.castRingHom ℂ) (Polynomial.X ^ m * Pz + Qz) = SalemCircle.R alpha inside m

The complex image of the integer family is the family R of PdtSalemCircle.

The main theorem: the arithmetic Salem-ness certificate

theorem PDT.SalemArith.salem_certificate_of_root_trichotomy (Rz : Polynomial ℤ) (hRzMonic : Rz.Monic) (tau : ℝ) (htau : 1 < tau) (haevalR : (Polynomial.aeval tau) Rz = 0) (htri : ∀ (z : ℂ), Polynomial.eval z (Polynomial.map (Int.castRingHom ℂ) Rz) = 0 → ‖z‖ = 1 ∨ z = ↑tau ∨ z = (↑tau)⁻¹) (hτZ : ∀ (n : ℤ), tau ≠ ↑n) (hτtr : ∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) : IsIntegral ℤ tau ∧ (∀ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 → z ≠ ↑tau → ‖z‖ ≤ 1) ∧ (∃ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 ∧ ‖z‖ = 1) ∧ (Polynomial.aeval (↑tau)⁻¹) (minpoly ℚ tau) = 0

A monic integral polynomial whose roots lie on the unit circle or at tau and tau⁻¹ certifies Salem-ness once the two integral degeneracies are excluded.

theorem PDT.SalemArith.salem_certificate (Pz : Polynomial ℤ) (hmonic : Pz.Monic) (alpha : ℝ) (halpha : 1 < alpha) (inside : Multiset ℂ) (hin : ∀ r ∈ inside, ‖r‖ < 1) (hconj : Multiset.map (⇑(starRingEnd ℂ)) inside = inside) (hfacC : Polynomial.map (Int.castRingHom ℂ) Pz = SalemCircle.P alpha inside) (Qz : Polynomial ℤ) (hQmap : Polynomial.map (Int.castRingHom ℂ) Qz = SalemCircle.Q alpha inside) (m : ℕ) (hm : 1 ≤ m) (hmp : 3 ≤ m + (inside.card + 1)) (tau : ℝ) (htau : 1 < tau) (hroot : Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Polynomial.X ^ m * Pz + Qz)) = 0) (hτZ : ∀ (n : ℤ), tau ≠ ↑n) (hτtr : ∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) : IsIntegral ℤ tau ∧ (∀ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 → z ≠ ↑tau → ‖z‖ ≤ 1) ∧ (∃ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 ∧ ‖z‖ = 1) ∧ (Polynomial.aeval (↑tau)⁻¹) (minpoly ℚ tau) = 0

The arithmetic Salem-ness certificate. A real root tau > 1 of the integer family X^m·Pz + Qz — whose complex image is the PdtSalemCircle family — is a Salem number, provided tau avoids the two integer degeneracies tau ∈ ℤ and tau + 1/tau ∈ ℤ: it is an algebraic integer, its conjugates lie in the closed unit disk, at least one lies ON the circle, and 1/tau is among them. All degenerate exclusions run through the Gauss step (minpoly ℚ tau is the mapped minpoly ℤ tau, since ℤ is integrally closed).

The reverse bridge — the companion IS the reverse

theorem PDT.SalemArith.reflect_P_eq_Q (alpha : ℝ) (inside : Multiset ℂ) : Polynomial.reflect (inside.card + 1) (SalemCircle.P alpha inside) = SalemCircle.Q alpha inside

The reflect of the product P at its degree is the mirrored product Q: they agree at every z ≠ 0 (mirror_P), and a cofinite agreement set forces polynomial equality.

theorem PDT.SalemArith.reverse_bridge (Pz : Polynomial ℤ) (hmonic : Pz.Monic) (alpha : ℝ) (inside : Multiset ℂ) (hfacC : Polynomial.map (Int.castRingHom ℂ) Pz = SalemCircle.P alpha inside) : Polynomial.map (Int.castRingHom ℂ) Pz.reverse = SalemCircle.Q alpha inside

The reverse bridge: the actual Salem companion — the reverse polynomial of Pz — has complex image the mirrored product Q, discharging the hypothesis hQmap of salem_certificate for Qz = Pz.reverse.