theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_order_eventually (r : ℕ) : ∀ᶠ (x : ℕ) in Filter.atTop, r + 1 ≤ chen1973PerronOrder ↑x + 1

Any fixed logarithmic growth degree is paid by the source smoothing order.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_strip_logDerivative {M c : ℝ} (hM : 0 ≤ M) (hc : 0 < c) (r : ℕ) : ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → Chen1973Lemma6Eq21ZeroFreeInput x L c → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d) (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x → ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M * (1 + Real.log (↑d * (1 + |s.im|))) ^ r) → chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20

Conditional source-level equation (21), with all integral payments internal. The pointwise quantitative hypothesis is on the entire source strip, which is stronger than a left-line bound. Neither it nor full-height zero-freeness is asserted unconditionally by this theorem.