Layouts of disconnected graphs

The layout hypothesis Cslib.Circuits.Frontier.LayoutBound is stated for connected graphs. A disconnected graph is laid out one connected component after another, each component by the layout hypothesis (LayoutBound.exists_layout_componentwise). Every frontier of the result lies among the edges of a single component, and is bounded in terms of the cycle rank of that component alone (Cslib.Circuits.Frontier.Multigraph.cycleRankOn): the components before it are closed, so they do not change its edge cuts.

Main results

• Cslib.Circuits.Frontier.LayoutBound.exists_layout_componentwise: under the layout hypothesis, every loopless graph of maximum degree d, connected or not, has a layout whose frontiers at each step lie among the edges of the component of the vertex processed and are at most (A + η) β₁ + η |V| + C, for the cycle rank β₁ of that component.

theorem Cslib.Circuits.Frontier.LayoutBound.exists_layout_componentwise {d : ℕ} {A : ℝ} (h : LayoutBound d A) {η : ℝ} (hη : 0 < η) : ∃ (C : ℝ), ∀ (V E : Type) [Finite V] [inst : Finite E] (G : Multigraph V E), G.Loopless → G.MaxDegreeLE d → ∃ (π : Layout V), ∀ (t : ℕ) (ht : t < Nat.card V) (s : ℕ), t ≤ s → s ≤ t + 1 → G.frontier π s ⊆ G.touching (G.component ((Equiv.symm π) ⟨t, ht⟩)) ∧ ↑(G.frontier π s).ncard ≤ (A + η) * ↑(G.cycleRankOn (G.component ((Equiv.symm π) ⟨t, ht⟩))) + η * ↑(Nat.card V) + C

Layouts of disconnected graphs. Under the layout hypothesis for maximum degree d, every loopless graph of maximum degree d, connected or not, has a layout such that at every step t, with W the component of the vertex processed, the frontiers at times t and t + 1 lie among the edges of W and have at most (A + η) β₁(W) + η |V| + C edges.

The components are laid out one after another, each by the layout hypothesis.