PdtSalemCircle — the circle count

The circle count for Salem's construction: R_m's roots on the unit circle, counted by the explicit-phase route; Salem-ness / arithmetic assembly is NOT here (that is PdtSalemArith); the companion Q is the mirrored product, its identification with the reverse polynomial is deferred to PdtSalemArith.

Fixed data: alpha : ℝ with 1 < alpha, and a conjugation-closed multiset roots : Multiset ℂ of "inside" conjugates (‖r‖ < 1; it may be empty). With p := roots.card + 1,

• P = (X − C α)·∏ (X − C r) — monic of degree p, the root α outside the circle and the rest inside;
• Q = (1 − C α·X)·∏ (1 − C r·X) — the mirrored product, so that z^p·P(1/z) = Q(z) pointwise (mirror_P);
• R m = X^m·P + Q.

The three theorems:

• the self-inversive pairing (salem_root_inv): for z ≠ 0, R_m(z) = 0 → R_m(1/z) = 0 — pure product algebra, no reverse- polynomial API;
• the circle count (salem_circle_count): R_m has m + p − 2 distinct roots exp(t·I) with t ∈ (0, 2π). The route is the explicit phase: on the circle R_m(E t) = 2·N t·cos(ψ t)·E((m+p)·t/2) with N > 0 and ψ t = (m+p)·t/2 + A t, where A is an explicit sum of arg-terms each valued in an open half-plane, hence continuous; ψ climbs by (m+p−2)·π across [0, 2π], and the intermediate value theorem plants one root per half-period grid point — no argument principle, no Rouché theorem;
• the trichotomy (salem_root_trichotomy): if moreover τ > 1 is a root of R_m, then EVERY root is unimodular or lies in {τ, 1/τ} — the circle points, τ, and 1/τ already exhaust the degree m + p, by the multiset squeeze S.val ≤ (R m).roots.

The pairing salem_root_inv and the count salem_circle_count are stated without the hypothesis 1 ≤ m — it is not needed (for the count, 3 ≤ m + p alone drives the phase climb); the trichotomy carries both 1 ≤ m and 3 ≤ m + p.

The fixed objects

noncomputable def PDT.SalemCircle.E (t : ℝ) : ℂ

The circle parametrization E t = exp(t·I).

Equations

• PDT.SalemCircle.E t = Complex.exp (↑t * Complex.I)

noncomputable def PDT.SalemCircle.P (alpha : ℝ) (roots : Multiset ℂ) : Polynomial ℂ

P = (X − C α)·∏_{r ∈ roots} (X − C r): monic, degree roots.card + 1, roots α and the inside conjugates.

Equations

• PDT.SalemCircle.P alpha roots = (Polynomial.X - Polynomial.C ↑alpha) * (Multiset.map (fun (r : ℂ) => Polynomial.X - Polynomial.C r) roots).prod

noncomputable def PDT.SalemCircle.Q (alpha : ℝ) (roots : Multiset ℂ) : Polynomial ℂ

Q = (1 − C α·X)·∏_{r ∈ roots} (1 − C r·X): the mirrored product, z^p·P(1/z) = Q(z) for z ≠ 0 (mirror_P).

Equations

• PDT.SalemCircle.Q alpha roots = (1 - Polynomial.C ↑alpha * Polynomial.X) * (Multiset.map (fun (r : ℂ) => 1 - Polynomial.C r * Polynomial.X) roots).prod

noncomputable def PDT.SalemCircle.R (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) : Polynomial ℂ

The Salem family R_m = X^m·P + Q.

Equations

• PDT.SalemCircle.R alpha roots m = Polynomial.X ^ m * PDT.SalemCircle.P alpha roots + PDT.SalemCircle.Q alpha roots

noncomputable def PDT.SalemCircle.V (alpha : ℝ) (roots : Multiset ℂ) (t : ℝ) : ℂ

The reduced product on the circle: Q(E t) = conj (V t) and P(E t) = E(p·t)·V t.

Equations

• PDT.SalemCircle.V alpha roots t = (1 - ↑alpha * PDT.SalemCircle.E (-t)) * (Multiset.map (fun (r : ℂ) => 1 - r * PDT.SalemCircle.E (-t)) roots).prod

