Lower bounds from the graph-ordering hypothesis

Root the component of a vertex r and split it. The split graph is a connected loopless multigraph of maximum degree three, so the graph-ordering hypothesis gives an ordering whose prefix cuts are small. If every ordering of the split graph also has a prefix cut with at least h edges, as the cut lemmas show for the split graphs of superconcentrators, concentrators and hyperconcentrators, then h ≤ (A + η) (K - n)⁺ + 3 log₂ (2 K) + C for K kept edges and n vertices with a slot (le_of_orderingBound_split): the split graph has 2 K vertices, and its edges minus vertices are K - n. A connected multigraph has at least its number of vertices minus one edges, so also n ≤ K + 1.

If at least T vertices have a slot, then K - n ≤ M - T for M edges. When T sources of in-degree zero have a slot and every vertex has in-degree at most two, the kept edges enter non-source vertices with a slot, at most two each, which gives K - n ≤ (V - T) - T.

Every input of a superconcentrator reaches every output, so all terminals lie in the component of the first input, all have a slot, and T = 2 N.

Numeric lemmas turn these bounds into asymptotic ones: if Q is less than (D + 1/A - ε) N, the log term must absorb (A ε / 2) N, which fails for large N.

Connected multigraphs

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_le_card_add_one_of_connected {V E : Type} {G : Multigraph V E} [Fintype V] [Fintype E] (hG : G.Connected) : Fintype.card V ≤ Fintype.card E + 1

A connected multigraph has at least its number of vertices minus one edges.

Slots at the ends of walks

theorem Algebraic.Cutwidth.Superconcentrator.Internal.slots_le_two_mul_card {V E : Type} {G : Multigraph V E} (K : Finset E) (w : V) : slots G K w ≤ 2 * K.card

theorem Algebraic.Cutwidth.Superconcentrator.Internal.slots_pos_of_isDirWalk_left {V E : Type} {G : Multigraph V E} [Fintype E] {r : V} {p : List V} {u v : V} (hp : G.IsDirWalk p u v) (huv : u ≠ v) (hu : Relation.ReflTransGen G.Adj u r) : 0 < slots G (compEdges G r) u

The first vertex of a directed walk with distinct ends, in the component of r, has a kept edge leaving it.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.slots_pos_of_isDirWalk_right {V E : Type} {G : Multigraph V E} [Fintype E] {r : V} {p : List V} {u v : V} (hp : G.IsDirWalk p u v) (huv : u ≠ v) (hu : Relation.ReflTransGen G.Adj u r) : 0 < slots G (compEdges G r) v

The last vertex of a directed walk with distinct ends, in the component of r, has a kept edge entering it.

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

A component in which r has a slot has a kept edge.

The core inequality

theorem Algebraic.Cutwidth.Superconcentrator.Internal.card_slotted_le_card_compEdges_add_one {V E : Type} {G : Multigraph V E} [Fintype E] [Fintype V] {r : V} (hr : 0 < slots G (compEdges G r) r) : {w : V | slots G (compEdges G r) w ≠ 0}.card ≤ (compEdges G r).card + 1

The vertices with a slot number at most one more than the kept edges: the split graph is connected.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.le_of_orderingBound_split {V E : Type} {G : Multigraph V E} [Fintype E] [Fintype V] {A η C : ℝ} (hord : Multigraph.OrderingBound A η C) {r : V} (hr : 0 < slots G (compEdges G r) r) {h : ℕ} (hcut : ∀ [inst : LinearOrder (SplitVertex G (compEdges G r))], ∃ (L : Finset (SplitVertex G (compEdges G r))), IsLowerSet ↑L ∧ h ≤ ((split G (compEdges G r)).cut L).card) : ↑h ≤ (A + η) * max (↑(compEdges G r).card - ↑{w : V | slots G (compEdges G r) w ≠ 0}.card) 0 + 3 * Real.logb 2 (2 * ↑(compEdges G r).card) + C

