Proofs for concentrators

Let G be an (n, m)-concentrator with 1 ≤ m < n and h = min(m, n - m).

• The cut lemma (exists_le_card_cut). In a linear order of the vertices, take a lower set L with exactly h inputs, and let b outputs lie in L. Since h ≤ m, the h inputs in L are joined to distinct outputs; at most b of the walks end in L, and each of the others leaves L along an edge of its own. Since n - h ≥ m, some m inputs outside L are joined to m distinct outputs, that is, to all outputs, and each of the b walks ending in L enters it along an edge of its own. So the cut of L has at least h edges.
• Connectivity (reflTransGen_root). A set of vertices closed under adjacency holding a inputs holds at least min(a, m) outputs, as the walks from its inputs stay in it. If both the component of the first input and its complement held fewer than m outputs, each would hold no more inputs than outputs, so n ≤ m. Hence the component holds all m outputs, and then its complement holds no input.
• Every input is joined to an output and every output is reached from an input, so all terminals have a slot in the split graph of the component, which is again a concentrator (split_concentrator). The core inequality of Superconcentrator.Internal then gives h ≤ (A + η) (M - n - m)⁺ + 3 log₂ (2 M) + C, and the connected split graph gives the baseline n + m ≤ M + 1.

The cut lemma

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

The cut lemma. Every linear order of the vertices of an (n, m)-concentrator has a lower set whose cut has at least min(m, n - m) edges.

The terminals lie in one component

theorem Algebraic.Cutwidth.Concentrator.Internal.iff_of_reflTransGen {V E : Type} {G : Multigraph V E} {P : V → Prop} (hP : ∀ (u v : V), G.Adj u v → (P u ↔ P v)) {u v : V} (huv : Relation.ReflTransGen G.Adj u v) : P u ↔ P v

A predicate constant along edges is constant along undirected walks.

theorem Algebraic.Cutwidth.Concentrator.Internal.card_le_card_of_closed {V E : Type} {G : Multigraph V E} {n m : ℕ} {input : Fin n → V} {output : Fin m → V} (h : G.Concentrator input output) {P : V → Prop} (hP : ∀ (u v : V), G.Adj u v → (P u ↔ P v)) {X : Finset (Fin n)} (hXm : X.card ≤ m) (hX : ∀ i ∈ X, P (input i)) {Y : Finset (Fin m)} (hY : ∀ (j : Fin m), P (output j) → j ∈ Y) : X.card ≤ Y.card

Walks stay in closed sets. If P is constant along edges and holds at the inputs of a set X of at most m inputs, then at least |X| outputs satisfy P: every set Y containing the outputs that satisfy P has at least |X| elements.

theorem Algebraic.Cutwidth.Concentrator.Internal.min_card_le_card_of_closed {V E : Type} {G : Multigraph V E} {n m : ℕ} {input : Fin n → V} {output : Fin m → V} (h : G.Concentrator input output) {P : V → Prop} (hP : ∀ (u v : V), G.Adj u v → (P u ↔ P v)) {S : Finset (Fin n)} (hS : ∀ i ∈ S, P (input i)) {Y : Finset (Fin m)} (hY : ∀ (j : Fin m), P (output j) → j ∈ Y) : min S.card m ≤ Y.card

A closed set holding the inputs of S holds at least min(|S|, m) outputs.

theorem Algebraic.Cutwidth.Concentrator.Internal.reflTransGen_root {V E : Type} {G : Multigraph V E} {n m : ℕ} {input : Fin n → V} {output : Fin m → V} (h : G.Concentrator input output) (hm : 1 ≤ m) (hmn : m < n) : (∀ (i : Fin n), Relation.ReflTransGen G.Adj (input i) (input ⟨0, ⋯⟩)) ∧ ∀ (j : Fin m), Relation.ReflTransGen G.Adj (output j) (input ⟨0, ⋯⟩)

All terminals lie in one component. If 1 ≤ m < n, every input and every output of an (n, m)-concentrator is joined to the first input by an undirected walk.

The split graph

theorem Algebraic.Cutwidth.Concentrator.Internal.slots_input_pos {V E : Type} {G : Multigraph V E} {n m : ℕ} {input : Fin n → V} {output : Fin m → V} [Fintype E] (h : G.Concentrator input output) (hm : 1 ≤ m) (hmn : m < n) (i : Fin n) : 0 < Superconcentrator.Internal.slots G (Superconcentrator.Internal.compEdges G (input ⟨0, ⋯⟩)) (input i)

Every input has a kept edge leaving it.

theorem Algebraic.Cutwidth.Concentrator.Internal.slots_output_pos {V E : Type} {G : Multigraph V E} {n m : ℕ} {input : Fin n → V} {output : Fin m → V} [Fintype E] (h : G.Concentrator input output) (hm : 1 ≤ m) (hmn : m < n) (j : Fin m) : 0 < Superconcentrator.Internal.slots G (Superconcentrator.Internal.compEdges G (input ⟨0, ⋯⟩)) (output j)

Every output has a kept edge entering it.

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

The split graph of a concentrator. 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 concentrator with inputs at first slots and outputs at last slots.

theorem Algebraic.Cutwidth.Concentrator.Internal.exists_le_card_cut_split {V E : Type} {G : Multigraph V E} {n m : ℕ} {input : Fin n → V} {output : Fin m → V} [Fintype E] [Fintype V] (h : G.Concentrator input output) (hm : 1 ≤ m) (hmn : m < n) [LinearOrder (Superconcentrator.Internal.SplitVertex G (Superconcentrator.Internal.compEdges G (input ⟨0, ⋯⟩)))] : ∃ (L : Finset (Superconcentrator.Internal.SplitVertex G (Superconcentrator.Internal.compEdges G (input ⟨0, ⋯⟩)))), IsLowerSet ↑L ∧ min m (n - m) ≤ ((Superconcentrator.Internal.split G (Superconcentrator.Internal.compEdges G (input ⟨0, ⋯⟩))).cut L).card

The cut lemma holds in the split graph of the component of the first input.

theorem Algebraic.Cutwidth.Concentrator.Internal.add_le_card_slotted {V E : Type} {G : Multigraph V E} {n m : ℕ} {input : Fin n → V} {output : Fin m → V} [Fintype E] [Fintype V] (h : G.Concentrator input output) (hm : 1 ≤ m) (hmn : m < n) : n + m ≤ {w : V | Superconcentrator.Internal.slots G (Superconcentrator.Internal.compEdges G (input ⟨0, ⋯⟩)) w ≠ 0}.card

The n + m terminals have a slot.

theorem Algebraic.Cutwidth.Concentrator.Internal.add_le_card_add_one {V E : Type} {G : Multigraph V E} {n m : ℕ} {input : Fin n → V} {output : Fin m → V} [Fintype E] [Fintype V] (h : G.Concentrator input output) (hm : 1 ≤ m) (hmn : m < n) : n + m ≤ Fintype.card E + 1

The edge baseline. An (n, m)-concentrator with 1 ≤ m < n has at least n + m - 1 edges.

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

The finite bound.

Asymptotics

theorem Algebraic.Cutwidth.Concentrator.Internal.eventually_le_card_edges_of_orderingBound {A : ℝ} (hA : 0 < A) (hord : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ), 1 ≤ 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 → ↑n + ↑m + ↑(min m (n - m)) / A - ε * ↑n ≤ ↑(Fintype.card E)

The asymptotic edge bound for a general ordering coefficient.

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

The balanced asymptotic edge bound for a general ordering coefficient. With ⌊n/2⌋ outputs, at least (3/2 + 1/(2A) - ε) n edges.