Counting arrows by weighted height differences

theorem MagnitudeConjecture.HeightArrowCount.weighted_difference {V : Type u} [Fintype V] (a : V → V → ℤ) (h : V → ℤ) (ha : ∀ (x y : V), a x y ≠ 0 → h y = h x + 1) : ∑ x : V, ∑ y : V, a x y = ∑ y : V, h y * ∑ x : V, a x y - ∑ x : V, h x * ∑ y : V, a x y

Each arrow contributes one to the difference of incoming and outgoing height-weighted sums. Multiplicities are retained.

theorem MagnitudeConjecture.HeightArrowCount.count_of_balance (A N p L Hp Hm outside : ℤ) (hheight : Hm - Hp = 2 * (N - p)) (hout : outside = A - p + 1) (hbalance : A = 2 * outside + Hp - Hm + L) : A = 2 * N - L - 2 ∧ 2 * N - A - p - 1 = L - (p - 1)

Solving the weighted-height balance gives the arrow count and excess. Here A is the arrow count, N the vertex count, p the projective count, and L the sink height.