Sharp coefficient control from the integer grid. The absolute coefficient sum of each Lagrange basis polynomial is at most a binomial coefficient; summing gives the factor 3^d in CCDN Lemma 3.4.1, over the complex numbers.

theorem CCDN.complex_polynomial_coefficient_bound_of_integer_grid (f : Polynomial ℂ) {d : ℕ} (hd : f.natDegree ≤ d) {H : ℝ} (hH : 0 ≤ H) (heval : ∀ i ≤ d, ‖Polynomial.eval (↑i) f‖ ≤ H) (k : ℕ) : ‖f.coeff k‖ ≤ 3 ^ d * H

CCDN Lemma 3.4.1 in coefficientwise form, with the exact factor 3^d.

theorem CCDN.exists_complex_integer_grid_height_witness (f : Polynomial ℂ) {d : ℕ} (hd : f.natDegree ≤ d) : ∃ a ≤ d, ∀ (k : ℕ), ‖f.coeff k‖ ≤ 3 ^ d * ‖Polynomial.eval (↑a) f‖

One bounded integer evaluation controls every coefficient simultaneously.