A uniform arrow error from exact interior and bounded boundary sums

theorem MagnitudeConjecture.GradedInterval.arrow_error_bound_from_partition {α : Type u} {β : Type v} [Fintype α] [Fintype β] (f : α → α → ℕ) (g : β → β → ℕ) (P : α → Prop) [DecidablePred P] (m h B : ℕ) (hm : 2 * h ≤ m) (hi : ∑ b : { b : α // P b }, ∑ a : α, f a ↑b = (m - 2 * h + 1) * ∑ b : β, ∑ a : β, g a b) (hb : ∑ b : { b : α // ¬P b }, ∑ a : α, f a ↑b ≤ B) : |ARCount.arrowCount f - (↑m + 1) * ARCount.arrowCount g| ≤ ↑B + 2 * ↑h * ARCount.arrowCount g

The exact interior contribution and a bounded exceptional contribution control the error from the full interval-length multiple.