From cubic graphs to subcubic multigraphs #
This file proves LayoutBound.of_cubic: a layout bound for simple cubic graphs with
coefficient c (CubicLayoutBound c) gives the layout bound for connected multigraphs of
maximum degree three with coefficient 2c. Throughout, G has N vertices, M edges, and
cycle rank β₁ = M - N + 1.
Compression. Partition the vertices of G into blocks, each listing its vertices in
order, starting from single vertices. Two distinct blocks joined by an edge are merged when
their union still has at most three edges leaving it, as happens when one of them has at most
two edges leaving it or when two edges join them. The merged block lists the longer block first.
A Compression records the invariants of this process:
- at most three edges leave a block;
- at most
3 log₂ |B|edges leave a proper prefix of a blockB. A proper prefix of a merged block is a proper prefix of its first part, or all of its first part followed by a proper prefix of its second part, which has at most half as many vertices; - there are at least as many blocks and edges inside blocks as vertices, since a merge loses one block and moves at least one edge inside.
Each merge loses a block, so merging ends in a final compression (exists_final).
The quotient. In a final compression two distinct blocks are joined by at most one edge,
and if there are at least two blocks then exactly three edges leave each block: by
connectivity, a block with fewer would merge with a neighbor. So the quotient, the graph on
the blocks in which two blocks are adjacent when an edge joins them, is a simple cubic graph
(isRegularOfDegree). Its h vertices span 3h/2 edges, which are the edges of G between
blocks, and the counting invariant gives h + 2N ≤ 2M (card_add_two_mul_le). So the quotient
has at most 2 β₁ vertices.
Expansion. Lay out G block by block, ordering the blocks by a layout of the quotient and
each block by its list. A frontier consists of whole blocks followed by a prefix of one more
block. The edges leaving the whole blocks are edges of the quotient crossing its frontier
(ncard_cut_le), and at most 3 log₂ N + 3 edges leave the prefix (exists_layout).
The bound. Given η > 0, take the cubic bound with slack ξ = η/2. A quotient on h > N₀
vertices has a layout whose frontiers have at most (c + ξ) h + 2 ≤ (2c + η) β₁ + 2 edges, and
a quotient on at most N₀ + 1 vertices has at most (N₀ + 1) N₀ / 2 edges. So every frontier
of G has at most (2c + η) β₁ + 3 log₂ N + C edges, for a constant C, and
3 log₂ N ≤ η N + C' (exists_log_le_mul_add).
The compression structure, merging, quotient, and expansion also work at any boundary
budget d. QuarticCompression supplies the terminal-core argument at degree four.
Main definitions #
Frontier.Multigraph.Compression: a partition into ordered blocks, with its invariants.Frontier.Multigraph.Compression.Final: no merge applies.Frontier.Multigraph.Compression.quotient: the simple graph on the blocks.
Main results #
Frontier.Multigraph.Compression.exists_final: merging terminates.Frontier.Multigraph.Compression.isRegularOfDegree: the quotient is cubic.Frontier.Multigraph.Compression.card_add_two_mul_le: the quotient is small.Frontier.Multigraph.Compression.exists_layout: expanding a layout of the quotient.Frontier.LayoutBound.of_cubic: the layout bound.
Preliminaries #
Listing the vertices in increasing order of an injective key gives a layout that is monotone in the key.
The cut of a disjoint union: the edges leaving both parts are counted twice on the right and not at all on the left.
In a connected multigraph, some edge leaves every set of vertices other than the empty set and the whole vertex set.
Compressions #
A compression of G: a partition of its vertices into blocks, each listing its
vertices in order, with the invariants maintained by merging. A block B is identified with
its vertex set {v | v ∈ B}.
The blocks.
Every vertex lies in a block.
Blocks sharing a vertex are equal.
A block lists each of its vertices once.
Blocks are nonempty.
At most
dedges leave a block.- cut_take_le (B : List V) : B ∈ self.blocks → ∀ k < B.length, (G.cut {v : V | v ∈ List.take k B}).ncard ≤ d * Nat.log 2 B.length
At most
d log₂ |B|edges leave a proper prefix of a blockB. - card_le : Nat.card V ≤ self.blocks.card + {e : E | ∃ B ∈ self.blocks, G.src e ∈ B ∧ G.tgt e ∈ B}.ncard
There are at least as many blocks and edges inside blocks as vertices.
Instances For
Merging. Two distinct blocks joined by an edge, whose union has at most d edges
leaving it, may be replaced by their union, listing the longer block first.
The initial compression: every vertex is a block of its own.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quotient properties needed for expansion: adjacent blocks are joined by only one edge, and at least three edges leave each nonisolated block. In degree three these characterize a terminal compression.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Merging terminates. Every multigraph of maximum degree three has a final compression: one with fewest blocks.
The quotient #
The block containing a vertex.
Instances For
The quotient of a compression: the simple graph on the blocks in which two distinct blocks are adjacent when an edge joins them.
Equations
Instances For
The edges of the quotient are the ends of the edges of G between distinct blocks.
In a final compression, an edge between two distinct blocks is determined by its ends.
In a final compression of a connected multigraph with at least two blocks, exactly three edges leave every block.
In a final compression, the quotient degree equals the block's boundary size.
The quotient of a final cubic compression is regular.
The size of the quotient. A final compression of a connected multigraph with N
vertices and M edges into h ≥ 2 blocks has h + 2N ≤ 2M.
The cut of a union of whole blocks embeds in the quotient's cut.
Expansion #
The position of a vertex in its block.
Equations
- c.idx v = List.idxOf v ↑(c.blockOf v)
Instances For
At most d log₂ N + d edges leave the first r vertices of a block.
Expansion. Lay out the vertices block by block, ordering the blocks by an injective
key and each block by its list. If at most X edges of the quotient cross each prefix of the
key, at most X + d log₂ N + d edges cross each frontier of the layout.
The layout bound #
From cubic graphs to subcubic multigraphs. A cubic layout bound with coefficient c
gives the layout bound for maximum degree three with coefficient 2c.