---
id: C-0050
type: claim
title: "Axler's global fourth prime-counting coefficient improves from 6.024334 to 6.0145407"
status: proved-unconditional
family: adjacent-unconditional
statement: >
  For every real x>1, pi(x) is strictly less than
  x/log x+x/log^2 x+2x/log^3 x+6.0145407x/log^4 x+
  24x/log^5 x+120x/log^6 x+720x/log^7 x+
  6097.2x/log^8 x. This replaces Axler's published fourth
  coefficient 6.024334 by 6.0145407, retains C-0048's
  coefficients 24, 120, 720, and 6097.2, and preserves the
  full range x>1.
verifier: canon/witnesses/C-0050/verify.py
depends: [C-0048]
supersedes: []
sources:
  - literature/2026-07-19-axler-pi-fourth-coefficient-6-0145407-search.md
  - experiments/axler_pi_fourth_coefficient/verify.py
  - scratch/adjacent-unconditional--axler-pi-fourth-6-0145407-fifth-24-sixth-120-seventh-720-eighth-6097-2/RESULT.md
  - canon/witnesses/C-0050/source/dependency/c0048/claim.md
  - canon/witnesses/C-0050/source/primary/axler-integers-24-A34.pdf
  - canon/witnesses/C-0050/source/primary/buthe-1511.02032.pdf
  - canon/witnesses/C-0050/source/primary/fiori-kadiri-swidinsky-2206.12557v2.pdf
  - canon/witnesses/C-0050/results.json
  - canon/witnesses/C-0050/PIN.md
tags: [prime-counting, explicit-bound, axler, pnt-error, interval-arithmetic, prime-sieve]
caveats: >
  This is a strict same-form records improvement. The decimal
  6.0145407 is a short upward rounding of the exact reserve forced by
  the published dense Table 4 splice; it is not claimed to be the
  least possible fourth coefficient for the actual prime-counting
  function with the other seven coefficients fixed.
---

## Statement

For every real \(x>1\), with \(L=\log x\),

\[
\boxed{
\begin{aligned}
\pi(x)<{}&
\frac{x}{L}+\frac{x}{L^2}+\frac{2x}{L^3}
+\frac{6.0145407x}{L^4}
+\frac{24x}{L^5}\\
&+\frac{120x}{L^6}
+\frac{720x}{L^7}
+\frac{6097.2x}{L^8}.
\end{aligned}}
\tag{1}
\]

Axler's published Proposition 5 has fourth-through-eighth
coefficients

\[
(6.024334,24.024334,120.12167,720.73002,6098).
\]

C-0040, C-0044, C-0046, and C-0048 improved the last four to
\((24,120,720,6097.2)\). Equation (1) retains those values and reduces
the fourth coefficient to \(6.0145407\).

The right-hand side of (1) is C-0048's right-hand side minus

\[
\frac{0.0097933x}{L^4},
\]

so this result strictly dominates C-0048 for every \(x>1\).

## Mechanism

Put \(\delta=0.0145407\), and let \(F\) be the right-hand side of
(1). Exact rational differentiation gives

\[
F'(x)=\frac1L+\frac{\delta}{L^4}
-\frac{4\delta}{L^5}
+\frac{1057.2}{L^8}
-\frac{48777.6}{L^9}.
\tag{2}
\]

