A fixed lower cutoff for all large-prefix bands

theorem NairTenenbaum.exists_primeBand_lower_cutoff {g : ℕ} (hg : 0 < g) (κ : ℝ) : ∃ (w₀ : ℝ), 1 < w₀ ∧ ∀ (x α : ℝ), 0 < x → w₀ ≤ x ^ (2 * α) → 2 ≤ x ^ α ∧ 2 * ↑g ≤ x ^ α ∧ 16 ≤ Real.log (x ^ α) ∧ 8 * ↑g ^ 2 * κ ≤ Real.log (x ^ (2 * α))

A fixed cutoff on the upper edge of a band supplies every lower-cutoff condition in the sieve and moment estimates. It is independent of coefficients, discriminants, and the band index.

theorem NairTenenbaum.exists_primeBand_moment {g : ℕ} (hg : 0 < g) {ε A c : ℝ} (hε : 0 < ε) (hA : 1 ≤ A) (hc : 0 ≤ c) : ∃ (κ : ℝ), 0 < κ ∧ c * Real.log A + 4 * ↑g * Real.log 4 + 1 ≤ κ * (3 * ↑g ^ 2 * ε / 2) / 2

A moment strength with strictly positive decay margin always exists for the nonnegative polynomial-value exponent used in the main proof.

theorem NairTenenbaum.exists_largePrefixBands_mainTerm_bound {g : ℕ} (hg : 0 < g) {ε A c : ℝ} (hε : 0 < ε) (hA : 1 ≤ A) (hc : 0 ≤ c) : ∃ (K : ℝ) (x₀ : ℝ) (κ : ℝ) (w₀ : ℝ), 0 < K ∧ 1 ≤ x₀ ∧ 0 < κ ∧ 1 < w₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (B σ : ℝ) (F : ArithmeticMap k), Admissible A B σ F → 1 ≤ B → 0 < σ → ↑g ^ 2 * σ ≤ 1 / 8 → ∀ (x y u : ℝ) (N : ℕ+) (a b : ℤ) (J : Finset ℕ), x₀ ≤ x → 1 < x → 1 ≤ Real.log x → 0 < u → u ≤ 1 → u ≤ ↑g * ε / 16 → (∀ j ∈ J, w₀ ≤ x ^ (2 * (u / 2 ^ (j + 1)))) → ↑↑N ≤ x ^ (3 * ↑g ^ 2 * ε) → 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) → ∑ j ∈ J, P.smoothTailPrefixContribution F N (Finset.Icc 0 ⌊x ^ (2 * (u / 2 ^ (j + 1)))⌋₊) (x ^ (3 * ↑g ^ 2 * ε / 2)) a b (x ^ (u / 2 ^ (j + 1))) ≤ K * smoothTailSieveCost A B κ g P.badDiscriminant * mainTerm P F x y

All bands above a single fixed smoothness cutoff satisfy the summed main-term bound. The moment and cutoff are chosen before the polynomials.