Finite multigraphs given by their ends

A multigraph on the vertices V with edges E, parallel edges and self-loops allowed, is given here by the map ends : E → Sym2 V sending each edge to its unordered pair of ends; a self-loop has equal ends. Assignments of values to the edges are then functions on E, as in Tseitin formulas (Cslib.Logic.PL.CNF.tseitinFormula), and relabelling the edges along an equivalence changes none of the quantities below (Multigraph.card_incidence_comp, Multigraph.minBalancedCut_comp, ...).

The multigraph is connected when its underlying simple graph (Multigraph.toSimpleGraph) is, that is, exactly when an edge leaves every nonempty set of vertices other than the set of all vertices (Multigraph.connected_toSimpleGraph_iff). The least number of edges between a set of between a third and two thirds of the vertices and its complement (Multigraph.minBalancedCut) is the expansion e(G) of Ben-Sasson and Wigderson, which bounds the width of resolution refutations of Tseitin formulas.

Main definitions

• Cslib.Multigraph.toGraph: the multigraph as a Mathlib Graph.
• Cslib.Multigraph.toSimpleGraph: the simple graph underlying a multigraph.
• Cslib.Multigraph.incidence: the edges at a vertex other than self-loops.
• Cslib.Multigraph.edgeCut: the edges between a set of vertices and its complement.
• Cslib.Multigraph.minBalancedCut: the expansion e(G) of Ben-Sasson and Wigderson.

Main results

• Cslib.Multigraph.incidenceSet_toGraph, Cslib.Multigraph.coe_edgeCut_eq_toGraph_edgeCut: incidence sets and edge cuts match those of Mathlib's Graph.
• Cslib.Multigraph.coe_incidence_eq_incidenceSet_toGraph: the edges at a vertex other than self-loops are the non-loop incident edges of toGraph ends.
• Cslib.Multigraph.edgeSet_toSimpleGraph: the edges of the underlying simple graph.
• Cslib.Multigraph.connected_toSimpleGraph_iff: connectivity as a cut condition.
• Cslib.Multigraph.le_minBalancedCut_iff: the characterization of e(G).

References

• E. Ben-Sasson, A. Wigderson, Short proofs are narrow—resolution made simple

def Cslib.Multigraph.toGraph {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) : Graph V E

A multigraph given by ends : E → Sym2 V as a Mathlib Graph whose vertex set and edge set are everything.

@[simp]

theorem Cslib.Multigraph.toGraph_isLink {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} {e : E} {x y : V} : (toGraph ends).IsLink e x y ↔ ends e = s(x, y)

An edge e links x and y in toGraph ends iff its unordered endpoints are s(x, y).

@[simp]

theorem Cslib.Multigraph.incidenceSet_toGraph {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) (v : V) : Graph.incidenceSet v = {e : E | v ∈ ends e}

The incident edges of v in toGraph ends are those having v as an endpoint.

def Cslib.Multigraph.toSimpleGraph {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) : SimpleGraph V

The simple graph underlying the multigraph ends: distinct vertices are adjacent when an edge joins them. Self-loops are dropped and parallel edges merged.

theorem Cslib.Multigraph.toSimpleGraph_adj {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} {u v : V} : (toSimpleGraph ends).Adj u v ↔ u ≠ v ∧ ∃ (e : E), ends e = s(u, v)

u and v are adjacent in the underlying simple graph exactly when they are distinct and some edge has ends u and v.

theorem Cslib.Multigraph.edgeSet_toSimpleGraph {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) : (toSimpleGraph ends).edgeSet = Set.range ends \ {e : Sym2 V | e.IsDiag}

The edges of the underlying simple graph are the ends of edges other than self-loops.

theorem Cslib.Multigraph.toSimpleGraph_comp {V : Type u_1} {E : Type u_2} {E' : Type u_3} (ends : E → Sym2 V) (f : E' ≃ E) : toSimpleGraph (ends ∘ ⇑f) = toSimpleGraph ends

Relabelling the edges does not change the underlying simple graph.

def Cslib.Multigraph.incidence {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] (v : V) : Finset E

The edges at v other than self-loops. A self-loop at v is left out: it would count twice towards the parity of the edges at v, as in Tseitin formulas, and so not at all.

@[simp]

theorem Cslib.Multigraph.mem_incidence {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] {v : V} {e : E} : e ∈ incidence ends v ↔ v ∈ ends e ∧ ¬(ends e).IsDiag

An edge is at v, and not a self-loop, exactly when v is one of its ends and its ends are distinct.

theorem Cslib.Multigraph.mem_incidence_of_ends_eq {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] {v a b : V} {e : E} (h : ends e = s(a, b)) : e ∈ incidence ends v ↔ (v = a ∨ v = b) ∧ a ≠ b

An edge with ends a and b is at v, and not a self-loop, when v is one of its ends and a ≠ b.

