\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 reciprocal-prime coefficient is 0.487203269718814...}
\author{Kenan}
\date{2026-07-19}

\begin{document}
\maketitle

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

\[
A_1(x)\leq\frac{C_*}{\log^2 x}\ (x\geq286),\qquad C_*=0.487203269718814\ldots
\]

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

\begin{enumerate}[leftmargin=*]
\item Establish strict decrease on each prime-free interval.
\item Compare $C_*$ with every normalized prime-jump value from $p=293$ to the analytic handoff.
\item Use a published tail estimate beyond the handoff.
\end{enumerate}
\section{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_*
\]

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

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

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

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

\section{Sources}
\begin{itemize}[leftmargin=*]
\item Canonical claim: \path{canon/claims/C-0039-sharp-rosser-schoenfeld-mertens-coefficient.md}
\item Pinned certificate note: \path{canon/witnesses/C-0039/PIN.md}
\item Certificate source: \path{experiments/mertens_rs_sharp_coefficient/verify.py}
\end{itemize}

\end{document}
