The handshaking lemma is a simple result in graph theory that establishes a relationship between the degrees of the vertices in a finite graph and the number of edges in the graph. It states that the sum of the degrees of all the vertices in a graph is twice the number of edges in the graph

The Handshaking Lemma. Any finite simple graph satisfies \(\sum_{v} \deg(v) = 2 |E|\).

The above formula is also sometimes referred to as the sum degree formula with the term handshaking lemma used to refer to the corollary that the number of vertices that touch an odd number of edges is even. The proof of the sum degree formula will be short and sweet and canonically relies on double counting. Aigner and Ziegler write it up as follows:

Proof. For the proof consider \(S \subseteq V \times E\), where \(S\) is the set of pairs \((v,e)\) such that \(v \in V\) is an end-vertex of \(e \in E\). Counting \(S\) in two ways gives on the one hand \(\sum_{v \in V} \deg(v)\), since every vertex contributes \(\deg(v)\) to the count, and on the other hand \(2|E|\), since every edge has two ends.
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 185.

Graphs are represented by the SimpleGraph structure in mathlib:

1
2
3
4

structure SimpleGraph (V : Type u) where
  Adj : V → V → Prop
  symm : Symmetric Adj := by aesop_graph
  loopless : Irreflexive Adj := by aesop_graph

Given some type of vertices V, a graph consists of a symmetric and irreflexive (meaning loopless) relation on V. It is a finite graph if the type V has the typeclass Fintype. This notion is perhaps slightly different from how many extremal combinatorialists might think of it in two way: First, there is no underlying vertex set, but instead an underlying vertex type. We have already discussed this previously, but for now all this means is that we write ∑ v : V, ... or simply ∑ v, ... instead of ∑ v ∈ V, .... The second and more important distinction is that edges are not defined as sets of two vertices but through a relation on the type of vertices. Invoking edgeSet or edgeFinset does yield the set of edges. However, on closer inspection we will see that the underlying type of the elements of these is not Finset V but rather Sym2 V, the type of unordered pairs of elements of V. Notably this type inherently does not prohibit loops and instead one needs to invoke the irreflexivity of the adjacency relation to exclude them. See [17587] for an example of how this can make handling edges somewhat unintuitive.

Let us fix some notation to make the proof nicer to read, i.e., we use # to denote the cardinality of a Finset [17646] , E to denote the edgeFinset of a given G, and finally d(v) and I(v) to denote the degree and incidenceFinset of a given vertex v.

1
2
3
4

prefix:100 "#" => Finset.card
local notation "E" => G.edgeFinset
local notation "d(" v ")" => G.degree v
local notation "I(" v ")" => G.incidenceFinset v

Using this notation, we can state and prove the sum degree formula in a concise and readable form using the calc tactic.

1
2
3
4
5
6
7
8

lemma handshaking : ∑ v, d(v) = 2 * #E := by
  calc  ∑ v, d(v)
    _ = ∑ v, #I(v)             := by simp [G.card_incidenceFinset_eq_degree]
    _ = ∑ v, #{e ∈ E | v ∈ e}  := by simp [G.incidenceFinset_eq_filter]
    _ = ∑ e ∈ E, #{v | v ∈ e}  := Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow _
    _ = ∑ e ∈ E, 2             := Finset.sum_congr rfl (λ e he ↦ (G.card_filter_mem_of_mem_edgeFinset e he))
    _ = 2 * ∑ e ∈ E, 1         := (Finset.mul_sum E (λ _ ↦ 1) 2).symm
    _ = 2 * #E                 := by rw [Finset.card_eq_sum_ones E]

The decisive step here is going from ∑ v, #{e ∈ E | v ∈ e} to ∑ e ∈ E, #{v | v ∈ e}, which is possible precisely due to the double counting argument. There are a number of double counting arguments in mathlib, but the one relevant for our purposes is sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow. This lemma states that for any sets (s : Finset α) and (t : Finset β) along with a relation (r : α → β → Prop) the sum ∑ a ∈ s, #(t.bipartiteAbove r a) is the same as ∑ b ∈ t, #(s.bipartiteBelow r b); this means that summing the number of elements in t related to a given a ∈ s is the same as summing the number of elements in s related to a given b ∈ t. Everything before this step simply modifies the summand to make the application of this lemma possible: card_incidenceFinset_eq_degree allows us to rewrite the degree as the cardinality of the incidence finset, and incidenceFinset_eq_filter essentially unfolds the definition of the incidence finset. After this, we simple use the fact that an edge contains two vertices in the form of card_filter_mem_of_mem_edgeFinset [17587] and that summing ones over a finite set yields the cardinality of that set.

This concludes the proof. 🎉