Terminal compression in every degree

Keep all edges between blocks, including parallel edges. Endpoint charging bounds the edge count of the terminal core by 3d/(2d-3) times the original cycle rank. Expanding a layout of this multigraph core costs only d log₂ |V| + d.

def Complexity.Frontier.Multigraph.Compression.External {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : Set E

Edges whose endpoints lie in different blocks.

Equations

• c.External = {e : E | c.blockOf (G.src e) ≠ c.blockOf (G.tgt e)}

noncomputable def Complexity.Frontier.Multigraph.Compression.multiQuotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : Multigraph ↥c.blocks ↑c.External

The quotient retaining every edge between blocks.

Equations

• c.multiQuotient = { src := fun (e : ↑c.External) => c.blockOf (G.src ↑e), tgt := fun (e : ↑c.External) => c.blockOf (G.tgt ↑e) }

theorem Complexity.Frontier.Multigraph.Compression.multiQuotient_loopless {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : c.multiQuotient.Loopless

theorem Complexity.Frontier.Multigraph.Compression.external_of_cut {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) {B : ↥c.blocks} {e : E} (he : e ∈ G.cut {v : V | v ∈ ↑B}) : e ∈ c.External

theorem Complexity.Frontier.Multigraph.Compression.ncard_edgesAt_multiQuotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (B : ↥c.blocks) : (c.multiQuotient.edgesAt B).ncard = (G.cut {v : V | v ∈ ↑B}).ncard

theorem Complexity.Frontier.Multigraph.Compression.multiQuotient_maxDegreeLE {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : c.multiQuotient.MaxDegreeLE d

theorem Complexity.Frontier.Multigraph.Compression.Terminal.multi_degree_sum {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] (hc : c.Terminal) (e : ↑c.External) : d + 3 ≤ (c.multiQuotient.edgesAt (c.multiQuotient.src e)).ncard + (c.multiQuotient.edgesAt (c.multiQuotient.tgt e)).ncard

theorem Complexity.Frontier.Multigraph.Compression.Terminal.multi_degree_ge_three {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] (hc : c.Terminal) (hG : G.Connected) (two : 2 ≤ c.blocks.card) (B : ↥c.blocks) : 3 ≤ (c.multiQuotient.edgesAt B).ncard

theorem Complexity.Frontier.Multigraph.Compression.external_add_vertices_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] : c.External.ncard + Nat.card V ≤ Nat.card E + c.blocks.card

Every merge moves at least one edge inside a block.

theorem Complexity.Frontier.Multigraph.Compression.Terminal.multi_blocks_le_edges {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] (hc : c.Terminal) (hG : G.Connected) (two : 2 ≤ c.blocks.card) : c.blocks.card ≤ c.External.ncard

A nontrivial terminal core has at least as many edges as blocks.

theorem Complexity.Frontier.Multigraph.Compression.Terminal.multi_edge_bound {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] (hc : c.Terminal) (hG : G.Connected) (two : 2 ≤ c.blocks.card) : (2 * d - 3) * c.External.ncard ≤ 3 * d * G.cycleRank

The terminal multigraph core has at most 3d/(2d-3) times the original cycle rank edges, expressed without division.

theorem Complexity.Frontier.Multigraph.Compression.ncard_cut_multiQuotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (T : Set ↥c.blocks) : (G.cut {v : V | c.blockOf v ∈ T}).ncard = (c.multiQuotient.cut T).ncard

theorem Complexity.Frontier.Multigraph.Compression.exists_layout_multi {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite V] [Finite E] {key : ↥c.blocks → ℕ} (hkey : Function.Injective key) {X : ℝ} (hX : ∀ (q : ℕ), ↑(c.multiQuotient.cut {B : ↥c.blocks | key B < q}).ncard ≤ X) : ∃ (π : Layout V), ∀ (t : ℕ), ↑(G.cut (π.initial t)).ncard ≤ X + ↑d * ↑(Nat.log 2 (Nat.card V)) + ↑d

Expand any layout of the multigraph core, with only logarithmic additional width.