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_pathwidthBound combines compression, the pathwidth hypothesis, the median ordering, and this expansion: PathwidthBound ξ N₀ implies Multigraph.OrderingBound (2 ξ) (N₀ + 9).

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_pathwidthBound {ξ : ℝ} (hξ : 0 ≤ ξ) {N₀ : ℕ} (FH : PathwidthBound ξ N₀) : OrderingBound (2 * ξ) (↑N₀ + 9)

The graph-ordering bound from the pathwidth hypothesis.