# Proof of the Axler compact denominator coefficient 44.053

Let

\[
A=44.053,\qquad L=\log x,
\]

and define

\[
F_A(x)=
\frac{x}{
L-1-L^{-1}-3L^{-2}-AL^{-3}
}.
\]

The claim is

\[
\pi(x)<F_A(x)\qquad(x\geq29.53).
\]

Axler's published Proposition 4 proves the identical statement with
\(A=70.935\).

## Positive denominator

Write

\[
D_A(L)=L-1-L^{-1}-3L^{-2}-AL^{-3}.
\]

At \(L=3.385\), exact rational arithmetic gives

\[
D_A(3.385)=
\frac{42941765641}{62057746600}>0.
\]

Also

\[
D_A'(L)=1+L^{-2}+6L^{-3}+3AL^{-4}>0.
\]

The verifier proves

\[
\log(29.53)>3.385,
\]

so the new denominator is positive on the full claimed range. It also
checks that Axler's published denominator is positive at \(x=29.53\);
its derivative is positive thereafter.

## The li bridge through log x = 40

Put \(t=L^{-1}\) and

\[
s_A(t)=1-t-t^2-3t^3-At^4.
\]

The normalized gap between \(F_A\) and the standard logarithmic
integral is

\[
B_{\rm exact}(L)
=
\frac{L}{e^L}\bigl(F_A(e^L)-\operatorname{li}(e^L)\bigr)
=
\frac1{s_A(1/L)}
-Le^{-L}\operatorname{Ei}(L).
\tag{1}
\]

The 256-bit Arb verifier covers \(3.385\leq L\leq10\) by 16384
rational cells. Every interval enclosure in (1) is positive; the
least lower endpoint exceeds

\[
1.0957\cdot10^{-3}.
\tag{2}
\]

For \(L\geq10\), define

\[
u(L)=
\frac1L+\frac1{L^2}+\frac2{L^3}+\frac6{L^4}
+\frac{55}{L^5}.
\]

If \(r(L)=e^{-L}\operatorname{Ei}(L)\), then

\[
r'(L)+r(L)=\frac1L.
\]

At \(L=10\), Arb proves

\[
u(10)-r(10)>2.9795\cdot10^{-6}.
\]

Moreover,

\[
(u-r)' +(u-r)
=
\frac{55(1-5/L)-24}{L^5},
\]

whose numerator is at least \(7/2\) for \(L\geq10\). Hence
\(u(L)>r(L)\) throughout that range.

Let

\[
T(t)=1+t+2t^2+6t^3+55t^4.
\]

Exact multiplication gives

\[
1-s_A(t)T(t)
=
\frac{t^4}{1000}
\left(
53+111053t+161106t^2+429318t^3+2422915t^4
\right)>0.
\tag{3}
\]

Since \(s_A(t)>0\), equations (3) and \(T(1/L)=Lu(L)\) imply
\(F_A(e^L)>\operatorname{li}(e^L)\) for every \(L\geq10\).

Buethe's published computation gives

\[
\pi(x)\leq\operatorname{li}(x)
\qquad(2\leq x\leq10^{19}).
\]

The verifier proves \(40<19\log10\). Together with (1)--(3), this
proves the target through \(L=40\).

## Rational Ei majorant

For \(L\geq40\), set

\[
U(L)=
\sum_{j=0}^{15}\frac{j!}{L^j}
+\frac{1673823191040000}{23L^{16}}.
\tag{4}
\]

This majorizes \(Le^{-L}\operatorname{Ei}(L)\). At \(L=40\), the
directed-rounding gap is positive, and the differential forcing
numerator is exactly

\[
16!=20922789888000.
\]

Thus

\[
B_A(L)=\frac1{s_A(1/L)}-U(L)
\tag{5}
\]

is a rigorous lower bound for the normalized \(F_A-\operatorname{li}\)
gap.

For \(t=1/L\), the numerator of \(dB_A/dt\) after multiplication by
\(s_A(t)^2\) has an exact factor \(t^3\). The remaining degree-20
polynomial is certified positive on \(0\leq t\leq1/40\); its least
interval lower bound exceeds \(114.674\). Therefore \(B_A(L)\) is
decreasing for \(L\geq40\).

## FKS numerical range

Fiori--Kadiri--Swidinsky define

