Common height and growth margins for Theorems 1 and 3

Only one eighth of a power is spent absorbing the degree-dependent evaluation constant. This leaves a positive saving at the paper's exponent εδ/3.

theorem NairTenenbaum.primeArgument_growth_margin {g : ℕ} (hg : 0 < g) {ε δ : ℝ} (hε : 0 ≤ ε) (hδ : 0 < δ) (hδ₁ : δ ≤ 1) : (↑g + 1 / δ + 1 / 8) * (ε * δ / 3) ≤ 17 * ↑g * ε / 24

theorem NairTenenbaum.eval_natAbs_le_primeArgument_rpow {Q : Polynomial ℤ} {g : ℕ} (hdeg : Q.natDegree = g) {x δ : ℝ} (hx : 1 ≤ x) (hδ : 0 < δ) (hheight : ↑(polynomialHeight Q) ^ δ ≤ x) (hlarge : ((↑g + 1) * 2 ^ g) ^ 8 ≤ x) {t : ℤ} (ht : ↑t.natAbs ≤ 2 * x) : ↑(Polynomial.eval t Q).natAbs ≤ x ^ (↑g + 1 / δ + 1 / 8)

theorem NairTenenbaum.exists_height_interval_threshold (g : ℕ) {δ τ : ℝ} (hδ : 0 < δ) (hτ : 0 < τ) (x₀ : ℝ) : ∃ (c₀ : ℝ), 0 < c₀ ∧ ∀ (Q : Polynomial ℤ), Q ≠ 0 → Q.natDegree = g → ∀ (x y : ℝ), c₀ * ↑(polynomialHeight Q) ^ δ < x → x ^ τ ≤ y → y ≤ x → x₀ ≤ x ∧ ↑⌊x⌋₊ ≤ ↑⌊x + y⌋₊ ∧ y / 2 ≤ ↑↑⌊x + y⌋₊ - ↑↑⌊x⌋₊ ∧ ↑↑⌊x + y⌋₊ - ↑↑⌊x⌋₊ ≤ 2 * y ∧ ∀ t ∈ Finset.Ioc ↑⌊x⌋₊ ↑⌊x + y⌋₊, ↑(Polynomial.eval t Q).natAbs ≤ x ^ (↑g + 1 / δ + 1 / 8)

One coefficient-independent threshold supplies the rounded interval and value bounds.