PdtSalemQuadUnit — the reciprocal-quadratic case and the pattern-form theorem

The reciprocal-quadratic case of Salem's theorem, via Salem's second construction in its explicit form B = (X² − rX + 1)(X^{2m} + 1) ± X^{m+1} (Chebyshev-free), the reduction lemma (a Pisot-pattern polynomial vanishing at 1/alpha forces alpha reciprocal quadratic), and salem_theorem_full — the pattern-form theorem, which unifies Salem's two cases in one statement (supporting; the compared Salem's Theorem IV for Pisot numbers is SalemPisot.salem_theorem). The sign eps = −1 approaches from above, eps = +1 from below.

Setting: alpha > 1 a reciprocal quadratic Pisot unit — alpha² = r·alpha − 1 with r : ℤ, 3 ≤ r, so alpha + 1/alpha = r and the conjugate is 1/alpha. The excluded case of PdtSalemEndgame.salem_two_sided is exactly this one (P(1/alpha) = 0 forces it — the reduction lemma), and the explicit family

• Bfam r eps m = (X² − C r·X + 1)·(X^{2m} + 1) + C eps·X^{m+1}

covers it: on the circle B(E t) = E((m+1)t)·((2cos t − r)·2cos(mt) + eps) gives 2m circle roots by sign alternation on the grid t_k = kπ/m (no phase, no argument principle); off the circle the normalized form B(y) = y^{m+1}·((y + 1/y − r)(y^m + y^{−m}) + eps) plants one real root just above alpha (eps = −1) or just below (eps = +1), at distance O(2^{−m}); the multiset squeeze and the arithmetic certificate (the third certificate, the second port of PdtSalemArith.salem_certificate) promote the root to a Salem number, the two integer degeneracies being excluded DIRECTLY: the root lies in (r − 1, r) which contains no integer, and its trace displacement tau + 1/tau − r = −eps/(tau^m + tau^{−m}) is nonzero of absolute value < 1/2.

Main results:

• salem_two_sided_quad_unit: the degenerate case closed — Salem numbers approach a reciprocal quadratic Pisot unit from both sides;
• reciprocal_quadratic_of_inv_root: a Pisot-pattern polynomial vanishing at 1/alpha forces alpha² = r·alpha − 1, 3 ≤ r;
• salem_theorem_full: the pattern-form theorem — every Pisot-pattern polynomial has Salem numbers approaching its large root from both sides; it unifies Salem's two cases in one statement (supporting; the compared Salem's Theorem IV for Pisot numbers is SalemPisot.salem_theorem).

The reduction lemma is proved without conjugation-closure.

Scalar facts about the reciprocal quadratic unit

theorem PDT.SalemQuadUnit.trace_eq {r : ℤ} {alpha : ℝ} (halpha : 1 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) : alpha + alpha⁻¹ = ↑r

The trace identity: alpha + 1/alpha = r.

theorem PDT.SalemQuadUnit.alpha_gt_two {r : ℤ} {alpha : ℝ} (hr : 3 ≤ r) (halpha : 1 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) : 2 < alpha

The unit is larger than 2 (indeed larger than r − 1 ≥ 2).

theorem PDT.SalemQuadUnit.quad_factor {r : ℤ} {alpha : ℝ} (halpha : 1 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) (y : ℝ) : y ^ 2 - ↑r * y + 1 = (y - alpha) * (y - alpha⁻¹)

The real quadratic factors through the two conjugates.

theorem PDT.SalemQuadUnit.alpha_lt_r {r : ℤ} {alpha : ℝ} (halpha : 1 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) : alpha < ↑r

The window (r − 1, r) around alpha: upper part.

theorem PDT.SalemQuadUnit.r_sub_one_lt_alpha {r : ℤ} {alpha : ℝ} (halpha : 1 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) : ↑r - 1 < alpha

The window (r − 1, r) around alpha: lower part.

theorem PDT.SalemQuadUnit.no_int_in_window {r : ℤ} {x : ℝ} (h1 : ↑r - 1 < x) (h2 : x < ↑r) (n : ℤ) : x ≠ ↑n

No integer lies in the open interval (r − 1, r).

The IVT helper

