certificate C-0081 2026-07-19

Axler's Table 9 coefficient-1.149 row fails at its endpoint and has a sharp repair

Axler's coefficient-$1.149$ bound for $\pi(x)$ fails at its published composite endpoint $x_0=42\,575\,222\,481$. The exact same-range non-strict coefficient threshold is $1.1490003091852194519\ldots$, so $1.14900031$ gives a strict repair with the same least integer start. If the printed coefficient $1.149$ is retained, the least valid integer start is $42\,575\,222\,505$.

\[\pi(x)<\frac{x}{\log x-1-1.14900031/\log x}\quad(x\ge 42\,575\,222\,481)\]

Download PDF LaTeX source Verifier bundle

What is proved

At $x_0=42\,575\,222\,481$, the exact count is $\pi(x_0)=1\,817\,311\,115$, and the published strict inequality has its sides in the wrong order. Defining $a_*=\log x_0(\log x_0-1-x_0/\pi(x_0))$ gives the exact threshold on the entire published half-line.

Equality for the non-strict bound with coefficient $a_*$ occurs only at $x_0$. Every larger admissible coefficient gives the strict bound from $x_0$, while the decimal $1.14900031$ is small enough that $x_0-1$ still fails, preserving minimality of the published start.

a_*=1.1490003091852194519030898606008869\ldots

\pi(x_0)-\frac{x_0}{\log x_0-1-1.149/\log x_0}=0.9799543748\ldots>0

Normalize the inequality

On the positive-denominator domain, the prime-counting inequality is equivalent to a comparison with $B(x)=\log x(\log x-1-x/\pi(x))$. Between consecutive primes, $\pi(x)$ is constant and $B(x)$ is strictly decreasing for $x\ge 9$. Therefore, after the initial endpoint, only prime points can create a new maximum.

This reduction turns a real-variable statement into an endpoint check, a finite list of prime candidates, and an analytic tail.

\pi(x)<\frac{x}{\log x-1-c/\log x}\quad\Longleftrightarrow\quad B(x)<c

B'(x)\le -\frac{3}{x}<0\quad\text{between prime jumps}

Exhaust the finite range

The pinned scanner covers every prime between $x_0$ and $H=55\,576\,240\,054$, a total of $528\,206\,511$ prime candidates. It bounds each logarithm from above with directed fixed-point arithmetic and converts $B(p)<1.149$ into an exact integer inequality.

The least finite-range reserve occurs at the first later prime $42\,575\,222\,531$ and remains positive. Segment counts are reconciled with pinned prime-count computations, and the arithmetic-width bounds show that the scanner's signed and unsigned integer operations cannot overflow.

1149\cdot 2^{56}-1000U>0

1.149-B(42\,575\,222\,531)=1.9879406218\ldots\times10^{-8}

Close the infinite tail

At the finite handoff, the proof compares the target rational function with $\operatorname{li}(x)$. A derivative polynomial shows that this difference is increasing from $H$, while Buthe's verified inequality $\operatorname{li}(x)>\pi(x)$ covers the range through $10^{19}$.

Beyond $10^{19}$, Dusart's explicit upper bound for $\pi(x)$ reduces the target inequality to positivity of a cubic polynomial in $\log x$. Its value and first three derivatives have the required signs at the handoff, so positivity persists for the full tail.

F_c(x)=\frac{x}{\log x-1-c/\log x}-\operatorname{li}(x)

(\log x)^3D_c(x)^2F_c'(x)=(c-1)(\log x)^2-3c\log x-c^2

Locate the sharp repairs

The endpoint, finite scan, and analytic continuation prove $B(x)<a_*$ for every $x>x_0$. This establishes the exact same-range coefficient classification, not merely a rounded improvement.

For coefficient $1.149$, the initial prime-free plateau has a unique real crossing at $42\,575\,222\,504.9836\ldots$. Hence the inequality fails at integer $42\,575\,222\,504$ and holds for every real $x\ge42\,575\,222\,505$.

1.14900031-a_*=8.14780548\ldots\times10^{-10}>0

N_{\min}(1.149)=42\,575\,222\,505

Role of the certificate

The public command runs the pinned independent reconstruction. It checks the decisive counts and endpoints, reconstructs all finite-tail partition boundaries with two prime-counting algorithms, and re-evaluates the analytic margins without rerunning the primary exhaustive prime scanner.

The primary proof package separately contains the full scanner and directed Arb verification. The disclosed residual limitation is that the $528\,206\,511$-prime interior has one complete prime-enumeration implementation, although its partition counts and fixed-point inequalities receive independent checks.

Pinned certificate

The public independent checker reconstructs the endpoint failure, sharp coefficient, corrected start, all partition-boundary counts, and the analytic handoffs. It corroborates the pinned primary scanner while explicitly retaining the one-enumerator caveat for the full finite interior.

uv run --frozen python canon/witnesses/C-0081/independent_check.py

canon/witnesses/C-0081/independent_check.py
canon/witnesses/C-0081/tail-output.txt
canon/witnesses/C-0081/source

Scope

The correction applies to Axler's coefficient-$1.149$ row in Proposition 11 and Table 9, on the positive-denominator domain and the published starting range.

Sources

Canonical claimcanon/claims/C-0081-axler-table9-1149-counterexample-sharp-repair.md
Certificate pincanon/witnesses/C-0081/PIN.md
Independent reviewcanon/witnesses/C-0081/INDEPENDENT-REVIEW.md