theorem AnalyticNumberTheory.LargeSieve.eq21FiniteScalar_tail_eventually (C : ℝ) (n : ℕ) (hC : 0 < C) : ∀ᶠ (u : ℝ) in Filter.atTop, ∀ (N : ℕ), u ≤ ↑N → C * Real.exp (1 + √u) * (u ^ (11 / 10) / u ^ 2) ^ N * u ^ n ≤ 1

The complete smoothing order pays both right-line tails and finite horizontal edges at T=u². The threshold precedes N; no finite-order scan is used.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_finite_tail_eventually (C : ℝ) (n : ℕ) (hC : 0 < C) : ∀ᶠ (x : ℕ) in Filter.atTop, C * Real.exp (1 + √(Real.log ↑x)) * (chen1973PerronScale ↑x / Real.log ↑x ^ 2) ^ (chen1973PerronOrder ↑x + 1) * Real.log ↑x ^ n ≤ 1

Tail payment uses the actual Perron floor, uniformly before all cells.

noncomputable def AnalyticNumberTheory.LargeSieve.eq21FiniteScalarMbar (u : ℝ) : ℝ

The finite-disk derivative bound after the conductor cap.

Equations

• AnalyticNumberTheory.LargeSieve.eq21FiniteScalarMbar u = 20 * √u * (Real.log 32 + 205 / 2 * Real.log u)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_finite_left_budget_eventually : ∀ᶠ (x : ℕ) in Filter.atTop, ∀ (σ : ℝ), 1 / 2 ≤ σ → eq21FiniteScalarMbar (Real.log ↑x) * (σ⁻¹ + Real.log (Real.log ↑x ^ 2)) ≤ Real.log ↑x / 3

The short left segment, unlike the right tails, needs the sharper sqrt(u) log(u) derivative budget. Its cutoff precedes the contour real part.