Surplus bounds for finite graded intervals

The integer surplus of an interval has a linear main term and a uniformly bounded error. These lemmas implement the limiting arguments in the frozen September 20 manuscript using integer inequalities. The categorical interval construction and its counting estimates must supply their hypotheses.

theorem MagnitudeConjecture.GradedInterval.surplus_error_bound (N a p Nₘ aₘ pₘ c Cₙ Cₐ : ℤ) (hN : |Nₘ - c * N| ≤ Cₙ) (ha : |aₘ - c * a| ≤ Cₐ) (hp : pₘ = c * p) : |2 * Nₘ - aₘ - 2 * pₘ - c * (2 * N - a - 2 * p)| ≤ 2 * Cₙ + Cₐ

Object and arrow error bounds give the surplus error bound when the number of simple modules scales exactly. Surplus is 2N-a-2p.

theorem MagnitudeConjecture.GradedInterval.slope_nonpositive_of_eventually_bounded (s C : ℤ) (n₀ : ℕ) (h : ∀ (n : ℕ), n₀ ≤ n → ↑n * s ≤ C) : s ≤ 0

An eventually bounded sequence of integer multiples has nonpositive slope.

theorem MagnitudeConjecture.GradedInterval.ambient_nonnegative_of_interval_bound (σ : ℤ) (interval : ℕ → ℤ) (C : ℤ) (m₀ : ℕ) (hnonneg : ∀ (m : ℕ), 0 ≤ interval m) (hupper : ∀ (m : ℕ), m₀ ≤ m → interval m ≤ (↑m + 1) * σ + C) : 0 ≤ σ

Nonnegative interval surpluses with a uniform upper error force the ambient surplus to be nonnegative.

theorem MagnitudeConjecture.GradedInterval.interval_le_length_mul_of_packing (σ δ : ℤ) (ℓ : ℕ) (C : ℤ) (q₀ : ℕ) (hpacking : ∀ (q : ℕ), q₀ ≤ q → ↑q * δ ≤ ↑q * ↑ℓ * σ + C) : δ ≤ ↑ℓ * σ

Packing arbitrarily many separated copies bounds each interval surplus by the separation length times the ambient surplus. The constant absorbs both the fixed end correction and the uniform counting error.

theorem MagnitudeConjecture.GradedInterval.interval_eq_zero_of_packing (δ C : ℤ) (q₀ : ℕ) (hnonneg : 0 ≤ δ) (hpacking : ∀ (q : ℕ), q₀ ≤ q → ↑q * δ ≤ C) : δ = 0

At zero ambient surplus, packing and directed nonnegativity force every finite interval surplus to vanish.