Expanding a block ordering to a vertex ordering

Given a final compression of a multigraph and an ordering of its blocks with small quotient cuts, list the vertices block by block in that order, each block in its own recorded order. A lower set of the resulting order is a union of whole blocks followed by a prefix of one more block, so its cut is bounded by the quotient cut of the block prefix plus the boundary of the partial block, which the compression invariant keeps logarithmic.

orderingBound_of_cubicKeys combines compression and this expansion: if every large simple cubic graph on h vertices has an injective vertex key whose prefixes are crossed by at most (a + ξ) h + 2 edges, then Multigraph.OrderingBound (2 a) (2 ξ) (N₀ + 8) holds. The factor two is the cubic core: the quotient of a final compression has h ≤ 2 (M - N)⁺ vertices. orderingBound_of_pathwidthBound takes the median ordering of a path decomposition as the key (PathwidthBound.exists_key): PathwidthBound p ξ N₀ implies Multigraph.OrderingBound (2 p) (2 ξ) (N₀ + 9). orderingBound_of_cutwidthBound takes a cutwidth key instead: CutwidthBound c ξ N₀ implies Multigraph.OrderingBound (2 c) (2 ξ) (N₀ + 8). A pathwidth bound also gives a cutwidth bound with the same coefficient (cutwidthBound_of_pathwidthBound).

theorem Algebraic.Cutwidth.PathwidthBound.exists_key {p ξ : ℝ} {N₀ : ℕ} (PW : PathwidthBound p ξ N₀) (W : Type) [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (large : N₀ < Fintype.card W) : ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.cutFinset {w : W | key w < t}).card ≤ (p + ξ) * ↑(Fintype.card W) + 2

The median ordering of a decomposition supplied by a pathwidth bound with coefficient p has prefixes crossed by at most (p + ξ) h + 2 edges.

theorem Algebraic.Cutwidth.Multigraph.exists_forall_mem_iff_key_lt {V : Type} {key : V → ℕ} (L : Finset V) (hL : ∀ (a b : V), key b ≤ key a → a ∈ L → b ∈ L) : ∃ (t : ℕ), ∀ (v : V), v ∈ L ↔ key v < t

Every lower set of the order lifted from an injective key is a key prefix.

theorem Algebraic.Cutwidth.Multigraph.mixed_lt_iff {k i q r N : ℕ} (hi : i < N) (hr : r < N) : k * N + i < q * N + r ↔ k < q ∨ k = q ∧ i < r

Mixed-radix comparison against a threshold q * N + r with i, r < N.

theorem Algebraic.Cutwidth.Multigraph.clog_le_logb_add_one (N : ℕ) : ↑(Nat.clog 2 N) ≤ Real.logb 2 ↑N + 1

⌈log₂ N⌉ is at most log₂ N + 1.

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

The position of a vertex inside its block.

Equations

• c.idx v = List.idxOf v ↑(c.blockOf v)

