Compressing a degree-three multigraph to a simple cubic graph

A connected loopless multigraph of maximum degree three is compressed by repeatedly merging two adjacent vertices when one of them has degree at most two or they are joined by parallel edges. A Compression records the current state as a set of blocks, each block being an ordered list of original vertices, together with the invariants the process maintains:

• every block has at most three edges leaving it, its current degree;
• every proper prefix of a block has boundary at most 3 ⌈log₂ |block|⌉, because merges place the larger block first;
• the number of blocks plus the number of edges inside blocks is at least the number of original vertices, so the quotient's edge excess never grows.

When no merge applies and there are at least two blocks, the quotient graph Compression.quotient is simple and 3-regular (quotient_isRegularOfDegree), and its vertex count h satisfies h + 2 N ≤ 2 M (card_blocks_add_le).

noncomputable def Algebraic.Cutwidth.Multigraph.between {V E : Type} [Fintype E] (G : Multigraph V E) (S T : Finset V) : Finset E

The edges joining S to T.

Equations

• G.between S T = {e : E | G.fst e ∈ S ∧ G.snd e ∈ T ∨ G.fst e ∈ T ∧ G.snd e ∈ S}

theorem Algebraic.Cutwidth.Multigraph.mem_between {V E : Type} [Fintype E] (G : Multigraph V E) {S T : Finset V} {e : E} : e ∈ G.between S T ↔ G.fst e ∈ S ∧ G.snd e ∈ T ∨ G.fst e ∈ T ∧ G.snd e ∈ S

theorem Algebraic.Cutwidth.Multigraph.between_comm {V E : Type} [Fintype E] (G : Multigraph V E) (S T : Finset V) : G.between S T = G.between T S

theorem Algebraic.Cutwidth.Multigraph.cut_union_subset {V E : Type} [Fintype E] (G : Multigraph V E) (S T : Finset V) : G.cut (S ∪ T) ⊆ G.cut S ∪ G.cut T

Cuts are subadditive.

theorem Algebraic.Cutwidth.Multigraph.card_cut_union_add {V E : Type} [Fintype E] (G : Multigraph V E) (S T : Finset V) (h : Disjoint S T) : (G.cut (S ∪ T)).card + 2 * (G.between S T).card = (G.cut S).card + (G.cut T).card

The cut of a disjoint union, accounting for the edges between the parts.

theorem Algebraic.Cutwidth.Multigraph.mem_of_reflTransGen {V E : Type} [Fintype E] (G : Multigraph V E) {S : Finset V} (hcut : G.cut S = ∅) {u v : V} (h : Relation.ReflTransGen G.Adj u v) (hu : u ∈ S) : v ∈ S

A walk starting inside a set with empty cut stays inside it.

theorem Algebraic.Cutwidth.Multigraph.cut_nonempty_of_connected {V E : Type} [Fintype E] (G : Multigraph V E) (connected : G.Connected) {S : Finset V} (hne : S.Nonempty) {v : V} (hv : v ∉ S) : (G.cut S).Nonempty

In a connected graph, every proper nonempty vertex set has a crossing edge.

Compressions

noncomputable def Algebraic.Cutwidth.Multigraph.insideBlocks {V E : Type} [Fintype E] (G : Multigraph V E) (blocks : Finset (List V)) : Finset E

The edges with both endpoints in a common block.

Equations

• G.insideBlocks blocks = {e : E | ∃ B ∈ blocks, G.fst e ∈ B ∧ G.snd e ∈ B}

theorem Algebraic.Cutwidth.Multigraph.mem_insideBlocks {V E : Type} [Fintype E] (G : Multigraph V E) {blocks : Finset (List V)} {e : E} : e ∈ G.insideBlocks blocks ↔ ∃ B ∈ blocks, G.fst e ∈ B ∧ G.snd e ∈ B

theorem Algebraic.Cutwidth.Multigraph.clog_add_one_le {a b : ℕ} (ha : 0 < a) (h : 2 * a ≤ b) : Nat.clog 2 a + 1 ≤ Nat.clog 2 b

