Proofs for hyperconcentrators

Let G be an N-hyperconcentrator and h = ⌊N/2⌋.

• 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 c of the first h outputs lie in L. The h inputs in L are joined to the first h outputs; at most c of the walks end in L, and each of the others leaves L along an edge of its own. The N - h ≥ h inputs outside L are joined to the first N - h outputs, among them the first h, and each of the c 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). Every input is joined to the first output, and every output is reached when all inputs are routed, so all terminals lie in one component.
• The split graph of that component is again a hyperconcentrator (split_hyperconcentrator), and the core inequalities of Superconcentrator.Internal give h ≤ (A + η) (M - 2 N)⁺ + 3 log₂ (2 M) + C, and, when the inputs are sources and every vertex has in-degree at most two, h ≤ (A + η) ((V - N) - N)⁺ + 3 log₂ (4 (V - N)) + C.

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.hyperconcentrator_of_superconcentrator {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} (h : G.Superconcentrator input output) : G.Hyperconcentrator input output

Every superconcentrator is a hyperconcentrator.

The cut lemma

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.card_filter_lt_le {N : ℕ} (k : ℕ) : {j : Fin N | ↑j < k}.card ≤ k

The first k labels number at most k.

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

The cut lemma. Every linear order of the vertices of an N-hyperconcentrator has a lower set whose cut has at least ⌊N/2⌋ edges.

The terminals lie in one component

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.exists_isDirWalk_first {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} (h : G.Hyperconcentrator input output) (hN : 0 < N) (i : Fin N) : ∃ (p : List V), G.IsDirWalk p (input i) (output ⟨0, hN⟩)

Every input is joined to the first output by a directed walk.

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

Every output is reached from some input by a directed walk.

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.reflTransGen_root {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} (h : G.Hyperconcentrator input output) (hN : 0 < N) : (∀ (i : Fin N), Relation.ReflTransGen G.Adj (input i) (input ⟨0, hN⟩)) ∧ ∀ (j : Fin N), Relation.ReflTransGen G.Adj (output j) (input ⟨0, hN⟩)

All terminals lie in one component. Every input and every output of an N-hyperconcentrator with N > 0 is joined to the first input by an undirected walk.

The split graph

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.slots_input_pos {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype E] (h : G.Hyperconcentrator input output) (hN : 0 < N) (i : Fin N) : 0 < Superconcentrator.Internal.slots G (Superconcentrator.Internal.compEdges G (input ⟨0, hN⟩)) (input i)

Every input has a kept edge leaving it.

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.slots_output_pos {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype E] (h : G.Hyperconcentrator input output) (hN : 0 < N) (j : Fin N) : 0 < Superconcentrator.Internal.slots G (Superconcentrator.Internal.compEdges G (input ⟨0, hN⟩)) (output j)

Every output has a kept edge entering it.

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.split_hyperconcentrator {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype E] (h : G.Hyperconcentrator 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 N), 0 < Superconcentrator.Internal.slots G (Superconcentrator.Internal.compEdges G r) (output j)) : (Superconcentrator.Internal.split G (Superconcentrator.Internal.compEdges G r)).Hyperconcentrator (fun (i : Fin N) => ⟨input i, ⟨0, ⋯⟩⟩) fun (j : Fin N) => ⟨output j, ⟨Superconcentrator.Internal.slots G (Superconcentrator.Internal.compEdges G r) (output j) - 1, ⋯⟩⟩

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

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.exists_le_card_cut_split {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype E] [Fintype V] (h : G.Hyperconcentrator input output) (hN : 0 < N) [LinearOrder (Superconcentrator.Internal.SplitVertex G (Superconcentrator.Internal.compEdges G (input ⟨0, hN⟩)))] : ∃ (L : Finset (Superconcentrator.Internal.SplitVertex G (Superconcentrator.Internal.compEdges G (input ⟨0, hN⟩)))), IsLowerSet ↑L ∧ N / 2 ≤ ((Superconcentrator.Internal.split G (Superconcentrator.Internal.compEdges G (input ⟨0, hN⟩))).cut L).card

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

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.card_terminals {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} (h : G.Hyperconcentrator input output) : (Finset.image input Finset.univ ∪ Finset.image output Finset.univ).card = 2 * N

The 2 N terminals are distinct vertices.

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.two_mul_le_card_vertices {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype V] (h : G.Hyperconcentrator input output) : 2 * N ≤ Fintype.card V

A hyperconcentrator has at least 2 N vertices.

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.two_mul_le_card_slotted {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype E] [Fintype V] (h : G.Hyperconcentrator input output) (hN : 0 < N) : 2 * N ≤ {w : V | Superconcentrator.Internal.slots G (Superconcentrator.Internal.compEdges G (input ⟨0, hN⟩)) w ≠ 0}.card

The 2 N terminals have a slot.

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.two_mul_le_card_add_one {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype E] [Fintype V] (h : G.Hyperconcentrator input output) (hN : 0 < N) : 2 * N ≤ Fintype.card E + 1

The edge baseline. An N-hyperconcentrator has at least 2 N - 1 edges.

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

The finite edge bound.

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.le_of_orderingBound_of_inDegree {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype E] [Fintype V] {A η C : ℝ} (hord : Multigraph.OrderingBound A η C) (hAη : 0 ≤ A + η) (h : G.Hyperconcentrator input output) (hN : 0 < N) (hsrc : ∀ (i : Fin N), G.inDegree (input i) = 0) (hdeg : ∀ (w : V), G.inDegree w ≤ 2) : ↑(N / 2) ≤ (A + η) * max (↑(Fintype.card V) - ↑N - ↑N) 0 + 3 * Real.logb 2 (4 * (↑(Fintype.card V) - ↑N)) + C

The finite vertex bound under in-degree two.

Asymptotics

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.half_div_ge {A ε : ℝ} (hA : 0 < A) (hε : 0 < ε) {n : ℕ} (hn : ⌈1 / (A * ε)⌉₊ ≤ n) : 1 / (2 * A) * ↑n - ε / 2 * ↑n ≤ ↑(n / 2) / A

⌊N/2⌋/A is at least N/(2A) minus ε N/2 once N ≥ 1/(A ε).

theorem Algebraic.Cutwidth.Hyperconcentrator.Internal.eventually_le_card_edges_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 output : Fin N → V), G.Hyperconcentrator input output → (2 + 1 / (2 * A) - ε) * ↑N ≤ ↑(Fintype.card E)

The asymptotic edge bound for a general ordering coefficient.

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

The asymptotic vertex bound under in-degree two, for a general ordering coefficient.