theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_actualPhi_mul_eq_alphaTerm {x d : ℕ} (χ : PrimitiveCharacter d) (hd : 1 < d) (hx : 3 ≤ x) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = -(↑(1 / (2 * Real.pi)) * ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x) t)

The actual weighted source term equals the normalized signed alpha integral.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_actualPhi_mul_eq_neg_vertical_of_boundary {x L B k m l₂ d : ℕ} {c C : ℝ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) (hC : 0 ≤ C) (hleft : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x)) MeasureTheory.volume) (hhoriz : ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)) : chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = -chen1973Lemma6Eq21VerticalIntegral x d χ pp

Genuine source-term shift from the printed strip and explicit boundary payments. This does not infer the width bridge or the boundary estimates.

structure AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21TermBoundaryPayments (x d : ℕ) (χ : PrimitiveCharacter d) (pp : ℕ × ℕ) : Prop

Boundary estimates, not a contour-equality or level-zero conclusion.

• left_integrable : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x)) MeasureTheory.volume
• right_integrable : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x)) MeasureTheory.volume
• horizontal_decay : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primitiveShift_of_boundary {x L B k m l₂ : ℕ} {c : ℝ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hboundary : ∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d), ∀ pp ∈ chen1973Lemma6PrimePairShell x B k m, Chen1973Lemma6Eq21TermBoundaryPayments x d χ pp) : Chen1973Lemma6Eq21PrimitiveAlphaToLeftShift x L B k m

The termwise shift is derived, rather than assumed, from the genuine zero-free strip and its boundary payments.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_boundary_inputs (Cvert : ℝ) : ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (L B k m l₂ : ℕ) (c : ℝ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → chen1973Lemma6PrimePairShell x B k m ⊆ chen1973Lemma6Eq21PrimeRegion x → Chen1973Lemma6Eq21ZeroFreeInput x L c → Chen1973Lemma6Eq21ZeroFreeContourBridge x L c → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d), ∀ pp ∈ chen1973Lemma6PrimePairShell x B k m, Chen1973Lemma6Eq21TermBoundaryPayments x d χ pp) → Chen1973Lemma6Eq21PrimitiveVerticalEstimate Cvert x L B k m → chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20

Uniform actual-cell consequence. The width comparison, boundary estimates, and vertical estimate remain genuine analytic hypotheses; neither a termwise shift equality nor the terminal cell bound is assumed.