The uniform-error consequence of separated interval packing

theorem MagnitudeConjecture.GradedInterval.interval_le_length_mul_of_separated_packing (σ : ℤ) (interval : ℕ → ℤ) (C : ℤ) (h : ℕ) (hupper : ∀ (m : ℕ), 2 * h ≤ m → |interval m - (↑m + 1) * σ| ≤ C) (hpack : ∀ (r q : ℕ), ↑q * interval r ≤ interval (packingEnd r h q)) (r : ℕ) : interval r ≤ (↑r + ↑h + 1) * σ

A uniform linear error and separated packing bound every interval by its separation length times the ambient surplus.