Finite multigraphs, prefix cuts, and the graph-ordering hypothesis

A Multigraph V E records the two endpoints of every edge in E. Parallel edges are distinct elements of E and are counted separately. For a vertex ordering, the cut after a vertex is the set of edges with exactly one endpoint among the vertices up to it; these are exactly the cuts of the lower sets of the order.

OrderingBound η C is the graph-ordering hypothesis: every connected loopless multigraph of maximum degree three has a vertex ordering whose prefix cuts have at most (1/3 + η) (M - N)⁺ + 3 log₂ N + C edges, where N and M are the numbers of vertices and edges. The lower bound takes this statement as a hypothesis; it is not proved in this development.

structure Algebraic.Cutwidth.Multigraph (V E : Type) : Type

A multigraph: every edge has a first and a second endpoint. Parallel edges are distinct elements of E.

• fst : E → V

  The first endpoint of an edge.

• snd : E → V

  The second endpoint of an edge.

def Algebraic.Cutwidth.Multigraph.Incident {V E : Type} (G : Multigraph V E) (v : V) (e : E) : Prop

An edge is incident to each of its endpoints.

Equations

• G.Incident v e = (G.fst e = v ∨ G.snd e = v)

def Algebraic.Cutwidth.Multigraph.Loopless {V E : Type} (G : Multigraph V E) : Prop

No edge joins a vertex to itself.

Equations

• G.Loopless = ∀ (e : E), G.fst e ≠ G.snd e

def Algebraic.Cutwidth.Multigraph.Adj {V E : Type} (G : Multigraph V E) (u v : V) : Prop

Two vertices are adjacent when some edge joins them, in either direction.

Equations

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

theorem Algebraic.Cutwidth.Multigraph.Adj.symm {V E : Type} {G : Multigraph V E} {u v : V} (h : G.Adj u v) : G.Adj v u

def Algebraic.Cutwidth.Multigraph.Connected {V E : Type} (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

theorem Algebraic.Cutwidth.Multigraph.reflTransGen_adj_symm {V E : Type} {G : Multigraph V E} {u v : V} (h : Relation.ReflTransGen G.Adj u v) : Relation.ReflTransGen G.Adj v u

Reachability along walks is symmetric.

theorem Algebraic.Cutwidth.Multigraph.connected_of_forall_reflTransGen {V E : Type} {G : Multigraph V E} (root : V) (h : ∀ (v : V), Relation.ReflTransGen G.Adj v root) : G.Connected

A multigraph in which every vertex reaches a common vertex is connected.

noncomputable def Algebraic.Cutwidth.Multigraph.edgesAt {V E : Type} (G : Multigraph V E) [Fintype E] (v : V) : Finset E

The edges incident to a vertex.

Equations

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

theorem Algebraic.Cutwidth.Multigraph.mem_edgesAt {V E : Type} (G : Multigraph V E) [Fintype E] {v : V} {e : E} : e ∈ G.edgesAt v ↔ G.Incident v e

noncomputable def Algebraic.Cutwidth.Multigraph.degree {V E : Type} (G : Multigraph V E) [Fintype E] (v : V) : ℕ

The number of edges incident to a vertex.

Equations

• G.degree v = (G.edgesAt v).card

def Algebraic.Cutwidth.Multigraph.MaxDegreeLE {V E : Type} (G : Multigraph V E) [Fintype E] (d : ℕ) : Prop

Every vertex has at most d incident edges.

Equations

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

noncomputable def Algebraic.Cutwidth.Multigraph.cut {V E : Type} (G : Multigraph V E) [Fintype E] (L : Finset V) : Finset E

The edges with exactly one endpoint in L.

Equations

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

theorem Algebraic.Cutwidth.Multigraph.mem_cut {V E : Type} (G : Multigraph V E) [Fintype E] {L : Finset V} {e : E} : e ∈ G.cut L ↔ ¬(G.fst e ∈ L ↔ G.snd e ∈ L)

@[simp]

theorem Algebraic.Cutwidth.Multigraph.cut_empty {V E : Type} (G : Multigraph V E) [Fintype E] : G.cut ∅ = ∅

@[simp]

theorem Algebraic.Cutwidth.Multigraph.cut_univ {V E : Type} (G : Multigraph V E) [Fintype E] [Fintype V] : G.cut Finset.univ = ∅

theorem Algebraic.Cutwidth.Multigraph.exists_mem_of_mem_cut {V E : Type} (G : Multigraph V E) [Fintype E] {L : Finset V} {e : E} (h : e ∈ G.cut L) : G.fst e ∈ L ∧ G.snd e ∉ L ∨ G.fst e ∉ L ∧ G.snd e ∈ L

An edge in a cut is incident to a vertex in the set and to one outside it.

def Algebraic.Cutwidth.Multigraph.CutsAtMost {V E : Type} (G : Multigraph V E) [Fintype E] (L : Set (Finset V)) (w : ℕ) : Prop

Every cut has at most w edges.

Equations

• G.CutsAtMost L w = ∀ S ∈ L, (G.cut S).card ≤ w

def Algebraic.Cutwidth.Multigraph.OrderingBound (η C : ℝ) : Prop

The graph-ordering hypothesis with slack η and additive constant C: every connected loopless multigraph of maximum degree three has a linear vertex ordering all of whose lower-set cuts have at most (1/3 + η) (M - N)⁺ + 3 log₂ N + C edges.

Equations

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