Finite simple undirected graphs: neighbours, degrees and the handshake formula

Goal and scope

Let V={1,2,3,4,5}, with edges entered as a list of endpoint pairs: (1,2), (2,1), (2,3), (3,4), (2,4), (4,2), each entry denoting an undirected edge. Normalize the input to the edge set E, find the neighbour set N(v) and degree deg(v) of every vertex, check that the degree sum equals 2|E|, and prove the handshake formula Σ_{v∈V} deg(v)=2|E| for every finite simple undirected graph.

Works inside the MKO's scope: a finite vertex set, edges as two-element subsets, no loops or multiple edges, and the empty graph allowed. Proves the handshake formula by double counting; the double-counting principle (counting a finite set of pairs by grouping on either coordinate) is a premise. Directed graphs, multigraphs, loop counting, connectivity and trees are not treated; adjacency is never inferred from a drawing; the canonical MKO and its English edition are not changed.

Givens and symbols

• set_extensionality
• set_builder
• finite_counting_basics
• finite_sum_rules
• numeric_evaluation
• graph_defs

• G1 — V={1,2,3,4,5}, with distinct vertex labels (MKO assumption a1).
• G2 — The input list is, in order, (1,2), (2,1), (2,3), (3,4), (2,4), (4,2); each entry (u,v) denotes the undirected edge {u,v}, and an undirected edge ignores endpoint order (MKO assumption a2).
• G3 — A second graph G₀=({1,2,3},∅) is used to check the boundary case of an empty edge set.

• G=(V,E) — a finite simple undirected graph
• \{u,v\} — the undirected edge with endpoints u, v (u≠v)
• N(v) — the neighbour set {u∈V ∣ {u,v}∈E} of v
• \deg(v) — the degree |N(v)| of v
• E_v — the set {e∈E ∣ v∈e} of edges at v
• I — the incidence set {(v,e)∈V×E ∣ v∈e}

Rules and sources

• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_graph_def · cited — A finite simple undirected graph G=(V,E) consists of a finite vertex set V and an edge set E of two-element subsets of V. There are no loops or multiple edges. N(v)={u∈V:{u,v}∈E}, deg(v)=|N(v)|, and the sum of all vertex degrees is 2|E|. · mko-graph
• graph_defs · prerequisite — The definitions only (without the degree-sum conclusion): G=(V,E) with V finite and every element of E a two-element subset {u,v} of V (u≠v); N(v)={u∈V ∣ {u,v}∈E}; deg(v)=|N(v)|.
• two_element_set · prerequisite — {u,v}={v,u}; when u≠v, {u,v} has exactly two elements; {u,u}={u} has one element; z∈{u,v} exactly when z=u or z=v.
• roster_membership · prerequisite — Membership in a listed set: for a finite set given by listing, S={s_i ∣ 1≤i≤n}, z∈S exactly when z=s_i for some i.
• double_counting · prerequisite — Double counting: for finite sets X, Y and I⊆X×Y, |I|=Σ_{x∈X} |{y∈Y ∣ (x,y)∈I}|=Σ_{y∈Y} |{x∈X ∣ (x,y)∈I}| (I splits into disjoint slices by either coordinate, and the addition rule for disjoint finite sets applies).
• L_handshake · lemma — For every finite simple undirected graph G=(V,E), Σ_{v∈V} deg(v)=2|E|.

Main derivation

(1,2),(2,1),(2,3),(3,4),(2,4),(4,2)

\text{each entry has two distinct endpoints in}\ V

\{1,2\},\{2,1\},\{2,3\},\{3,4\},\{2,4\},\{4,2\}

E=\{\{1,2\},\{2,3\},\{3,4\},\{2,4\}\}

E=\{\{1,2\},\{2,3\},\{3,4\},\{2,4\}\}

|E|=4

N(1)=\{u\in V\mid\{u,1\}\in E\}

N(1)=\{2\}

N(2)=\{u\in V\mid\{u,2\}\in E\}

N(2)=\{1,3,4\}

N(3),\ N(4)

N(3)=\{2,4\},\ N(4)=\{2,3\}

N(5)=\{u\in V\mid\{u,5\}\in E\}

N(5)=\varnothing

N(1),N(2),N(3),N(4),N(5)

\deg(1)=1,\ \deg(2)=3,\ \deg(3)=2,\ \deg(4)=2,\ \deg(5)=0

\sum_{v\in V}\deg(v),\ 2|E|

1+3+2+2+0=8=2\cdot 4

G=(V,E)\ \text{finite simple undirected}

\sum_{v\in V}\deg(v)=2|E|

|E'|=6\ \text{(counting list entries)}

2\cdot 6=12\neq 8=\sum_{v}\deg(v)

G_0=(\{1,2,3\},\varnothing)

\deg(v)=0\ \text{for every}\ v,\ \sum_{v}\deg(v)=0=2\cdot 0

\text{S02, S03, S08, S10, S12}

|E|=4,\ (\deg(v))_{v=1}^{5}=(1,3,2,2,0),\ \sum_v\deg(v)=2|E|

Substeps and lemmas

E_v=\{e\in E\mid v\in e\}

|E_v|=\deg(v)

\{v\in V\mid v\in e\}\ \text{for}\ e\in E

|\{v\in V\mid v\in e\}|=|e|=2

I=\{(v,e)\in V\times E\mid v\in e\}

\sum_{v\in V}\deg(v)=|I|=\sum_{e\in E}2=2|E|

Reverse audits

