PdtSalemMinus — the minus family

The minus family of Salem's construction, X^m·P − Q — anti-self-inversive pairing, the sine-anchored circle count (z = 1 is always a root, so the phase starts on the grid: m+p−3 interior circle roots plus z = 1), the trichotomy, and the ported arithmetic certificate. The assembly (both ladders, the two-sided statement) is PdtSalemEndgame.

The fixed objects (P, Q, E, V, N, A, psi) are reused from PdtSalemCircle; the arithmetic helpers from PdtSalemArith. With p := roots.card + 1 and Rm m = X^m·P − Q, the three sign-flips against the plus family are:

• the functional equation gains a minus (Rm_eval_inv): z^(m+p)·Rm(1/z) = −Rm(z) — anti-self-inversive, but a zero of a negation is a zero, so the pairing survives (salem_root_inv_minus);
• the key identity produces SINE instead of cosine (Rm_eval_E): Rm(E t) = 2·N t·sin(ψ t)·(i·E((m+p)·t/2));
• z = 1 is ALWAYS a root (Rm_one_root: P(1) = Q(1) exactly), so the phase starts ON the sine grid and the interior count is anchored at m+p−3 (salem_circle_count_minus) — no floor function; the point z = 1 is the (m+p−2)nd circle root and is inserted explicitly in the trichotomy (salem_root_trichotomy_minus).

The arithmetic certificate salem_certificate_minus is the verbatim port of PdtSalemArith.salem_certificate with the family Rz = X^m·Pz − Qz.

The minus family

noncomputable def PDT.SalemMinus.Rm (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) : Polynomial ℂ

The minus Salem family Rm_m = X^m·P − Q.

Equations

• PDT.SalemMinus.Rm alpha roots m = Polynomial.X ^ m * PDT.SalemCircle.P alpha roots - PDT.SalemCircle.Q alpha roots

theorem PDT.SalemMinus.eval_Rm (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) (z : ℂ) : Polynomial.eval z (Rm alpha roots m) = z ^ m * Polynomial.eval z (SalemCircle.P alpha roots) - Polynomial.eval z (SalemCircle.Q alpha roots)

The anti-self-inversive pairing and the anchor root

theorem PDT.SalemMinus.Rm_eval_inv (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) {z : ℂ} (hz : z ≠ 0) : z ^ (m + (roots.card + 1)) * Polynomial.eval z⁻¹ (Rm alpha roots m) = -Polynomial.eval z (Rm alpha roots m)

The anti-self-inversive functional equation: z^(m+p)·Rm(1/z) = −Rm(z) for z ≠ 0 — the sign flip against the plus family.

theorem PDT.SalemMinus.salem_root_inv_minus (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) {z : ℂ} (hz : z ≠ 0) (hroot : Polynomial.eval z (Rm alpha roots m) = 0) : Polynomial.eval z⁻¹ (Rm alpha roots m) = 0

The pairing: a nonzero root of Rm_m pairs with its inverse — a zero of a negation is a zero.

theorem PDT.SalemMinus.Rm_one_root (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) : Polynomial.eval 1 (Rm alpha roots m) = 0

The anchor: z = 1 is ALWAYS a root of the minus family — P(1) and Q(1) are literally the same product.

The sine key identity on the circle

theorem PDT.SalemMinus.E_sub_E_neg (x : ℝ) : SalemCircle.E x - SalemCircle.E (-x) = 2 * Complex.I * ↑(Real.sin x)

exp(iψ) − exp(−iψ) = 2i·sin ψ, over the reals — the sine mirror of SalemCircle.E_add_E_neg.

theorem PDT.SalemMinus.Rm_eval_E (alpha : ℝ) (roots : Multiset ℂ) (hconj : Multiset.map (⇑(starRingEnd ℂ)) roots = roots) (m : ℕ) (t : ℝ) : Polynomial.eval (SalemCircle.E t) (Rm alpha roots m) = ↑(2 * SalemCircle.N alpha roots t * Real.sin (SalemCircle.psi alpha roots m t)) * (Complex.I * SalemCircle.E (↑(m + roots.card + 1) * t / 2))

The key identity: on the circle, Rm_m(E t) = 2·N t·sin(ψ t)·(i·E((m+p)·t/2)) — the sine phase that replaces the plus family's cosine.

theorem PDT.SalemMinus.Rm_eval_E_eq_zero_iff (alpha : ℝ) (roots : Multiset ℂ) (halpha : 1 < alpha) (hroots : ∀ r ∈ roots, ‖r‖ < 1) (hconj : Multiset.map (⇑(starRingEnd ℂ)) roots = roots) (m : ℕ) (t : ℝ) : Polynomial.eval (SalemCircle.E t) (Rm alpha roots m) = 0 ↔ Real.sin (SalemCircle.psi alpha roots m t) = 0

The zero test on the circle: Rm_m(E t) = 0 ↔ sin(ψ t) = 0.

theorem PDT.SalemMinus.sin_psi_zero_eq_zero (alpha : ℝ) (roots : Multiset ℂ) (halpha : 1 < alpha) (hroots : ∀ r ∈ roots, ‖r‖ < 1) (hconj : Multiset.map (⇑(starRingEnd ℂ)) roots = roots) (m : ℕ) : Real.sin (SalemCircle.psi alpha roots m 0) = 0

