Proofs for acyclic concentrators

Let G be an acyclic (n, m)-concentrator whose inputs are sources (in-degree zero), with 2 ≤ m < n.

• Elimination (exists_eliminate). Removing at least two edges, G turns into an acyclic (n - 1, m)-concentrator on the same vertices, with sources as inputs. Every input has an edge leaving it. If some input has two, remove its edges and drop it: the other walks never visit a source. Otherwise every input x has one edge, to its head, and distinct inputs have distinct heads, since two inputs with a common head cannot be routed together. If some head u of x is entered by that edge only, remove it and make u an input in place of x: u is neither an input nor an output, as every output is reached from inputs other than x. Otherwise let w be a first vertex, in the topological order, among the non-input vertices that meet an edge. The edges entering w come from inputs whose head is w, so there is at most one, and then w would be a head entered only by it; so no edge enters w. Then w is no output, and its edges can be removed. The last two steps keep n and remove an edge, so induction on the number of edges applies.
• Eliminating n - 2 m inputs leaves a (2 m, m)-concentrator with at least 2 (n - 2 m) fewer edges, and the concentrator bound applies to it. For h = min(m, n - m) this gives h ≤ (A + η) (M - 2 n + h)⁺ + 3 log₂ (2 M) + C and the baseline M ≥ 2 n - h - 1.

Removing the edges at a vertex

