SalemPisot — Salem's theorem for Pisot numbers, and the two

constructions with their family roots exposed

The bridge from a Pisot number to the Pisot-pattern data of its minimal polynomial; Salem's theorem stated for Pisot numbers (every Pisot number is a limit of Salem numbers from both sides); and the two constructions of the proof modules with the index m and the family polynomial kept in the conclusion.

A Pisot number is a real algebraic integer α > 1 all of whose other complex conjugates lie strictly inside the unit circle; it is spelled here as 1 < α, IsIntegral ℤ α, and ∀ z ∈ (minpoly ℚ α).aroots ℂ, z ≠ α → ‖z‖ < 1.

• pattern_of_simple_root: a monic integer polynomial with a simple complex root α (root multiplicity exactly one) whose other complex roots lie strictly inside the unit circle carries the Pisot-pattern data — the multiset inside of its other roots is interior and conjugation-closed, and the complex image factors as (X − α)·∏ (X − z), the product over inside. The conjugation closure comes from the integer coefficients (Splits.roots_map against the cast triangle), the factorization from Splits.eq_prod_roots_of_monic and Multiset.cons_erase.
• pattern_of_pisot: the minimal polynomial over ℤ of a Pisot number carries the pattern data. Ingredients: the Gauss step minpoly ℚ α = (minpoly ℤ α).map ℚ (ℤ is integrally closed), the separability of the irreducible minpoly ℚ α in characteristic zero (so α is a simple root of its complex image), and the identification of the complex roots with (minpoly ℚ α).aroots ℂ.
• salem_theorem: Salem's theorem for Pisot numbers — for every ε > 0 there is a Salem number in (α − ε, α) and one in (α, α + ε) — by transport through salem_theorem_full.
• salem_construction_two_sided: the assembly PdtSalemEndgame.salem_construction_two_sided, keeping the index and the root equation — under the Pisot pattern and P(1/α) ≠ 0, with e = ±1 the sign of P(1/α), some X^m·P + e·P.reverse (m ≥ 2) has a Salem root in (α − ε, α) and some X^m·P − e·P.reverse (m ≥ 2) one in (α, α + ε); the halves exists_salem_below_root and exists_salem_above_root are the ladder lemmas of PdtSalemEndgame with the root kept.
• salem_quadratic_unit: PdtSalemQuadUnit.salem_two_sided_quad_unit with the index and the root equation retained, the family spelled as (X² − rX + 1)(X^{2m} + 1) ± X^{m+1} (m ≥ 1).

The pattern data from a simple dominant root

theorem PDT.SalemPisot.pattern_of_simple_root (Pz : Polynomial ℤ) (hmonic : Pz.Monic) (alpha : ℝ) (hsimple : Polynomial.rootMultiplicity (↑alpha) (Polynomial.map (Int.castRingHom ℂ) Pz) = 1) (hsmall : ∀ (z : ℂ), Polynomial.eval z (Polynomial.map (Int.castRingHom ℂ) Pz) = 0 → z ≠ ↑alpha → ‖z‖ < 1) : ∃ (inside : Multiset ℂ), (∀ z ∈ inside, ‖z‖ < 1) ∧ Multiset.map (⇑(starRingEnd ℂ)) inside = inside ∧ Polynomial.map (Int.castRingHom ℂ) Pz = SalemCircle.P alpha inside

The Pisot-pattern data from a simple root. For a monic integer polynomial whose complex image has α as a root of multiplicity exactly one and every other complex root strictly inside the unit circle, the multiset inside = roots.erase α satisfies the three pattern hypotheses: strict interiority, conjugation closure, and the factorization Pz = SalemCircle.P α inside.

The pattern data of a Pisot number's minimal polynomial

theorem PDT.SalemPisot.pattern_of_pisot (alpha : ℝ) (hint : IsIntegral ℤ alpha) (hsmall : ∀ z ∈ (minpoly ℚ alpha).aroots ℂ, z ≠ ↑alpha → ‖z‖ < 1) : ∃ (inside : Multiset ℂ), (∀ z ∈ inside, ‖z‖ < 1) ∧ Multiset.map (⇑(starRingEnd ℂ)) inside = inside ∧ Polynomial.map (Int.castRingHom ℂ) (minpoly ℤ alpha) = SalemCircle.P alpha inside

The minimal polynomial of a Pisot number carries the pattern. For a real algebraic integer α every other complex root of whose minimal polynomial over ℚ lies strictly inside the unit circle, minpoly ℤ α (monic) has the Pisot-pattern data: its complex image is (X − α)·∏ (X − z) over an interior, conjugation-closed multiset. The Gauss step identifies minpoly ℚ α with the rational image of minpoly ℤ α; irreducibility gives separability in characteristic zero, so α is a simple root of the complex image.

Salem's theorem for Pisot numbers

theorem PDT.SalemPisot.salem_theorem (alpha : ℝ) (halpha : 1 < alpha) (hint : IsIntegral ℤ alpha) (hsmall : ∀ z ∈ (minpoly ℚ alpha).aroots ℂ, z ≠ ↑alpha → ‖z‖ < 1) (eps : ℝ) (heps : 0 < eps) : (∃ (tau : ℝ), SalemEndgame.IsSalem tau ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (tau : ℝ), SalemEndgame.IsSalem tau ∧ alpha < tau ∧ tau < alpha + eps

Salem's theorem. Every Pisot number α — a real algebraic integer α > 1 whose other complex conjugates lie strictly inside the unit circle — is a limit of Salem numbers from both sides: for every ε > 0 there is a Salem number in (α − ε, α) and one in (α, α + ε). Transported through salem_theorem_full along the pattern data of minpoly ℤ α.

The constructions with their family roots exposed

The lower-level modules retain the family witnesses. Their traditional two-sided statements discard those witnesses, and this module re-exports the stronger interfaces.