OAI/NumberTheory/Ostmann/ZeroDensity/PublishedSmoothExplicitFormula.lean

The published smooth explicit formula, for one fixed test function

H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I (2007), Chapter 10: the functional equation, ordinary zero count and explicit formula. See also H. A. Helfgott, The ternary Goldbach problem, Part I (15 December 2019), §§3.7.1 and 3.7.3. We use only the fixed primeMeanTest, supported in [5/8,7/8]. Its Mellin transform has eighth-order decay in the fixed strip.

The formula shifts to Re(s)=-1/2, retaining the even-character residue at zero. Its error has no dependence on an exceptional zero's distance from 1. The count is the ordinary individual zero count summed over a finite primitive family; there are at most Q² Dirichlet characters of conductor ≤Q. This input contains no prime-average or favorable-prime conclusion.