\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{Axler's compact prime-counting denominator coefficient improves from 70.935 to 44.053}
\author{Kenan}
\date{2026-07-19}

\begin{document}
\maketitle

\begin{abstract}
For every real $x\ge29.53$, Axler's compact upper bound for $\pi(x)$ remains valid when the final denominator coefficient $70.935$ is replaced by $44.053$. The proof keeps the published denominator shape and range, establishes positivity of the denominator, bridges through $\operatorname{li}(x)$ on the low range, checks the published numerical error envelopes, and closes the asymptotic tail with a pinned absolute-error estimate.
\end{abstract}

\[
\pi(x)<\frac{x}{\log x-1-(\log x)^{-1}-3(\log x)^{-2}-44.053(\log x)^{-3}}\quad(x\ge29.53)
\]

\section{What is proved}

Let $L=\log x$. The new denominator is larger than Axler's published denominator because the subtracted coefficient is smaller, so its reciprocal gives a strictly smaller upper bound wherever both denominators are positive.

\[
\pi(x)<\frac{x}{L-1-L^{-1}-3L^{-2}-44.053L^{-3}},\qquad x\ge29.53
\]

\[
70.935-44.053=26.882
\]
\section{Denominator and li comparison}

Set $s_A(t)=1-t-t^2-3t^3-At^4$ with $A=44.053$. After dividing by $x/L$, the gap between the proposed reciprocal denominator and $\operatorname{li}(x)$ is expressed through $s_A(1/L)$ and the exponential integral.

The certificate proves both the new and published denominators are positive at the lower endpoint and remain positive thereafter. It then covers $3.385\le L\le10$ by 16384 directed rational cells.

\[
B_{\mathrm{exact}}(L)=\frac{1}{s_A(1/L)}-Le^{-L}\operatorname{Ei}(L)
\]

\[
\min B_{\mathrm{exact}}(L)>1.0957\times10^{-3}\qquad(3.385\le L\le10)
\]
\section{Rational majorants and the finite bridge}

For $L\ge10$, a short rational majorant for $e^{-L}\operatorname{Ei}(L)$ has positive initial gap and positive differential forcing. Exact multiplication shows that the proposed reciprocal denominator dominates this majorant.

This proves that the proposed right-hand side exceeds $\operatorname{li}(x)$. Buethe's strict computation $\pi(x)<\operatorname{li}(x)$ through $10^{19}$ then supplies the prime-counting inequality over the corresponding range.

\[
u(L)=L^{-1}+L^{-2}+2L^{-3}+6L^{-4}+55L^{-5}
\]

\[
1-s_A(t)(1+t+2t^2+6t^3+55t^4)=\frac{t^4}{1000}\left(53+111053t+161106t^2+429318t^3+2422915t^4\right)>0
\]
\section{Published numerical envelopes}

A higher-order rational majorant handles $L\ge40$. Fiori--Kadiri--Swidinsky Table 7 covers the initial high range, and the independently source-checked 164-row Table 4 transcript covers the numerical intervals through $L=3000$.

On each interval the proof computes the exact coefficient required by that row. The unique largest requirement occurs on $2100\le L\le2200$ and is strictly below $44.053$.

\[
A_{\mathrm{req}}=\frac{2709976113860085547103395243942841453423728245400}{61517068085059134496927148872832330483236342381}=44.05242639511077\ldots
\]

\[
44.053-A_{\mathrm{req}}=0.000573604889227\ldots>0
\]
\section{Asymptotic closure and certificate}

For $L\ge3000$, exact polynomial arithmetic gives a simple positive lower bound for the reciprocal-denominator gap. A pinned global absolute estimate for $\pi(x)-\operatorname{Li}(x)$ closes the tail, with the source identity $\operatorname{Li}(x)=\operatorname{li}(x)-\operatorname{li}(2)$ retained.

At the handoff the certified margin exceeds $1.8130\times10^{-13}$ and the comparison improves afterward. The pinned certificate checks the imported tail dependency before checking every local gate.

\[
\text{tail margin at }L=3000>1.8130\times10^{-13}
\]

\section{Pinned certificate}
The pinned certificate checks denominator positivity, the 16384-cell low li cover, two rational Ei majorants, exact residual polynomials, Table 7, all 164 source-checked Table 4 rows, and the asymptotic handoff.

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

\subsection*{Pinned files}
\begin{itemize}[leftmargin=*]
\item \path{canon/witnesses/C-0055/verify.py}
\item \path{canon/witnesses/C-0055/PIN.md}
\item \path{canon/witnesses/C-0055/results.json}
\item \path{canon/witnesses/C-0055/source/dependency/c0050/results.json}
\end{itemize}

\section{Scope}
The certified coefficient $44.053$ preserves Axler's denominator shape and applies for every real $x\ge29.53$.

\section{Sources}
\begin{itemize}[leftmargin=*]
\item Canonical claim: \path{canon/claims/C-0055-axler-compact-pi-denominator-44-053.md}
\item Certificate pin: \path{canon/witnesses/C-0055/PIN.md}
\item Accepted certificate data: \path{canon/witnesses/C-0055/results.json}
\item Axler source: \path{canon/witnesses/C-0055/source/primary/axler-integers-24-A34.pdf}
\item Buethe source: \path{canon/witnesses/C-0055/source/primary/buthe-1511.02032.pdf}
\item Fiori--Kadiri--Swidinsky source: \path{canon/witnesses/C-0055/source/primary/fiori-kadiri-swidinsky-2206.12557v2.pdf}
\end{itemize}

\end{document}
