PrimeNumberTheoremAnd

admissible_bound A 1.5 C 1 is antitone beyond log x ≥ (3/C)²: the workhorse for step-function interpolation against Tables 4/5.

Step-interval bridge for the Table 4/5 interpolation. A constant bound V on Eπ over a grid cell [x₁, x₂] (as produced by theorem_6_alt with V = εθ_num x₁ * (1 + μ_num_2 …)), dominated by the admissible curve at the right endpoint, yields the classical bound across the whole cell, by admissible_bound_anti. The mid-range verification is this lemma instantiated once per grid cell, with hrow a numeric endpoint check.

Corollary 14, converted to the normalized Corollary 22 coordinates.

Corollary 22 asymptotic tail: from exp 20000 onward.

Li x ≤ 2 on [2, e): the integrand 1/log t ≤ 1/log 2, integrated over a length < 1.04 interval.

The direct Eπ bound on [2, e): |pi x − Li x| ≤ 1 and x/log x ≥ e.

Generic mid-range: every row's [e^10, e^20000] segment via the allCells envelope transported by cell_Epi_le_admissible_gen. Rows supply P, the curve params (A,B,C), the cell-param numeric witnesses, and the native_decide check. Shared by every row's mid_row (the cover_of_chainOk plumbing was identical).

admissible_bound A (3/2) C R x in terms of s = √(log x): = (A / R^{3/2}) · s³ · exp(−(C/√R)·s). Reusable for tail domination.

admissible_bound A (1/2) C R x in terms of s = √(log x): = (A/√R)·s·exp(−(C/√R)·s). The B = 1/2 analogue of admissible_three_halves_eq (used by row 3).

Any s ∈ [lo, lo + n·0.05) lands in some slab of slabsFrom lo n.

Generic B = 3/2 floor-curve domination: the evaluated dyadic floor curve coeff·s³·exp(−rate·s) (s = √(log x)) is below the row's admissible curve when coeff ≤ A/R^{3/2} and rate ≥ C/√R. Shared by every B = 3/2 row's rhsE_le_rowcurve (rows 5/6/7).

Generic B = 3/2 tail: Corollary 22 dominates any (A, 3/2, C) row curve for x ≥ e^20000. Inputs: a rational rate upper bound rateUB ≥ C/√R, a rational coefficient lower bound coeffLB ≤ A/R^{3/2}, that the gap 0.8476 − rateUB is nonneg, and the single numeric fact 9.2211 ≤ coeffLB·exp((0.8476−rateUB)·141) (s = √(log x) ≥ 141 on [e^20000, ∞)). Shared by every B = 3/2 row's tail.

Generic Buthe floor assembler: any curve rE whose dyadic slab check passes (hchk) and which dominates the admissible curve on [e^5, e^10] (hcurve) gives Eπ ≤ that curve there. The Buthe Eπ-upper-bound (lhsE, Epi_le_evalLhsE) and the slab cover (slabs, cover) are curve-independent and reused by every row. Bottoms out only at Buthe theorem_2e/2f + li.two_approx.