Core inequality. If every linear order of the split graph of the component of r has a lower set whose cut has at least h edges, then h ≤ (A + η) (K - n)⁺ + 3 log₂ (2 K) + C for K kept edges and n vertices with a slot.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.le_of_orderingBound_split_card {V E : Type} {G : Multigraph V E} [Fintype E] [Fintype V] {A η C : ℝ} (hord : Multigraph.OrderingBound A η C) (hAη : 0 ≤ A + η) {r : V} (hr : 0 < slots G (compEdges G r) r) {h : ℕ} (hcut : ∀ [inst : LinearOrder (SplitVertex G (compEdges G r))], ∃ (L : Finset (SplitVertex G (compEdges G r))), IsLowerSet ↑L ∧ h ≤ ((split G (compEdges G r)).cut L).card) {T : ℕ} (hT : T ≤ {w : V | slots G (compEdges G r) w ≠ 0}.card) : ↑h ≤ (A + η) * max (↑(Fintype.card E) - ↑T) 0 + 3 * Real.logb 2 (2 * ↑(Fintype.card E)) + C

The edge form of the core inequality. If at least T vertices have a slot, then h ≤ (A + η) (M - T)⁺ + 3 log₂ (2 M) + C for M edges.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.le_card_add_one_of_le_slotted {V E : Type} {G : Multigraph V E} [Fintype E] [Fintype V] {r : V} (hr : 0 < slots G (compEdges G r) r) {T : ℕ} (hT : T ≤ {w : V | slots G (compEdges G r) w ≠ 0}.card) : T ≤ Fintype.card E + 1

The edge baseline. If at least T vertices have a slot, the multigraph has at least T - 1 edges.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.le_of_orderingBound_split_inDegree {V E : Type} {G : Multigraph V E} [Fintype E] [Fintype V] {A η C : ℝ} (hord : Multigraph.OrderingBound A η C) (hAη : 0 ≤ A + η) {r : V} (hr : 0 < slots G (compEdges G r) r) {h : ℕ} (hcut : ∀ [inst : LinearOrder (SplitVertex G (compEdges G r))], ∃ (L : Finset (SplitVertex G (compEdges G r))), IsLowerSet ↑L ∧ h ≤ ((split G (compEdges G r)).cut L).card) {T : ℕ} {source : Fin T → V} (hinj : Function.Injective source) (hin : ∀ (i : Fin T), 0 < slots G (compEdges G r) (source i)) (hsrc : ∀ (i : Fin T), G.inDegree (source i) = 0) (hdeg : ∀ (w : V), G.inDegree w ≤ 2) : ↑h ≤ (A + η) * max (↑(Fintype.card V) - ↑T - ↑T) 0 + 3 * Real.logb 2 (4 * (↑(Fintype.card V) - ↑T)) + C

The vertex form of the core inequality. If the T vertices source i are distinct, have a slot and in-degree zero, and every vertex has in-degree at most two, then h ≤ (A + η) ((V - T) - T)⁺ + 3 log₂ (4 (V - T)) + C.

The terminals of a superconcentrator

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

The 2 N terminals are distinct.

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

Every input is joined to the first input by an undirected walk.

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

Every input has a kept edge leaving it.

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

Every output has a kept edge entering it.

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

The component of the first input has a kept edge.

