Fixed polynomial-value and prime-cutoff constants for Theorem 2

theorem NairTenenbaum.exists_theoremTwo_value_cutoff {Q : Polynomial ℤ} {k : ℕ} (hk : Q.natDegree < k) : ∃ (A : ℝ) (C : ℝ), 1 ≤ A ∧ 1 ≤ C ∧ A < C ^ k ∧ (2 ≤ k → 2 * A < C ^ (k - 1)) ∧ ∀ (x : ℝ), 1 ≤ x → have y := x ^ (↑Q.natDegree / ↑k); ∀ n ∈ shortInterval x y, ↑(Polynomial.eval (↑n) Q).natAbs ≤ A * y ^ k