A finite family of distinct coordinate vectors is separated by a bounded integer linear form on the moment curve (1,t,...,t^(n-1)). The proof avoids an unquantified genericity argument.

theorem CCDN.polynomial_exists_small_nat_eval_ne_zero {K : Type u_1} [Field K] [CharZero K] (P : Polynomial K) (hP : P ≠ 0) : ∃ k ≤ P.natDegree, Polynomial.eval (↑k) P ≠ 0

In characteristic zero, a nonzero polynomial P does not vanish at some natural number k ≤ P.natDegree.

theorem CCDN.exists_bounded_moment_nonvanishing {K : Type u_1} {ι : Type u_2} [Field K] [CharZero K] [Fintype ι] {n : ℕ} (v : ι → Fin n → K) (hv : ∀ (i : ι), v i ≠ 0) : ∃ k ≤ n * Fintype.card ι, ∀ (i : ι), ∑ j : Fin n, v i j * ↑k ^ ↑j ≠ 0

A moment form with parameter at most n times the number of directions is nonzero on all those directions.

theorem CCDN.exists_bounded_moment_separation {K : Type u_1} {ι : Type u_2} [Field K] [CharZero K] [Fintype ι] {n : ℕ} (v : ι → Fin n → K) (hv : Function.Injective v) : ∃ k ≤ n * Fintype.card ι ^ 2, Function.Injective fun (i : ι) => ∑ j : Fin n, v i j * ↑k ^ ↑j

Bounded integer moment-curve coefficients separate every pair of a finite family of distinct vectors.