\[
E_\pi(x)=
\frac{|\pi(x)-\operatorname{Li}(x)|}{x/\log x},
\qquad
\operatorname{Li}(x)=\operatorname{li}(x)-\operatorname{li}(2).
\]

Hence

\[
\pi(x)
\leq
\operatorname{li}(x)-\operatorname{li}(2)
+E_\pi(x)\frac{x}{L}
<
\operatorname{li}(x)+E_\pi(x)\frac{x}{L}.
\tag{6}
\]

On \(40\leq L\leq44\), their Corollary 24 and Table 7 give

\[
E_\pi(x)
\leq
\frac{L^2e^{-L/2}}{8\pi}.
\]

The error decreases on this interval, while (5) decreases. The
verifier proves

\[
B_A(44)
-
\frac{40^2e^{-20}}{8(3.14159)}
>
8.0215\cdot10^{-6}.
\tag{7}
\]

For \(44\leq L\leq3000\), the verifier embeds all 164 decreasing
Table 4 rows \((L_i,\epsilon_i)\). On
\([L_i,L_{i+1}]\), monotonicity reduces the comparison to

\[
B_A(L_{i+1})>\epsilon_i.
\]

Solving this inequality exactly for \(A\) gives the requirement

\[
A>
L_{i+1}^4
\left(
1-\frac1{L_{i+1}}-\frac1{L_{i+1}^2}
-\frac3{L_{i+1}^3}
-\frac1{U(L_{i+1})+\epsilon_i}
\right).
\tag{8}
\]

The unique maximum of (8) occurs on \([2100,2200]\):

\[
A_{\rm req}=
\frac{
2709976113860085547103395243942841453423728245400
}{
61517068085059134496927148872832330483236342381
}
=44.05242639511077\ldots.
\tag{9}
\]

The exact reserve is

\[
44.053-A_{\rm req}
=
\frac{
35286491024504889736445352041201354282345510193
}{
61517068085059134496927148872832330483236342381000
}
>0.
\tag{10}
\]

The least exact normalized interval margin is
\(2.45085\cdot10^{-17}\).

## Asymptotic tail

Let

\[
K=\frac{A-13}{2}=15.5265.
\]

Exact polynomial interval arithmetic proves

\[
B_A(L)>\frac{K}{L^4}
\qquad(L\geq3000).
\tag{11}
\]

Indeed, after multiplying by \(s_A(1/L)\), the residual has a factor
\(L^{-4}\), and the remaining degree-16 polynomial is greater than
\(15\) on \(0\leq1/L\leq1/3000\).

C-0051 gives

\[
E_\pi(x)
\leq
9.221056L^{3/2}
e^{-0.84768363\sqrt L}.
\tag{12}
\]

At \(L=3000\), the verifier proves

\[
\frac{15.5265}{3000^4}
-
9.221056(3000)^{3/2}
e^{-0.84768363\sqrt{3000}}
>
1.8130\cdot10^{-13}.
\tag{13}
\]

The ratio of the left comparison terms improves thereafter because
\(0.84768363\sqrt L>11\). Equations (6), (11), and (12) complete the
proof.

```text
exact_map: Axler Integers 24 Proposition 4 denominator coefficient 70.935 -> preserve the denominator shape and exact range x>=29.53 -> replace 70.935 by 44.053 -> certify denominator positivity, the li bridge, Table 7, every Table 4 interval, and the C-0051 tail
counterfeit: floating-point-only scans, a log(x)>=29.53 range substitution, or a denominator comparison that freezes published error terms without proving the Li offset and interval handoffs
counterfeit_failure: PASS -- the actual x>=29.53 range is covered from log(29.53), all source bounds retain their stated normalizations, and every transcendental or table comparison has a directed or exact positive margin
success_delta: PASS -- a named compact prime-counting coefficient falls by 26.882 on the identical range, producing a strictly smaller right-hand side everywhere and a substantially stronger reusable bound than the preceding decimal-normalization successes
failure_delta: PASS -- any nonpositive denominator, low-range cell, majorant forcing, source-row match, active interval, or asymptotic margin would leave Axler's published 70.935 unchanged
stop_condition: a prior same-form coefficient at most 44.053 on x>=29.53, any source-range or Li-normalization mismatch, a nonpositive denominator, or any nonpositive verifier margin
```

