bibkey: broadbent2026mertens authors: Samuel Broadbent, Andrew Fiori, Habiba Kadiri, Nathan Ng, Kirsten Wilk year: 2026 title: Bounds for Mertens sums doi: null url: https://arxiv.org/abs/2608.01498v1 claim: Weighted Mertens estimates supply the higher-prime-power derivative budget. The entire-xi account and classical Stechkin comparison retain a positive fraction of the shifted Gamma energy in the logarithmic upper budget; the same-test primary-prime comparison remains unresolved. strata_touched: [] license: citation-only triage: anchor
Weighted Mertens input and the Weil prime-power budget
This is a paper-level application of classical weighted Mertens asymptotics and existing effective estimates. It is not a new prime-distribution theorem, a priority claim, or a compiled Lean result. The Mertens and prime-counting statements and their indicated constants were inspected on 1 October 2026; neither preprint’s complete proofs or table-generating computations were independently rerun.
Exact source and error moment
Broadbent–Fiori–Kadiri–Ng–Wilk, arXiv:2608.01498v1, printed pp.1–2, equations (2) and (6), identify
For put
Theorem 3(ii), equation (18), printed p.4, and Table 5, printed p.42, give
Thus the required moment is supplied directly by an existing Mertens bound. For an explicit coarse finite-interval bound, : use , , and . Also by harmonic-sum comparison, so . Consequently, using the external Table 5 constant,
Theorem 3(i)’s printed exponential rate differs from the used in its proof; its prefactor also differs from equation (150)’s . Neither exponential version is used here.
An alternative explicit supplier, independent of that Table 5 value, is Fiori–Jaskari, arXiv:2609.23222v1. Theorem 1.1, printed p.3, applies for ; Table 1, printed p.4, gives . With
its estimate implies for : use and . For , the elementary higher-power comparison gives
Equation (137) of the Mertens source, extended below by partial summation, is
Tonelli therefore yields the alternative budget
For the last comparison, follows by an exact rational fifth-power comparison, and suffices. This alternative still uses the Fiori–Jaskari theorem and its Table 1 constant as external inputs. It does not certify either source’s computations. The weaker row in the Dusart note alone does not supply this weighted moment.
Application to every compact smooth test
Let , without an evenness, normalization or nonnegativity assumption. Set
The sum defining has finitely many nonzero terms by compact support. The series defining and converge absolutely. The common-test estimate is
Here is a complete paper derivation. The real autocorrelation is even, with
The last inequality follows by integration by parts and Cauchy–Schwarz. Thus and .
For the square contribution, Stieltjes integration from gives the exact identity
Since and , there is no omitted prime-2 endpoint correction. The last remainder term, including its factor , has absolute value at most . For , the quadratic autocorrelation bound gives
Primewise geometric summation shows , proving (1). No pointwise positivity of is used; for complex or sign-changing tests it can be negative.
The higher-power remainder has a definite sign. Write . The identity gives
This energy sum generally has infinitely many nonzero terms but converges absolutely, even though the correlation sum is finite; its convergent constant part supplies the tail. It satisfies . Hence the error has the sharper asymmetric bound
In the full form, . The energy is an independently nonnegative contribution; the remaining integral keeps its unknown sign.
For a simple explicit constant, gives . Comparison on each gives
Hence . With the alternative supplier one may use in place of . This constant is deliberately coarse. The sharper Table 5 route is not needed for it.
For fixed with and , (1) specializes to
Mean zero removes the linear term, not the constant. The square part alone then tends to . For the combined constant, primes 2 and 3 already give , using , , , and .
Reuse and remaining boundary
The project’s Mertens estimates already supply the correction-series summability and a bounded first-Mertens error. Its log-zeta source contains a private general logarithmic-moment summability lemma. Mathlib supplies prime-power reindexing and the finite part of at , after subtracting . These are reusable inputs, not new declarations to wrap. The inspected bounded first-Mertens statement alone does not identify or prove ; the external suppliers above fill those paper-level premises.
The earlier triangular-kernel account already treats a prime-square correction with a different kernel and scaling. Equation (1) specifies the current smooth autocorrelation, norm and uniformity; no priority claim follows from changing that formulation.
In the full Weil form the contribution is . Omitting higher prime powers on the ground that their ordinary counting mass is therefore loses the displayed linear and scalar terms in this normalization. Equation (1) is uniform in support and coefficients with its derivative-norm weight. The complementary logarithmic budget below uses a different supplier. Neither supplies a sign bound for the remaining primary-prime/continuum discrepancy. The actual localization residual retains that separate obligation. No all-support positivity, Robin inequality or RH conclusion has been established here.
An upper budget in the actual logarithmic Gamma energy
Keep every definition of the same compact smooth complex above. The following is a paper application of classical Hadamard and Gamma identities, with their specific boundary pairing made explicit. It is not a new Hadamard theorem, a priority claim, or a Lean-verified estimate. In particular the Mertens derivative estimate is reused rather than proved again.
Fix the angular Fourier convention
Write for digamma and use the entire function
The removable value at one is understood. This is not the meromorphic completion used in the project’s XiLogDeriv. The entire reading has the appropriate pole removal. The existing normalized resolvent, xi_reading_normalized_resolvent_hasSum, supplies the global multiplicity-weighted sum of for every actual exhaustive injective ZeroData and nonzero entire reading, without RH. The first-Li normalization, first_li_coefficient_normalization, fixes the derivative at one. These are source-level reuse addresses, not a current build or a claim that the unnormalized positive-real series and the pairings below have already been compiled; no replacement Hadamard or normalized-resolvent implementation is needed.
An exact external Lean source for the real unnormalized series is Anthropic’s formal-math, commit fbdc36bbf17d20af3fd0447c6d1a8a02773c9844, zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean. In namespace Zeta23.XiPrime.ZeroFree, summable_re_one_div states absolute summability of the multiplicity-weighted real kernels, and re_logDeriv_xi_eq_tsum identifies their sum with for every with , including nonzero points inside the strip. The carrier is the actual nontrivial zero set of , with multiplicity zeroMult; despite the file’s XiPrime location, this series is not a sum over zeros of . The same file’s Zeta23.XiPrime.re_logDeriv_xi_pos states strict positivity for . The entire-function seam, xi_eq_weilXi' and xi_eq_Gammaℝ_mul_zeta, identifies the usual entire normalization.
This external source is Apache-2.0 licensed. Its pinned Lean version is v4.33.0-rc2 and its Mathlib revision is 51e6992efd06126df61a496bebf8f49482a4e129; the project pins are Lean v4.33.0 and Mathlib db584cd6d46c92f209a44c0f1c829460d327499d. The source statements and pins have been inspected, but the external project has not been built here and is not an admitted dependency. Reuse requires compatible dependency admission or an assessed selective port and identification with the local xiReading and zero carrier. The real resolvent formula is therefore existing mathematics with an external implementation, not a new theorem target. Its source alone supplies neither the Fourier boundary pairing below nor the unresolved same-test primary-prime comparison.
The source for that expansion is Lagarias, arXiv:math/0404394v4: the paragraph before Theorem 2.1 identifies ; Theorem 2.1(3), (4), (6), printed p.7, supplies the strict zero strip, counting estimate and order one; Lemma 4.1’s proof, printed p.14, supplies the Hadamard product and cancellation of its linear coefficient by the starred reciprocal-zero sum. The factor two leaves the logarithmic derivative unchanged. The inspected PDF has SHA-256 86f3d3c49f5a889f121bb1f04f67694cb9066dc8360f6988165788679594a4a7. These classical results are cited, not reproved or independently certified here.
The direct positive-logarithmic-derivative supplier is Matiyasevich–Saidak–Zvengrowski, Horizontal Monotonicity of the Modulus of the Riemann Zeta Function and Related Functions, arXiv:1205.2773v1, §2, the proof of Theorem 1.1, printed p.4. It displays the conjugate-paired Hadamard logarithmic-derivative series and its positive real summands to the right of all zeros. Its definition on printed p.2 is , equal to the entire above by Gamma recurrence. Its calculation has no height restriction; the height restrictions for its later and comparisons are not used. This known positivity is reused, not claimed as a new result.
Taking real parts of that expansion gives, for ,
Every zero is counted with its actual multiplicity. The real series is absolutely convergent; the strict strip makes each term positive. This uses no RH. The zero-counting estimate also gives .
The actual even-power boundary pairing
Let , a nonnegative Schwartz function, and put
For , absolute convergence in and Parseval give
The left side has finitely many nonzero correlations, so its limit is the actual sum of every even prime power. No ordinarily convergent undamped Dirichlet series on is asserted.
The regular-part pairing on the right also converges to its stated boundary value. Here is the needed uniform justification, which does not require a quantitative zero-free region. For and a real ordinate ,
where depends only on . For , split at . On the first region the kernel is at most ; on the second, and the full kernel integral is . For the same full integral and give a uniform bound. For each fixed zero, its width tends to the positive width . Equation (5) and reciprocal-square zero summability therefore allow the limit through the paired sum in (3).
The identity
reduces the remaining pairing to a bounded rational term and digamma. The classical digamma asymptotic, DLMF 5.11.2, gives logarithmic growth uniformly in , so Schwartz decay dominates these terms. Thus
The pole is accounted for separately:
Its factor two in (4), followed by , contributes exactly . In particular the pole is not absorbed into the regular multiplier or silently discarded.
Positive residual accounting
The remaining odd powers have an absolutely and uniformly convergent series
Combining (4)–(6) with these odd powers identifies the actual residual as
Use the shifted energy appearing in the full-form account,
The existing Gamma energy decomposition supplies the unshifted representation for its bundled even tests. Here its paper-level Fourier calculation is used for a general compact smooth complex ; Parseval and Tonelli apply to the nonnegative translation energy without an evenness restriction. The kernel difference and the digamma recurrence give , where . The classical duplication and reflection formulas give
Consequently, with and
the exact multiplier identity is
Pairing with the same yields the paper-level decomposition
All three contributions are nonnegative and finite. For , use (3) and (5). For the odd energy, . For , its multiplier is bounded and nonnegative because
Thus (8) supplies the upper budget
It is uniform over all compact supports and complex coefficients. The logarithmic energy replaces the derivative expense on the upper side needed by the full form. The original two-sided derivative estimate remains useful on slow dilations and is not superseded by a two-sided logarithmic claim.
This pairing argument and its all-test application have not been compiled in Lean. The original-source Hadamard expansion and classical Gamma identities are reused inputs; the displayed accounting is a repository synthesis with no claim of worldwide novelty. No extension beyond the stated compact smooth core is asserted without an additional domain argument.
Retaining a Gamma fraction by the classical Stechkin comparison
Kadiri, Explicit zero-free regions for Dedekind zeta functions, arXiv:1106.1868v1, printed p.4, equation (2.2), fixes
The constant is distinct from the Mertens constant . The definition on printed p.5 and Lemma 2.1, equation (2.15), printed p.8, give
The source’s standing range suffices for the limit used here. Equation (2.15) has no requirement ; that condition belongs to the separate equation (2.16), which is not used. Kadiri attributes the lemma to Stechkin, Zeros of the Riemann zeta-function, Mat. Zametki 8 (1970), 419–429, English translation Math. Notes 8, 706–711. The inspected Kadiri PDF has SHA-256 8c20f3fc7b27d080e97b1304bcf95f54cbf5905fba59fbf1a3f0dc4d3e78d368. This is a source application of a published inequality, not a new zero-comparison theorem or a certification of either source’s proof.
Write and . The reflected zero has the same real ordinate . Reflection preserves actual multiplicities, so half of the full reflected sum gives by (3), including zeros on the critical line. Sum (10) using the already supplied absolute convergence. Continuity of the entire- logarithmic derivative on the zero-free line , including its removable value at one, then yields
The auxiliary golden line is a parameter in the classical Stechkin comparison. Its appearance is not a proved FIB ATOM-to-prime intertwiner. No fixed-width zero-count estimate or new boundary-pairing argument is needed for (11).
To match the actual shifted energy, put . The classical digamma series, DLMF 5.7.6, gives, for ,
Each summand increases with and decreases with . Thus
On the auxiliary line, define
Here and . The absolutely convergent logarithmic derivative of the Euler product, entirely in , gives
Subtract the entire- logarithmic-derivative identity at from the one at . This keeps both the rational terms and the Gamma frequency:
Since (3) gives , equations (11)–(12) and imply the pointwise bound
Pair (13) with the same nonnegative and angular measure . The previously identified energy multiplier and Parseval give
Consequently (8), retaining the independent odd and rational energies, gives
Dropping the last two terms preserves an upper bound. Equations (14)–(15) hold at paper level for every , with no fixed support, parity, mean or frequency restriction. They strengthen only the upper budget; the two-sided derivative estimate is still available independently. They do not supply the remaining signed primary-prime/pole comparison, an all-test positivity result, Robin’s inequality or RH. The parameter application has not been compiled in Lean and is not presented as a new formal declaration.
Squarefree prime-shift geometry: two printed obstruction gaps
Luca Eliseo Pavesi’s sixth-revision preprint, Prime-shift operators on
Björner’s complex of squarefree integers: an exact decomposition of the
Mertens invariant, exact kernel asymptotics, rigorous recovery bounds for
the Guinand–Weil pipeline, and a structural obstruction to the spectral
modification, is identified by Zenodo record 22831623,
published 18 September 2026. The inspected PDF has 22 pages, SHA-256
d08f8f9855ebe3c2a2b1995bc2ff0d6b74a79c42b976d52f54e987dbb8ed5f9c,
and MD5 matching the publisher record. The locators below use printed
pages. The inspected interfaces are the unsigned shifts in §2.1, p.4;
Proposition 3.4 and Remark 3.5, p.6; the kernel representation in §5.1,
pp.9–10; and the two advertised spectral obstructions in §7, pp.13–14.
No whole-paper proof audit, reproduction of rank or zero computations,
peer-review claim, or Lean verification is supplied.
The uniform norm premise has a smaller valid range
The source’s carrier has orthonormal basis indexed by squarefree , including . Its actual unsigned operations are
Write for . Proposition 7.1, printed p.13, claims for that
The prime series is finite only for . The source’s own Proposition 3.4 uses that correct range; Remark 3.5 explicitly states when . Thus the compact-support argument cannot use (S1) as a finite uniform budget throughout its printed range.
There is also an actual operator lower bound, rather than merely a vacuous upper bound. Let and, for every , take the unit vector
For each , the operator pairs the divisors containing with those not containing it, wholly inside the cutoff. Its compression to this divisor span fixes . For , all nonzero images leave that span and have zero inner product with . Consequently
Classical divergence of , and for , show that, for every fixed , these norms tend to infinity as . In particular, the claimed uniform norm budget fails for . This calculation does not simultaneously diagonalize the truncated prime shifts; it uses only one supported vector and a Rayleigh quotient.
For , the source’s already supplied finite bound remains applicable. Divergence of the norms for does not decide the support of a weak limiting empirical measure: a small mass of escaping eigenvalues can coexist with a compactly supported weak limit. Neither spectral convergence to zeta zeros nor its general impossibility follows from (S2).
The projection in the source’s (30) is specifically onto . Self-adjointness gives , so . Removing the zero subspace changes the carrier or the normalization of a spectral measure, but this displayed compression leaves every nonzero eigenvalue unchanged. That is different from constructing a new spectral operator.
The displayed Gaussian prime term vanishes at small width
Proposition 7.4, printed p.13, asserts that the displayed contribution
is asymptotic to as . This claimed divergence is incompatible with (S3), including all its prime powers.
For , split the Gaussian into two equal exponent factors. The first is at most ; the second is at most . The constant
is finite. Indeed , and for , implies ; the resulting series converges. Hence the entire positive sum obeys
No numerical prime truncation or PNT estimate is needed for this bound. The statement that the sum is dominated by does not provide an asymptotic density near zero: once , there is no integer in that interval. Other terms of the explicit formula are separate contributions and cannot supply the claimed divergence of the particular prime sum (S3). Thus the printed second-moment obstruction cannot be imported through its asserted small-width asymptotic. This assessment does not certify or reject every other possible spectral comparison for these operators.
What remains to connect this geometry to the Robin source
The source’s and its squarefree-chain residual are different arithmetic quantities from and the same-source Robin integral. Its Proposition 5.1 labels its zero expansion formal and displays both the critical-line parametrization and weights . Those passages supply no replacement for the already available actual all-strip, multiplicity-preserving logarithmic-derivative formula. A uniform extension to all actual zeros, treatment of possible multiple zeros, and a quantitative transport to the Robin kernel would be additional obligations.
The first-175-zero exponent fits in the source are reported observations, not a uniform bound over all heights and all zeros. None of the two corrected obstruction interfaces above supplies a lower bound for at the selected integer. The original signed estimate and RH remain unproved. This is a paper-level source scope assessment and elementary counterestimate, not an originality claim or a new Hilbert–Pólya criterion.