Superconcentrators

Every edge of a Multigraph V E is directed from its first endpoint fst to its second endpoint snd. A directed walk is a list of vertices in which each vertex is joined to the next by an edge directed towards it.

An N-superconcentrator has N inputs and N outputs, 2 N distinct vertices in all, such that for every k, every k inputs can be joined to every k outputs by vertex-disjoint directed walks. The walks are not required to be paths. Every path is a walk, so a graph that is a superconcentrator in the usual sense, with paths, is one in this sense, and lower bounds for this notion apply to it.

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

Some edge is directed from u to v.

Equations

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

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

A directed walk from u to v, given by its list of vertices: the list starts at u, ends at v, and each vertex is joined to the next one by an edge directed towards it.

Equations

• G.IsDirWalk p u v = (p.head? = some u ∧ p.getLast? = some v ∧ List.IsChain G.DirAdj p)

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

The number of edges directed into v.

Equations

• G.inDegree v = {e : E | G.snd e = v}.card

structure Algebraic.Cutwidth.Multigraph.Superconcentrator {V E : Type} (G : Multigraph V E) {N : ℕ} (input output : Fin N → V) : Prop

G is an N-superconcentrator with inputs input and outputs output. The N inputs and the N outputs are 2 N distinct vertices. For all sets X of inputs and Y of outputs with the same number of elements, there are pairwise vertex-disjoint directed walks, one from each input in X to some output in Y. Disjointness forces distinct walks to end at distinct outputs, so the walks join X to all of Y.

• input_injective : Function.Injective input

  The inputs are distinct.

• output_injective : Function.Injective output

  The outputs are distinct.

• input_ne_output (i j : Fin N) : input i ≠ output j

  No input is an output.

• exists_walks (X Y : Finset (Fin N)) : X.card = Y.card → ∃ (target : Fin N → Fin N) (walk : Fin N → List V), (∀ i ∈ X, target i ∈ Y ∧ G.IsDirWalk (walk i) (input i) (output (target i))) ∧ ∀ i ∈ X, ∀ j ∈ X, i ≠ j → (walk i).Disjoint (walk j)

  Equally large sets of inputs and outputs are joined by vertex-disjoint directed walks.