theorem PDT.SalemQuadUnit.exists_root_between (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (hsign : f a * f b < 0) : ∃ (x : ℝ), a < x ∧ x < b ∧ f x = 0

A sign change of a continuous function plants a root strictly between the endpoints.

The family over ℤ and its basic structure

noncomputable def PDT.SalemQuadUnit.Bfam (r eps : ℤ) (m : ℕ) : Polynomial ℤ

Salem's second construction, Chebyshev-free: the integer family B = (X² − rX + 1)·(X^{2m} + 1) + eps·X^{m+1}, eps = ±1.

Equations

• PDT.SalemQuadUnit.Bfam r eps m = (Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1) * (Polynomial.X ^ (2 * m) + 1) + Polynomial.C eps * Polynomial.X ^ (m + 1)

theorem PDT.SalemQuadUnit.quad_monic (r : ℤ) : (Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1).Monic

theorem PDT.SalemQuadUnit.quad_natDegree (r : ℤ) : (Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1).natDegree = 2

theorem PDT.SalemQuadUnit.cyc_monic (m : ℕ) (hm : 1 ≤ m) : (Polynomial.X ^ (2 * m) + 1).Monic

theorem PDT.SalemQuadUnit.cyc_natDegree (m : ℕ) : (Polynomial.X ^ (2 * m) + 1).natDegree = 2 * m

theorem PDT.SalemQuadUnit.lead_monic (r : ℤ) (m : ℕ) (hm : 1 ≤ m) : ((Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1) * (Polynomial.X ^ (2 * m) + 1)).Monic

theorem PDT.SalemQuadUnit.lead_natDegree (r : ℤ) (m : ℕ) (hm : 1 ≤ m) : ((Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1) * (Polynomial.X ^ (2 * m) + 1)).natDegree = 2 * m + 2

theorem PDT.SalemQuadUnit.pert_degree_lt (r eps : ℤ) (m : ℕ) (hm : 1 ≤ m) : (Polynomial.C eps * Polynomial.X ^ (m + 1)).degree < ((Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1) * (Polynomial.X ^ (2 * m) + 1)).degree

theorem PDT.SalemQuadUnit.Bfam_monic (r eps : ℤ) {m : ℕ} (hm : 1 ≤ m) : (Bfam r eps m).Monic

theorem PDT.SalemQuadUnit.Bfam_natDegree (r eps : ℤ) {m : ℕ} (hm : 1 ≤ m) : (Bfam r eps m).natDegree = 2 * m + 2

theorem PDT.SalemQuadUnit.Bfam_eval_R (r eps : ℤ) (m : ℕ) (y : ℝ) : Polynomial.eval y (Polynomial.map (Int.castRingHom ℝ) (Bfam r eps m)) = (y ^ 2 - ↑r * y + 1) * (y ^ (2 * m) + 1) + ↑eps * y ^ (m + 1)

The real evaluation form.

theorem PDT.SalemQuadUnit.Bfam_eval_C (r eps : ℤ) (m : ℕ) (z : ℂ) : Polynomial.eval z (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = (z ^ 2 - ↑r * z + 1) * (z ^ (2 * m) + 1) + ↑eps * z ^ (m + 1)

The complex evaluation form.

theorem PDT.SalemQuadUnit.key_identity {K : Type u_1} [Field K] (a b : K) (m : ℕ) {u : K} (hu : u ≠ 0) : (u ^ 2 - a * u + 1) * (u ^ (2 * m) + 1) + b * u ^ (m + 1) = u ^ (m + 1) * ((u + u⁻¹ - a) * (u ^ m + u⁻¹ ^ m) + b)

The key algebraic identity (the whole "Chebyshev" content): for u ≠ 0, (u² − au + 1)(u^{2m} + 1) + b·u^{m+1} = u^{m+1}·((u + u⁻¹ − a)(u^m + u^{−m}) + b).

theorem PDT.SalemQuadUnit.Bfam_self_inversive (r eps : ℤ) (m : ℕ) {z : ℂ} (hz : z ≠ 0) : z ^ (2 * m + 2) * Polynomial.eval z⁻¹ (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = Polynomial.eval z (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m))

Self-inversive, both signs: z^{2m+2}·B(1/z) = B(z) for z ≠ 0 — the middle monomial X^{m+1} is its own reverse.

theorem PDT.SalemQuadUnit.Bfam_root_inv (r eps : ℤ) (m : ℕ) {z : ℂ} (hz : z ≠ 0) (hroot : Polynomial.eval z (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = 0) : Polynomial.eval z⁻¹ (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = 0

The pairing: a nonzero root of B pairs with its inverse.

The circle count — 2m distinct unimodular roots

noncomputable def PDT.SalemQuadUnit.hfun (r eps : ℤ) (m : ℕ) (t : ℝ) : ℝ

The real sign function on the circle: B(E t) = E((m+1)t)·h(t) with h t = (2cos t − r)·2cos(mt) + eps.

Equations

• PDT.SalemQuadUnit.hfun r eps m t = (2 * Real.cos t - ↑r) * (2 * Real.cos (↑m * t)) + ↑eps

theorem PDT.SalemQuadUnit.continuous_hfun (r eps : ℤ) (m : ℕ) : Continuous (hfun r eps m)

theorem PDT.SalemQuadUnit.Bfam_eval_E (r eps : ℤ) (m : ℕ) (t : ℝ) : Polynomial.eval (SalemCircle.E t) (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = SalemCircle.E ((↑m + 1) * t) * ↑(hfun r eps m t)

The key identity on the circle (no phase, no arg): B(E t) = E((m+1)t)·h(t).

theorem PDT.SalemQuadUnit.Bfam_eval_E_eq_zero_iff (r eps : ℤ) (m : ℕ) (t : ℝ) : Polynomial.eval (SalemCircle.E t) (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = 0 ↔ hfun r eps m t = 0

The zero test on the circle: B(E t) = 0 ↔ h(t) = 0.

theorem PDT.SalemQuadUnit.hfun_at_grid (r eps : ℤ) {m : ℕ} (hm : 1 ≤ m) (k : ℕ) : hfun r eps m (↑k * Real.pi / ↑m) = (2 * Real.cos (↑k * Real.pi / ↑m) - ↑r) * (2 * (-1) ^ k) + ↑eps

h on the grid t_k = kπ/m: the second cosine collapses to (−1)^k.

theorem PDT.SalemQuadUnit.hfun_grid_neg (r eps : ℤ) (hr : 3 ≤ r) (heps : eps = 1 ∨ eps = -1) {m : ℕ} (hm : 1 ≤ m) (k : ℕ) (hk : Even k) : hfun r eps m (↑k * Real.pi / ↑m) < 0

The alternation, even leg: h(t_k) < 0 for k even — REGARDLESS of the sign eps = ±1 (|eps| = 1 < 2 ≤ |product|).

theorem PDT.SalemQuadUnit.hfun_grid_pos (r eps : ℤ) (hr : 3 ≤ r) (heps : eps = 1 ∨ eps = -1) {m : ℕ} (hm : 1 ≤ m) (k : ℕ) (hk : Odd k) : 0 < hfun r eps m (↑k * Real.pi / ↑m)

The alternation, odd leg: 0 < h(t_k) for k odd.

theorem PDT.SalemQuadUnit.circle_count (r eps : ℤ) (hr : 3 ≤ r) (heps : eps = 1 ∨ eps = -1) {m : ℕ} (hm : 1 ≤ m) : ∃ (T : Finset ℝ), T.card = 2 * m ∧ ∀ t ∈ T, (0 < t ∧ t < 2 * Real.pi) ∧ Polynomial.eval (SalemCircle.E t) (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = 0

The circle count: B has 2m distinct roots E t, t ∈ (0, 2π) — one in each open grid interval (kπ/m, (k+1)π/m), k = 0, …, 2m − 1, by sign alternation.

The ladder roots — direct endpoint signs

theorem PDT.SalemQuadUnit.eval_at_alpha (r eps : ℤ) {alpha : ℝ} (hmin : alpha ^ 2 = ↑r * alpha - 1) (m : ℕ) : Polynomial.eval alpha (Polynomial.map (Int.castRingHom ℝ) (Bfam r eps m)) = ↑eps * alpha ^ (m + 1)

At alpha the leading factor vanishes: B(alpha) = eps·alpha^{m+1}.

theorem PDT.SalemQuadUnit.eval_above_pos (r : ℤ) {alpha : ℝ} (halpha2 : 2 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) (m : ℕ) {d : ℝ} (hd0 : 0 < d) (hd1 : d ≤ 1) (hdm : alpha + 1 < d * (alpha - alpha⁻¹) * 2 ^ m) : 0 < Polynomial.eval (alpha + d) (Polynomial.map (Int.castRingHom ℝ) (Bfam r (-1) m))

Above sign: with y = alpha + d, 0 < d ≤ 1 and alpha + 1 < d·(alpha − 1/alpha)·2^m, the eps = −1 member is positive at y — the second factor y^m ≥ alpha^m > 2^m cancels the 2^{−m} displacement.

theorem PDT.SalemQuadUnit.eval_below_neg (r : ℤ) {alpha : ℝ} (halpha2 : 2 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) (m : ℕ) {d : ℝ} (hd0 : 0 < d) (hd2 : d ≤ alpha - 2) (hdm : alpha < d * 2 ^ m) : Polynomial.eval (alpha - d) (Polynomial.map (Int.castRingHom ℝ) (Bfam r 1 m)) < 0

Below sign: with y = alpha − d ≥ 2, 0 < d and alpha < d·2^m, the eps = +1 member is negative at y.

theorem PDT.SalemQuadUnit.trace_displacement (r eps : ℤ) (m : ℕ) {tau : ℝ} (htau0 : 0 < tau) (hroot : Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Bfam r eps m)) = 0) : (tau + tau⁻¹ - ↑r) * (tau ^ m + tau⁻¹ ^ m) = -↑eps

The exact trace displacement at a root: (tau + 1/tau − r)·(tau^m + tau^{−m}) = −eps.

theorem PDT.SalemQuadUnit.trace_not_int (r eps : ℤ) (heps : eps = 1 ∨ eps = -1) {m : ℕ} (hm : 1 ≤ m) {tau : ℝ} (htau2 : 2 < tau) (hroot : Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Bfam r eps m)) = 0) (n : ℤ) : tau + tau⁻¹ ≠ ↑n

Direct exclusion of the trace degeneracy: at a root tau > 2 the trace tau + 1/tau differs from r by 0 < |·| < 1/2, so it is not an integer.

The trichotomy — the third multiset squeeze

theorem PDT.SalemQuadUnit.Bfam_trichotomy (r eps : ℤ) (hr : 3 ≤ r) (heps : eps = 1 ∨ eps = -1) {m : ℕ} (hm : 1 ≤ m) (tau : ℝ) (htau : 1 < tau) (hroot : Polynomial.eval (↑tau) (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = 0) (z : ℂ) : Polynomial.eval z (Polynomial.map (Int.castRingHom ℂ) (Bfam r eps m)) = 0 → ‖z‖ = 1 ∨ z = ↑tau ∨ z = (↑tau)⁻¹

The trichotomy for the quadratic-unit family: if tau > 1 is a root of B, then EVERY complex root is unimodular or lies in {tau, 1/tau} — the 2m circle points, tau, and 1/tau already exhaust the degree 2m + 2.

The arithmetic Salem-ness certificate

theorem PDT.SalemQuadUnit.salem_certificate_quad (r eps : ℤ) (hr : 3 ≤ r) (heps : eps = 1 ∨ eps = -1) {m : ℕ} (hm : 1 ≤ m) (tau : ℝ) (htau : 1 < tau) (hroot : Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Bfam r eps m)) = 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 certificate for the quadratic-unit family — the specialization of the shared arithmetic certificate: a real root tau > 1 of B, excluded from the two integer degeneracies, is an algebraic integer whose conjugates fill the closed unit disk, one ON the circle, with 1/tau among them.

theorem PDT.SalemQuadUnit.isSalem_of_quad_root (r eps : ℤ) (hr : 3 ≤ r) (heps : eps = 1 ∨ eps = -1) {m : ℕ} (hm : 1 ≤ m) (tau : ℝ) (htau : 1 < tau) (hroot : Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) (Bfam r eps m)) = 0) (hτZ : ∀ (n : ℤ), tau ≠ ↑n) (hτtr : ∀ (n : ℤ), tau + tau⁻¹ ≠ ↑n) : SalemEndgame.IsSalem tau

The packaged certificate: a nondegenerate root tau > 1 of the quadratic-unit family is a Salem number.

The degenerate case closed

theorem PDT.SalemQuadUnit.salem_quadratic_unit (r : ℤ) (hr : 3 ≤ r) (alpha : ℝ) (halpha : 1 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) (eps : ℝ) (heps : 0 < eps) : (∃ (m : ℕ), 1 ≤ m ∧ ∃ (tau : ℝ), SalemEndgame.IsSalem tau ∧ Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) ((Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1) * (Polynomial.X ^ (2 * m) + 1) + Polynomial.X ^ (m + 1))) = 0 ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (m : ℕ), 1 ≤ m ∧ ∃ (tau : ℝ), SalemEndgame.IsSalem tau ∧ Polynomial.eval tau (Polynomial.map (Int.castRingHom ℝ) ((Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1) * (Polynomial.X ^ (2 * m) + 1) - Polynomial.X ^ (m + 1))) = 0 ∧ alpha < tau ∧ tau < alpha + eps

