PdtSalemEndgame — the two-sided assembly

The two-sided assembly of Salem's construction: for every monic integer polynomial with the Pisot pattern and P(1/alpha) ≠ 0 (the nondegeneracy — it fails exactly when 1/alpha is a root of P, i.e. when X² − rX + 1 divides P, by the reduction lemma of PdtSalemQuadUnit; there the construction itself degenerates), Salem numbers approach alpha from both sides. Assembles PdtPisotLadder (below-ladder), the above-ladder, PdtSalemCircle/PdtSalemMinus (circle counts + trichotomies through the certificates), and PdtSalemArith (certificates + reverse bridge).

Structure:

• the bridges — the cast triangle ℤ → ℝ → ℂ, the real/complex evaluation transfer, and the reflect-evaluation identity Q(α) = α^p·P(1/α) that turns the nondegeneracy hypothesis into the sign fork of the assembly;
• the quotient and the windows — the real quotient G with P = (X − C α)·G and G > 0 on [1, ∞) (nonvanishing by transfer to the complex factorization, positivity by blow-up + IVT), plus the two one-sided sign windows around α;
• the above-ladder — pisot_ladder_above, the sInf mirror of PdtPisotLadder.pisot_ladder_family: for a companion negative on a window [α, w], the family X^m·P + Q has a smallest root above α, strictly decreasing in m and tending to α;
• the finiteness discharge — along any injective ladder tail bounded in (1, B), the two integer degeneracies (τ ∈ ℤ, τ + 1/τ ∈ ℤ) fail eventually: the bad set is finite (integer branch inside a finite cast interval; trace branch inside finitely many quadratic root sets);
• the assembly — salem_two_sided: the sign of Q(α) = α^p·P(1/α) routes the PLUS family (X^m·P + Q, certificate PdtSalemArith.salem_certificate) to one side of α and the MINUS family (X^m·P − Q, certificate PdtSalemMinus.salem_certificate_minus) to the other, and both ladders deliver Salem numbers in (α − ε, α) and (α, α + ε).

salem_two_sided carries the single nondegeneracy hypothesis P(1/α) ≠ 0; the conjugation closure of inside is retained as a hypothesis although it follows from the integer coefficients.

def PDT.SalemEndgame.IsSalem (tau : ℝ) : Prop

A Salem number: a real algebraic integer tau > 1 whose other conjugates all lie in the closed unit disk, at least one ON the unit circle, with 1/tau among them.

Equations

• One or more equations did not get rendered due to their size.

Cast bridges

theorem PDT.SalemEndgame.map_int_real_complex (W : Polynomial ℤ) : Polynomial.map (algebraMap ℝ ℂ) (Polynomial.map (Int.castRingHom ℝ) W) = Polynomial.map (Int.castRingHom ℂ) W

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

theorem PDT.SalemEndgame.eval_map_ofReal (W : Polynomial ℝ) (x : ℝ) : Polynomial.eval (↑x) (Polynomial.map (algebraMap ℝ ℂ) W) = ↑(Polynomial.eval x W)

Evaluation of a mapped real polynomial at a real point, over ℂ.

theorem PDT.SalemEndgame.eval_int_transfer (W : Polynomial ℤ) (x : ℝ) : Polynomial.eval (↑x) (Polynomial.map (Int.castRingHom ℂ) W) = ↑(Polynomial.eval x (Polynomial.map (Int.castRingHom ℝ) W))

The real-to-complex evaluation transfer for integer polynomials.

theorem PDT.SalemEndgame.reflect_eval_eq (W : Polynomial ℝ) {alpha : ℝ} (ha : alpha ≠ 0) (p : ℕ) (hdeg : W.natDegree ≤ p) : Polynomial.eval alpha (Polynomial.reflect p W) = alpha ^ p * Polynomial.eval alpha⁻¹ W

The reflect-evaluation identity over ℝ: (reflect p W)(α) = α^p·W(1/α) for α ≠ 0.

The real quotient and the windows

theorem PDT.SalemEndgame.G_pos (G : Polynomial ℝ) (hGmonic : G.Monic) (inside : Multiset ℂ) (hin : ∀ r ∈ inside, ‖r‖ < 1) (hGmapC : Polynomial.map (algebraMap ℝ ℂ) G = (Multiset.map (fun (r : ℂ) => Polynomial.X - Polynomial.C r) inside).prod) (x : ℝ) : 1 ≤ x → 0 < Polynomial.eval x G

