Back to all results
certificate C-0045

The sharp Rosser--Schoenfeld weighted-prime-sum upper coefficient

For $S(x)=\sum_{p\leq x}(\log p)/p$, the exact upper coefficient in the Rosser--Schoenfeld formula on $x\geq319$ is attained uniquely at $x=467$. A separate splice of finite-range positivity with a global analytic estimate gives a lower coefficient $C_{\rm low}<1/221$ for every real $x>1$.

\[C_{\rm up}=0.492206382859887\ldots,\qquad C_{\rm low}=0.004513569432713\ldots\]
Download PDF LaTeX source Verifier bundle

Upper and lower statements

The constant $B_3$ centers the weighted prime sum around its main term $\log x$. The claim treats the two signed errors separately: an exact same-range upper optimum and a non-optimal global lower coefficient.

\[S(x)=\sum_{p\leq x}\frac{\log p}{p},\qquad B_3=\gamma+\sum_p\frac{\log p}{p(p-1)}\]
\[S(x)\leq\log x-B_3+\frac{C_{\rm up}}{\log x}\qquad(x\geq319)\]
\[S(x)>\log x-B_3-\frac{C_{\rm low}}{\log x}\qquad(x>1)\]

Upper normalization

Multiplying the upper error by $\log x$ converts the coefficient problem into maximizing a function that is smooth between prime jumps. On such an interval the weighted prime sum is constant.

The derivative is negative at the composite endpoint $319$ and after every later checked prime. Thus the only candidates are $x=319$ and the values immediately after prime jumps.

\[F(x)=\log x\left(S(x)-\log x+B_3\right)\]
\[F'(x)=\frac{S(x)+B_3-2\log x}{x}\]

Unique upper maximum

The finite comparison identifies $x=467$ as the unique maximizer. It lies only about $6.85\times10^{-5}$ above the endpoint value at $319$, so the endpoint comparison is one of the load-bearing numerical checks.

Beyond $912560$, Dusart's estimate bounds the normalized upper error by $0.3/\log x$, which is below $0.022$ at the handoff and then decreases.

\[C_{\rm up}=F(467)=0.4922063828598873676216976896219548566\ldots\]
\[\left|S(x)-\log x+B_3\right|\leq\frac{0.3}{\log^2x}\qquad(x\geq912560)\]
\[F(467)-F(319)>6.8\times10^{-5}\]
  1. Prove decrease on each prime-free interval.
  2. Compare the endpoint and every finite prime jump.
  3. Separate the candidate from the analytic tail.

Global lower splice

Rosser and Schoenfeld proved $S(x)>\log x-B_3$ through $10^8$, so the desired negative lower allowance is automatic there. Axler's global estimate supplies the tail.

After factoring out $1/\log x$, the remaining coefficient function is decreasing. Its endpoint value at $10^8$ is $C_{\rm low}$, which gives a strict bound beyond the splice.

\[S(x)-\log x+B_3\geq-\frac3{40\log^2x}-\frac3{20\log^3x}\]
\[g(L)=\frac3{40L}+\frac3{20L^2},\qquad C_{\rm low}=g(\log10^8)\]
\[C_{\rm low}=0.004513569432713956030838616810073784\ldots<\frac1{221}\]

Certificate role

The certificate encloses $B_3$ through a Mobius-inverted zeta-derivative series with an explicit omitted tail. It enumerates the primes through $912560$, certifies the inter-prime derivative signs, proves the unique finite maximum at $467$, and checks the Dusart tail margin.

It also evaluates the lower splice coefficient and proves $C_{\rm low}<1/221$. The cited source theorems, their ranges, and the symbolic monotonicity of the lower coefficient function remain analytic inputs to the written proof.

\[B_3=\gamma+\sum_{m=2}^{\infty}\mu(m)\frac{\zeta'(m)}{\zeta(m)}\]
\[C_{\rm up}<0.492207<\frac12,\qquad C_{\rm low}<\frac1{221}\]

Pinned certificate

The pinned certificate rigorously encloses B3, checks every finite prime-jump and derivative comparison needed for the unique upper maximum at x=467, separates the Dusart tail, and certifies the lower splice constant and its 1/221 rounding.

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

Scope

The upper coefficient is sharp on $x\ge319$ for the stated $1/\log x$ formula; the lower coefficient is a certified global value for the companion formula.

Sources

  • Canonical claimcanon/claims/C-0045-sharp-rosser-schoenfeld-weighted-prime-sum-coefficients.md
  • Pinned certificate notecanon/witnesses/C-0045/PIN.md
  • Certificate sourceexperiments/weighted_prime_sum_rs_coefficients/verify.py