Equation (21): genuine horizontal boundary decay

The sole quantitative analytic input is a pointwise bound for the actual L'/L quotient throughout the closed strip. This file does not prove that input. The smoothing-order condition is explicit and may be paid eventually by a caller. Constants may depend on this fixed cell.

Writing a = PerronScale x, N = PerronOrder x + 1, σ = Eq21Sigma x, α = Alpha x, and y = x/(p₁p₂), the proof constructs K = 2 * (σ⁻¹ + a^N) * (2*d)^r, B = (M*y^α)*K, and C = 2*B*(α-σ). The coarse inequality 1 + log z ≤ z suffices because no conductor-uniform constant is requested.

Horizontal integrability is proved separately using measurability and the pointwise majorant on a finite interval. Thus no nonintegrability/zero-integral convention is used, and no extra zero-free hypothesis is necessary here. The existing contour deformation still requires its own genuine zero-free input; this result does not discharge it.

theorem AnalyticNumberTheory.LargeSieve.eq21_horizontal_log_bound {d t : ℝ} (hd : 1 ≤ d) (ht : 0 ≤ t) : 0 ≤ 1 + Real.log (d * (1 + t)) ∧ 1 + Real.log (d * (1 + t)) ≤ 2 * d * max 1 t

A deliberately coarse conductor-dependent logarithmic bound.

theorem AnalyticNumberTheory.LargeSieve.eq21_horizontal_weightedKernel_bound {x : ℕ} (hx : 3 ≤ x) {σ u d : ℝ} (hσ : 0 < σ) (hu : σ ≤ u) (hd : 1 ≤ d) (r : ℕ) (horder : r + 1 ≤ chen1973PerronOrder ↑x + 1) (t : ℝ) : ‖chen1973MellinKernel (↑x) (↑u + ↑t * Complex.I)‖ * (1 + Real.log (d * (1 + |t|))) ^ r ≤ 2 * (σ⁻¹ + chen1973PerronScale ↑x ^ (chen1973PerronOrder ↑x + 1)) * (2 * d) ^ r / (1 + t ^ 2)

Full true kernel power, reduced to a square tail only after paying the polynomial weight. The small-height estimate uses the positive real part.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_term_pointwise_decay_of_strip_logDerivative {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hy : 1 < ↑x / (↑pp.1 * ↑pp.2)) {M : ℝ} (hM : 0 ≤ M) (r : ℕ) (horder : r + 1 ≤ chen1973PerronOrder ↑x + 1) (hderiv : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x → ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M * (1 + Real.log (↑d * (1 + |s.im|))) ^ r) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ u ∈ Set.Icc (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x), ∀ (t : ℝ), ‖chen1973Lemma6Eq21TermShiftIntegrand x d χ pp (↑u + ↑t * Complex.I)‖ ≤ B / (1 + t ^ 2)

Actual integrand pointwise decay on the whole strip. The character coefficient is bounded by one, never silently deleted.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_horizontal_measurable {x d : ℕ} (hd : 1 < d) (χ : PrimitiveCharacter d) (pp : ℕ × ℕ) (t : ℝ) : Measurable fun (u : ℝ) => chen1973Lemma6Eq21TermShiftIntegrand x d χ pp (↑u + ↑t * Complex.I)

Each actual horizontal section is measurable. This uses the entire nonprincipal L-function and its measurable derivative, not zero integral conventions. Nonvanishing is not needed for this measurability fact.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_horizontal_integrable_and_decay_of_strip_logDerivative {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hy : 1 < ↑x / (↑pp.1 * ↑pp.2)) {M : ℝ} (hM : 0 ≤ M) (r : ℕ) (horder : r + 1 ≤ chen1973PerronOrder ↑x + 1) (hderiv : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x → ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M * (1 + Real.log (↑d * (1 + |s.im|))) ^ r) : (∀ (t : ℝ), IntervalIntegrable (fun (u : ℝ) => chen1973Lemma6Eq21TermShiftIntegrand x d χ pp (↑u + ↑t * Complex.I)) MeasureTheory.volume (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x)) ∧ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)

The two genuine horizontal integrals are integrable, and their oriented bottom-minus-top difference has square decay. The conclusion carries the factor two for the two edges and their actual length. No horizontal bound or integrability premise is assumed.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_horizontal_decay_of_strip_logDerivative {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hy : 1 < ↑x / (↑pp.1 * ↑pp.2)) {M : ℝ} (hM : 0 ≤ M) (r : ℕ) (horder : r + 1 ≤ chen1973PerronOrder ↑x + 1) (hderiv : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x → ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M * (1 + Real.log (↑d * (1 + |s.im|))) ^ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)

The exact horizontal_decay output consumed by the contour bridge.