theorem HexRootsMathlib.norm_esymm_le {s : Multiset ℂ} {B : ℝ} (hs : ∀ z ∈ s, ‖z‖ ≤ B) (k : ℕ) : ‖s.esymm k‖ ≤ ↑(s.card.choose k) * B ^ k

If every entry of a multiset has norm at most B, its k-th elementary symmetric function has norm at most choose(card, k) * B^k.

theorem HexRootsMathlib.esymm_tail_le {s : Multiset ℂ} {B ρ : ℝ} (hρ : 0 ≤ ρ) (hs : ∀ z ∈ s, ‖z‖ ≤ B) : ∑ k ∈ (Finset.range (s.card + 1)).erase 0, ‖s.esymm k‖ * ρ ^ k ≤ (1 + ρ * B) ^ s.card - 1

The positive-degree elementary-symmetric tail is bounded by the binomial tail generated by a uniform norm bound.

theorem HexRootsMathlib.remote_tail_le {s : Multiset ℂ} {d ρ : ℝ} (hd : 0 < d) (hρ : 0 ≤ ρ) (hs : ∀ z ∈ s, d ≤ ‖z‖) : ∑ k ∈ (Finset.range (s.card + 1)).erase 0, ‖(Multiset.map Inv.inv s).esymm k‖ * ρ ^ k ≤ (1 + ρ / d) ^ s.card - 1

If every remote root has norm at least d, the normalized coefficient tail is bounded by (1 + ρ / d)^n - 1. The next completeness layer connects this elementary-symmetric data to the coefficients of the normalized product ∏ z, (1 - X / z).