Positivity of the quotient on [1, ∞): its complex image is the product of the inside factors, so it cannot vanish at any real x ≥ 1; a monic polynomial positive at infinity and nonvanishing on the connected set [1, ∞) is positive there.

theorem PDT.SalemEndgame.window_below (W : Polynomial ℝ) {alpha : ℝ} (halpha : 1 < alpha) (hWa : 0 < Polynomial.eval alpha W) : ∃ (c : ℝ), 1 < c ∧ c < alpha ∧ ∀ (x : ℝ), c ≤ x → x ≤ alpha → 0 < Polynomial.eval x W

The window below α: positivity of W at α extends to a closed window [c, α] with 1 < c < α.

theorem PDT.SalemEndgame.window_above (W : Polynomial ℝ) (alpha : ℝ) (hWa : Polynomial.eval alpha W < 0) : ∃ (w : ℝ), alpha < w ∧ w ≤ alpha + 1 / 2 ∧ ∀ (x : ℝ), alpha ≤ x → x ≤ w → Polynomial.eval x W < 0

The window above α: negativity of W at α extends to a closed window [α, w] with α < w ≤ α + 1/2.

The above-ladder — the sInf mirror of PdtPisotLadder

theorem PDT.SalemEndgame.exists_eval_pos_above (P G Q : Polynomial ℝ) (alpha t : ℝ) (ht1 : 1 < t) (hat : alpha < t) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) : ∃ (M0 : ℕ), ∀ (m : ℕ), M0 ≤ m → 0 < Polynomial.eval t (Polynomial.X ^ m * P + Q)

At any point t > α (hence t > 1) the family is eventually positive in m: t^m·P(t) blows up past the fixed value Q(t).

def PDT.SalemEndgame.rootSetA (P Q : Polynomial ℝ) (alpha w : ℝ) (m : ℕ) : Set ℝ

The roots of R_m in [α, w].

Equations

• PDT.SalemEndgame.rootSetA P Q alpha w m = {x : ℝ | x ∈ Set.Icc alpha w ∧ Polynomial.eval x (Polynomial.X ^ m * P + Q) = 0}

noncomputable def PDT.SalemEndgame.muA (P Q : Polynomial ℝ) (alpha w : ℝ) (m : ℕ) : ℝ

The canonical root above: the smallest root of R_m in [α, w].

Equations

• PDT.SalemEndgame.muA P Q alpha w m = sInf (PDT.SalemEndgame.rootSetA P Q alpha w m)

theorem PDT.SalemEndgame.rootSetA_isCompact (P Q : Polynomial ℝ) (alpha w : ℝ) (m : ℕ) : IsCompact (rootSetA P Q alpha w m)

theorem PDT.SalemEndgame.rootSetA_nonempty (P Q : Polynomial ℝ) (alpha w : ℝ) (haw : alpha ≤ w) (m : ℕ) (hneg : Polynomial.eval alpha (Polynomial.X ^ m * P + Q) < 0) (hpos : 0 < Polynomial.eval w (Polynomial.X ^ m * P + Q)) : (rootSetA P Q alpha w m).Nonempty

theorem PDT.SalemEndgame.muA_mem (P Q : Polynomial ℝ) (alpha w : ℝ) (m : ℕ) (hne : (rootSetA P Q alpha w m).Nonempty) : muA P Q alpha w m ∈ rootSetA P Q alpha w m

theorem PDT.SalemEndgame.muA_gt_alpha (P Q : Polynomial ℝ) (alpha w : ℝ) (m : ℕ) (hne : (rootSetA P Q alpha w m).Nonempty) (hneg : Polynomial.eval alpha (Polynomial.X ^ m * P + Q) < 0) : alpha < muA P Q alpha w m

theorem PDT.SalemEndgame.muA_lt_w (P Q : Polynomial ℝ) (alpha w : ℝ) (m : ℕ) (hne : (rootSetA P Q alpha w m).Nonempty) (hpos : 0 < Polynomial.eval w (Polynomial.X ^ m * P + Q)) : muA P Q alpha w m < w

theorem PDT.SalemEndgame.muA_min (P Q : Polynomial ℝ) (alpha w : ℝ) (m : ℕ) (hne : (rootSetA P Q alpha w m).Nonempty) {y : ℝ} (h1 : alpha < y) (h2 : y < muA P Q alpha w m) : Polynomial.eval y (Polynomial.X ^ m * P + Q) ≠ 0

Minimality: no roots of R_m strictly between α and muA m.