theorem Algebraic.Cutwidth.Superconcentrator.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.Superconcentrator input output) (hN : 0 < N) [LinearOrder (SplitVertex G (compEdges G (input ⟨0, hN⟩)))] : ∃ (L : Finset (SplitVertex G (compEdges G (input ⟨0, hN⟩)))), IsLowerSet ↑L ∧ N ≤ ((split G (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.Superconcentrator.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.Superconcentrator input output) (hN : 0 < N) : 2 * N ≤ {w : V | slots G (compEdges G (input ⟨0, hN⟩)) w ≠ 0}.card

The 2 N terminals have a slot.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.le_of_orderingBound_core {V E : Type} {G : Multigraph V E} {N : ℕ} {input output : Fin N → V} [Fintype E] [Fintype V] {A η C : ℝ} (hord : Multigraph.OrderingBound A η C) (h : G.Superconcentrator input output) (hN : 0 < N) : ↑N ≤ (A + η) * max (↑(compEdges G (input ⟨0, hN⟩)).card - ↑{w : V | slots G (compEdges G (input ⟨0, hN⟩)) w ≠ 0}.card) 0 + 3 * Real.logb 2 (2 * ↑(compEdges G (input ⟨0, hN⟩)).card) + C

Core inequality. For K the kept edges of the component of the first input and n the vertices with a slot, N ≤ (A + η) (K - n)⁺ + 3 log₂ (2 K) + C.

theorem Algebraic.Cutwidth.Superconcentrator.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.Superconcentrator input output) (hN : 0 < N) : ↑N ≤ (A + η) * max (↑(Fintype.card E) - 2 * ↑N) 0 + 3 * Real.logb 2 (2 * ↑(Fintype.card E)) + C

The finite bound.

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

The finite bound for connected superconcentrators.

theorem Algebraic.Cutwidth.Superconcentrator.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.Superconcentrator input output) (hN : 0 < N) (hsrc : ∀ (i : Fin N), G.inDegree (input i) = 0) (hdeg : ∀ (w : V), G.inDegree w ≤ 2) : ↑N ≤ (A + η) * max (↑(Fintype.card V) - ↑N - ↑N) 0 + 3 * Real.logb 2 (4 * (↑(Fintype.card V) - ↑N)) + C

The finite bound under in-degree two. If the inputs have in-degree zero and every vertex has in-degree at most two, then N ≤ (A + η) ((V - N) - N)⁺ + 3 log₂ (4 (V - N)) + C.

Asymptotics

theorem Algebraic.Cutwidth.Superconcentrator.Internal.eventually_le_of_bound {A ε D B : ℝ} (hA : 0 < A) (hε : 0 < ε) (hεA : ε * A ≤ 1) (hD : 1 ≤ D) (hB : 1 ≤ B) (C : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (Q : ℝ), 0 ≤ Q → ↑N ≤ (A + A ^ 2 * ε / 2) * max (Q - D * ↑N) 0 + 3 * Real.logb 2 (B * Q) + C → (D + 1 / A - ε) * ↑N ≤ Q

Numeric core. If N ≤ (A + A² ε/2) (Q - D N)⁺ + 3 log₂ (B Q) + C, then (D + 1/A - ε) N ≤ Q for all large N.

theorem Algebraic.Cutwidth.Superconcentrator.Internal.eventually_le_of_bound_of_baseline {A ε D B : ℝ} (hA : 0 < A) (hε : 0 < ε) (hD : 0 ≤ D) (hB : 1 ≤ B) (C : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (h base Q : ℝ), 0 ≤ h → h ≤ ↑n → base ≤ D * ↑n → base - 1 ≤ Q → 0 ≤ Q → h ≤ (A + A ^ 2 * ε / 2) * max (Q - base) 0 + 3 * Real.logb 2 (B * Q) + C → base + h / A - ε * ↑n ≤ Q

Numeric core with a baseline. Let 0 ≤ h ≤ n, base ≤ D n, base - 1 ≤ Q and 0 ≤ Q. If h ≤ (A + A² ε/2) (Q - base)⁺ + 3 log₂ (B Q) + C, then base + h/A - ε n ≤ Q for all large n. The baseline covers small h, where the log term need not be absorbed.

theorem Algebraic.Cutwidth.Superconcentrator.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.Superconcentrator input output → (2 + 1 / A - ε) * ↑N ≤ ↑(Fintype.card E)

The asymptotic edge bound for a general ordering coefficient.

theorem Algebraic.Cutwidth.Superconcentrator.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.Superconcentrator input output → (∀ (i : Fin N), G.inDegree (input i) = 0) → (∀ (w : V), G.inDegree w ≤ 2) → (1 + 1 / A - ε) * ↑N ≤ ↑(Fintype.card V) - ↑N

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