theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_printedWidth_eventually {c : ℝ} (hc : 0 < c) : ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (L : ℕ), ↑L ≤ Real.log ↑x ^ 100 → Chen1973Lemma6Eq21ZeroFreeContourBridge x L c

The correctly transcribed exponent pays the source width for every later conductor and cell, with a cutoff depending only on the positive constant.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_actualShell_subset_primeRegion (x B k m : ℕ) : chen1973Lemma6PrimePairShell x B k m ⊆ chen1973Lemma6Eq21PrimeRegion x

The corrected printed region contains every actual source shell.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_source_analytic_inputs (Cvert c : ℝ) (hc : 0 < c) : ∃ (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), ∀ 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

Corrected transcription eliminates both the extra width bridge and the shell-region hypothesis. Full-height zero-freeness, boundary payments, and the primitive vertical estimate are still genuine inputs.