The four prime-argument contributions assembled with uniform constants

theorem NairTenenbaum.exists_primeIntegerSum_mainTerm_bound {g : ℕ} (hg : 0 < g) {A B ε σ c : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hσ : 0 < σ) (hσsmall : ↑g ^ 2 * σ ≤ 1 / 8) (hc : 0 ≤ c) (hmargin : c * σ ≤ 17 * ↑g * ε / 24) : ∃ (x₀ : ℝ), 1 < x₀ ∧ ∃ (C : ℕ → ℝ), (∀ (D : ℕ), 0 < C D) ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → Polynomial.eval 0 P.total ≠ 0 → ∀ (F : ArithmeticMap k), Admissible A B σ F → ∀ (x y : ℝ) (a b : ℤ), x₀ ≤ x → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → ↑b - ↑a ≤ 2 * y → (∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) → P.primeIntegerSum F x a b ≤ C P.badDiscriminant * primeMainTerm P F x y