• S13 · sufficient_goal_reduction · S02, S03, S08, S10, S12, and_intro_elim — Goal G: E, the degrees, the check and the general proof of the handshake formula. Sufficient condition H: S02, S03, S08, S10, S12; H⇒G is just conjunction, H is proved forwards from G1 to G3, and G is never used as a premise.
• S12 · premise_audit · graph_defs, finite_sum_rules, L_handshake — It needs the convention that the empty sum is 0 (finite sum rules); N5 recomputes 0+0+0=2·0.
• S11 · premise_audit · S08, S10, contradiction, numeric_evaluation — This step only shows the wrong count contradicts the proved formula (N3); the correct |E|=4 comes from S02 and S03.
• S10.3 · premise_audit · S10.1, S10.2, double_counting, finite_sum_rules, eq_refl_symm_trans — V and E must be finite for double counting to apply; for an empty graph both sides are 0 and it still holds.
• S10.2 · premise_audit · graph_defs, two_element_set — It needs the endpoints to be distinct; both endpoints lying in V guarantees e⊆V.
• S10.1 · premise_audit · graph_defs, two_element_set, injective_surjective_def, finite_counting_basics — The guide fixes loop-free edges as two-element sets, and this injectivity argument uses u≠v. Allowing loops does not inevitably destroy the neighbour-to-incident-edge correspondence: with a loop represented by a singleton set it can remain bijective, while the later count of exactly two endpoints per edge fails. Loop-degree conventions would need a separate definition and are outside this guide.
• S10 · premise_audit · L_handshake, S03, S08 — G must be a finite simple undirected graph (confirmed in S01 and S02); directed graphs and multigraphs are out of scope.
• S09 · premise_audit · S03, S08, numeric_evaluation — This can be recomputed (N1, N2); it is not used to claim the formula for all graphs.
• S08 · premise_audit · S04, S05, S06, S07, graph_defs — Each N(v) must have been found correctly as a set; a degree counts distinct neighbours, not occurrences in the list.
• S07 · inverse_equivalence · graph_defs, set_extensionality — Both sets have no elements, so they are equal; this needs all four edges of E to be checked.
• S06 · inverse_equivalence · graph_defs, set_extensionality — As in S05, each candidate vertex is checked, so both directions hold.
• S05 · inverse_equivalence · graph_defs, set_extensionality — Checking the four candidates u≠2 in V, namely 1, 3, 4, 5, gives both inclusions.
• S04 · inverse_equivalence · graph_defs, set_extensionality — Both inclusions are checked: 2∈N(1) because {2,1}∈E; no other u has an edge containing both 1 and u.
• S03 · premise_audit · set_extensionality, finite_counting_basics — Distinctness must be confirmed before counting; this is exactly the point stressed in MKO paragraph one.
• S02 · inverse_equivalence · set_extensionality, two_element_set — The list and E describe the same edge set: every entry of the list is in E and every edge of E appears in the list, so it holds both ways.
• S01 · premise_audit · G1, G2, mko_graph_def, two_element_set — An entry (3,3) would correspond to {3,3}={3}, a one-element set, which is not an edge; this input has no such entry. This step only checks eligibility and does not count.

Error controls and negative controls

Do not count one undirected edge twice

One misconception named by the MKO is counting the two orderings of an undirected edge as two edges. {1,2}={2,1} and {2,4}={4,2}, so the six input entries give only four edges (S02, S03). Counting 6 would give 2·6=12, which disagrees with the degree sum 8 (S11); the handshake formula exposes the error at once.

A crossing in a drawing is not a vertex

The other misconception named by the MKO is treating a crossing of drawn lines as a new vertex. If 1, 2, 3, 4 are drawn at (0,0), (2,2), (0,2), (2,0), the segments of the edges {1,2} and {3,4} cross at (1,1), yet V is still {1,2,3,4,5}; (1,1) is not a vertex and creates no new edge. Adjacency is decided by E alone, not by a drawing.

Degree counts distinct neighbours, and isolated vertices still count

deg(2)=|{1,3,4}|=3, not the 5 occurrences of 2 in the list. 5 has no neighbour and deg(5)=0, but 5 is still a vertex and the degree sum includes it (adding 0). A loop {v,v}={v} is not a two-element set and does not exist in a simple graph.

• (1,2) and (2,1) are two different edges, so |E|=6 → reject — {1,2}={2,1}; |E|=4, and 2·6=12 disagrees with the degree sum 8.
• The point where two drawn edges cross is a new vertex → reject — The vertex set V is given; a crossing belongs only to the drawing, is not in V, and does not change E.
• 5 has no neighbour, so 5 is not a vertex of the graph → reject — 5∈V; it is an isolated vertex of degree 0.
• The edge {3,3} can be added, making deg(3) equal to 3 → reject — {3,3}={3} has one element and is not a two-element subset; a simple graph has no loops.

Result and limitations

The six input entries normalize to only four distinct undirected edges: E={{1,2},{2,3},{3,4},{2,4}}. The neighbour sets are N(1)={2}, N(2)={1,3,4}, N(3)={2,4}, N(4)={2,3}, N(5)=∅, the degrees are 1, 3, 2, 2, 0 in order, and the degree sum is 8=2·4=2|E|. For every finite simple undirected graph, Σ_v deg(v)=2|E| (proved by double counting); with an empty edge set the degree sum is 0.

• The double-counting principle (double_counting) is a premise of this guide and is not derived here step by step from the addition rule.
• This guide does not treat consequences of the handshake formula (such as the number of odd-degree vertices being even), nor directed graphs, multigraphs or connectivity.

Verification and source binding

6 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 56916889c62315f978ca130e85048a57dac57e96f65188fb5224dbb0fa53182f
• original source SHA-256: 695ff8e49c105f1940c6ba7abe0fe527fc5fa6cc710601419531ac68bc4782e4
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)