Thus \(F'(x)=Q(L)/L^9\), where

\[
Q(L)=L^8+\delta L^4(L-4)+1057.2L-48777.6.
\]

For \(L\geq\log47\),

\[
Q'(L)=8L^7+\delta L^3(5L-16)+1057.2>0.
\]

The verifier proves \(Q(\log47)>3578.05\), so \(F\) is increasing
above 47.

An exact odd-only sieve gives

\[
\pi(1100000000)=55662470.
\]

The verifier covers the finite range by 58006 consecutive prime-count
blocks. Each block is accepted only after Arb proves \(F\) at its
first prime exceeds the last count in the block. The least slack
exceeds \(0.2500116\). A direct interval cover handles \([2,47]\).

At \(X=1100000000\), Arb proves

\[
F(X)-\operatorname{li}(X)>0.4280795.
\tag{3}
\]

The derivative numerator for \(F-\operatorname{li}\) is

\[
P(L)=\delta L^4(L-4)+1057.2L-48777.6.
\]

The verifier proves \(P(\log X)>19170.48\), while

\[
P'(L)=\delta L^3(5L-16)+1057.2>0
\qquad(L\geq20).
\]

Hence (3) remains positive. Buethe's
\(\pi(x)\leq\operatorname{li}(x)\) computation through \(10^{19}\)
completes the bridge through \(e^{40}\).

## Dense published PNT tail

For \(L\geq40\), the verifier uses

\[
U(L)=\sum_{j=0}^{15}\frac{j!}{L^{j+1}}
+\frac{1673823191040000}{23L^{17}}
\]

as a rigorous upper majorant for \(e^{-L}\operatorname{Ei}(L)\).
This yields the normalized lower gap

\[
B_\delta(L)=
\frac{\delta}{L^3}
+\frac{1057.2}{L^7}
-\sum_{j=8}^{15}\frac{j!}{L^j}
-\frac{1673823191040000}{23L^{16}}.
\tag{4}
\]

An exact polynomial interval evaluation proves
\(B_\delta'(L)<0\) for all \(L\geq40\).

Fiori--Kadiri--Swidinsky's Corollary 24 and Table 7 cover
\(40\leq L\leq44\) with margin exceeding
\(3.9154\times10^{-8}\).

Their Table 4 gives 164 decreasing upper bounds
\((L_i,\epsilon_i)\) through \(L=3000\). The verifier embeds every
row as an exact rational and computes the reserve required on all 163
successive intervals. The unique maximum is on
\([2000,2100]\):

\[
\max_i d_i=
\frac{
28246867609287917082201314322797
}{
1942607666008652343750000000000000
}
=0.0145406960466314\ldots.
\tag{5}
\]

The proposed \(\delta=0.0145407\) exceeds (5) exactly. The minimum
directed-rounding interval margin is greater than
\(4.2688\times10^{-19}\).

Their Corollary 22 gives

\[
\left|
\frac{\pi(x)-\operatorname{Li}(x)}{x/\log x}
\right|
\leq9.2211L^{3/2}e^{-0.84768363\sqrt L}.
\]

For \(L\geq3000\), (4) exceeds \(\delta/(2L^3)\). At \(L=3000\),
the certified margin over the published error is greater than
\(2.5888\times10^{-13}\), and the comparison improves thereafter.

```text
exact_map: Axler Proposition 5 and C-0048 -> retain coefficients one through three and C-0048's coefficients 24, 120, 720, and 6097.2 -> replace the published fourth coefficient 6.024334 by 6.0145407 -> certify finite prime blocks, the li bridge, every dense Table 4 interval, and the published asymptotic pi-Li tail
counterfeit: the published upper envelopes li(x), Fiori--Kadiri--Swidinsky Table 4/Table 7, and their Corollary 22 asymptotic error
counterfeit_failure: PASS -- the stronger coefficient vector dominates every envelope on its stated range, including the exact active Table 4 interval, with directed-rounding positive margins
success_delta: PASS -- a named published coefficient is lowered one full logarithmic order earlier than C-0048, and the result strictly dominates C-0048 for every x>1
failure_delta: PASS -- any failed finite block, source-row transcript, Ei majorant, numerical handoff, or asymptotic comparison would leave C-0048 as the retained bound
stop_condition: a prior same-form all-x result with fourth coefficient at most 6.0145407, any source-table mismatch, or any nonpositive verifier margin
```

## Witness

The pinned 256-bit verifier proves:

\[
\begin{aligned}
\pi(1100000000)&=55662470,\\
\min(\text{finite block slack})&>0.2500116,\\
F(1100000000)-\operatorname{li}(1100000000)&>0.4280795,\\
\min(\text{dense Table 4 margin})&>4.2688\times10^{-19},\\
\text{asymptotic margin at }L=3000&>2.5888\times10^{-13}.
\end{aligned}
\]

Independent PARI/GP and SymPy computations agree on the split prime
count. SymPy independently reconstructs (2) with exact zero residual.
An independent parser recovered all 164 Table 4 rows from the pinned
source text and matched the verifier tuple exactly.

## Hostile audit

Verdict: **ACCEPT**, after repairing a material certificate defect.

The previous canonical verifier used bare assertions without rejecting
optimized Python and did not retain the primary sources it cited. The
replacement witness fails closed under `python -O`, pins the accepted
C-0048 dependency and every source artifact it consumes, and independently
reconstructs the changed derivative, all 58006 finite prime-count blocks,
the split count, the `li` bridge, the rational `Ei` majorant, the signed
\(E_\pi\) and \(\operatorname{Li}/\operatorname{li}\) normalization, all
164 Table 4 rows, the Table 7 splice, and the asymptotic handoff.

The source parser separately rejects the two PDF-text artifacts in which
\(10^6\) and \(10^7\) appear as `106` and `107`. It then matches the
remaining 164 rows byte-for-value against the frozen verifier literal and
recomputes every interval reserve using exact fractions. The unique active
interval remains \([2000,2100]\).

All directed-rounding margins are positive. The smallest finite block slack
exceeds \(0.2500116\), the split gap exceeds \(0.4280795\), the smallest
dense-table margin exceeds \(4.2688\cdot10^{-19}\), and the asymptotic
handoff margin exceeds \(2.5888\cdot10^{-13}\).

## What survives

The result improves a term one logarithmic order earlier than C-0048
and strictly dominates it pointwise. It also retains the exact
factorial coefficients \(24\), \(120\), and \(720\). No global
minimality claim is made for the fourth coefficient.

## Provenance

The named prior record is Christian Axler, *Effective Estimates for
Some Functions Defined over Primes*, Integers **24** (2024), paper
A34, Proposition 5. The bridge uses Jan Buethe's 2018 computation, and
the tail uses Andrew Fiori, Habiba Kadiri, and Joshua Swidinsky,
Research in Number Theory **9** (2023), article 63.

A targeted exact-formula and primary-source search through 2026-07-19
found no same-range result with coefficient vector
\((6.0145407,24,120,720,6097.2)\).
