Multigraphs, layouts, and the layout hypothesis

A Multigraph V E gives every edge two endpoints. Parallel edges are distinct elements of E; the orientation of an edge plays no role. A layout numbers the vertices v₀, v₁, ..., and its frontier at time t is the cut between the first t vertices and the rest. The width of a layout is the size of its largest frontier; the cutwidth of a graph is the least width of a layout.

For a connected graph, the cycle rank β₁ = |E| - |V| + 1 counts its independent cycles. Trees have cycle rank zero and, in bounded degree, logarithmic cutwidth. The circuit lower bound 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. For subcubic graphs (d = 3, the case of circuits of fan-in two) it is proved in Frontier.Layouts with A = (3/π) arccos((1 + 2√2)/4) ≈ 0.2807, from Gaussian edge-score layouts, and hence with A = 1/3. The circuit lower bounds take LayoutBound (r + 1) A as an assumption and prove the coefficient (1 + 1/A) / (r - 1) for circuits of fan-in r.

Main definitions

• Frontier.Multigraph: a multigraph, with Incident, edgesAt, MaxDegreeLE, Loopless, Adj, Connected, cut, and cycleRank.
• Frontier.Layout V: a numbering of the vertices, with Layout.initial.
• Frontier.LayoutBound d A: the layout hypothesis for maximum degree d with coefficient A.

Main results

• Frontier.Multigraph.Connected.card_vertex_le: a connected graph has at least |V| - 1 edges, so its cycle rank |E| + 1 - |V| involves no truncation.

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

A multigraph: every edge has two endpoints, its source and its target. Parallel edges are distinct elements of E. 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 Complexity.Frontier.Multigraph.Incident {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) (e : E) : Prop

An edge is incident to each of its endpoints.

Equations

• G.Incident v e = (G.src e = v ∨ G.tgt e = v)

def Complexity.Frontier.Multigraph.edgesAt {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) : Set E

The edges incident to a vertex.

Equations

• G.edgesAt v = {e : E | G.Incident v e}

def Complexity.Frontier.Multigraph.MaxDegreeLE {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (d : ℕ) : Prop

Every vertex has at most d incident edges.

Equations

• G.MaxDegreeLE d = ∀ (v : V), (G.edgesAt v).ncard ≤ d

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

No edge joins a vertex to itself.

Equations

• G.Loopless = ∀ (e : E), G.src e ≠ G.tgt e

def Complexity.Frontier.Multigraph.Adj {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (u v : V) : Prop

Two vertices are adjacent when an edge joins them.

Equations

• G.Adj u v = ∃ (e : E), G.src e = u ∧ G.tgt e = v ∨ G.src e = v ∧ G.tgt e = u

def Complexity.Frontier.Multigraph.Connected {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : Prop

Every two vertices are joined by a walk.

Equations

• G.Connected = ∀ (u v : V), Relation.ReflTransGen G.Adj u v

def Complexity.Frontier.Multigraph.cut {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (L : Set V) : Set E

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

Equations

• G.cut L = {e : E | ¬(G.src e ∈ L ↔ G.tgt e ∈ L)}

def Complexity.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.

Equations

• G.touching L = {e : E | G.src e ∈ L ∨ G.tgt e ∈ L}

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

The connected cycle-rank expression max (|E| - |V| + 1) 0. For a nonempty connected graph, this is the number of independent cycles. On disconnected graphs it is not the sum of the component cycle ranks.

Equations

• _G.cycleRank = Nat.card E + 1 - Nat.card V

theorem Complexity.Frontier.Multigraph.mem_cut {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {L : Set V} {e : E} : e ∈ G.cut L ↔ ¬(G.src e ∈ L ↔ G.tgt e ∈ L)

@[simp]

theorem Complexity.Frontier.Multigraph.cut_empty {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : G.cut ∅ = ∅

@[simp]

theorem Complexity.Frontier.Multigraph.cut_univ {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : G.cut Set.univ = ∅

theorem Complexity.Frontier.Multigraph.cut_insert_subset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) (L : Set V) : G.cut (insert v L) ⊆ G.cut L ∪ G.edgesAt v

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

theorem Complexity.Frontier.Multigraph.Adj.symm {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {u v : V} (h : G.Adj u v) : G.Adj v u

Adjacency is symmetric.

theorem Complexity.Frontier.Multigraph.reflTransGen_adj_symm {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {u v : V} (h : Relation.ReflTransGen G.Adj u v) : Relation.ReflTransGen G.Adj v u

Walks can be reversed.

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

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

theorem Complexity.Frontier.Multigraph.connected_of_forall_reflTransGen {V : Type u_1} {E : Type u_2} {G : Multigraph V E} (root : V) (h : ∀ (v : V), Relation.ReflTransGen G.Adj v root) : G.Connected

A graph in which every vertex reaches one fixed vertex is connected.

@[reducible, inline]

abbrev Complexity.Frontier.Layout (V : Type u_1) : Type u_1

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

Equations

• Complexity.Frontier.Layout V = (V ≃ Fin (Nat.card V))

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

The first t vertices of a layout.

Equations

• π.initial t = {v : V | ↑(π v) < t}

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

@[simp]

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

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

theorem Complexity.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.

def Complexity.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 all of whose frontiers have at most (A + η) β₁ + η |V| + C edges, where β₁ is the cycle rank.

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

Equations

• One or more equations did not get rendered due to their size.