Every vertex ordering of a superconcentrator has a large prefix cut

Take a prefix S of the ordering containing exactly N of the 2 N terminals, say a inputs and N - a outputs. The complement contains N - a inputs and a outputs. The superconcentrator joins the a inputs in S to the a outputs outside S by vertex-disjoint walks, each of which leaves S along an edge directed out of S; it also joins the N - a inputs outside S to the N - a outputs in S, each walk entering S along an edge directed into S. Since the walks of one family are vertex-disjoint, their crossing edges are distinct, so the cut of S has at least N edges.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_eq_cons_of_isDirWalk {V E : Type} {G : Multigraph V E} {p : List V} {u v : V} (h : G.IsDirWalk p u v) : ∃ (l : List V), p = u :: l ∧ List.IsChain G.DirAdj (u :: l) ∧ (u :: l).getLast ⋯ = v

A directed walk is a nonempty chain of directed adjacencies from its first to its last vertex.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.isDirWalk_of_isChain {V E : Type} {G : Multigraph V E} {u : V} {l : List V} (h : List.IsChain G.DirAdj (u :: l)) : G.IsDirWalk (u :: l) u ((u :: l).getLast ⋯)

A chain of vertices is a directed walk from its first to its last vertex.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_cross_of_isChain {V E : Type} {G : Multigraph V E} {L : Set V} (u : V) (l : List V) : List.IsChain G.DirAdj (u :: l) → u ∈ L → (u :: l).getLast ⋯ ∉ L → ∃ x ∈ u :: l, ∃ (y : V), x ∈ L ∧ y ∉ L ∧ G.DirAdj x y

A chain of directed adjacencies that starts in L and ends outside L leaves L along some step.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_cross_of_isDirWalk {V E : Type} {G : Multigraph V E} {p : List V} {u v : V} (h : G.IsDirWalk p u v) {L : Set V} (hu : u ∈ L) (hv : v ∉ L) : ∃ (e : E), G.fst e ∈ p ∧ G.fst e ∈ L ∧ G.snd e ∉ L

A directed walk from inside L to outside L uses an edge directed out of L whose first endpoint lies on the walk.

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

The edges directed from L to its complement.

Equations

• Algebraic.Cutwidth.Superconcentrator.Internal.outCut G L = {e : E | G.fst e ∈ L ∧ G.snd e ∉ L}

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_outCut_add_card_outCut_compl_le {V E : Type} {G : Multigraph V E} [Fintype E] (L : Finset V) : (outCut G ↑L).card + (outCut G (↑L)ᶜ).card ≤ (G.cut L).card

The edges directed out of L and those directed into L together lie in its cut.

Families of vertex-disjoint walks

theorem Algebraic.Cutwidth.Superconcentrator.Internal.mem_of_isDirWalk_left {V E : Type} {G : Multigraph V E} {p : List V} {u v : V} (h : G.IsDirWalk p u v) : u ∈ p

The first vertex of a directed walk lies on it.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.mem_of_isDirWalk_right {V E : Type} {G : Multigraph V E} {p : List V} {u v : V} (h : G.IsDirWalk p u v) : v ∈ p

The last vertex of a directed walk lies on it.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.injOn_target_of_walks {V E : Type} {G : Multigraph V E} {ι : Type u_1} {κ : Type u_2} {X : Finset ι} {walk : ι → List V} {src : ι → V} {output : κ → V} {target : ι → κ} (hwalk : ∀ i ∈ X, G.IsDirWalk (walk i) (src i) (output (target i))) (hdisj : ∀ i ∈ X, ∀ j ∈ X, i ≠ j → (walk i).Disjoint (walk j)) : Set.InjOn target ↑X

Disjoint walks end apart. Vertex-disjoint directed walks ending at the outputs output (target i) of an injective labelling have distinct targets.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_le_card_outCut_of_walks {V E : Type} {G : Multigraph V E} [Fintype E] {ι : Type u_1} (L : Set V) {X : Finset ι} {walk : ι → List V} {src dst : ι → V} (hwalk : ∀ i ∈ X, G.IsDirWalk (walk i) (src i) (dst i)) (hdisj : ∀ i ∈ X, ∀ j ∈ X, i ≠ j → (walk i).Disjoint (walk j)) (hsrc : ∀ i ∈ X, src i ∈ L) (hdst : ∀ i ∈ X, dst i ∉ L) : X.card ≤ (outCut G L).card

