theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_termVertical_integrable_of_logDerivative_bound {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hy : 0 < ↑x / (↑pp.1 * ↑pp.2)) {σ M : ℝ} (hσ : 0 < σ) (r : ℕ) (hderiv : ∀ (t : ℝ), ‖chen1973PrimitiveLDeriv d (↑σ + ↑t * Complex.I) χ / chen1973Lemma6PrimitiveLValue d (↑σ + ↑t * Complex.I) χ‖ ≤ M * (1 + Real.log (↑d * (1 + |t|))) ^ r) : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) σ) MeasureTheory.volume

Integrability on an arbitrary positive line from an actual pointwise bound.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_alphaTerm_integrable {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hy : 0 < ↑x / (↑pp.1 * ↑pp.2)) : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x)) MeasureTheory.volume

The right-line boundary integrability is unconditional on every source pair.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_logDerivative_and_horizontal {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) (t : ℝ), ‖chen1973PrimitiveLDeriv d (chen1973Lemma6Eq21Line x t) χ / chen1973Lemma6PrimitiveLValue d (chen1973Lemma6Eq21Line x t) χ‖ ≤ M * (1 + Real.log (↑d * (1 + |t|))) ^ r) → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d), ∀ pp ∈ chen1973Lemma6PrimePairShell x B k m, ∃ (C : ℝ), 0 ≤ C ∧ ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)) → chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20

Source-level terminal with the vertical estimate and both vertical integrability premises removed. The full-height zero-free strip, the actual left-line logarithmic-derivative bound, and horizontal decay remain explicit.