Uniform Buchstab asymptotics for the actual rough-integer count

For each fixed u₀ > 1, one real threshold works for every u ∈ [u₀,100]. The normalization is proved positive, and the count retains the unit, real floor endpoint, strict small-prime cutoff, and prime-square endpoint.

theorem LiLiuPrereqBuchstab.rpow_cutoff_bounds {x u : ℝ} (hx : 1 < x) (hu : 1 ≤ u) (hu100 : u ≤ 100) : 1 < x ^ (1 / u) ∧ x ^ (1 / 100) ≤ x ^ (1 / u) ∧ x ^ (1 / u) ≤ x ∧ x ≤ (x ^ (1 / u)) ^ 100 ∧ Real.log x / Real.log (x ^ (1 / u)) = u

theorem LiLiuPrereqBuchstab.rpow_buchstab_main_eq {x u : ℝ} (hx : 1 < x) (hu : 0 < u) : x * buchstab u / Real.log (x ^ (1 / u)) = u * buchstab u * x / Real.log x

theorem LiLiuPrereqBuchstab.buchstab_normalization_pos {x u : ℝ} (hx : 1 < x) (hu : 1 ≤ u) : 0 < u * buchstab u * x / Real.log x

theorem LiLiuPrereqBuchstab.roughCount_relative_band_error {x y : ℝ} (hy : primeErrorStart ≤ y) (hyx : y ≤ x) (hxy : x ≤ y ^ 100) : |↑(roughCount x y) / (x * buchstab (Real.log x / Real.log y) / Real.log y) - 1| ≤ 2 * buchstabBandConstant 100 * (buchstabRemainder y + y / x)

theorem LiLiuPrereqBuchstab.roughCount_uniform_error_bound {x u u₀ : ℝ} (hx : 1 < x) (hu₀ : 1 < u₀) (hlo : u₀ ≤ u) (hhi : u ≤ 100) (hstart : primeErrorStart ≤ x ^ (1 / 100)) : |↑(roughCount x (x ^ (1 / u))) / (u * buchstab u * x / Real.log x) - 1| ≤ 2 * buchstabBandConstant 100 * (buchstabRemainder (x ^ (1 / 100)) + x ^ (1 / u₀ - 1))

A parameter-free upper bound for every normalized error in the compact band.

theorem LiLiuPrereqBuchstab.tendsto_uniform_buchstab_majorant {u₀ : ℝ} (hu₀ : 1 < u₀) : Filter.Tendsto (fun (x : ℝ) => 2 * buchstabBandConstant 100 * (buchstabRemainder (x ^ (1 / 100)) + x ^ (1 / u₀ - 1))) Filter.atTop (nhds 0)

The majorant tends to zero before a value of u is chosen.

theorem LiLiuPrereqBuchstab.roughCount_uniform_buchstab {u₀ : ℝ} (hu₀ : 1 < u₀) {ε : ℝ} (hε : 0 < ε) : ∃ (X : ℝ), 1 < X ∧ ∀ x ≥ X, ∀ u ∈ Set.Icc u₀ 100, 0 < u * buchstab u * x / Real.log x ∧ |↑(roughCount x (x ^ (1 / u))) / (u * buchstab u * x / Real.log x) - 1| < ε

Uniform asymptotics for the actual rough count. The single threshold X precedes both x and u; no pointwise-to-uniform inference is used.