theorem Algebraic.Cutwidth.Multigraph.Compression.idx_lt_length {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (v : V) : c.idx v < (↑(c.blockOf v)).length

theorem Algebraic.Cutwidth.Multigraph.Compression.length_blockOf_le {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (v : V) : (↑(c.blockOf v)).length ≤ Fintype.card V

theorem Algebraic.Cutwidth.Multigraph.Compression.idx_lt_card {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (v : V) : c.idx v < Fintype.card V

theorem Algebraic.Cutwidth.Multigraph.Compression.eq_of_blockOf_eq_of_idx_eq {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {v w : V} (hb : c.blockOf v = c.blockOf w) (hi : c.idx v = c.idx w) : v = w

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

The vertex key: the key of its block, refined by its position in the block.

Equations

• c.vertexKey keyH v = keyH (c.blockOf v) * Fintype.card V + c.idx v

theorem Algebraic.Cutwidth.Multigraph.Compression.vertexKey_injective {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) {keyH : ↥c.blocks → ℕ} (injH : Function.Injective keyH) : Function.Injective (c.vertexKey keyH)

theorem Algebraic.Cutwidth.Multigraph.Compression.card_cut_blockUnion_le {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (final : ¬c.Mergeable) (T : Finset ↥c.blocks) : (G.cut {v : V | c.blockOf v ∈ T}).card ≤ (c.quotient.cutFinset T).card

The cut of a union of whole blocks embeds into the quotient cut.

theorem Algebraic.Cutwidth.Multigraph.Compression.card_cut_blockPrefix_le {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (B : ↥c.blocks) (r : ℕ) : (G.cut {v : V | c.blockOf v = B ∧ c.idx v < r}).card ≤ 3 * Nat.clog 2 (Fintype.card V) + 3

A prefix of one block, cut by position, has small boundary.

theorem Algebraic.Cutwidth.Multigraph.Compression.exists_linearOrder {V E : Type} [Fintype V] [Fintype E] {G : Multigraph V E} (c : G.Compression) (final : ¬c.Mergeable) (keyH : ↥c.blocks → ℕ) (injH : Function.Injective keyH) {X : ℕ} (hX : ∀ (q : ℕ), (c.quotient.cutFinset {B : ↥c.blocks | keyH B < q}).card ≤ X) : ∃ (x : LinearOrder V), ∀ (L : Finset V), IsLowerSet ↑L → (G.cut L).card ≤ X + 3 * Nat.clog 2 (Fintype.card V) + 3

Expansion. A final compression with an injective block key whose quotient prefix cuts are at most X yields a vertex ordering whose lower-set cuts are at most X + 3 ⌈log₂ N⌉ + 3.

theorem Algebraic.Cutwidth.Multigraph.orderingBound_of_cubicKeys {a ξ C : ℝ} (haξ : 0 ≤ a + ξ) {N₀ : ℕ} (hC : ↑N₀ + 8 ≤ C) (keys : ∀ (W : Type) [inst : Fintype W] [DecidableEq W] (H : SimpleGraph W) [inst_2 : DecidableRel H.Adj], H.IsRegularOfDegree 3 → N₀ < Fintype.card W → ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.cutFinset {w : W | key w < t}).card ≤ (a + ξ) * ↑(Fintype.card W) + 2) : OrderingBound (2 * a) (2 * ξ) C

The graph-ordering bound from cubic keys. Suppose every simple cubic graph on h > N₀ vertices has an injective vertex key whose prefixes are crossed by at most (a + ξ) h + 2 edges. A final compression with at least two blocks has a cubic quotient on h ≤ 2 (M - N)⁺ blocks, ordered by such a key or, with at most N₀ blocks, by the median ordering of its one-bag decomposition. The expansion then gives an ordering bound with coefficient 2 a and every additive constant C ≥ N₀ + 8.

theorem Algebraic.Cutwidth.Multigraph.orderingBound_of_pathwidthBound {p ξ : ℝ} (hpξ : 0 ≤ p + ξ) {N₀ : ℕ} (FH : PathwidthBound p ξ N₀) : OrderingBound (2 * p) (2 * ξ) (↑N₀ + 9)

The graph-ordering bound from the pathwidth hypothesis. A pathwidth bound with coefficient p gives an ordering bound with coefficient 2 p.

theorem Algebraic.Cutwidth.Multigraph.orderingBound_one_third_of_pathwidthBound {ξ : ℝ} (hξ : 0 ≤ ξ) {N₀ : ℕ} (FH : PathwidthBound (1 / 6) ξ N₀) : OrderingBound (1 / 3) (2 * ξ) (↑N₀ + 9)

The coefficient-four ordering bound from a cubic pathwidth bound with coefficient 1/6 at a fixed slack.

theorem Algebraic.Cutwidth.Multigraph.orderingBound_of_cutwidthBound {c ξ : ℝ} (hcξ : 0 ≤ c + ξ) {N₀ : ℕ} (CW : CutwidthBound c ξ N₀) : OrderingBound (2 * c) (2 * ξ) (↑N₀ + 8)

The graph-ordering bound from a cutwidth hypothesis. A cutwidth bound with coefficient c orders the cubic quotient of a final compression directly, giving an ordering bound with coefficient 2 c.

theorem Algebraic.Cutwidth.Multigraph.exists_orderingBound_of_pathwidthBound {p : ℝ} (hp : 0 ≤ p) (pathwidth : ∀ (ξ : ℝ), 0 < ξ → ∃ (N₀ : ℕ), PathwidthBound p ξ N₀) (η : ℝ) : 0 < η → ∃ (C : ℝ), OrderingBound (2 * p) η C

A pathwidth bound with coefficient p at every positive slack gives the graph-ordering hypothesis with coefficient 2 p at every positive slack.

theorem Algebraic.Cutwidth.Multigraph.exists_orderingBound_of_cutwidthBound {c : ℝ} (hc : 0 ≤ c) (cutwidth : ∀ (ξ : ℝ), 0 < ξ → ∃ (N₀ : ℕ), CutwidthBound c ξ N₀) (η : ℝ) : 0 < η → ∃ (C : ℝ), OrderingBound (2 * c) η C

A cutwidth bound with coefficient c at every positive slack gives the graph-ordering hypothesis with coefficient 2 c at every positive slack.

theorem Algebraic.Cutwidth.cutwidthBound_of_pathwidthBound {p ξ : ℝ} {N₀ : ℕ} (PW : PathwidthBound p ξ N₀) : CutwidthBound p (ξ + 2 / (↑N₀ + 1)) N₀

A pathwidth bound gives a cutwidth bound with the same coefficient. The median ordering of a path decomposition has prefix cuts at most one more than its bag sizes, and the two extra edges cost 2 / (N₀ + 1) per vertex above the threshold.