Hyperconcentrators need (3.78 - o(1)) N edges

Every N-hyperconcentrator (Multigraph.Hyperconcentrator) has at least (2 + κ/2 - ε) N ≈ (3.78 - ε) N edges for all large N, where κ = π/(3 arccos((1 + 2√2)/4)) ≈ 3.5625 is 1/(2p) for the Gaussian edge-score pathwidth coefficient p (eventually_le_card_edges), and at least (34/9 - ε) N. When the inputs have in-degree zero and every vertex has in-degree at most two, as in a network of fan-in-two nodes, at least (1 + κ/2 - ε) N ≈ (2.78 - ε) N vertices are not inputs (eventually_le_card_vertices). Every superconcentrator is a hyperconcentrator (Superconcentrator.hyperconcentrator).

The argument follows the superconcentrator bound (Multigraph.Superconcentrator).

• Cut lemma (exists_le_card_cut). In any linear order of the vertices, take a lower set L with exactly h = ⌊N/2⌋ inputs, and let c of the first h outputs lie in L. The h inputs in L are joined to the first h outputs, and at least h - c of these walks leave L, each 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 the c walks ending in L enter it along distinct edges. So the cut of L has at least h edges.
• Degree reduction and ordering bound. All terminals lie in one undirected component, which splits into a connected loopless hyperconcentrator of maximum degree three with the same edges minus vertices, and the graph-ordering hypothesis OrderingBound A η C gives ⌊N/2⌋ ≤ (A + η) (M - 2 N)⁺ + 3 log₂ (2 M) + C (le_of_orderingBound), so M ≥ (2 + 1/(2A) - ε) N for large N.

theorem Algebraic.Cutwidth.Multigraph.Superconcentrator.hyperconcentrator {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.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.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.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.le_of_orderingBound {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype V] [Fintype E] {A η C : ℝ} (hord : 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. Under the graph-ordering hypothesis OrderingBound A η C with A + η ≥ 0, an N-hyperconcentrator with N > 0 and M edges satisfies ⌊N/2⌋ ≤ (A + η) (M - 2 N)⁺ + 3 log₂ (2 M) + C.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.le_of_orderingBound_of_inDegree {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype V] [Fintype E] {A η C : ℝ} (hord : 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. Under OrderingBound A η C with A + η ≥ 0, an N-hyperconcentrator with N > 0 and V vertices, whose inputs have in-degree zero and whose vertices have in-degree at most two, satisfies ⌊N/2⌋ ≤ (A + η) ((V - N) - N)⁺ + 3 log₂ (4 (V - N)) + C.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.eventually_le_card_edges_of_orderingBound {A : ℝ} (hA : 0 < A) (hord : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), 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)

Edges from a general ordering coefficient. If A > 0 and every slack η > 0 admits a constant C with OrderingBound A η C, then for every ε > 0 and all large N, every N-hyperconcentrator has at least (2 + 1/(2A) - ε) N edges.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.eventually_le_card_vertices_of_orderingBound {A : ℝ} (hA : 0 < A) (hord : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), 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

Vertices from a general ordering coefficient, under in-degree two. If A > 0 and every slack η > 0 admits a constant C with OrderingBound A η C, then for every ε > 0 and all large N, every N-hyperconcentrator whose inputs have in-degree zero and whose vertices have in-degree at most two has at least (1 + 1/(2A) - ε) N vertices that are not inputs.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.eventually_le_card_edges {ε : ℝ} (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 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) / 2 - ε) * ↑N ≤ ↑(Fintype.card E)

Hyperconcentrators need (3.78 - ε) N edges. For every ε > 0 and all large N, every N-hyperconcentrator has at least (2 + κ/2 - ε) N edges, where κ = π/(3 arccos((1 + 2√2)/4)) ≈ 3.5625.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.eventually_thirtyFour_div_nine_sub_mul_le_card_edges {ε : ℝ} (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 → (34 / 9 - ε) * ↑N ≤ ↑(Fintype.card E)

Hyperconcentrators need (34/9 - ε) N edges. For every ε > 0 and all large N, every N-hyperconcentrator has at least (34/9 - ε) N edges; 34/9 ≈ 3.78.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.eventually_le_card_vertices {ε : ℝ} (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 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) / 2 - ε) * ↑N ≤ ↑(Fintype.card V) - ↑N

Hyperconcentrators of in-degree two need (2.78 - ε) N non-input vertices. For every ε > 0 and all large N, every N-hyperconcentrator whose inputs have in-degree zero and whose vertices have in-degree at most two has at least (1 + κ/2 - ε) N vertices that are not inputs, where κ = π/(3 arccos((1 + 2√2)/4)) ≈ 3.5625.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.eventually_twentyFive_div_nine_sub_mul_le_card_vertices {ε : ℝ} (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) → (25 / 9 - ε) * ↑N ≤ ↑(Fintype.card V) - ↑N

Hyperconcentrators of in-degree two need (25/9 - ε) N non-input vertices.

theorem Algebraic.Cutwidth.Multigraph.Hyperconcentrator.eventually_seven_div_two_sub_mul_le_card_edges {ε : ℝ} (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 → (7 / 2 - ε) * ↑N ≤ ↑(Fintype.card E)

The cubic pathwidth coefficient. For every ε > 0 and all large N, every N-hyperconcentrator has at least (7/2 - ε) N edges: the ordering coefficient 1/3.