Disjoint walks leave along distinct edges. If vertex-disjoint directed walks indexed by X start in L and end outside L, then at least |X| edges are directed out of L.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_target_eq_of_walks {V E : Type} {G : Multigraph V E} {ι : Type u_1} {κ : Type u_2} {X : Finset ι} {Y : Finset κ} {walk : ι → List V} {src : ι → V} {output : κ → V} {target : ι → κ} (hwalk : ∀ i ∈ X, G.IsDirWalk (walk i) (src i) (output (target i))) (hdisj : ∀ i ∈ X, ∀ j ∈ X, i ≠ j → (walk i).Disjoint (walk j)) (hY : ∀ i ∈ X, target i ∈ Y) (hcard : Y.card ≤ X.card) {j : κ} (hj : j ∈ Y) : ∃ i ∈ X, target i = j

Disjoint walks onto a set of outputs. If vertex-disjoint walks indexed by X end at outputs with labels in Y, and Y has at most |X| labels, then every label in Y is the target of one of the walks.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_le_card_outCut_add_card_filter {V E : Type} {G : Multigraph V E} [Fintype E] {ι : Type u_1} {κ : Type u_2} (L : Set V) {X : Finset ι} {Y : Finset κ} {walk : ι → List V} {src : ι → V} {output : κ → V} {target : ι → κ} (hwalk : ∀ i ∈ X, G.IsDirWalk (walk i) (src i) (output (target i))) (hdisj : ∀ i ∈ X, ∀ j ∈ X, i ≠ j → (walk i).Disjoint (walk j)) (hsrc : ∀ i ∈ X, src i ∈ L) (hY : ∀ i ∈ X, target i ∈ Y) : X.card ≤ (outCut G L).card + {j ∈ Y | output j ∈ L}.card

Walks leaving L. If vertex-disjoint walks indexed by X start in L and end at outputs with labels in Y, then |X| is at most the number of edges directed out of L plus the number of labels in Y whose outputs lie in L.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_filter_le_card_outCut_compl {V E : Type} {G : Multigraph V E} [Fintype E] {ι : Type u_1} {κ : Type u_2} (L : Set V) {X : Finset ι} {Y : Finset κ} {walk : ι → List V} {src : ι → V} {output : κ → V} {target : ι → κ} (hwalk : ∀ i ∈ X, G.IsDirWalk (walk i) (src i) (output (target i))) (hdisj : ∀ i ∈ X, ∀ j ∈ X, i ≠ j → (walk i).Disjoint (walk j)) (hsrc : ∀ i ∈ X, src i ∉ L) (hY : ∀ i ∈ X, target i ∈ Y) (hcard : Y.card ≤ X.card) : {j ∈ Y | output j ∈ L}.card ≤ (outCut G Lᶜ).card

Walks entering L. If vertex-disjoint walks indexed by X start outside L and end at outputs with labels in Y, and Y has at most |X| labels, then at least as many edges are directed into L as there are labels in Y whose outputs lie in L.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_le_card_cross {V E : Type} {G : Multigraph V E} [Fintype E] {N : ℕ} {input output : Fin N → V} (h : G.Superconcentrator input output) (L : Set V) {X Y : Finset (Fin N)} (hXY : X.card = Y.card) (hX : ∀ i ∈ X, input i ∈ L) (hY : ∀ j ∈ Y, output j ∉ L) : X.card ≤ (outCut G L).card

One walk family. If X and Y are equally large, the inputs in X lie in L, and the outputs in Y lie outside L, then at least |X| edges are directed out of L.

Lower sets with a prescribed number of chosen vertices

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_isLowerSet_card_filter {V : Type} [Fintype V] [LinearOrder V] (T : Finset V) {k : ℕ} (hk : k ≤ T.card) : ∃ (L : Finset V), IsLowerSet ↑L ∧ {x ∈ T | x ∈ L}.card = k

Prefixes of a chosen set. In a linear order, for every k at most the size of a set T, some lower set contains exactly k elements of T.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_le_card_cut {V E : Type} {G : Multigraph V E} [Fintype V] [Fintype E] [LinearOrder V] {N : ℕ} {input output : Fin N → V} (h : G.Superconcentrator input output) : ∃ (L : Finset V), IsLowerSet ↑L ∧ N ≤ (G.cut L).card

The cut lemma. Every linear order of the vertices of an N-superconcentrator has a lower set whose cut has at least N edges.