A layout bound in every fixed degree

A spanning tree has a layout of width d log₂ |V|. Adding the remaining edges pays once per independent cycle. Thus every fixed maximum degree has layout coefficient one, giving unconditional higher-fan-in instantiations of the circuit lower-bound theorem.

def Complexity.Frontier.Multigraph.restrictEdges {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (F : Set E) : Multigraph V ↑F

Keep a selected set of edges, retaining all vertices.

Equations

• G.restrictEdges F = { src := fun (e : ↑F) => G.src ↑e, tgt := fun (e : ↑F) => G.tgt ↑e }

theorem Complexity.Frontier.Multigraph.restrictEdges_walk_mono {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {F F' : Set E} (h : F ⊆ F') {u v : V} (hp : Relation.ReflTransGen (G.restrictEdges F).Adj u v) : Relation.ReflTransGen (G.restrictEdges F').Adj u v

theorem Complexity.Frontier.Multigraph.exists_spanning_tree {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite V] [Finite E] [Nonempty V] (hG : G.Connected) : ∃ (F : Set E), (G.restrictEdges F).Connected ∧ F.ncard + 1 = Nat.card V

A connected multigraph has a spanning tree with exactly one fewer edge than vertices. The construction grows a connected set by one new vertex and one edge at a time.

theorem Complexity.Frontier.Multigraph.Compression.sum_cut_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] : ∑ B ∈ c.blocks, (G.cut {v : V | v ∈ B}).ncard ≤ 2 * {e : E | ¬∃ B ∈ c.blocks, G.src e ∈ B ∧ G.tgt e ∈ B}.ncard

The cuts of disjoint blocks count each edge between blocks twice. Only the upper bound is needed for tree compression.

theorem Complexity.Frontier.Multigraph.Compression.exists_small_cut {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] (hcard : Nat.card E + 1 = Nat.card V) : ∃ B ∈ c.blocks, (G.cut {v : V | v ∈ B}).ncard ≤ 2

In a compression of a tree some block has at most two boundary edges.

theorem Complexity.Frontier.Multigraph.exists_tree_list {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite V] [Finite E] (hG : G.Connected) (hcard : Nat.card E + 1 = Nat.card V) {d : ℕ} (hdeg : G.MaxDegreeLE d) : ∃ (B : List V), B.Nodup ∧ (∀ (v : V), v ∈ B) ∧ ∀ k < B.length, (G.cut {v : V | v ∈ List.take k B}).ncard ≤ d * Nat.log 2 B.length

A bounded-degree tree compresses to one ordered block.

theorem Complexity.Frontier.Multigraph.exists_layout_tree {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite V] [Finite E] (hG : G.Connected) (hcard : Nat.card E + 1 = Nat.card V) {d : ℕ} (hdeg : G.MaxDegreeLE d) : ∃ (π : Layout V), ∀ (t : ℕ), (G.cut (π.initial t)).ncard ≤ d * Nat.log 2 (Nat.card V)

A tree of maximum degree d has cutwidth at most d log₂ |V|.

theorem Complexity.Frontier.Multigraph.maxDegreeLE_restrictEdges {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] {d : ℕ} (hd : G.MaxDegreeLE d) (F : Set E) : (G.restrictEdges F).MaxDegreeLE d

Restricting edges cannot increase degree.

theorem Complexity.Frontier.Multigraph.exists_layout_cycleRank {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite V] [Finite E] (hG : G.Connected) {d : ℕ} (hd : G.MaxDegreeLE d) : ∃ (π : Layout V), ∀ (t : ℕ), (G.cut (π.initial t)).ncard ≤ G.cycleRank + d * Nat.log 2 (Nat.card V)

Putting back the edges outside a spanning tree costs exactly the cycle rank.

theorem Complexity.Frontier.layoutBound_one (d : ℕ) : LayoutBound d 1

Every fixed degree has layout coefficient one. This bound is weaker than the Gaussian coefficient at degree three, but supplies every higher-fan-in instantiation.