PrimeNumberTheoremAnd

Row-8 mid-range LO flank [e^10, e^5500] - restricted envelope cover (cells with b ≤ 5500, all below the gap band).

Row-8 mid-range HI flank [e^9500, e^20000] - restricted envelope cover (cells with b' ≥ 9500, all above the gap band).

Corollary 23, row 8 (A=121.107, B=3/2, C=2, x₀=1).

admissible_bound A 2 C R x in terms of s = √(log x): = (A/R²)·s⁴·exp(−(C/√R)·s). The B = 2 analogue of admissible_three_halves_eq.

Generic B = 2 floor-curve domination: coeff·s⁴·exp(−rate·s) ≤ rowcurve when coeff ≤ A/R² and rate ≥ C/√R. s⁴ analogue of rowcurve_dom_three_halves.

Row-9 tail [e^20000, ∞): cor14_tail gives Eπ ≤ admissible 121.107 (3/2) 2 R (a B=3/2, rate-2/√R curve), which DOMINATES the row-9 B=2 curve here because L^{3/2} ≤ (6.60/121.107·R^{1/2})·L² for s = √L ≥ 43.29 (and s ≥ 141 on this range).

Buthe bound in x^{-1/2} form (shared core for all Table-7 rows): from Buthe.theorem_2e/2f (valid x ∈ [2, 10^19]), Eπ x ≤ (1.95 + 3.9/log x + 19.5/(log x)²)·x^{-1/2} + 1.0452·(log x)/x.

FKS2 Corollary 24 (complete). Every Table-7 row (B, I) gives the pointwise bound Eπ x ≤ B x for all x with log x ∈ I.

Row-1 Buthe floor [e^4, e^43] via floor_xhalf_of_check.

FKS2 Corollary 24, row 1 (table7 entry (x ↦ 2·log x·x^{-1/2}, Icc 1 57)): Eπ x ≤ 2·log x·x^{-1/2} whenever log x ∈ [1, 57]. For x > 0 this splits into the three segments above; for x < 0 (possible since log is even) the exponent -(1)/2 gives cos((-(1)/2)·π) = cos(-π/2) = 0, so x^{-1/2} = 0 and the RHS is 0, while Eπ x ≤ 0.

Row-10 floor (Buthe) [e^4, e^10] via floor_xpow_of_check.

FKS2 Corollary 24, row 10 (table7 entry (x ↦ x^{-1/50}, Icc 1 1358.6)): Eπ x ≤ x^{-1/50} whenever log x ∈ [1, 1358.6]. For x > 0 this splits into the four segments above; for x ≤ 0 (possible since log is even) Eπ x ≤ 0 < x^{-1/50}.

Transport: a checked cell dominated by the table value eps, with the per-cell numeric certificate eps ≤ exp(-b'/n), gives the row-n curve x^{-1/n} bound for Eπ on the whole cell [exp b, exp b'].

Soundness: a checked cell obeys eps ≤ exp(-b'/n).

expSplitNegXpow n evaluated at s = √(log x) is exactly x^{-1/n} (for x > 0, log x ≥ 0).

Support of lhsE - expSplitNegXpow n for the dyadic slab kernel.

Buthe Eπ-upper-bound as eval_lhsE on the LOW range [2, e^10] (vs the committed FloorButhe.Epi_le_evalLhsE's [e^5, e^10]): identical reconciliation, only the hypothesis is 2 ≤ x. Curve-independent (FloorButhe.lhsE is the Buthe x^{-1/2} bound), so reusable by every x^{-1/n} row floor. Bottoms out at Buthe theorem_2e/2f + li.two_approx.

Generic x^{-1/n} mid assembler: over the allCells prefix take k (chained from 10 to m, every cell passing the row-n checkXpowCell), Eπ ≤ x^{-1/n} on [e^10, e^m]. Uses cover_of_chainOk + cell_Epi_le_xpow_of_check + allCells_trusted. Row 11: k = 3746, m = 3756.