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.
Once the low Siegel--Walfisz contract is supplied, the unconditional chosen high source closes Standard Bombieri--Vinogradov.
Inspect dependencies
AnalyticNumberTheory.LargeSieve.standardBombieriVinogradov_of_lowSiegelWalfiszSource · compiled type and proof/definition references.
Final source-level low-only producer. There is no historical Vaughan-row
premise: the high source is standardBVHighChosenUnconditional.
Inspect dependencies
AnalyticNumberTheory.LargeSieve.standardBombieriVinogradov_of_nonprincipalPrimitivePsi_lowOnly · compiled type and proof/definition references.