theorem AnalyticNumberTheory.LargeSieve.fourFactor_nonprincipalPrimitivePsiSiegelWalfiszSource : NonprincipalPrimitivePsiSiegelWalfiszSource

The existing low source with its raw Siegel input now proved internally.

theorem AnalyticNumberTheory.LargeSieve.fourFactor_standardBombieriVinogradov : MathlibNt.SieveTheory.BombieriVinogradov.StandardBombieriVinogradov

Unconditional Standard BV through the preserved nonprincipal-primitive endpoint.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_all_level_actual_cell_small_unconditional (ε : ℝ) (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

All actual cells under the existing rounded parameters and conductor cutoff. The corrected positive-level kernel and finite-height level-zero repair are retained. This is not the final Chen prime theorem or a literal full-height contour claim.