\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 global Rosser--Schoenfeld reciprocal-prime lower coefficient is below 1/306}
\author{Kenan}
\date{2026-07-19}

\begin{document}
\maketitle

\begin{abstract}
For $A_1(x)=\sum_{p\leq x}p^{-1}-\log\log x-B$, a positivity theorem through $10^8$ and a global large-$x$ estimate combine to give a lower bound of the Rosser--Schoenfeld form for every real $x>1$. The resulting coefficient is $C_0=0.003266913842984036606\ldots<1/306$.
\end{abstract}

\[
A_1(x)>-\frac{C_0}{\log^2x}>-\frac1{306\log^2x}\qquad(x>1)
\]

\section{Statement}

The claim concerns the lower side of the reciprocal-prime Mertens error on its full natural range. The coefficient is obtained by evaluating a decreasing tail coefficient at the splice point $10^8$.

\[
A_1(x)=\sum_{p\leq x}\frac1p-\log\log x-B
\]

\[
C_0=\frac1{20\log(10^8)}+\frac3{16\log^2(10^8)}
\]

\[
A_1(x)>-\frac{C_0}{\log^2x}>-\frac1{306\log^2x}\qquad(x>1)
\]
\section{Why a splice is available}

Rosser and Schoenfeld proved that $A_1(x)$ is positive for $1<x\leq10^8$. Any negative lower comparison of the stated form is therefore automatic on that entire interval.

For larger $x$, Axler's estimate supplies a lower bound with the stronger decay terms $\log^{-3}x$ and $\log^{-4}x$.

\[
A_1(x)>0\qquad(1<x\leq10^8)
\]

\[
A_1(x)\geq-\frac1{20\log^3x}-\frac3{16\log^4x}\qquad(x>1)
\]
\section{Tail normalization}

Write $L=\log x$ and factor the tail estimate into the desired $L^{-2}$ shape. The remaining coefficient function is strictly decreasing for $L>0$, so its largest value after the splice occurs at $L=\log(10^8)$.

For $x>10^8$ the inequality is strict because the coefficient function has already decreased below its endpoint value.

\[
g(L)=\frac1{20L}+\frac3{16L^2}
\]

\[
A_1(x)\geq-\frac{g(L)}{L^2},\qquad g'(L)=-\frac1{20L^2}-\frac3{8L^3}<0
\]

\[
g(\log10^8)=C_0
\]

\begin{enumerate}[leftmargin=*]
\item Use positivity on $1<x\leq10^8$.
\item Normalize Axler's tail estimate by $\log^2x$.
\item Apply monotonicity of $g$ beyond the splice.
\end{enumerate}
\section{Certificate role}

The pinned certificate evaluates $\log(10^8)$ and $C_0$ with directed 256-bit Arb arithmetic. It proves the strict rational comparison $C_0<1/306$, confirms that $1/307<C_0$, and verifies an improvement factor greater than $153$ relative to the earlier coefficient $1/2$.

The certificate does not encode the cited positivity theorem, Axler's analytic estimate, or the symbolic monotonicity argument. Those are the written proof obligations that connect the certified constants to the global theorem.

\[
\frac1{306}-C_0>1.0600\times10^{-6}
\]

\[
C_0-\frac1{307}>9.5848\times10^{-6}
\]

\section{Pinned certificate}
Directed 256-bit Arb arithmetic certifies the splice coefficient at log(10\textasciicircum{}8), its strict comparison with 1/306 and 1/307, and the improvement factor. The literature estimates and monotonicity remain explicit analytic inputs.

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

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

\section{Scope}
The result is a global lower bound in the fixed Rosser--Schoenfeld $C/\log^2x$ shape, obtained by splicing the stated published finite- and large-range estimates.

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

\end{document}
