theorem LiLiuBuchstabSharp.closure_seed_upper {u : ℝ} (hu : 2 ≤ u) (hu' : u ≤ 3) : rationalStage 0 u ≤ Polynomial.eval (3 - u) closureP0

Concrete degree-32 polynomial majorant on the full seed interval.