theorem PDT.SalemEndgame.muA_strictAnti (P G Q : Polynomial ℝ) (alpha w : ℝ) (halpha : 1 < alpha) (haw : alpha < w) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hwin : ∀ (x : ℝ), alpha ≤ x → x ≤ w → Polynomial.eval x Q < 0) (m : ℕ) (hpos : 0 < Polynomial.eval w (Polynomial.X ^ m * P + Q)) : muA P Q alpha w (m + 1) < muA P Q alpha w m

The heart of the strict decrease: at the root muA m, the next member is positive — R_{m+1}(y) = (1 − y)·Q(y) > 0 when y > 1 and Q(y) < 0 — so the IVT plants a smaller root of R_{m+1}.

theorem PDT.SalemEndgame.muA_tendsto (P G Q : Polynomial ℝ) (alpha w : ℝ) (halpha : 1 < alpha) (haw : alpha < w) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hwin : ∀ (x : ℝ), alpha ≤ x → x ≤ w → Polynomial.eval x Q < 0) (M0 : ℕ) (hM0 : ∀ (m : ℕ), M0 ≤ m → 0 < Polynomial.eval w (Polynomial.X ^ m * P + Q)) : Filter.Tendsto (fun (m : ℕ) => muA P Q alpha w m) Filter.atTop (nhds alpha)

The canonical roots above tend to α.

theorem PDT.SalemEndgame.pisot_ladder_above (P G Q : Polynomial ℝ) (alpha : ℝ) (halpha : 1 < alpha) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hQa : Polynomial.eval alpha Q < 0) : ∃ (M : ℕ) (mu : ℕ → ℝ), (∀ (m : ℕ), M ≤ m → (alpha < mu m ∧ mu m < alpha + 1) ∧ Polynomial.eval (mu m) (Polynomial.X ^ m * P + Q) = 0 ∧ (∀ (y : ℝ), alpha < y → y < mu m → Polynomial.eval y (Polynomial.X ^ m * P + Q) ≠ 0) ∧ mu (m + 1) < mu m) ∧ Filter.Tendsto mu Filter.atTop (nhds alpha)

The above-ladder. For P = (X − C α)·G with α > 1 and G > 0 on [1, ∞), and a companion Q with Q(α) < 0: for m large the family R_m = X^m·P + Q has a canonical root mu m ∈ (α, α + 1), the smallest root above α; the sequence is strictly decreasing; and it tends to α. The sInf mirror of PDT.PisotLadder.pisot_ladder_family.

The finiteness discharge

def PDT.SalemEndgame.badSet (B : ℝ) : Set ℝ

The degeneracy set: points of (1, B) that are integers or have integer trace x + 1/x.

Equations

• PDT.SalemEndgame.badSet B = {x : ℝ | 1 < x ∧ x < B ∧ ((∃ (n : ℤ), x = ↑n) ∨ ∃ (n : ℤ), x + x⁻¹ = ↑n)}

theorem PDT.SalemEndgame.mem_badSet {B x : ℝ} : x ∈ badSet B ↔ 1 < x ∧ x < B ∧ ((∃ (n : ℤ), x = ↑n) ∨ ∃ (n : ℤ), x + x⁻¹ = ↑n)

theorem PDT.SalemEndgame.badSet_finite (B : ℝ) : (badSet B).Finite

The degeneracy set is finite: the integer branch lies in the cast of [1, ⌈B⌉]; the trace branch lies in the (finite) root sets of the quadratics X² − n·X + 1 for the finitely many integers n ∈ [2, ⌈B+1⌉].

theorem PDT.SalemEndgame.injOn_of_strict_mono_step (lam : ℕ → ℝ) (M : ℕ) (hstep : ∀ (m : ℕ), M ≤ m → lam m < lam (m + 1)) : Set.InjOn lam (Set.Ici M)

Injectivity on a tail from a strictly increasing step.

theorem PDT.SalemEndgame.injOn_of_strict_anti_step (mu : ℕ → ℝ) (M : ℕ) (hstep : ∀ (m : ℕ), M ≤ m → mu (m + 1) < mu m) : Set.InjOn mu (Set.Ici M)

Injectivity on a tail from a strictly decreasing step.