def Algebraic.Cutwidth.Concentrator.Internal.removeEdgesAt {V E : Type} (G : Multigraph V E) (x : V) : Multigraph V { e : E // G.fst e ≠ x ∧ G.snd e ≠ x }

The multigraph with the edges at x removed.

Equations

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

theorem Algebraic.Cutwidth.Concentrator.Internal.isDirWalk_removeEdgesAt {V E : Type} {G : Multigraph V E} {x : V} {p : List V} {u v : V} (hp : G.IsDirWalk p u v) (hx : ∀ z ∈ p, z ≠ x) : (removeEdgesAt G x).IsDirWalk p u v

Walks avoiding x survive the removal of the edges at x.

theorem Algebraic.Cutwidth.Concentrator.Internal.inDegree_removeEdgesAt_le {V E : Type} {G : Multigraph V E} [Fintype E] (x v : V) : (removeEdgesAt G x).inDegree v ≤ G.inDegree v

Removing edges does not increase in-degrees.

theorem Algebraic.Cutwidth.Concentrator.Internal.acyclic_removeEdgesAt {V E : Type} {G : Multigraph V E} (hG : G.Acyclic) (x : V) : (removeEdgesAt G x).Acyclic

Removing edges keeps a multigraph acyclic.

theorem Algebraic.Cutwidth.Concentrator.Internal.card_removeEdgesAt_add {V E : Type} {G : Multigraph V E} [Fintype E] (x : V) : Fintype.card { e : E // G.fst e ≠ x ∧ G.snd e ≠ x } + {e : E | ¬(G.fst e ≠ x ∧ G.snd e ≠ x)}.card = Fintype.card E

The edges kept and the edges at x partition the edges.

Walks and sources

theorem Algebraic.Cutwidth.Concentrator.Internal.exists_dirAdj_of_mem_tail {V E : Type} {G : Multigraph V E} {u : V} {l : List V} : List.IsChain G.DirAdj (u :: l) → ∀ z ∈ l, ∃ (y : V), G.DirAdj y z

Every vertex of a chain after its first is entered by an edge.

theorem Algebraic.Cutwidth.Concentrator.Internal.inDegree_pos_of_dirAdj {V E : Type} {G : Multigraph V E} [Fintype E] {y z : V} (h : G.DirAdj y z) : 0 < G.inDegree z

A vertex entered by an edge has positive in-degree.

theorem Algebraic.Cutwidth.Concentrator.Internal.not_mem_of_inDegree_eq_zero {V E : Type} {G : Multigraph V E} [Fintype E] {p : List V} {u v x : V} (hp : G.IsDirWalk p u v) (hx : G.inDegree x = 0) (hux : u ≠ x) : x ∉ p

Walks avoid sources. A directed walk visits a vertex of in-degree zero only at its start.

theorem Algebraic.Cutwidth.Concentrator.Internal.exists_tail_of_isDirWalk {V E : Type} {G : Multigraph V E} [Fintype E] {p : List V} {x v : V} (hp : G.IsDirWalk p x v) (hx : G.inDegree x = 0) (hxv : x ≠ v) : ∃ (e : E) (q : List V), G.fst e = x ∧ G.IsDirWalk q (G.snd e) v ∧ (∀ z ∈ q, z ∈ p) ∧ x ∉ q

A directed walk from a vertex of in-degree zero to another vertex continues along an edge leaving it, and the rest of the walk avoids it.

The three elimination steps

theorem Algebraic.Cutwidth.Concentrator.Internal.inDegree_removeEdgesAt_eq_zero {V E : Type} {G : Multigraph V E} [Fintype E] {x v : V} (hv : G.inDegree v = 0) : (removeEdgesAt G x).inDegree v = 0

Removing the edges at a vertex keeps the inputs sources.

theorem Algebraic.Cutwidth.Concentrator.Internal.concentrator_drop {V E : Type} {G : Multigraph V E} [Fintype E] {n m : ℕ} {output : Fin m → V} {input : Fin (n + 1) → V} (h : G.Concentrator input output) (hsrc : ∀ (i : Fin (n + 1)), G.inDegree (input i) = 0) (i₀ : Fin (n + 1)) : (removeEdgesAt G (input i₀)).Concentrator (fun (j : Fin n) => input (i₀.succAbove j)) output

Dropping an input. Removing the edges at a source input leaves a concentrator on the other inputs.

theorem Algebraic.Cutwidth.Concentrator.Internal.concentrator_contract {V E : Type} {G : Multigraph V E} [Fintype E] {n m : ℕ} {output : Fin m → V} {input : Fin (n + 1) → V} (h : G.Concentrator input output) (hsrc : ∀ (i : Fin (n + 1)), G.inDegree (input i) = 0) (hmn : m ≤ n) {i₀ : Fin (n + 1)} {e₀ : E} (he₀ : G.fst e₀ = input i₀) (hout : ∀ (e : E), G.fst e = input i₀ → e = e₀) (hin : ∀ (e : E), G.snd e = G.snd e₀ → e = e₀) : (removeEdgesAt G (input i₀)).Concentrator (Function.update input i₀ (G.snd e₀)) output ∧ ∀ (i : Fin (n + 1)), (removeEdgesAt G (input i₀)).inDegree (Function.update input i₀ (G.snd e₀) i) = 0

Contracting an input into its head. Let the input input i₀ be a source whose only edge e₀ leads to a vertex u entered by no other edge, and let every other input be a source. Removing e₀ and making u an input in place of input i₀ leaves a concentrator, provided m inputs other than input i₀ exist.

theorem Algebraic.Cutwidth.Concentrator.Internal.concentrator_removeDead {V E : Type} {G : Multigraph V E} [Fintype E] {n m : ℕ} {output : Fin m → V} {input : Fin n → V} (h : G.Concentrator input output) {w : V} (hw : G.inDegree w = 0) (hwin : ∀ (i : Fin n), input i ≠ w) : (removeEdgesAt G w).Concentrator input output

Removing a dead vertex. Removing the edges at a non-input vertex entered by no edge leaves a concentrator with the same inputs and outputs.

Elimination

theorem Algebraic.Cutwidth.Concentrator.Internal.snd_mem_of_isDirWalk {V E : Type} {G : Multigraph V E} [Fintype E] {p : List V} {x v : V} {e : E} (hp : G.IsDirWalk p x v) (hx : G.inDegree x = 0) (hxv : x ≠ v) (huniq : ∀ (e' : E), G.fst e' = x → e' = e) : G.snd e ∈ p

The head of the only edge leaving a source lies on every walk from it to another vertex.

theorem Algebraic.Cutwidth.Concentrator.Internal.exists_fst_eq_input {V E : Type} {G : Multigraph V E} [Fintype E] {n m : ℕ} {input : Fin n → V} {output : Fin m → V} (h : G.Concentrator input output) (hsrc : ∀ (i : Fin n), G.inDegree (input i) = 0) (hm : 1 ≤ m) (i : Fin n) : ∃ (e : E), G.fst e = input i

An edge leaves a source input that reaches an output.

theorem Algebraic.Cutwidth.Concentrator.Internal.exists_eliminate {V : Type} {m : ℕ} {output : Fin m → V} (hm : 2 ≤ m) (k : ℕ) {E : Type} [Fintype E] (G : Multigraph V E) {n : ℕ} (input : Fin (n + 1) → V) : Fintype.card E ≤ k → G.Concentrator input output → G.Acyclic → (∀ (i : Fin (n + 1)), G.inDegree (input i) = 0) → m ≤ n → ∃ (E' : Type) (x : Fintype E') (G' : Multigraph V E') (input' : Fin n → V), G'.Concentrator input' output ∧ G'.Acyclic ∧ (∀ (i : Fin n), G'.inDegree (input' i) = 0) ∧ Fintype.card E' + 2 ≤ Fintype.card E

Elimination. An acyclic (n + 1, m)-concentrator whose inputs are sources, with 2 ≤ m ≤ n, turns into an acyclic (n, m)-concentrator on the same vertices and outputs, whose inputs are sources, with at least two fewer edges.

theorem Algebraic.Cutwidth.Concentrator.Internal.exists_eliminate_iter {V : Type} {m : ℕ} {output : Fin m → V} (hm : 2 ≤ m) (j : ℕ) {E : Type} [Fintype E] (G : Multigraph V E) {n : ℕ} (input : Fin n → V) : m + j ≤ n → G.Concentrator input output → G.Acyclic → (∀ (i : Fin n), G.inDegree (input i) = 0) → ∃ (n' : ℕ) (E' : Type) (x : Fintype E') (G' : Multigraph V E') (input' : Fin n' → V), n' + j = n ∧ G'.Concentrator input' output ∧ G'.Acyclic ∧ (∀ (i : Fin n'), G'.inDegree (input' i) = 0) ∧ Fintype.card E' + 2 * j ≤ Fintype.card E

Repeated elimination. Eliminating j inputs from an acyclic (n, m)-concentrator whose inputs are sources, with 2 ≤ m and m + j ≤ n, removes at least 2 j edges.

Acyclicity

theorem Algebraic.Cutwidth.Concentrator.Internal.rank_lt_of_transGen {V E : Type} {G : Multigraph V E} {rank : V → ℕ} (hrank : ∀ (e : E), rank (G.fst e) < rank (G.snd e)) {u v : V} (h : Relation.TransGen G.DirAdj u v) : rank u < rank v

Ranks increase along directed walks of positive length.

theorem Algebraic.Cutwidth.Concentrator.Internal.acyclic_iff_forall_not_transGen {V E : Type} {G : Multigraph V E} [Fintype V] : G.Acyclic ↔ ∀ (v : V), ¬Relation.TransGen G.DirAdj v v

Acyclicity is the absence of directed cycles. A finite multigraph has a vertex numbering increasing along every edge exactly when no vertex reaches itself along a directed walk of positive length.

Bounds

theorem Algebraic.Cutwidth.Concentrator.Internal.two_mul_le_card_add_min_of_acyclic {V E : Type} {G : Multigraph V E} [Fintype V] [Fintype E] {n m : ℕ} {input : Fin n → V} {output : Fin m → V} (h : G.Concentrator input output) (hacyc : G.Acyclic) (hsrc : ∀ (i : Fin n), G.inDegree (input i) = 0) (hm : 2 ≤ m) (hmn : m < n) : 2 * n ≤ Fintype.card E + min m (n - m) + 1

The edge baseline for acyclic concentrators. For h = min(m, n - m), an acyclic (n, m)-concentrator with M edges whose inputs are sources, with 2 ≤ m < n, has 2 n ≤ M + h + 1.

theorem Algebraic.Cutwidth.Concentrator.Internal.le_of_orderingBound_of_acyclic {V E : Type} {G : Multigraph V E} [Fintype V] [Fintype E] {n m : ℕ} {input : Fin n → V} {output : Fin m → V} {A η C : ℝ} (hord : Multigraph.OrderingBound A η C) (hAη : 0 ≤ A + η) (h : G.Concentrator input output) (hacyc : G.Acyclic) (hsrc : ∀ (i : Fin n), G.inDegree (input i) = 0) (hm : 2 ≤ m) (hmn : m < n) : ↑(min m (n - m)) ≤ (A + η) * max (↑(Fintype.card E) - (2 * ↑n - ↑(min m (n - m)))) 0 + 3 * Real.logb 2 (2 * ↑(Fintype.card E)) + C

The finite bound for acyclic concentrators. For h = min(m, n - m), an acyclic (n, m)-concentrator with M edges whose inputs are sources, with 2 ≤ m < n, satisfies h ≤ (A + η) (M - (2 n - h))⁺ + 3 log₂ (2 M) + C.

theorem Algebraic.Cutwidth.Concentrator.Internal.eventually_le_card_edges_of_acyclic_of_orderingBound {A : ℝ} (hA : 0 < A) (hord : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ), 2 ≤ m → m < n → ∀ (V E : Type) [Fintype V] [inst : Fintype E] (G : Multigraph V E) (input : Fin n → V) (output : Fin m → V), G.Concentrator input output → G.Acyclic → (∀ (i : Fin n), G.inDegree (input i) = 0) → 2 * ↑n + (1 / A - 1) * ↑(min m (n - m)) - ε * ↑n ≤ ↑(Fintype.card E)

The asymptotic edge bound for acyclic concentrators, for a general ordering coefficient.