Multigraphs, layouts, and the layout hypothesis

A Multigraph V E gives every edge two endpoints. Parallel edges are distinct elements of E, and the orientation of an edge plays no role: incidence, cuts and connectivity depend only on the unordered pair G.ends e. A multigraph is the spanning case of Mathlib's Graph V E (Multigraph.toGraph), presented with the vertices and edges as types, so that layouts are numberings of a type and assignments of values to the edges are functions on E. Its map Multigraph.ends presents it as a multigraph given by its ends (Cslib.Multigraph): the two share the underlying simple graph by definition, and their edge cuts agree (Multigraph.coe_edgeCut_ends). Unlike Cslib.Multigraph.incidence, which leaves self-loops out for parity arguments, Multigraph.incidenceSet counts a self-loop at its vertex once (Multigraph.coe_incidence_ends).

A layout numbers the vertices v₀, v₁, ..., and its frontier at time t is the edge cut between the first t vertices and the rest. The width of a layout is the size of its largest frontier.

For a connected graph, the cycle rank β₁ = |E| - |V| + 1 counts its independent cycles. The frontier method needs one fact from graph theory: that graphs of maximum degree d have layouts whose width is at most a fixed multiple A of their cycle rank, up to lower-order terms. LayoutBound d A states this as a hypothesis, so that any layout theorem can be plugged in.

A set of vertices W is closed when no edge leaves it: G.edgeCut W = ∅. Connected components (Multigraph.component) are closed, and adding a disjoint closed set to a set of vertices does not change its edge cut (Multigraph.edgeCut_union_of_edgeCut_eq_empty). The cycle rank of a closed set W is |E(W)| + 1 - |W|, where E(W) are the edges with an endpoint in W (Multigraph.cycleRankOn); it is the cycle rank of the subgraph induced on W (Multigraph.induce).

Main definitions

• Cslib.Circuits.Frontier.Multigraph: a multigraph, with incidenceSet, MaxDegreeLE, Loopless, toSimpleGraph (whose connectivity is that of the multigraph), edgeCut, and cycleRank.
• Cslib.Circuits.Frontier.Layout V: a numbering of the vertices, with Layout.initial.
• Cslib.Circuits.Frontier.Multigraph.cycleRankOn: the cycle rank of a set of vertices.
• Cslib.Circuits.Frontier.Multigraph.component: the connected component of a vertex.
• Cslib.Circuits.Frontier.Multigraph.induce: the subgraph induced on a set of vertices.
• Cslib.Circuits.Frontier.Multigraph.frontier, Multigraph.width: the frontiers of a layout and its width.
• Cslib.Circuits.Frontier.LayoutBound d A: the layout hypothesis for maximum degree d with coefficient A.

Main results

• Cslib.Circuits.Frontier.Multigraph.edgeCut_toGraph: edge cuts are those of Mathlib's multigraphs.
• Cslib.Circuits.Frontier.Multigraph.toSimpleGraph_eq, Cslib.Circuits.Frontier.Multigraph.coe_edgeCut_ends, Cslib.Circuits.Frontier.Multigraph.coe_incidence_ends: the simple graph, edge cuts and incidences of the multigraph given by the ends.
• Cslib.Circuits.Frontier.Multigraph.card_le_card_add_one_of_connected: a connected graph has at least |V| - 1 edges, so its cycle rank |E| + 1 - |V| involves no truncation.
• Cslib.Circuits.Frontier.Multigraph.edgeCut_union_of_edgeCut_eq_empty: closed sets do not change edge cuts.
• Cslib.Circuits.Frontier.Multigraph.edgeCut_component, Cslib.Circuits.Frontier.Multigraph.connected_induce_component: components are closed and connected.
• Cslib.Circuits.Frontier.Multigraph.ncard_component_le_ncard_touching_add_one: a component W has at least |W| - 1 edges.
• Cslib.Circuits.Frontier.Multigraph.frontier_succ_subset: consecutive frontiers differ only at the edges of the vertex processed in between.

