theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_eventually_powerLoss_loglog_absorb (C : ℝ) (n : ℕ) {θ : ℝ} (hθ : θ < 1) : ∀ᶠ (x : ℕ) in Filter.atTop, C * Real.log ↑x ^ θ * (1 + Real.log (Real.log ↑x)) ^ n ≤ Real.log ↑x

A fixed sublinear log-power loss is still absorbed uniformly before cells.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primitiveVerticalEstimate_one_eventually_of_powerLoss {M θ : ℝ} (hM : 0 ≤ M) (hθ : θ < 1) (r : ℕ) : ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d) (t : ℝ), ‖chen1973PrimitiveLDeriv d (chen1973Lemma6Eq21Line x t) χ / chen1973Lemma6PrimitiveLValue d (chen1973Lemma6Eq21Line x t) χ‖ ≤ M * Real.log ↑x ^ θ * (1 + Real.log (↑d * (1 + |t|))) ^ r) → Chen1973Lemma6Eq21PrimitiveVerticalEstimate 1 x L B k m

Fixed sublinear loss: the cutoff remains before all cells.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_strip_powerLoss {M c θ : ℝ} (hM : 0 ≤ M) (hc : 0 < c) (hθ : θ < 1) (r : ℕ) : ∃ (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) (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x → ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M * Real.log ↑x ^ θ * (1 + Real.log (↑d * (1 + |s.im|))) ^ r) → chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20

Source-level equation (21) with a real sublinear log-power loss. All integral and geometric payments are internal; the full-height zero-free input and the displayed actual strip logarithmic-derivative bound remain.