Boundary sums with one exceptional vertex

theorem MagnitudeConjecture.HeightArrowCount.boundary_sums {V : Type u} [Fintype V] [DecidableEq V] (s : V) (h d : V → ℤ) (hd : ∀ (x : V), d x = if x = s then 0 else 1) : ∑ x : V, d x = ↑(Fintype.card V) - 1 ∧ ∑ x : V, h x * d x = ∑ x : V, h x - h s

Boundary degrees are one except at a single distinguished vertex.

theorem MagnitudeConjecture.HeightArrowCount.boundary_card_eq {V : Type u} [Fintype V] (P I : V → Prop) [DecidablePred P] [DecidablePred I] (e : { x : V // ¬P x } ≃ { x : V // ¬I x }) : Fintype.card { x : V // P x } = Fintype.card { x : V // I x }

Complementary translation sets have equally many boundary vertices.