Raw Landau--Siegel lower bounds supply the low Siegel--Walfisz source

The quadratic and nonquadratic uniform pointwise estimates are combined at the same requested exponents and ambient endpoint. The finite pointwise-to-prefix amplitude bridge then supplies the exact low source used by Standard BV.

theorem AnalyticNumberTheory.LargeSieve.nonprincipalPrimitivePsiSiegelWalfiszSource_of_rawLandauSiegelLowerBound (hLandauSiegel : RawLandauSiegelLowerBound) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : NonprincipalPrimitivePsiSiegelWalfiszSource

A raw Landau--Siegel lower bound supplies the nonprincipal primitive prefix-amplitude Siegel--Walfisz source. The split is the literal dichotomy χ² = 1 versus χ² ≠ 1; both branches use one shared eventual endpoint and the common constant Kn + Kq.

theorem AnalyticNumberTheory.LargeSieve.standardBombieriVinogradov_of_rawLandauSiegelLowerBound (hLandauSiegel : RawLandauSiegelLowerBound) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : MathlibNt.SieveTheory.BombieriVinogradov.StandardBombieriVinogradov

Honest conditional Standard Bombieri--Vinogradov headline: after the fixed smoothing data, the only analytic hypothesis is the raw Landau--Siegel lower bound.