Uniform elementary quotient transport through PanQuotientBounds; no nonprincipal-character theorem is consumed.
theorem
AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount_li_moving_prefix
(s : ℝ)
(hs : 0 < s)
:
Uniform PNT at the literal real quotient. The threshold precedes every a. The proof uses only the q=1 Standard BV extraction above, never nonprincipal SW.