theorem LiLiuPrereqBuchstab.buchstab_weighted_sub_eq_integral {a u : ℝ} (ha : 2 ≤ a) (hu : a ≤ u) : u * buchstab u - a * buchstab a = ∫ (t : ℝ) in a..u, buchstab (t - 1)

The actual global Buchstab equation rebased at an arbitrary real anchor.

theorem LiLiuPrereqBuchstab.buchstab_upper_on_tail {a W : ℝ} (ha : 2 ≤ a) (hbase : ∀ u ∈ Set.Icc a (a + 1), buchstab u ≤ W) (u : ℝ) : a ≤ u → buchstab u ≤ W

A proved upper bound on one complete unit interval propagates to the full tail. No decimal bound or finite starting-interval certificate is assumed to exist here.