Back to all results
certificate C-0039

The sharp Rosser--Schoenfeld reciprocal-prime coefficient is 0.487203269718814...

Let $A_1(x)=\sum_{p\leq x}p^{-1}-\log\log x-B$, where $B$ is the Meissel--Mertens constant. On the fixed range $x\geq286$, the largest value of $A_1(x)\log^2x$ occurs uniquely at $x=286$. Its value is $C_*=0.487203269718814568\ldots$, giving the exact coefficient for the Rosser--Schoenfeld formula shape on that range.

\[A_1(x)\leq\frac{C_*}{\log^2 x}\ (x\geq286),\qquad C_*=0.487203269718814\ldots\]
Download PDF LaTeX source Verifier bundle

Statement and normalization

The reciprocal-prime Mertens error compares the partial sum of $1/p$ with its main term $\log\log x+B$. Multiplying the desired inequality by $\log^2x$ turns the coefficient question into a maximization problem for a normalized error.

Because there is no prime between $283$ and $293$, the value at the left endpoint uses the reciprocal-prime sum through $283$. The candidate coefficient is therefore an exact expression in that finite sum and the constant $B$.

\[A_1(x)=\sum_{p\leq x}\frac1p-\log\log x-B\]
\[C_*=A_1(286)\log^2 286=\left(\sum_{p\leq283}\frac1p-\log\log286-B\right)\log^2 286\]

Classical context

Rosser and Schoenfeld proved the same upper-bound shape with coefficient $1/2$ for every real $x\geq286$. The present statement keeps both that formula and that starting point, replacing only the coefficient.

A convenient rounded consequence is $C_*<121801/250000=0.487204<1/2$.

\[A_1(x)<\frac{1}{2\log^2x}\qquad(x\geq286)\]
\[A_1(x)<\frac{121801}{250000\log^2x}\qquad(x\geq286)\]

Reduction to prime jumps

Fix $C=C_*$ and subtract the comparison term. Between consecutive primes, the reciprocal-prime sum is constant, so the resulting function is differentiable and strictly decreasing on the entire range.

At a prime, $A_1$ jumps upward by $1/p$. It is therefore enough to compare the endpoint value with the normalized error immediately after every later prime jump. The value at $286$ is zero after subtraction, while all later checked jumps are negative.

\[D_C(x)=A_1(x)-\frac{C}{\log^2x}\]
\[D_C'(x)=\frac{-\log^2x+2C}{x\log^3x}<0\qquad(x\geq286)\]
  1. Establish strict decrease on each prime-free interval.
  2. Compare $C_*$ with every normalized prime-jump value from $p=293$ to the analytic handoff.
  3. Use a published tail estimate beyond the handoff.

Closing the infinite tail

The finite comparison ends at the threshold in Dusart's reciprocal-prime estimate. That estimate is stronger by one power of $\log x$ than the target shape, so after normalization its right-hand side decreases with $x$.

At the handoff the normalized tail bound is already more than $0.473$ below $C_*$. This closes every remaining real $x$ without further prime enumeration.

\[\lvert A_1(x)\rvert\leq\frac1{5\log^3x}\qquad(x\geq2\,278\,383)\]
\[A_1(x)\log^2x\leq\frac1{5\log x}<C_*\]

Pinned certificate

Directed 256-bit Arb arithmetic encloses the Meissel--Mertens constant, certifies the unique finite maximum at x=286 over every later prime jump through 2,278,383, and verifies that Dusart's normalized tail remains strictly below the candidate.

uv run --frozen python canon/witnesses/C-0039/verify.py
  • canon/witnesses/C-0039/verify.py
  • canon/witnesses/C-0039/PIN.md

Scope

The coefficient is exact for the upper reciprocal-prime error on the fixed range $x\ge286$ and the stated $C/\log^2x$ formula.

Sources

  • Canonical claimcanon/claims/C-0039-sharp-rosser-schoenfeld-mertens-coefficient.md
  • Pinned certificate notecanon/witnesses/C-0039/PIN.md
  • Certificate sourceexperiments/mertens_rs_sharp_coefficient/verify.py