theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation20_actual_cell_small (ε : ℝ) (hε : 0 < ε) (hεu : ε < 1 / 10) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ), Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑lastD ≤ ↑x ^ (1 / 2 - ε) → chen1973Lemma6NmBlockActual x L level B k m ≤ C * ↑x / Real.log ↑x ^ 20

Both actual complementary-cell integrals are paid at the same printed height. The cutoff is source geometry, not an analytic moment hypothesis.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_positive_level_actual_cell_small (ε : ℝ) (hε : 0 < ε) (hεu : ε < 1 / 10) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ), 0 < L → 0 < B → 1 ≤ level → ↑L ≤ Real.log ↑x ^ 100 → Real.log ↑x ^ 100 < ↑L + 1 → ↑B ≤ ↑x ^ (13 / 30) → ↑x ^ (13 / 30) < ↑B + 1 → L * 2 ^ level ≤ 2 * lastD → ↑lastD ≤ ↑x ^ (1 / 2 - ε) → chen1973Lemma6NmBlockActual x L level B k m ≤ C * ↑x / Real.log ↑x ^ 20

Uniform corrected-kernel estimate over every positive-level source cell. The branch split and Perron-order condition are derived internally. This does not cover the level-zero contour or assert the literal printed radial comparison.