theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_all_level_actual_cell_small_of_fixedQuadraticL1 (ε : ℝ) (hε : 0 < ε) (hεu : ε < 1 / 10) (c : ℝ) (hc : 0 < c) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (L B lastD level k m : ℕ), 0 < L → 0 < B → ↑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 - ε) → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d), ↑χ ^ 2 = 1 → c * ↑d ^ (-(1 / 10000)) ≤ (chen1973Lemma6PrimitiveLValue d 1 χ).re) → chen1973Lemma6NmBlockActual x L level B k m ≤ C * ↑x / Real.log ↑x ^ 20

All actual levels, with the finite-height repair at zero and the corrected positive-level argument. The fixed-c raw quadratic L(1) premise is explicit.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_all_level_actual_cell_small_of_rawLandauSiegel (hLS : RawLandauSiegelLowerBound) (ε : ℝ) (hε : 0 < ε) (hεu : ε < 1 / 10) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (L B lastD level k m : ℕ), 0 < L → 0 < B → ↑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

Existing raw Landau--Siegel data suffice for the source objects at all levels. This consumes the input; it does not prove the raw lower bound.