The modern Bombieri producer in Richert's weighted source chain #
The unconditional modern Standard BV theorem discharges the distribution premise in the existing ordinary-to-weighted Richert argument. The two Jurkat--Richert Theorem A density lemmas remain explicit assumptions; neither the historical Bombieri density proof nor a generic sieve theorem is claimed.
Richert's actual varying-level weighted error bound, now with no
distribution hypothesis. The existing payment uses ordinary exponent
2 * A + 10 and retains the combined-modulus and coprimality restrictions.
Inspect dependencies
MathlibNt.SieveTheory.Bombieri1965RichertWeightedConsumer.chenWeightedBombieriVinogradov · compiled type and proof/definition references.
Only the lower and upper Jurkat--Richert Theorem A inputs remain in the Chen-facing weighted lower bound.
Inspect dependencies
MathlibNt.SieveTheory.Bombieri1965RichertWeightedConsumer.chenWeightedLowerBound_of_importedTheoremA · compiled type and proof/definition references.
The existing literal Richert source certificate with its ordinary BV premise discharged by the proved modern producer, not by an added axiom.
Inspect dependencies
MathlibNt.SieveTheory.Bombieri1965RichertWeightedConsumer.chenFacingSourceChainCertificate_of_importedTheoremA · compiled type and proof/definition references.