theorem PDT.SalemEndgame.eventually_nondegenerate (lam : ℕ → ℝ) (M : ℕ) (B : ℝ) (hinj : Set.InjOn lam (Set.Ici M)) (hbounds : ∀ (m : ℕ), M ≤ m → 1 < lam m ∧ lam m < B) : ∃ (M' : ℕ), M ≤ M' ∧ ∀ (m : ℕ), M' ≤ m → (∀ (n : ℤ), lam m ≠ ↑n) ∧ ∀ (n : ℤ), lam m + (lam m)⁻¹ ≠ ↑n

The finiteness discharge. Along any injective tail of a ladder bounded in (1, B), the two integer degeneracies eventually fail: past some index, lam m is not an integer and lam m + (lam m)⁻¹ is not an integer.

The certificates and the assembly

theorem PDT.SalemEndgame.isSalem_of_plus_root (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) (m : ℕ) (hm : 2 ≤ m) (tau : ℝ) (htau : 1 < tau) (hroot : Polynomial.eval tau (Polynomial.X ^ m * Polynomial.map (Int.castRingHom ℝ) Pz + Polynomial.map (Int.castRingHom ℝ) Pz.reverse) = 0) (hτZ : ∀ (n : ℤ), tau ≠ ↑n) (hτtr : ∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) : IsSalem tau

The PLUS-family certificate, packaged: a nondegenerate root tau > 1 of X^m·Pz + Pz.reverse (over ℝ) is a Salem number.

theorem PDT.SalemEndgame.isSalem_of_minus_root (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) (m : ℕ) (hm : 2 ≤ m) (tau : ℝ) (htau : 1 < tau) (hroot : Polynomial.eval tau (Polynomial.X ^ m * Polynomial.map (Int.castRingHom ℝ) Pz - Polynomial.map (Int.castRingHom ℝ) Pz.reverse) = 0) (hτZ : ∀ (n : ℤ), tau ≠ ↑n) (hτtr : ∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) : IsSalem tau

The MINUS-family certificate, packaged: a nondegenerate root tau > 1 of X^m·Pz − Pz.reverse (over ℝ) is a Salem number.

theorem PDT.SalemEndgame.exists_salem_below_root (alpha : ℝ) (halpha : 1 < alpha) (Pr G Qc : Polynomial ℝ) (hfacR : Pr = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hQca : 0 < Polynomial.eval alpha Qc) (cert : ∀ (m : ℕ), 2 ≤ m → ∀ (tau : ℝ), 1 < tau → Polynomial.eval tau (Polynomial.X ^ m * Pr + Qc) = 0 → (∀ (n : ℤ), tau ≠ ↑n) → (∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) → IsSalem tau) (eps : ℝ) (heps : 0 < eps) : ∃ (m : ℕ), 2 ≤ m ∧ ∃ (tau : ℝ), IsSalem tau ∧ Polynomial.eval tau (Polynomial.X ^ m * Pr + Qc) = 0 ∧ alpha - eps < tau ∧ tau < alpha

PdtSalemEndgame.exists_salem_below with the index m ≥ 2 and the root equation (X^m·Pr + Qc)(τ) = 0 kept in the conclusion.

theorem PDT.SalemEndgame.exists_salem_below (alpha : ℝ) (halpha : 1 < alpha) (Pr G Qc : Polynomial ℝ) (hfacR : Pr = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hQca : 0 < Polynomial.eval alpha Qc) (cert : ∀ (m : ℕ), 2 ≤ m → ∀ (tau : ℝ), 1 < tau → Polynomial.eval tau (Polynomial.X ^ m * Pr + Qc) = 0 → (∀ (n : ℤ), tau ≠ ↑n) → (∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) → IsSalem tau) (eps : ℝ) (heps : 0 < eps) : ∃ (tau : ℝ), IsSalem tau ∧ alpha - eps < tau ∧ tau < alpha

The BELOW half, abstract in the companion: the below-ladder plus the finiteness discharge plus a certificate deliver a Salem number in (α − ε, α).

theorem PDT.SalemEndgame.exists_salem_above_root (alpha : ℝ) (halpha : 1 < alpha) (Pr G Qc : Polynomial ℝ) (hfacR : Pr = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hQca : Polynomial.eval alpha Qc < 0) (cert : ∀ (m : ℕ), 2 ≤ m → ∀ (tau : ℝ), 1 < tau → Polynomial.eval tau (Polynomial.X ^ m * Pr + Qc) = 0 → (∀ (n : ℤ), tau ≠ ↑n) → (∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) → IsSalem tau) (eps : ℝ) (heps : 0 < eps) : ∃ (m : ℕ), 2 ≤ m ∧ ∃ (tau : ℝ), IsSalem tau ∧ Polynomial.eval tau (Polynomial.X ^ m * Pr + Qc) = 0 ∧ alpha < tau ∧ tau < alpha + eps

PdtSalemEndgame.exists_salem_above with the index m ≥ 2 and the root equation (X^m·Pr + Qc)(τ) = 0 kept in the conclusion.

theorem PDT.SalemEndgame.exists_salem_above (alpha : ℝ) (halpha : 1 < alpha) (Pr G Qc : Polynomial ℝ) (hfacR : Pr = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hQca : Polynomial.eval alpha Qc < 0) (cert : ∀ (m : ℕ), 2 ≤ m → ∀ (tau : ℝ), 1 < tau → Polynomial.eval tau (Polynomial.X ^ m * Pr + Qc) = 0 → (∀ (n : ℤ), tau ≠ ↑n) → (∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) → IsSalem tau) (eps : ℝ) (heps : 0 < eps) : ∃ (tau : ℝ), IsSalem tau ∧ alpha < tau ∧ tau < alpha + eps

The ABOVE half, abstract in the companion: the above-ladder plus the finiteness discharge plus a certificate deliver a Salem number in (α, α + ε).

theorem PDT.SalemEndgame.eval_signed_family (Pz : Polynomial ℤ) (e : ℤ) (m : ℕ) (tau : ℝ) : Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Polynomial.X ^ m * Pz + Polynomial.C e * Pz.reverse)) = tau ^ m * Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) Pz) + ↑e * Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) Pz.reverse)