noncomputable def PDT.SalemCircle.N (alpha : ℝ) (roots : Multiset ℂ) (t : ℝ) : ℝ

The modulus of V: strictly positive on the whole circle.

Equations

• PDT.SalemCircle.N alpha roots t = ‖↑alpha - PDT.SalemCircle.E t‖ * (Multiset.map (fun (r : ℂ) => ‖1 - r * PDT.SalemCircle.E (-t)‖) roots).prod

noncomputable def PDT.SalemCircle.A (alpha : ℝ) (roots : Multiset ℂ) (t : ℝ) : ℝ

The explicit phase of V: every arg-term lives in an open half-plane, so A is continuous (continuous_A).

Equations

• PDT.SalemCircle.A alpha roots t = -t + Real.pi + (↑alpha - PDT.SalemCircle.E t).arg + (Multiset.map (fun (r : ℂ) => (1 - r * PDT.SalemCircle.E (-t)).arg) roots).sum

noncomputable def PDT.SalemCircle.psi (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) (t : ℝ) : ℝ

The half-angle phase of R_m on the circle: R_m(E t) = 2·N t·cos(ψ t)·E((m+p)·t/2).

Equations

• PDT.SalemCircle.psi alpha roots m t = ↑(m + roots.card + 1) * t / 2 + PDT.SalemCircle.A alpha roots t

Scalar evaluations and the self-inversive pairing

theorem PDT.SalemCircle.eval_P (alpha : ℝ) (roots : Multiset ℂ) (z : ℂ) : Polynomial.eval z (P alpha roots) = (z - ↑alpha) * (Multiset.map (fun (r : ℂ) => z - r) roots).prod

theorem PDT.SalemCircle.eval_Q (alpha : ℝ) (roots : Multiset ℂ) (z : ℂ) : Polynomial.eval z (Q alpha roots) = (1 - ↑alpha * z) * (Multiset.map (fun (r : ℂ) => 1 - r * z) roots).prod

theorem PDT.SalemCircle.eval_R (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) (z : ℂ) : Polynomial.eval z (R alpha roots m) = z ^ m * Polynomial.eval z (P alpha roots) + Polynomial.eval z (Q alpha roots)

theorem PDT.SalemCircle.prod_shift (s : Multiset ℂ) {z : ℂ} (hz : z ≠ 0) : z ^ s.card * (Multiset.map (fun (r : ℂ) => z⁻¹ - r) s).prod = (Multiset.map (fun (r : ℂ) => 1 - r * z) s).prod

Collecting one copy of z into each factor: z^card·∏ (1/z − r) = ∏ (1 − r·z).

theorem PDT.SalemCircle.prod_shift' (s : Multiset ℂ) {z : ℂ} (hz : z ≠ 0) : z ^ s.card * (Multiset.map (fun (r : ℂ) => 1 - r * z⁻¹) s).prod = (Multiset.map (fun (r : ℂ) => z - r) s).prod

The mirror of prod_shift: z^card·∏ (1 − r/z) = ∏ (z − r).

theorem PDT.SalemCircle.mirror_P (alpha : ℝ) (roots : Multiset ℂ) {z : ℂ} (hz : z ≠ 0) : z ^ (roots.card + 1) * Polynomial.eval z⁻¹ (P alpha roots) = Polynomial.eval z (Q alpha roots)

The first mirror identity: z^p·P(1/z) = Q(z) for z ≠ 0.

theorem PDT.SalemCircle.mirror_Q (alpha : ℝ) (roots : Multiset ℂ) {z : ℂ} (hz : z ≠ 0) : z ^ (roots.card + 1) * Polynomial.eval z⁻¹ (Q alpha roots) = Polynomial.eval z (P alpha roots)

The second mirror identity: z^p·Q(1/z) = P(z) for z ≠ 0.

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

The self-inversive functional equation: z^(m+p)·R_m(1/z) = R_m(z) for z ≠ 0.

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

The self-inversive pairing: a nonzero root of R_m pairs with its inverse. (Stated without the redundant 1 ≤ m.)

The E-calculus

