theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation20_actual_first_and_sharp_beta {x L B lastD level k m : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (ε : ℝ) : have H := chen1973Lemma6Equation20H x level k ε; have D := chen1973Lemma6Eq20SourceD L level; have Q := chen1973Lemma6Eq20SourceQ L level; chen1973Lemma6NmBlockActual x L level B k m ≤ 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq20CorrectedFirstIntegral x L level B k m H + 6 * Real.pi * ↑x ^ (1 / 2) * Real.log ↑x ^ (11 / 10) * chen1973Lemma6Eq20BetaLinearCoefficient x L level B k H D Q

The original complementary-cell cutoff feeds the new beta integral bound. The first integral is deliberately retained as an actual integral, not declared small.