structure Cslib.Circuits.Frontier.Multigraph (V : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A multigraph with vertices V and edges E: every edge has two endpoints, its source and its target. Parallel edges are distinct elements of E, and loops are allowed. The orientation plays no role in what follows.

• src : E → V

  One endpoint of an edge.

• tgt : E → V

  The other endpoint of an edge.

def Cslib.Circuits.Frontier.Multigraph.ends {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (e : E) : Sym2 V

The ends of an edge, as an unordered pair.

def Cslib.Circuits.Frontier.Multigraph.incidenceSet {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : Set E

The edges incident to a vertex.

def Cslib.Circuits.Frontier.Multigraph.MaxDegreeLE {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] (d : ℕ) : Prop

Every vertex is incident to at most d edges. In a loopless multigraph this says that the maximum degree is at most d. The finite edge type ensures that natural cardinalities count every incident edge.

def Cslib.Circuits.Frontier.Multigraph.Loopless {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : Prop

No edge joins a vertex to itself.

def Cslib.Circuits.Frontier.Multigraph.toSimpleGraph {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : SimpleGraph V

The simple graph underlying a multigraph: two distinct vertices are adjacent when an edge joins them. A multigraph is connected when this simple graph is. It is the simple graph of the multigraph given by the ends (Cslib.Multigraph.toSimpleGraph).

def Cslib.Circuits.Frontier.Multigraph.edgeCut {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (L : Set V) : Set E

The edge cut of a set of vertices L: the edges with exactly one endpoint in L.

def Cslib.Circuits.Frontier.Multigraph.touching {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (L : Set V) : Set E

The edges with an endpoint in L.

noncomputable def Cslib.Circuits.Frontier.Multigraph.cycleRank {V : Type u_1} {E : Type u_2} (_G : Multigraph V E) : ℕ

The cycle rank |E| + 1 - |V|. For a nonempty connected multigraph this is the number of independent cycles, the dimension of its cycle space; on disconnected graphs it is not the sum of the cycle ranks of the components.

theorem Cslib.Circuits.Frontier.Multigraph.mem_incidenceSet {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {v : V} {e : E} : e ∈ G.incidenceSet v ↔ G.src e = v ∨ G.tgt e = v

theorem Cslib.Circuits.Frontier.Multigraph.mem_edgeCut {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {L : Set V} {e : E} : e ∈ G.edgeCut L ↔ ¬(G.src e ∈ L ↔ G.tgt e ∈ L)

theorem Cslib.Circuits.Frontier.Multigraph.mem_touching {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {L : Set V} {e : E} : e ∈ G.touching L ↔ G.src e ∈ L ∨ G.tgt e ∈ L

theorem Cslib.Circuits.Frontier.Multigraph.toSimpleGraph_eq {V : Type u_1} {E : Type u_2} {G : Multigraph V E} : G.toSimpleGraph = Cslib.Multigraph.toSimpleGraph G.ends

The simple graph of a multigraph is that of the multigraph given by its ends.

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

theorem Cslib.Circuits.Frontier.Multigraph.reachable_src_tgt {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (e : E) : G.toSimpleGraph.Reachable (G.src e) (G.tgt e)

The endpoints of an edge are joined in the underlying simple graph.

@[simp]

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_empty {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : G.edgeCut ∅ = ∅

@[simp]

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_univ {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : G.edgeCut Set.univ = ∅

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_subset_touching {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (L : Set V) : G.edgeCut L ⊆ G.touching L

The edges of the cut of L touch L.

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_insert_subset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) (L : Set V) : G.edgeCut (insert v L) ⊆ G.edgeCut L ∪ G.incidenceSet v

Adding a vertex changes a cut only at the edges incident to it.

theorem Cslib.Circuits.Frontier.Multigraph.card_le_card_add_one_of_connected {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] (h : G.toSimpleGraph.Connected) : Nat.card V ≤ Nat.card E + 1

A connected multigraph has at least |V| - 1 edges: its cycle rank |E| + 1 - |V| involves no truncation.

Mathlib's multigraphs

def Cslib.Circuits.Frontier.Multigraph.toGraph {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : Graph V E

A multigraph as a Mathlib Graph whose vertex set and edge set are everything.

@[simp]

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

@[simp]

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_toGraph {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (L : Set V) : G.toGraph.edgeCut L = G.edgeCut L

The edge cuts of a multigraph are those of Mathlib's Graph.

@[simp]

theorem Cslib.Circuits.Frontier.Multigraph.incidenceSet_toGraph {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : Graph.incidenceSet v = G.incidenceSet v

The incidence sets of a multigraph are those of Mathlib's Graph.

Multigraphs given by their ends

@[simp]

theorem Cslib.Circuits.Frontier.Multigraph.coe_edgeCut_ends {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype V] [Fintype E] [DecidableEq V] (S : Finset V) : ↑(Cslib.Multigraph.edgeCut G.ends S) = G.edgeCut ↑S

The edge cuts are those of the multigraph given by the ends.

theorem Cslib.Circuits.Frontier.Multigraph.coe_incidence_ends {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype E] [DecidableEq V] (v : V) : ↑(Multigraph.incidence G.ends v) = G.incidenceSet v ∩ {e : E | G.src e ≠ G.tgt e}

The incidences of the multigraph given by the ends are the incident edges other than self-loops.

Cycle rank of a set of vertices

noncomputable def Cslib.Circuits.Frontier.Multigraph.cycleRankOn {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (W : Set V) : ℕ

The truncated expression |E(W)| + 1 - |W|, where E(W) are the edges with an endpoint in W. For a connected component it is the number of independent cycles of the component; it need not be additive over components.

Closed sets

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_eq_empty_iff {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} : G.edgeCut W = ∅ ↔ ∀ (e : E), G.src e ∈ W ↔ G.tgt e ∈ W

A set of vertices is closed exactly when every edge has either both endpoints in it or none.

theorem Cslib.Circuits.Frontier.Multigraph.touching_mono {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {L M : Set V} (h : L ⊆ M) : G.touching L ⊆ G.touching M

A larger set of vertices touches more edges.

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_union_of_edgeCut_eq_empty {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {K L : Set V} (hK : G.edgeCut K = ∅) (h : Disjoint K L) : G.edgeCut (K ∪ L) = G.edgeCut L

Closed sets do not change edge cuts. Adding a closed set K to a set L disjoint from it does not change the edge cut of L.

theorem Cslib.Circuits.Frontier.Multigraph.touching_eq_of_edgeCut_eq_empty {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} (hW : G.edgeCut W = ∅) : G.touching W = {e : E | G.src e ∈ W ∧ G.tgt e ∈ W}

The edges touching a closed set W are those with both endpoints in W.

Connected components

theorem Cslib.Circuits.Frontier.Multigraph.connectedComponentMk_src {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (e : E) : G.toSimpleGraph.connectedComponentMk (G.src e) = G.toSimpleGraph.connectedComponentMk (G.tgt e)

The endpoints of an edge lie in the same connected component.

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_setOf_connectedComponentMk {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (P : G.toSimpleGraph.ConnectedComponent → Prop) : G.edgeCut {v : V | P (G.toSimpleGraph.connectedComponentMk v)} = ∅

Unions of components are closed. A set of vertices described by their connected components has an empty edge cut.

def Cslib.Circuits.Frontier.Multigraph.component {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : Set V

The connected component of a vertex v: the vertices joined to v by a walk.

theorem Cslib.Circuits.Frontier.Multigraph.mem_component {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {u v : V} : u ∈ G.component v ↔ G.toSimpleGraph.connectedComponentMk u = G.toSimpleGraph.connectedComponentMk v

theorem Cslib.Circuits.Frontier.Multigraph.mem_component_self {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : v ∈ G.component v

Every vertex lies in its own component.

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_component {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : G.edgeCut (G.component v) = ∅

Connected components are closed.

Induced subgraphs

def Cslib.Circuits.Frontier.Multigraph.induce {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (W : Set V) : Multigraph ↑W { e : E // G.src e ∈ W ∧ G.tgt e ∈ W }

The subgraph induced on a set of vertices W: the edges with both endpoints in W.

theorem Cslib.Circuits.Frontier.Multigraph.Loopless.induce {V : Type u_1} {E : Type u_2} {G : Multigraph V E} (hG : G.Loopless) (W : Set V) : (G.induce W).Loopless

Induced subgraphs of loopless graphs are loopless.

theorem Cslib.Circuits.Frontier.Multigraph.MaxDegreeLE.induce {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite E] {d : ℕ} (hG : G.MaxDegreeLE d) (W : Set V) : (G.induce W).MaxDegreeLE d

Induced subgraphs have no larger degrees.

theorem Cslib.Circuits.Frontier.Multigraph.toSimpleGraph_induce {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (W : Set V) : (G.induce W).toSimpleGraph = SimpleGraph.induce W G.toSimpleGraph

The simple graph underlying an induced subgraph is the induced simple graph.

theorem Cslib.Circuits.Frontier.Multigraph.connected_induce_component {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : (G.induce (G.component v)).toSimpleGraph.Connected

Components are connected.

theorem Cslib.Circuits.Frontier.Multigraph.cycleRank_induce {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} (hW : G.edgeCut W = ∅) : (G.induce W).cycleRank = G.cycleRankOn W

The subgraph induced on a closed set W has the cycle rank of W.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_component_le_ncard_touching_add_one {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] (v : V) : (G.component v).ncard ≤ (G.touching (G.component v)).ncard + 1

A component W has at least |W| - 1 edges, so its cycle rank |E(W)| + 1 - |W| involves no truncation.

theorem Cslib.Circuits.Frontier.Multigraph.edgeCut_image_val {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {W : Set V} (hW : G.edgeCut W = ∅) (S : Set ↑W) : G.edgeCut (Subtype.val '' S) = Subtype.val '' (G.induce W).edgeCut S

On a closed set W, the edge cuts of the induced subgraph are those of G.

Layouts

@[reducible, inline]

abbrev Cslib.Circuits.Frontier.Layout (V : Type u_1) : Type u_1

A layout of a finite set of vertices: a numbering v₀, v₁, ..., v_{N-1}.

instance Cslib.Circuits.Frontier.Layout.instNonemptyOfFinite {V : Type u_1} [Finite V] : Nonempty (Layout V)

def Cslib.Circuits.Frontier.Layout.initial {V : Type u_1} (π : Layout V) (t : ℕ) : Set V

The first t vertices of a layout.

theorem Cslib.Circuits.Frontier.Layout.mem_initial {V : Type u_1} (π : Layout V) {t : ℕ} {v : V} : v ∈ π.initial t ↔ ↑(π v) < t

@[simp]

theorem Cslib.Circuits.Frontier.Layout.initial_zero {V : Type u_1} (π : Layout V) : π.initial 0 = ∅

theorem Cslib.Circuits.Frontier.Layout.initial_of_card_le {V : Type u_1} (π : Layout V) {t : ℕ} (ht : Nat.card V ≤ t) : π.initial t = Set.univ

theorem Cslib.Circuits.Frontier.Layout.initial_succ {V : Type u_1} (π : Layout V) {t : ℕ} (ht : t < Nat.card V) : π.initial (t + 1) = insert ((Equiv.symm π) ⟨t, ht⟩) (π.initial t)

The first t + 1 vertices are the first t and the vertex numbered t.

theorem Cslib.Circuits.Frontier.Layout.ncard_initial {V : Type u_1} (π : Layout V) {t : ℕ} (ht : t ≤ Nat.card V) : (π.initial t).ncard = t

The first t ≤ |V| vertices of a layout are t vertices.

def Cslib.Circuits.Frontier.Multigraph.frontier {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) (t : ℕ) : Set E

The frontier of a layout at time t: the edge cut between the first t vertices and the rest.

noncomputable def Cslib.Circuits.Frontier.Multigraph.width {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) [Finite E] : ℕ

The width of a layout with finitely many edges: the size of its largest frontier.

theorem Cslib.Circuits.Frontier.Multigraph.mem_frontier {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) {t : ℕ} {e : E} : e ∈ G.frontier π t ↔ ¬(↑(π (G.src e)) < t ↔ ↑(π (G.tgt e)) < t)

An edge is on the frontier at time t when exactly one of its ends is among the first t vertices.

@[simp]

theorem Cslib.Circuits.Frontier.Multigraph.frontier_zero {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) : G.frontier π 0 = ∅

theorem Cslib.Circuits.Frontier.Multigraph.frontier_of_card_le {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) {t : ℕ} (ht : Nat.card V ≤ t) : G.frontier π t = ∅

theorem Cslib.Circuits.Frontier.Multigraph.frontier_succ_subset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) {t : ℕ} (ht : t < Nat.card V) : G.frontier π (t + 1) ⊆ G.frontier π t ∪ G.incidenceSet ((Equiv.symm π) ⟨t, ht⟩)

Consecutive frontiers differ only at the edges of the vertex processed in between.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_frontier_le_width {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) [Finite E] (t : ℕ) : (G.frontier π t).ncard ≤ G.width π

theorem Cslib.Circuits.Frontier.Multigraph.width_le_iff {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) [Finite E] {w : ℕ} : G.width π ≤ w ↔ ∀ (t : ℕ), (G.frontier π t).ncard ≤ w

def Cslib.Circuits.Frontier.LayoutBound (d : ℕ) (A : ℝ) : Prop

The layout hypothesis for maximum degree d, with coefficient A. For every η > 0 there is a constant C such that every connected, loopless multigraph of maximum degree d has a layout of width at most (A + η) β₁ + η |V| + C, where β₁ is the cycle rank.

Only the coefficient A matters for the circuit lower bounds: any error term that is sublinear in the number of vertices may be absorbed into η |V| + C.