theorem PDT.SalemCircle.E_zero : E 0 = 1

theorem PDT.SalemCircle.E_add (s t : ℝ) : E (s + t) = E s * E t

theorem PDT.SalemCircle.E_congr {s t : ℝ} (h : s = t) : E s = E t

theorem PDT.SalemCircle.E_mul_E_neg (t : ℝ) : E t * E (-t) = 1

theorem PDT.SalemCircle.E_ne_zero (t : ℝ) : E t ≠ 0

theorem PDT.SalemCircle.norm_E (t : ℝ) : ‖E t‖ = 1

theorem PDT.SalemCircle.conj_E (t : ℝ) : (starRingEnd ℂ) (E t) = E (-t)

theorem PDT.SalemCircle.E_pow (n : ℕ) (t : ℝ) : E t ^ n = E (↑n * t)

theorem PDT.SalemCircle.E_pi : E Real.pi = -1

theorem PDT.SalemCircle.E_two_pi : E (2 * Real.pi) = 1

theorem PDT.SalemCircle.E_re (t : ℝ) : (E t).re = Real.cos t

theorem PDT.SalemCircle.E_add_E_neg (x : ℝ) : E x + E (-x) = 2 * ↑(Real.cos x)

exp(iψ) + exp(−iψ) = 2·cos ψ, over the reals.

theorem PDT.SalemCircle.norm_mul_E (w : ℂ) (t : ℝ) : ‖w * E t‖ = ‖w‖

Nonvanishing and the half-plane locations

theorem PDT.SalemCircle.one_sub_ne_zero_of_norm_ne_one {w : ℂ} (hw : ‖w‖ ≠ 1) : 1 - w ≠ 0

theorem PDT.SalemCircle.alpha_factor_ne_zero {alpha : ℝ} (halpha : 1 < alpha) (t : ℝ) : 1 - ↑alpha * E (-t) ≠ 0

theorem PDT.SalemCircle.root_factor_ne_zero {r : ℂ} (hr : ‖r‖ < 1) (t : ℝ) : 1 - r * E (-t) ≠ 0

theorem PDT.SalemCircle.alpha_sub_E_ne_zero {alpha : ℝ} (halpha : 1 < alpha) (t : ℝ) : ↑alpha - E t ≠ 0

theorem PDT.SalemCircle.N_pos (alpha : ℝ) (roots : Multiset ℂ) (halpha : 1 < alpha) (hroots : ∀ r ∈ roots, ‖r‖ < 1) (t : ℝ) : 0 < N alpha roots t

theorem PDT.SalemCircle.re_pos_of_norm_lt_one {w : ℂ} (hw : ‖w‖ < 1) : 0 < (1 - w).re

theorem PDT.SalemCircle.alpha_sub_E_mem_slitPlane {alpha : ℝ} (halpha : 1 < alpha) (t : ℝ) : ↑alpha - E t ∈ Complex.slitPlane

theorem PDT.SalemCircle.root_factor_mem_slitPlane {r : ℂ} (hr : ‖r‖ < 1) (t : ℝ) : 1 - r * E (-t) ∈ Complex.slitPlane

The polar form and the key identity

theorem PDT.SalemCircle.polar (w : ℂ) : w = ↑‖w‖ * E w.arg

The polar form, phrased through E.

theorem PDT.SalemCircle.prod_norm_mul_E (s : Multiset ℂ) (nf af : ℂ → ℝ) : (Multiset.map (fun (r : ℂ) => ↑(nf r) * E (af r)) s).prod = ↑(Multiset.map nf s).prod * E (Multiset.map af s).sum

A multiset product of polar forms is the polar form of the product: norms multiply, phases add.

theorem PDT.SalemCircle.prod_map_const_mul (c : ℂ) (s : Multiset ℂ) (f : ℂ → ℂ) : (Multiset.map (fun (r : ℂ) => c * f r) s).prod = c ^ s.card * (Multiset.map f s).prod

Pulling a constant out of every factor.

theorem PDT.SalemCircle.polar_mul (a b x y : ℝ) : ↑a * E x * (↑b * E y) = ↑(a * b) * E (x + y)

