Back to all results
certificate C-0057

Axler's Table 8 coefficient-1.071 row fails and has a sharp repair

Axler's published row $\pi(x)<x/(\log x-1.071)$ for $x\ge22{,}078{,}017$ fails at the prime $22{,}078{,}033$. The exact same-range threshold is $a_*=\log(22{,}078{,}033)-22{,}078{,}033/1{,}393{,}895$, so $1.07100036$ is a valid strict repair. If the coefficient $1.071$ is retained, the smallest valid integer start is $22{,}078{,}034$.

\[\pi(x)<\frac{x}{\log x-1.07100036}\ (x\ge22078017),\qquad \pi(x)<\frac{x}{\log x-1.071}\ (x\ge22078034)\]
Download PDF LaTeX source Verifier bundle

The false row and its repair

Put $x_0=22{,}078{,}017$, $p_*=22{,}078{,}033$, and $n_*=1{,}393{,}895$. At $p_*$ the published right-hand side is smaller than $\pi(p_*)$, so the strict inequality fails inside the stated range.

The normalized value at that prime determines the exact non-strict same-range coefficient.

\[a_*=\log p_*-\frac{p_*}{n_*}=1.07100035826576367645708887648\ldots\]
\[\pi(p_*)-\frac{p_*}{\log p_*-1.071}=0.0315286257171953\ldots>0\]
\[\pi(x)<\frac{x}{\log x-1.07100036}\qquad(x\ge x_0)\]

Why only endpoints matter

Define $A(x)=\log x-x/\pi(x)$. On an interval between consecutive primes, $\pi(x)$ is constant and $A$ decreases. At the next prime it jumps upward.

Therefore a global maximum on the published half-line can occur only at the actual starting endpoint or at a prime. This turns the finite part of the problem into an exact comparison of discrete candidates.

\[A'(x)=\frac1x-\frac1n<0\qquad(p_n\le x<p_{n+1})\]
\[A(p_{n+1})-\lim_{x\uparrow p_{n+1}}A(x)=\frac{p_{n+1}}{n(n+1)}>0\]

Finite maximizer and independent tail

The certificate enumerates the primes through $H=45{,}399{,}074$ and compares $1{,}347{,}034$ candidates. The unique maximum is $A(p_*)=a_*$; the published start is the unique runner-up.

Beyond $H$, the proof no longer relies on neighboring appendix rows. It first shows $\operatorname{li}(x)<x/(\log x-1.070)$, then uses Buethe's strict $\pi(x)<\operatorname{li}(x)$ computation through $10^{19}$ and an Axler Theorem 2 reduction with coefficient $1.0343$ for the remaining tail.

\[A(p_*)-A(x_0)=0.0000006092657002968\ldots>0\]
\[A(x)<1.070\qquad(x\ge H)\]

Sharp coefficient classification

The finite maximum and the independent tail prove that $a_*$ is the unique global maximum of $A$ on $x\ge x_0$. Hence the non-strict bound with coefficient $a_*$ has equality only at $p_*$.

For real coefficients $a<\log x_0$, the strict upper bound on the published range holds exactly when $a>a_*$. The rounded repair $1.07100036$ lies above $a_*$ by a certified positive margin.

\[\pi(x)\le\frac{x}{\log x-a_*}\qquad(x\ge x_0)\]
\[1.07100036-a_*=1.7342363235\ldots\times10^{-9}>0\]

Keeping the coefficient 1.071

On the prime-free interval beginning at $p_*$, the crossing equation can be solved exactly with the $W_{-1}$ branch of the Lambert $W$ function. The principal branch is irrelevant because it gives a solution below $n_*$.

The published inequality fails from $p_*$ through the crossing and holds afterward. Since the crossing lies strictly between $22{,}078{,}033$ and $22{,}078{,}034$, the latter is the smallest valid integer start.

\[r=-n_*W_{-1}\!\left(-\frac{e^{1.071}}{n_*}\right)=22{,}078{,}033.53303818298\ldots\]
\[\pi(x)<\frac{x}{\log x-1.071}\qquad(x\ge22{,}078{,}034)\]

Pinned certificate

The pinned certificate checks the published row against exact prime counts, proves the unique finite maximizer, closes the tail independently of neighboring rows, certifies the rounded coefficient repair, and encloses the Lambert-W crossing.

uv run --frozen python canon/witnesses/C-0057/verify.py
  • canon/witnesses/C-0057/verify.py
  • canon/witnesses/C-0057/PIN.md
  • canon/witnesses/C-0057/source/repository/original-verify.py
  • canon/witnesses/C-0057/source/repository/independent-check.py
  • canon/witnesses/C-0057/source/repository/INDEPENDENT-REVIEW.md

Scope

The repair concerns Axler's coefficient-$1.071$ row on $x\ge22{,}078{,}017$ within the one-parameter denominator $x/(\log x-a)$.

Sources

  • Canonical claimcanon/claims/C-0057-axler-table8-1071-counterexample-sharp-repair.md
  • Certificate pincanon/witnesses/C-0057/PIN.md
  • Axler journal sourcecanon/witnesses/C-0057/source/primary/axler-integers-24-A34.pdf
  • Axler arXiv sourcecanon/witnesses/C-0057/source/primary/axler-2203.05917.pdf
  • Buethe sourcecanon/witnesses/C-0057/source/primary/buthe-1511.02032.pdf
  • Independent reconstructioncanon/witnesses/C-0057/source/repository/INDEPENDENT-REVIEW.md