Splitting the terminal component of a superconcentrator

Keep the edges whose tail lies in the undirected component of a vertex r. The split graph of these edges is connected: the slots of one vertex are joined along its path, and an undirected walk to r crosses from path to path along kept edges. Every directed walk inside the component lifts to a directed walk of the split graph from any entering slot of its first vertex to the last slot of its last vertex, staying in the paths of the vertices of the walk.

Lifting each walk of a vertex-disjoint family from the first slot of its first vertex to the last slot of its last vertex gives a vertex-disjoint family of the split graph (exists_lift_walks). All terminals of a superconcentrator lie in the component of its first input, each input has a kept edge leaving it, and each output a kept edge entering it. Placing every input at the first slot of its path and every output at the last slot, the split graph is again a superconcentrator.

Walks and undirected reachability

theorem Algebraic.Cutwidth.Superconcentrator.Internal.adj_of_dirAdj {V E : Type} {G : Multigraph V E} {u v : V} (h : G.DirAdj u v) : G.Adj u v

theorem Algebraic.Cutwidth.Superconcentrator.Internal.reflTransGen_of_isDirWalk {V E : Type} {G : Multigraph V E} {p : List V} {u v : V} (h : G.IsDirWalk p u v) : Relation.ReflTransGen G.Adj u v

The ends of a directed walk are joined by an undirected walk.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.reflTransGen_of_mem_isDirWalk {V E : Type} {G : Multigraph V E} {p : List V} {u v : V} (h : G.IsDirWalk p u v) {z : V} (hz : z ∈ p) : Relation.ReflTransGen G.Adj u z

Every vertex of a directed walk is joined to its first vertex by an undirected walk.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_isDirWalk {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} (h : G.Superconcentrator input output) (i j : Fin N) : ∃ (p : List V), G.IsDirWalk p (input i) (output j)

In a superconcentrator, every input reaches every output.

The component of a vertex

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

The edges of the undirected component of r, identified by their tails.

Equations

• Algebraic.Cutwidth.Superconcentrator.Internal.compEdges G r = {e : E | Relation.ReflTransGen G.Adj (G.fst e) r}

theorem Algebraic.Cutwidth.Superconcentrator.Internal.mem_compEdges {V E : Type} {G : Multigraph V E} [Fintype E] {r : V} {e : E} : e ∈ compEdges G r ↔ Relation.ReflTransGen G.Adj (G.fst e) r

theorem Algebraic.Cutwidth.Superconcentrator.Internal.reflTransGen_snd_of_mem_compEdges {V E : Type} {G : Multigraph V E} [Fintype E] {r : V} {e : E} (he : e ∈ compEdges G r) : Relation.ReflTransGen G.Adj (G.snd e) r

theorem Algebraic.Cutwidth.Superconcentrator.Internal.reflTransGen_of_slots_pos {V E : Type} {G : Multigraph V E} [Fintype E] {r w : V} (hw : 0 < slots G (compEdges G r) w) : Relation.ReflTransGen G.Adj w r

A vertex with a slot lies in the component.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.split_connected {V E : Type} {G : Multigraph V E} [Fintype E] {r : V} (hr : 0 < slots G (compEdges G r) r) : (split G (compEdges G r)).Connected

The split graph of a component is connected.

Lifting walks

theorem Algebraic.Cutwidth.Superconcentrator.Internal.reflTransGen_lift {V E : Type} {G : Multigraph V E} [Fintype E] {r : V} (P : Set V) (u : V) (l : List V) : List.IsChain G.DirAdj (u :: l) → Relation.ReflTransGen G.Adj u r → (∀ z ∈ u :: l, z ∈ P) → ∀ (x y : SplitVertex G (compEdges G r)), x.fst = u → ↑x.snd ≤ (inEdges G (compEdges G r) u).card → y.fst = (u :: l).getLast ⋯ → ↑y.snd + 1 = slots G (compEdges G r) y.fst → Relation.ReflTransGen (stepIn P) x y

A directed walk in the component lifts from any entering slot of its first vertex to the last slot of its last vertex, through the paths of vertices of P ⊇ the walk.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_lift_isDirWalk {V E : Type} {G : Multigraph V E} [Fintype E] {r : V} {p : List V} {u v : V} (h : G.IsDirWalk p u v) (hr : Relation.ReflTransGen G.Adj u r) (hu : 0 < slots G (compEdges G r) u) (hv : 0 < slots G (compEdges G r) v) : ∃ (q : List (SplitVertex G (compEdges G r))), (split G (compEdges G r)).IsDirWalk q ⟨u, ⟨0, hu⟩⟩ ⟨v, ⟨slots G (compEdges G r) v - 1, ⋯⟩⟩ ∧ ∀ z ∈ q, z.fst ∈ p

Lifting one walk. A directed walk from u to v in the component of r, where u and v have slots, lifts to a directed walk of the split graph from the first slot of u to the last slot of v that stays in the paths of the vertices of the walk.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.exists_lift_walks {V E : Type} {G : Multigraph V E} [Fintype E] {ι : Type u_1} {κ : Type u_2} {r : V} {input : ι → V} {output : κ → V} (hr : ∀ (i : ι), Relation.ReflTransGen G.Adj (input i) r) (hin : ∀ (i : ι), 0 < slots G (compEdges G r) (input i)) (hout : ∀ (j : κ), 0 < slots G (compEdges G r) (output j)) {X : Finset ι} {target : ι → κ} {walk : ι → List V} (hwalk : ∀ i ∈ X, G.IsDirWalk (walk i) (input i) (output (target i))) (hdisj : ∀ i ∈ X, ∀ j ∈ X, i ≠ j → (walk i).Disjoint (walk j)) : ∃ (walk' : ι → List (SplitVertex G (compEdges G r))), (∀ i ∈ X, (split G (compEdges G r)).IsDirWalk (walk' i) ⟨input i, ⟨0, ⋯⟩⟩ ⟨output (target i), ⟨slots G (compEdges G r) (output (target i)) - 1, ⋯⟩⟩) ∧ ∀ i ∈ X, ∀ j ∈ X, i ≠ j → (walk' i).Disjoint (walk' j)

Lifting a family of vertex-disjoint walks. Let all terminals input i lie in the component of r, and let every input i and every output j have a slot. Vertex-disjoint directed walks from input i to output (target i) lift to vertex-disjoint directed walks of the split graph from the first slot of input i to the last slot of output (target i).

theorem Algebraic.Cutwidth.Superconcentrator.Internal.split_superconcentrator {V E : Type} {G : Multigraph V E} [Fintype E] {N : ℕ} {input output : Fin N → V} (h : G.Superconcentrator input output) {r : V} (hr : ∀ (i : Fin N), Relation.ReflTransGen G.Adj (input i) r) (hin : ∀ (i : Fin N), 0 < slots G (compEdges G r) (input i)) (hout : ∀ (j : Fin N), 0 < slots G (compEdges G r) (output j)) : (split G (compEdges G r)).Superconcentrator (fun (i : Fin N) => ⟨input i, ⟨0, ⋯⟩⟩) fun (j : Fin N) => ⟨output j, ⟨slots G (compEdges G r) (output j) - 1, ⋯⟩⟩

The split graph of a superconcentrator. If all inputs lie in the component of r, every input has a slot, and every output has a slot, then the split graph of the component is a superconcentrator with inputs at first slots and outputs at last slots.