External degrees in three-vertex stars

theorem ACMax.star_center_external_degree {V : Type u_1} [Fintype V] (G : SimpleGraph V) (h a b : V) (ha : G.Adj h a) (hb : G.Adj h b) (hab : a ≠ b) (hd : G.degree h = 4) : (G.neighborFinset h \ {h, a, b}).card = 2

A degree-four center has two neighbors outside a three-vertex star.

theorem ACMax.star_leaf_external_degree {V : Type u_1} [Fintype V] (G : SimpleGraph V) (h a b : V) (ha : G.Adj h a) (hab : ¬G.Adj a b) (hd : G.degree a = 3) : (G.neighborFinset a \ {h, a, b}).card = 2

A degree-three leaf has two neighbors outside an induced three-vertex star.

theorem ACMax.card_le_sum_excess {V : Type u_1} [Fintype V] (G : SimpleGraph V) (S : Finset V) (hdeg : ∀ x ∈ S, 4 ≤ G.degree x) : S.card ≤ ∑ x ∈ S, (G.degree x - 3)

Vertices of degree at least four each contribute at least one unit of excess.