Documentation

MathlibNt.AnalyticNumberTheory.BombieriVinogradov.Bombieri1965Richert418Unconditional

Unconditional modern producer for Richert (4.18) #

The proved fixed-witness Siegel theorem supplies the actual low-conductor primitive character estimate. The existing large-sieve/Vaughan argument and literal logarithmic-integral comparison then give the maximal prime-AP estimate. No analytic source proposition is assumed.

This is a modern replacement proof, not a transcription of Bombieri's Theorem 5 density argument or of an uninspected Prachar proof.

The exact raw interface is supplied by the proved, conductor-uniform quadratic L-value theorem.

The genuine nonprincipal primitive low-conductor Siegel--Walfisz input, with the smoothing function constructed rather than postulated.

Richert's exact nested integer-prefix and reduced-residue maximum, with li(x) = integral_2^x dt/log(t) and the full stated modulus range.