Direct arrow counts from boundary degrees and translation

theorem MagnitudeConjecture.HeightArrowCount.weighted_translation_sum {V : Type u} [Fintype V] (P I : V → Prop) [DecidablePred P] [DecidablePred I] (e : { x : V // ¬P x } ≃ { x : V // ¬I x }) (h incoming outgoing : V → ℤ) (he : ∀ (x : { x : V // ¬P x }), h ↑x = h ↑(e x) + 2) (ha : ∀ (x : { x : V // ¬P x }), incoming ↑x = outgoing ↑(e x)) : ∑ x : { x : V // ¬P x }, h ↑x * incoming ↑x = ∑ x : { x : V // ¬I x }, h ↑x * outgoing ↑x + 2 * ∑ x : { x : V // ¬I x }, outgoing ↑x

Translation reindexes the incoming weighted sum off the projective boundary into the outgoing weighted sum off the injective boundary.

theorem MagnitudeConjecture.HeightArrowCount.count_of_boundary_sums {V : Type u} [Fintype V] (P I : V → Prop) [DecidablePred P] [DecidablePred I] (e : { x : V // ¬P x } ≃ { x : V // ¬I x }) (h incoming outgoing : V → ℤ) (A L : ℤ) (he : ∀ (x : { x : V // ¬P x }), h ↑x = h ↑(e x) + 2) (ha : ∀ (x : { x : V // ¬P x }), incoming ↑x = outgoing ↑(e x)) (hflux : A = ∑ x : V, h x * incoming x - ∑ x : V, h x * outgoing x) (htotal : ∑ x : V, outgoing x = A) (hpin : ∑ x : { x : V // P x }, h ↑x * incoming ↑x = ∑ x : { x : V // P x }, h ↑x) (hiout : ∑ x : { x : V // I x }, h ↑x * outgoing ↑x = ∑ x : { x : V // I x }, h ↑x - L) (hicount : ∑ x : { x : V // I x }, outgoing ↑x = ↑(Fintype.card { x : V // P x }) - 1) : A = 2 * ↑(Fintype.card V) - L - 2 ∧ 2 * ↑(Fintype.card V) - A - ↑(Fintype.card { x : V // P x }) - 1 = L - (↑(Fintype.card { x : V // P x }) - 1)

The complete weighted-height count, with boundary sums explicit.