theorem Cslib.Multigraph.card_incidence_comp {V : Type u_1} {E : Type u_2} {E' : Type u_3} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype E'] (f : E' ≃ E) (v : V) : (incidence (ends ∘ ⇑f) v).card = (incidence ends v).card

Relabelling the edges does not change the number of edges at a vertex.

theorem Cslib.Multigraph.coe_incidence_eq_incidenceSet_toGraph {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] (v : V) : ↑(incidence ends v) = Graph.incidenceSet v \ {e : E | (ends e).IsDiag}

The edges at v other than self-loops are the non-loop incident edges of toGraph ends.

theorem Cslib.Multigraph.coe_incidence_subset_toGraph_incidenceSet {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] (v : V) : ↑(incidence ends v) ⊆ Graph.incidenceSet v

Every non-loop incident edge of v is in the incidence set of toGraph ends.

def Cslib.Multigraph.edgeCut {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] (S : Finset V) : Finset E

The edges between S and its complement.

theorem Cslib.Multigraph.mem_edgeCut {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] [Fintype V] {S : Finset V} {e : E} : e ∈ edgeCut ends S ↔ ∃ v ∈ S, ∃ w ∈ Sᶜ, ends e = s(v, w)

An edge is in the edge cut of S exactly when it joins a vertex of S to a vertex of Sᶜ.

theorem Cslib.Multigraph.coe_edgeCut_eq_toGraph_edgeCut {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] (S : Finset V) : ↑(edgeCut ends S) = (toGraph ends).edgeCut ↑S

The edge cuts of ends are those of Mathlib's Graph.

theorem Cslib.Multigraph.edgeCut_compl {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] (S : Finset V) : edgeCut ends Sᶜ = edgeCut ends S

The edges between a set and its complement are those between the complement and the set.

theorem Cslib.Multigraph.card_edgeCut_comp {V : Type u_1} {E : Type u_2} {E' : Type u_3} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] [Fintype E'] (f : E' ≃ E) (S : Finset V) : (edgeCut (ends ∘ ⇑f) S).card = (edgeCut ends S).card

Relabelling the edges does not change the number of edges leaving a set.

noncomputable def Cslib.Multigraph.minBalancedCut {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] : ℕ

The expansion e(G) of the multigraph ends Ben-Sasson and Wigderson: the least number of edges between a set S of vertices with |V| / 3 ≤ |S| ≤ 2 |V| / 3 and its complement, that is the least edge cut of a balanced partition of the vertices. With one vertex there is no such set; then e(G) = 0 by convention.

theorem Cslib.Multigraph.minBalancedCut_le_card_edgeCut {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] {S : Finset V} (h₁ : Fintype.card V ≤ 3 * S.card) (h₂ : 3 * S.card ≤ 2 * Fintype.card V) : minBalancedCut ends ≤ (edgeCut ends S).card

e(G) is at most the number of edges leaving any set of between a third and two thirds of the vertices.

theorem Cslib.Multigraph.exists_card_edgeCut_eq_minBalancedCut {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] (hV : 2 ≤ Fintype.card V) : ∃ (S : Finset V), Fintype.card V ≤ 3 * S.card ∧ 3 * S.card ≤ 2 * Fintype.card V ∧ (edgeCut ends S).card = minBalancedCut ends

With at least two vertices, e(G) is the number of edges leaving some set of between a third and two thirds of the vertices.

theorem Cslib.Multigraph.le_minBalancedCut_iff {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] (hV : 2 ≤ Fintype.card V) {k : ℕ} : k ≤ minBalancedCut ends ↔ ∀ (S : Finset V), Fintype.card V ≤ 3 * S.card → 3 * S.card ≤ 2 * Fintype.card V → k ≤ (edgeCut ends S).card

With at least two vertices, k ≤ e(G) exactly when at least k edges leave every set of between a third and two thirds of the vertices.

theorem Cslib.Multigraph.minBalancedCut_eq_zero_of_subsingleton {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] [Subsingleton V] : minBalancedCut ends = 0

With at most one vertex, e(G) = 0 by convention.

theorem Cslib.Multigraph.minBalancedCut_comp {V : Type u_1} {E : Type u_2} {E' : Type u_3} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] [Fintype E'] (f : E' ≃ E) : minBalancedCut (ends ∘ ⇑f) = minBalancedCut ends

Relabelling the edges does not change e(G).

theorem Cslib.Multigraph.connected_toSimpleGraph_iff {V : Type u_1} {E : Type u_2} (ends : E → Sym2 V) [Fintype E] [DecidableEq V] [Fintype V] : (toSimpleGraph ends).Connected ↔ Nonempty V ∧ ∀ (S : Finset V), S.Nonempty → S ≠ Finset.univ → (edgeCut ends S).Nonempty

Connectivity as a cut condition: a multigraph is connected exactly when it has a vertex and an edge leaves every nonempty set of vertices other than the set of all vertices.