A nonnegative family with bounded surplus error has nonnegative slope

theorem MagnitudeConjecture.GradedInterval.ambient_nonnegative_of_interval_absolute_error (s : ℤ) (f : ℕ → ℤ) (C : ℤ) (m₀ : ℕ) (hpos : ∀ (m : ℕ), 0 ≤ f m) (herr : ∀ (m : ℕ), m₀ ≤ m → |f m - (↑m + 1) * s| ≤ C) : 0 ≤ s

An eventual uniform absolute error and interval nonnegativity force a nonnegative ambient surplus.