Sieve levels at the small-divisor scales of the main proof

theorem NairTenenbaum.exists_sieve_scale_threshold {L α m d p e : ℝ} (hL : 1 ≤ L) (hα : 0 < α) (he : 0 < e) (hp : 0 ≤ p) (hgap : e + m + α * p ≤ d) : ∃ (x₀ : ℝ), 1 ≤ x₀ ∧ ∀ (x : ℝ), x₀ ≤ x → 2 ≤ x ^ α ∧ 16 ≤ Real.log (x ^ α) ∧ ∀ (N y z : ℝ), 0 ≤ N → N ≤ x ^ m → x ^ d ≤ y → 0 ≤ z → z ≤ x ^ α → L * N * z ^ p ≤ y / 2

A positive exponent gap pays the fixed sieve constant uniformly in every smaller cutoff. The same threshold supplies the logarithmic lower bound.

theorem NairTenenbaum.smallDivisor_scale_exponent {g : ℕ} (hg : 0 < g) (ε : ℝ) (hε : 0 ≤ ε) : 3 * ↑g ^ 2 * ε / 2 + ↑g * ε / 2 * (4 * ↑g * (1 + 1 / 16) + 1 / 4) + ↑g ^ 2 * ε / 4 ≤ 4 * ↑g ^ 2 * ε

The small-divisor and prime cutoffs leave a positive exponent gap beneath Theorem 1's lower bound on the interval length.

theorem NairTenenbaum.exists_smallDivisor_sieve_scales {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) {L : ℝ} (hL : 1 ≤ L) : ∃ (x₀ : ℝ), 1 ≤ x₀ ∧ ∀ (x : ℝ), x₀ ≤ x → 2 ≤ x ^ (↑g * ε / 2) ∧ 16 ≤ Real.log (x ^ (↑g * ε / 2)) ∧ ∀ (N y : ℝ), 0 ≤ N → N ≤ x ^ (3 * ↑g ^ 2 * ε / 2) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → L * N * (x ^ (↑g * ε / 2)) ^ (4 * ↑g * (1 + 1 / 16) + 1 / 4) ≤ y / 2

One uniform threshold makes the paper's two cutoffs satisfy the logarithmic and size conditions of the conditional sieve, including a factor two for passing to integer endpoints.

theorem NairTenenbaum.exists_smallDivisorSiftedSum_at_scales {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ) (x₀ : ℝ), 1 ≤ 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 * ε / 2) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → P.smallDivisorSiftedSum F N a b (x ^ (↑g * ε / 2)) ≤ K * smallDivisorSieveCost B σ g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total (x ^ (↑g * ε / 2)) * ∑ n ∈ Finset.Icc 1 N, P.weight F n

The small-divisor sum at the paper's scales, with constants chosen before all polynomial coefficients and the admissible arithmetic function.