Two polar forms multiply to a polar form.

theorem PDT.SalemCircle.first_factor_polar (alpha t : ℝ) : 1 - ↑alpha * E (-t) = ↑‖↑alpha - E t‖ * E (-t + Real.pi + (↑alpha - E t).arg)

The rotated polar form of the leading factor of V: 1 − α·E(−t) = ‖α − E t‖·E(−t + π + arg(α − E t)).

theorem PDT.SalemCircle.V_polar (alpha : ℝ) (roots : Multiset ℂ) (t : ℝ) : V alpha roots t = ↑(N alpha roots t) * E (A alpha roots t)

The polar decomposition of V: modulus N, phase A.

theorem PDT.SalemCircle.eval_P_E (alpha : ℝ) (roots : Multiset ℂ) (t : ℝ) : Polynomial.eval (E t) (P alpha roots) = E (↑(roots.card + 1) * t) * V alpha roots t

P on the circle: P(E t) = E(p·t)·V t.

theorem PDT.SalemCircle.eval_Q_E (alpha : ℝ) (roots : Multiset ℂ) (hconj : Multiset.map (⇑(starRingEnd ℂ)) roots = roots) (t : ℝ) : Polynomial.eval (E t) (Q alpha roots) = (starRingEnd ℂ) (V alpha roots t)

Q on the circle: Q(E t) = conj (V t) — this is where conjugation-closure of the root multiset enters.

theorem PDT.SalemCircle.R_eval_E (alpha : ℝ) (roots : Multiset ℂ) (hconj : Multiset.map (⇑(starRingEnd ℂ)) roots = roots) (m : ℕ) (t : ℝ) : Polynomial.eval (E t) (R alpha roots m) = ↑(2 * N alpha roots t * Real.cos (psi alpha roots m t)) * E (↑(m + roots.card + 1) * t / 2)

The key identity: on the circle, R_m(E t) = 2·N t·cos(ψ t)·E((m+p)·t/2) — the explicit phase that replaces the argument principle.

theorem PDT.SalemCircle.R_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 (E t) (R alpha roots m) = 0 ↔ Real.cos (psi alpha roots m t) = 0

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

Continuity of the phase

theorem PDT.SalemCircle.continuous_E : Continuous E

theorem PDT.SalemCircle.continuous_arg_alpha {alpha : ℝ} (halpha : 1 < alpha) : Continuous fun (t : ℝ) => (↑alpha - E t).arg

theorem PDT.SalemCircle.continuous_arg_root {r : ℂ} (hr : ‖r‖ < 1) : Continuous fun (t : ℝ) => (1 - r * E (-t)).arg

theorem PDT.SalemCircle.continuous_arg_sum (roots : Multiset ℂ) (hroots : ∀ r ∈ roots, ‖r‖ < 1) : Continuous fun (t : ℝ) => (Multiset.map (fun (r : ℂ) => (1 - r * E (-t)).arg) roots).sum

theorem PDT.SalemCircle.continuous_A (alpha : ℝ) (roots : Multiset ℂ) (halpha : 1 < alpha) (hroots : ∀ r ∈ roots, ‖r‖ < 1) : Continuous fun (t : ℝ) => A alpha roots t

theorem PDT.SalemCircle.continuous_psi (alpha : ℝ) (roots : Multiset ℂ) (halpha : 1 < alpha) (hroots : ∀ r ∈ roots, ‖r‖ < 1) (m : ℕ) : Continuous fun (t : ℝ) => psi alpha roots m t

The endpoints

theorem PDT.SalemCircle.A_two_pi (alpha : ℝ) (roots : Multiset ℂ) : A alpha roots (2 * Real.pi) = A alpha roots 0 - 2 * Real.pi

Across [0, 2π] every arg-term returns to its start; only the linear −t part moves: A(2π) = A(0) − 2π.

theorem PDT.SalemCircle.psi_two_pi (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) : psi alpha roots m (2 * Real.pi) = psi alpha roots m 0 + ↑(m + roots.card + 1) * Real.pi - 2 * Real.pi

The total climb of the phase: ψ(2π) = ψ(0) + (m+p)·π − 2π.