The reciprocal-quadratic construction with its family root exposed. The common assembly keeps the index m ≥ 1 and the root equation: below α a Salem root of (X² − rX + 1)(X^{2m} + 1) + X^{m+1}, above α a Salem root of (X² − rX + 1)(X^{2m} + 1) − X^{m+1} — the members eps = +1 and eps = −1 of PdtSalemQuadUnit.Bfam, spelled out.

theorem PDT.SalemQuadUnit.salem_two_sided_quad_unit (r : ℤ) (hr : 3 ≤ r) (alpha : ℝ) (halpha : 1 < alpha) (hmin : alpha ^ 2 = ↑r * alpha - 1) (eps : ℝ) (heps : 0 < eps) : (∃ (tau : ℝ), SalemEndgame.IsSalem tau ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (tau : ℝ), SalemEndgame.IsSalem tau ∧ alpha < tau ∧ tau < alpha + eps

The degenerate case closed: Salem numbers approach a reciprocal quadratic Pisot unit alpha (alpha² = r·alpha − 1, 3 ≤ r) from BOTH sides — the eps = +1 member of the family plants a root in (alpha − δ, alpha), the eps = −1 member in (alpha, alpha + δ), both inside the integer-free window (r − 1, r), and the certificate promotes them to Salem numbers.

theorem PDT.SalemQuadUnit.reflect_eval_eq_C (W : Polynomial ℂ) {z : ℂ} (hz : z ≠ 0) (p : ℕ) (hdeg : W.natDegree ≤ p) : Polynomial.eval z (Polynomial.reflect p W) = z ^ p * Polynomial.eval z⁻¹ W

The reflect-evaluation identity over ℂ (the verbatim complex twin of SalemEndgame.reflect_eval_eq): (reflect p W)(z) = z^p·W(1/z) for z ≠ 0.

theorem PDT.SalemQuadUnit.reciprocal_quadratic_of_inv_root (Pz : Polynomial ℤ) (hmonic : Pz.Monic) (alpha : ℝ) (halpha : 1 < alpha) (inside : Multiset ℂ) (hin : ∀ z ∈ inside, ‖z‖ < 1) (hfacC : Polynomial.map (Int.castRingHom ℂ) Pz = SalemCircle.P alpha inside) (h0 : Polynomial.eval alpha⁻¹ (Polynomial.map (Int.castRingHom ℝ) Pz) = 0) : ∃ (r : ℤ), 3 ≤ r ∧ alpha ^ 2 = ↑r * alpha - 1

The reduction: a Pisot-pattern polynomial vanishing at 1/alpha forces alpha to be a reciprocal quadratic Pisot unit — alpha² = r·alpha − 1 with 3 ≤ r : ℤ. (No conjugation-closure is needed.)

theorem PDT.SalemQuadUnit.salem_theorem_full (Pz : Polynomial ℤ) (hmonic : Pz.Monic) (alpha : ℝ) (halpha : 1 < alpha) (inside : Multiset ℂ) (hin : ∀ z ∈ inside, ‖z‖ < 1) (hconj : Multiset.map (⇑(starRingEnd ℂ)) inside = inside) (hfacC : Polynomial.map (Int.castRingHom ℂ) Pz = SalemCircle.P alpha inside) (eps : ℝ) (heps : 0 < eps) : (∃ (tau : ℝ), SalemEndgame.IsSalem tau ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (tau : ℝ), SalemEndgame.IsSalem tau ∧ alpha < tau ∧ tau < alpha + eps

The pattern-form theorem (supporting; the compared Salem's Theorem IV for Pisot numbers is SalemPisot.salem_theorem): every Pisot-pattern polynomial (monic over ℤ, one real root alpha > 1, all other roots strictly inside the unit circle, conjugation-closed) has Salem numbers approaching alpha from both sides; the statement unifies Salem's two cases in one. If P(1/alpha) ≠ 0 this is PdtSalemEndgame.salem_two_sided; if P(1/alpha) = 0 the reduction forces alpha reciprocal quadratic and the explicit family closes the case.