The anchor on the grid: Rm(1) = 0 at t = 0 puts the phase ON the sine grid — sin(ψ 0) = 0.

The anchored grid count

theorem PDT.SalemMinus.exists_interior_grid_anchored (f : ℝ → ℝ) (hf : Continuous f) (L : ℕ) (hclimb : f (2 * Real.pi) = f 0 + ↑L * Real.pi) (hsin0 : Real.sin (f 0) = 0) : ∃ (T : Finset ℝ), T.card = L - 1 ∧ ∀ t ∈ T, (0 < t ∧ t < 2 * Real.pi) ∧ Real.sin (f t) = 0

The anchored grid-count workhorse. A continuous phase f on [0, 2π] that climbs by exactly L·π and starts ON the sine grid (sin (f 0) = 0) attains L − 1 distinct interior grid values, planting L − 1 distinct zeros of sin ∘ f in (0, 2π) — simpler than the plus workhorse: the anchor kills the floor function.

theorem PDT.SalemMinus.salem_circle_count_minus (alpha : ℝ) (roots : Multiset ℂ) (halpha : 1 < alpha) (hroots : ∀ r ∈ roots, ‖r‖ < 1) (hconj : Multiset.map (⇑(starRingEnd ℂ)) roots = roots) (m : ℕ) (hmp : 3 ≤ m + (roots.card + 1)) : ∃ (T : Finset ℝ), T.card = m + (roots.card + 1) - 3 ∧ ∀ t ∈ T, (0 < t ∧ t < 2 * Real.pi) ∧ Polynomial.eval (Complex.exp (↑t * Complex.I)) (Rm alpha roots m) = 0

The anchored circle count: with p = roots.card + 1 and 3 ≤ m + p, the minus family Rm_m has m + p − 3 distinct INTERIOR roots exp(t·I), t ∈ (0, 2π), on the unit circle — z = 1 (i.e. t = 0) is the (m+p−2)nd circle root, always present (Rm_one_root), and it anchors the phase on the grid. (Stated without the redundant 1 ≤ m, as in the plus count.)

Degree bookkeeping — Rm_m is monic of degree m + p

theorem PDT.SalemMinus.Rm_eq_add_neg (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) : Rm alpha roots m = Polynomial.X ^ m * SalemCircle.P alpha roots + -SalemCircle.Q alpha roots

theorem PDT.SalemMinus.degree_neg_Q_lt (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) (hm : 1 ≤ m) : (-SalemCircle.Q alpha roots).degree < (Polynomial.X ^ m * SalemCircle.P alpha roots).degree

theorem PDT.SalemMinus.Rm_monic (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) (hm : 1 ≤ m) : (Rm alpha roots m).Monic

theorem PDT.SalemMinus.Rm_natDegree (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) (hm : 1 ≤ m) : (Rm alpha roots m).natDegree = m + (roots.card + 1)

The circle parametrization avoids 1 on the interior

theorem PDT.SalemMinus.E_ne_one {t : ℝ} (ht : 0 < t) (ht2 : t < 2 * Real.pi) : SalemCircle.E t ≠ 1

On the open interval (0, 2π) the circle parametrization avoids 1 — so inserting the anchor root z = 1 genuinely grows the root set.

The trichotomy

theorem PDT.SalemMinus.salem_root_trichotomy_minus (alpha : ℝ) (roots : Multiset ℂ) (halpha : 1 < alpha) (hroots : ∀ r ∈ roots, ‖r‖ < 1) (hconj : Multiset.map (⇑(starRingEnd ℂ)) roots = roots) (m : ℕ) (hm : 1 ≤ m) (hmp : 3 ≤ m + (roots.card + 1)) (tau : ℝ) (htau : 1 < tau) (hroot : Polynomial.eval (↑tau) (Rm alpha roots m) = 0) (z : ℂ) : Polynomial.eval z (Rm alpha roots m) = 0 → ‖z‖ = 1 ∨ z = ↑tau ∨ z = (↑tau)⁻¹

The trichotomy: if τ > 1 is a root of Rm_m (with 1 ≤ m and 3 ≤ m + p), then EVERY root of Rm_m is unimodular or lies in {τ, 1/τ} — the m + p − 3 interior circle points of the anchored count, the anchor root 1, and τ, 1/τ already exhaust the degree m + p of the monic Rm_m, by the multiset squeeze S.val ≤ (Rm_m).roots.

The arithmetic certificate for the minus family

theorem PDT.SalemMinus.family_monic_minus (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 minus family X^m·Pz − Qz is monic (for m ≥ 1).

theorem PDT.SalemMinus.family_map_C_minus (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) = Rm alpha inside m

The complex image of the integer minus family is Rm.

theorem PDT.SalemMinus.salem_certificate_minus (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 for the minus family. A real root tau > 1 of the integer family X^m·Pz − Qz — whose complex image is the minus family Rm — 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. Specializes SalemArith.salem_certificate_of_root_trichotomy; the shared proof excludes the degeneracies through the Gauss step.