theorem PDT.SalemCircle.eval_R_one_ne_zero (alpha : ℝ) (roots : Multiset ℂ) (halpha : 1 < alpha) (hroots : ∀ r ∈ roots, ‖r‖ < 1) (m : ℕ) : Polynomial.eval 1 (R alpha roots m) ≠ 0

R_m(1) = 2·P(1) ≠ 0: the phase starts off the cosine grid.

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

The grid count

theorem PDT.SalemCircle.exists_interior_grid (f : ℝ → ℝ) (hf : Continuous f) (L : ℕ) (hclimb : f (2 * Real.pi) = f 0 + ↑L * Real.pi) (hcos0 : Real.cos (f 0) ≠ 0) : ∃ (T : Finset ℝ), T.card = L ∧ ∀ t ∈ T, (0 < t ∧ t < 2 * Real.pi) ∧ Real.cos (f t) = 0

The grid-count workhorse. A continuous phase f on [0, 2π] that climbs by exactly L·π and starts off the cosine grid attains L distinct interior grid values, planting L distinct zeros of cos ∘ f in (0, 2π).

theorem PDT.SalemCircle.salem_circle_count (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) - 2 ∧ ∀ t ∈ T, (0 < t ∧ t < 2 * Real.pi) ∧ Polynomial.eval (Complex.exp (↑t * Complex.I)) (R alpha roots m) = 0

The circle count: with p = roots.card + 1 and 3 ≤ m + p, the polynomial R_m has m + p − 2 distinct roots exp(t·I), t ∈ (0, 2π), on the unit circle. (Stated without the redundant 1 ≤ m.)

Degree bookkeeping — R_m is monic of degree m + p

theorem PDT.SalemCircle.P_monic (alpha : ℝ) (roots : Multiset ℂ) : (P alpha roots).Monic

theorem PDT.SalemCircle.prod_X_sub_C_natDegree (roots : Multiset ℂ) : (Multiset.map (fun (r : ℂ) => Polynomial.X - Polynomial.C r) roots).prod.natDegree = roots.card

theorem PDT.SalemCircle.P_natDegree (alpha : ℝ) (roots : Multiset ℂ) : (P alpha roots).natDegree = roots.card + 1

theorem PDT.SalemCircle.XmP_monic (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) : (Polynomial.X ^ m * P alpha roots).Monic

theorem PDT.SalemCircle.XmP_natDegree (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) : (Polynomial.X ^ m * P alpha roots).natDegree = m + (roots.card + 1)

theorem PDT.SalemCircle.factor_natDegree_le (r : ℂ) : (1 - Polynomial.C r * Polynomial.X).natDegree ≤ 1

theorem PDT.SalemCircle.Q_natDegree_le (alpha : ℝ) (roots : Multiset ℂ) : (Q alpha roots).natDegree ≤ roots.card + 1

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

theorem PDT.SalemCircle.R_monic (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) (hm : 1 ≤ m) : (R alpha roots m).Monic

theorem PDT.SalemCircle.R_natDegree (alpha : ℝ) (roots : Multiset ℂ) (m : ℕ) (hm : 1 ≤ m) : (R alpha roots m).natDegree = m + (roots.card + 1)

Injectivity of the circle parametrization

theorem PDT.SalemCircle.E_inj {t s : ℝ} (ht : 0 < t) (ht2 : t < 2 * Real.pi) (hs : 0 < s) (hs2 : s < 2 * Real.pi) (heq : E t = E s) : t = s

The trichotomy

theorem PDT.SalemCircle.finset_val_eq_roots {K : Type u_1} [Field K] (P : Polynomial K) (hP : P ≠ 0) (S : Finset K) (hS : ∀ z ∈ S, Polynomial.eval z P = 0) (hcard : S.card = P.natDegree) : S.val = P.roots

A set of distinct roots whose cardinality is the degree exhausts the root multiset.

theorem PDT.SalemCircle.salem_root_trichotomy (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) (R alpha roots m) = 0) (z : ℂ) : Polynomial.eval z (R alpha roots m) = 0 → ‖z‖ = 1 ∨ z = ↑tau ∨ z = (↑tau)⁻¹

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