The sifted large-prefix sum bounded by the original main term

theorem NairTenenbaum.exists_largePrefixSiftedSum_mainTerm_bound {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) : ∃ (K : ℝ) (x₀ : ℝ), 0 < K ∧ 1 ≤ x₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (A B σ : ℝ) (F : ArithmeticMap k), Admissible A B σ F → 0 ≤ A → 1 ≤ B → 0 < σ → ↑g ^ 2 * σ ≤ 1 / 8 → ∀ (x y : ℝ) (N : ℕ+) (a b : ℤ), x₀ ≤ x → ↑↑N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → ↑b - ↑a ≤ 2 * y → P.smallDivisorSiftedSum F N a b (x ^ (↑g * ε / 16)) ≤ K * smallDivisorSieveCost B σ g P.badDiscriminant * mainTerm P F x y

The sifted large-prefix sum is bounded by the paper's original main term. The constants precede the polynomial family and arithmetic function. The interval endpoint hypotheses allow the natural rounding of a real interval.