Nat.clog 2 increases by one when the argument at least doubles.

structure Algebraic.Cutwidth.Multigraph.Compression {V E : Type} [Fintype V] [Fintype E] (G : Multigraph V E) : Type

A state of the compression process: an ordered partition of the vertices into blocks, with the invariants maintained by merging.

• blocks : Finset (List V)

  The blocks, each an ordered list of original vertices.

• nodup (B : List V) : B ∈ self.blocks → B.Nodup

  Each block lists distinct vertices.

• nonempty (B : List V) : B ∈ self.blocks → B ≠ []

  Blocks are nonempty.

• disjoint (B : List V) : B ∈ self.blocks → ∀ B' ∈ self.blocks, B ≠ B' → ∀ v ∈ B, v ∉ B'

  Distinct blocks are disjoint.

• cover (v : V) : ∃ B ∈ self.blocks, v ∈ B

  Every vertex lies in a block.

• degree (B : List V) : B ∈ self.blocks → (G.cut B.toFinset).card ≤ 3

  At most three edges leave a block.

• prefixBound (B : List V) : B ∈ self.blocks → ∀ k < B.length, (G.cut (List.take k B).toFinset).card ≤ 3 * Nat.clog 2 B.length

  Proper prefixes of a block have logarithmically small boundary.

• count : Fintype.card V ≤ self.blocks.card + (G.insideBlocks self.blocks).card

  Blocks plus inside edges dominate the vertex count.

def Algebraic.Cutwidth.Multigraph.Compression.Mergeable {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) : Prop

