\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,microtype}
\usepackage[colorlinks=true,linkcolor=black,urlcolor=black]{hyperref}
\usepackage{enumitem}
\setlength{\parindent}{0pt}
\setlength{\parskip}{0.7em}
\title{The sharp Rosser--Schoenfeld weighted-prime-sum upper coefficient}
\author{Kenan}
\date{2026-07-19}

\begin{document}
\maketitle

\begin{abstract}
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$.
\end{abstract}

\[
C_{\rm up}=0.492206382859887\ldots,\qquad C_{\rm low}=0.004513569432713\ldots
\]

\section{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)
\]
\section{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}
\]
\section{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}
\]

\begin{enumerate}[leftmargin=*]
\item Prove decrease on each prime-free interval.
\item Compare the endpoint and every finite prime jump.
\item Separate the candidate from the analytic tail.
\end{enumerate}
\section{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}
\]
\section{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}
\]

\section{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.

\subsection*{Run command}
\begin{verbatim}
uv run --frozen python canon/witnesses/C-0045/verify.py
\end{verbatim}

\subsection*{Pinned files}
\begin{itemize}[leftmargin=*]
\item \path{canon/witnesses/C-0045/verify.py}
\item \path{canon/witnesses/C-0045/PIN.md}
\end{itemize}

\section{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.

\section{Sources}
\begin{itemize}[leftmargin=*]
\item Canonical claim: \path{canon/claims/C-0045-sharp-rosser-schoenfeld-weighted-prime-sum-coefficients.md}
\item Pinned certificate note: \path{canon/witnesses/C-0045/PIN.md}
\item Certificate source: \path{experiments/weighted_prime_sum_rs_coefficients/verify.py}
\end{itemize}

\end{document}
