Final low-only producer for Standard Bombieri--Vinogradov

The chosen high-conductor source is unconditional, so the final assembly retains only the genuine low-end input. At source level this is exactly the nonprincipal primitive Siegel--Walfisz source together with the modulus-one global principal PNT source.

theorem AnalyticNumberTheory.LargeSieve.standardBombieriVinogradov_of_lowSiegelWalfiszSource (hlow : StandardBVLowSiegelWalfiszSource) : MathlibNt.SieveTheory.BombieriVinogradov.StandardBombieriVinogradov

Once the low Siegel--Walfisz contract is supplied, the unconditional chosen high source closes Standard Bombieri--Vinogradov.

theorem AnalyticNumberTheory.LargeSieve.standardBombieriVinogradov_of_nonprincipalPrimitivePsi_lowOnly (hSW : NonprincipalPrimitivePsiSiegelWalfiszSource) (hPNT : GlobalChebyshevToLiPrincipalPNTSourceContract) : MathlibNt.SieveTheory.BombieriVinogradov.StandardBombieriVinogradov

Final source-level low-only producer. There is no historical Vaughan-row premise: the high source is standardBVHighChosenUnconditional.