Evaluation of the mapped signed family X^m·Pz + e·Pz.reverse.

theorem PDT.SalemEndgame.eval_signed_family_sub (Pz : Polynomial ℤ) (e : ℤ) (m : ℕ) (tau : ℝ) : Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Polynomial.X ^ m * Pz - Polynomial.C e * Pz.reverse)) = tau ^ m * Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) Pz) - ↑e * Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) Pz.reverse)

Evaluation of the mapped signed family X^m·Pz − e·Pz.reverse.

theorem PDT.SalemEndgame.salem_construction_two_sided (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) (hnondeg : Polynomial.eval alpha⁻¹ (Polynomial.map (Int.castRingHom ℝ) Pz) ≠ 0) (eps : ℝ) (heps : 0 < eps) : ∃ (e : ℤ), (e = 1 ∨ e = -1) ∧ 0 < ↑e * Polynomial.eval alpha⁻¹ (Polynomial.map (Int.castRingHom ℝ) Pz) ∧ (∃ (m : ℕ), 2 ≤ m ∧ ∃ (tau : ℝ), IsSalem tau ∧ Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Polynomial.X ^ m * Pz + Polynomial.C e * Pz.reverse)) = 0 ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (m : ℕ), 2 ≤ m ∧ ∃ (tau : ℝ), IsSalem tau ∧ Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Polynomial.X ^ m * Pz - Polynomial.C e * Pz.reverse)) = 0 ∧ alpha < tau ∧ tau < alpha + eps

The main construction with its family root exposed. Under the hypotheses of PdtSalemEndgame.salem_two_sided — the Pisot pattern and P(1/α) ≠ 0 — there is a sign e = ±1, the sign of P(1/α), such that for every ε > 0 some member X^m·Pz + e·Pz.reverse (m ≥ 2) has a Salem root in (α − ε, α) and some member X^m·Pz − e·Pz.reverse (m ≥ 2) has a Salem root in (α, α + ε). The common assembly retains the index and root equation; salem_two_sided is its projection. The sign of Q(α) = α^p·P(1/α) routes the plus family below and the minus family above when P(1/α) > 0, and the reverse when P(1/α) < 0.

theorem PDT.SalemEndgame.salem_two_sided (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) (hnondeg : Polynomial.eval alpha⁻¹ (Polynomial.map (Int.castRingHom ℝ) Pz) ≠ 0) (eps : ℝ) (heps : 0 < eps) : (∃ (tau : ℝ), IsSalem tau ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (tau : ℝ), IsSalem tau ∧ alpha < tau ∧ tau < alpha + eps

The two-sided assembly. Every Pisot-pattern polynomial — monic over ℤ, complex factorization (X − C α)·∏ (X − C r) with α > 1 and the conjugation-closed inside roots strictly inside the unit circle — with the nondegeneracy P(1/α) ≠ 0 has Salem numbers approaching α from BOTH sides: for every ε > 0 there are Salem numbers in (α − ε, α) and in (α, α + ε).

The sign of Q(α) = α^p·P(1/α) (the reverse polynomial at α) routes the plus family X^m·P + Q to one side and the minus family X^m·P − Q to the other; each ladder's roots are nondegenerate eventually (the finiteness discharge), and the certificates of PdtSalemArith and PdtSalemMinus promote them to Salem numbers.