134 Graph Theory — Karger Min Cut
134.1 Overview
This file develops a multigraph model (a Multiset of unordered pairs, since Mathlib’s SimpleGraph has no parallel edges) together with edge contraction, cuts and their sizes, and the structural lemmas behind Karger’s randomized contraction algorithm: contraction of a non-crossing edge preserves a minimum cut, every vertex degree bounds the min-cut size, the handshake lemma \(\sum _v \deg (v) = 2\left\lvert E\right\rvert \), the telescoping survival product \(2/(n(n-1))\), and the standard corollaries on repetition and on the number of (approximate) minimum cuts.
134.2 Declarations
A multigraph on a vertex type \(\alpha \) consists of a finite vertex set together with a multiset of unordered pairs (elements of \(\mathrm{Sym}_2\, \alpha \)) as edges, subject to two conditions: every endpoint of every edge is a live vertex, and no edge is a self-loop (edges are loopless, since loops are deleted after each contraction).
The number of edges of \(G\) counted with multiplicity, i.e. the cardinality of the edge multiset.
The number of vertices of \(G\), i.e. the cardinality of its vertex Finset.
Given an edge \(e \in E(G)\) with endpoints \(u\) and \(v\), the contracted multigraph \(G/e\) is obtained by replacing every occurrence of \(v\) by \(u\) in all edges, deleting the resulting self-loops (in particular all parallel copies of \(e\)), and removing \(v\) from the vertex set. Parallel edges between the merged vertex and the rest of the graph are retained with multiplicity.
If \(e \in E(G)\) is not a diagonal (self-loop) pair, then
For every edge \(e \in E(G)\), the contracted multigraph satisfies
so contraction never increases the edge count and removes at least the contracted edge.
A cut of \(G\) is a subset \(S \subseteq V(G)\) that is nonempty and whose complement \(V(G) \setminus S\) inside \(V(G)\) is also nonempty; the two nonemptiness conditions rule out the trivial partitions.
The multiset of edges of \(G\) that cross the cut \(C\), i.e. those edges having exactly one endpoint in \(S\), counted with multiplicity. It is obtained by filtering the edge multiset by the condition that exactly one of the two representative endpoints lies in \(S\).
For a finite set \(S\) and an unordered pair \(e\), the predicate \(\texttt{Crosses}\; S\; e\) holds when some element of \(e\) lies in \(S\) and some element of \(e\) lies outside \(S\). This is a membership-based formulation independent of a choice of representative.
For every finite set \(S\) and unordered pair \(e\), the predicate \(\texttt{Crosses}\; S\; e\) holds if and only if, writing \((x, y)\) for the chosen representative of \(e\), either \(x \in S\) and \(y \notin S\), or \(x \notin S\) and \(y \in S\).
For every cut \(C\) of \(G\), the multiset of crossing edges equals the edge multiset of \(G\) filtered by the predicate \(\texttt{Crosses}\; S\).
The size of a cut \(C\) is the number of crossing edges, counted with multiplicity.
A cut \(C\) of \(G\) is a minimum cut when its size is at most the size of every cut \(C'\) of \(G\).
If \(e \in E(G)\) does not cross the cut \(C\), then \(C\) induces a cut of the contracted multigraph \(G/e\): the vertex side is the image of \(S\) after merging the endpoints of \(e\), and both nonemptiness conditions continue to hold because \(e\) has both endpoints on the same side.
If \(e \in E(G)\) does not cross the cut \(C\), then the induced cut on \(G/e\) has the same size as \(C\):
If \(C\) is a minimum cut of \(G\) and \(e \in E(G)\) does not cross \(C\), then the induced cut on \(G/e\) is again a minimum cut. Thus only crossing edges can destroy a fixed minimum cut during contraction.
Given a multigraph \(G\) with at least one edge, a step of the algorithm is modelled as a function from an index \(i \in \mathrm{Fin}\, \left\lvert E(G)\right\rvert \) — thought of as a uniformly random edge choice — to the multigraph obtained by contracting the \(i\)-th edge of \(G\).
A run of the algorithm on \(G_0\) is indexed by a sequence of edge choices, one for each of the \(\left\lvert V(G_0)\right\rvert - 2\) contraction steps, and produces a multigraph. The current Lean definition is a placeholder that returns \(G_0\); the state-threading version is not yet formalized.
The predicate stating that \(G\) is a valid output of the algorithm, namely that it has exactly two vertices; its remaining edges are then exactly the edges of the output cut.
The degree of \(v\) in a loopless multigraph \(G\) is the number of edges incident to \(v\), counted with multiplicity.
If \(z\) belongs to the unordered pair \(e\), then \(z\) equals one of the two components of the chosen representative of \(e\).
For a multiset \(m\) of unordered pairs and a vertex \(v\), the multiplicity of \(v\) in the multiset obtained by binding each edge to its set of endpoints equals the number of edges of \(m\) containing \(v\).
Let \(v \in V(G)\) be a vertex such that \(V(G) \setminus \{ v\} \) is nonempty. Then the cut given by \(S = \{ v\} \) is a legitimate cut of \(G\) and its size equals \(\deg (v)\).
If \(G\) admits a cut \(C\), then for every vertex \(v\) the set \(V(G) \setminus \{ v\} \) is nonempty, since both sides of \(C\) are nonempty.
If \(C\) is a minimum cut of \(G\) and \(v \in V(G)\), then \(\left\lvert C\right\rvert \le \deg (v)\): otherwise the singleton cut at \(v\) would be smaller.
Any \(x\) occurring in the multiset of all edge endpoints of \(G\) belongs to \(V(G)\).
If every element of a multiset \(m\) lies in the finite set \(s\), then
For every multigraph \(G\),
If every vertex of \(G\) has degree at least \(k\), then
For a cut size \(c\) and a current edge count \(m\), the probability that a uniformly chosen edge is not one of the \(c\) cut edges, namely
Let \(C_0\) be a minimum cut of \(G_0\) and let \(i \lt \left\lvert V(G_0)\right\rvert - 1\). Then
the invariant maintained after \(i\) contraction steps.
For every \(n \ge 2\),
Let \(C\) be a minimum cut of a multigraph \(G\) with \(n = \left\lvert V(G)\right\rvert \ge 4\). Then the telescoping product of per-step survival factors, which represents the probability that none of the \(n-2\) contractions picks a cut edge, is bounded below by
Let \(n = \left\lvert V(G)\right\rvert \ge 4\). Repeating the algorithm \(n(n-1)/2\) independent times, the success probability satisfies
If \(p \gt 0\) and \(m \cdot p \le 1\) (as is the case for \(m\) disjoint events each of probability at least \(p\)), then \(m \le p^{-1}\).
For \(n \ge 2\),
as real numbers.
For all \(n\) and \(\alpha \), \(\binom {n}{2\alpha } \le n^{2\alpha }\).
Let \(n = \left\lvert V(G)\right\rvert \ge 2\). If a family of \(\mathrm{numCuts}\) cuts is disjoint in the sense that \(\mathrm{numCuts} \cdot \frac{2}{n(n-1)} \le 1\), then
Let \(\alpha \gt 0\) with \(2\alpha \le n = \left\lvert V(G)\right\rvert \). If a family of \(\mathrm{numCuts}\) \(\alpha \)-minimum cuts satisfies \(\mathrm{numCuts} \cdot \binom {n}{2\alpha }^{-1} \le 1\), then