Two blocks can be merged when they are adjacent and one has degree at most two or they are joined by parallel edges. The smaller block is listed second.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Multigraph.Compression.toFinset_disjoint {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {B B' : List V} (hB : B ∈ c.blocks) (hB' : B' ∈ c.blocks) (hne : B ≠ B') : Disjoint B.toFinset B'.toFinset

theorem Algebraic.Cutwidth.Multigraph.Compression.merged_notMem {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {B B' : List V} (hB : B ∈ c.blocks) (hB' : B' ∈ c.blocks) (hne : B ≠ B') : B ++ B' ∉ (c.blocks.erase B).erase B'

noncomputable def Algebraic.Cutwidth.Multigraph.Compression.merge {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {B B' : List V} (hB : B ∈ c.blocks) (hB' : B' ∈ c.blocks) (hne : B ≠ B') (hlen : B'.length ≤ B.length) (hr : 0 < (G.between B.toFinset B'.toFinset).card) (hdeg : (G.cut B.toFinset).card ≤ 2 ∨ (G.cut B'.toFinset).card ≤ 2 ∨ 2 ≤ (G.between B.toFinset B'.toFinset).card) : G.Compression

Merge two blocks, listing the larger first.

Equations

• c.merge hB hB' hne hlen hr hdeg = { blocks := insert (B ++ B') ((c.blocks.erase B).erase B'), nodup := ⋯, nonempty := ⋯, disjoint := ⋯, cover := ⋯, degree := ⋯, prefixBound := ⋯, count := ⋯ }

theorem Algebraic.Cutwidth.Multigraph.Compression.merge_card_add_one {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {B B' : List V} (hB : B ∈ c.blocks) (hB' : B' ∈ c.blocks) (hne : B ≠ B') (hlen : B'.length ≤ B.length) (hr : 0 < (G.between B.toFinset B'.toFinset).card) (hdeg : (G.cut B.toFinset).card ≤ 2 ∨ (G.cut B'.toFinset).card ≤ 2 ∨ 2 ≤ (G.between B.toFinset B'.toFinset).card) : (c.merge hB hB' hne hlen hr hdeg).blocks.card + 1 = c.blocks.card

noncomputable def Algebraic.Cutwidth.Multigraph.Compression.initial {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (degree : G.MaxDegreeLE 3) : G.Compression

The initial compression: every vertex is its own block.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Multigraph.Compression.exists_not_mergeable {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (degree : G.MaxDegreeLE 3) : ∃ (c : G.Compression), ¬c.Mergeable

The compression process terminates in a state where no merge applies.

The quotient graph

noncomputable def Algebraic.Cutwidth.Multigraph.Compression.blockOf {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (v : V) : ↥c.blocks

The block containing a vertex.

Equations

• c.blockOf v = ⟨Classical.choose ⋯, ⋯⟩

theorem Algebraic.Cutwidth.Multigraph.Compression.mem_blockOf {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (v : V) : v ∈ ↑(c.blockOf v)

theorem Algebraic.Cutwidth.Multigraph.Compression.blockOf_eq_of_mem {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {v : V} {B : ↥c.blocks} (h : v ∈ ↑B) : c.blockOf v = B

theorem Algebraic.Cutwidth.Multigraph.Compression.blockOf_ne_of_notMem {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {v : V} {B : ↥c.blocks} (h : v ∉ ↑B) : c.blockOf v ≠ B

noncomputable def Algebraic.Cutwidth.Multigraph.Compression.quotient {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) : SimpleGraph ↥c.blocks

The quotient graph: two blocks are adjacent when an edge joins them.

Equations

• c.quotient = { Adj := fun (B B' : ↥c.blocks) => B ≠ B' ∧ (G.between (↑B).toFinset (↑B').toFinset).Nonempty, symm := ⋯, loopless := ⋯ }

theorem Algebraic.Cutwidth.Multigraph.Compression.quotient_adj {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {B B' : ↥c.blocks} : c.quotient.Adj B B' ↔ B ≠ B' ∧ (G.between (↑B).toFinset (↑B').toFinset).Nonempty

theorem Algebraic.Cutwidth.Multigraph.Compression.card_between_le_one {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (final : ¬c.Mergeable) {B B' : ↥c.blocks} (hne : B ≠ B') : (G.between (↑B).toFinset (↑B').toFinset).card ≤ 1

With no merge available, distinct blocks are joined by at most one edge.

noncomputable def Algebraic.Cutwidth.Multigraph.Compression.other {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (B : ↥c.blocks) (e : E) : V

The endpoint of an edge outside a block.

Equations

• c.other B e = if G.fst e ∈ ↑B then G.snd e else G.fst e

theorem Algebraic.Cutwidth.Multigraph.Compression.other_notMem {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {B : ↥c.blocks} {e : E} (he : e ∈ G.cut (↑B).toFinset) : c.other B e ∉ ↑B

theorem Algebraic.Cutwidth.Multigraph.Compression.mem_between_other {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {B : ↥c.blocks} {e : E} (he : e ∈ G.cut (↑B).toFinset) : e ∈ G.between (↑B).toFinset (↑(c.blockOf (c.other B e))).toFinset

theorem Algebraic.Cutwidth.Multigraph.Compression.card_cut_eq_three {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (final : ¬c.Mergeable) (connected : G.Connected) (two : 2 ≤ c.blocks.card) (B : ↥c.blocks) : (G.cut (↑B).toFinset).card = 3

With no merge available and at least two blocks, every block has degree three.

theorem Algebraic.Cutwidth.Multigraph.Compression.quotient_isRegularOfDegree {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (final : ¬c.Mergeable) (connected : G.Connected) (two : 2 ≤ c.blocks.card) : c.quotient.IsRegularOfDegree 3

The quotient of a final compression with at least two blocks is 3-regular.

theorem Algebraic.Cutwidth.Multigraph.Compression.card_quotient_edgeFinset_add {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (final : ¬c.Mergeable) : c.quotient.edgeFinset.card + (G.insideBlocks c.blocks).card = Fintype.card E

The quotient's edges are the edges between distinct blocks.

theorem Algebraic.Cutwidth.Multigraph.Compression.card_blocks_add_le {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (final : ¬c.Mergeable) (connected : G.Connected) (two : 2 ≤ c.blocks.card) : c.blocks.card + 2 * Fintype.card V ≤ 2 * Fintype.card E

With h blocks, N vertices, and M edges, a final compression with at least two blocks satisfies h + 2 N ≤ 2 M.