Documentation

Complexity.Computability.Circuit.Frontier.Layouts.Cubic

From cubic graphs to subcubic multigraphs #

The circuits of fan-in two give subcubic multigraphs, so the layout hypothesis that matters most is LayoutBound 3 A. This file reduces it to laying out cubic graphs, those without loops or parallel edges in which every vertex has exactly three edges.

CubicLayoutBound c says that for every ξ > 0, every large enough cubic graph on h vertices has a layout of width at most (c + ξ) h. A connected cubic graph on h vertices has cycle rank h/2 + 1, which is why a cubic coefficient c becomes the layout coefficient 2c (LayoutBound.of_cubic).

The quotient. Let G be a connected multigraph of maximum degree three, with N vertices, M edges and cycle rank β₁ = M - N + 1, and take a saturated compression of G with budget three. 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 neighbour. So the quotient is a cubic graph. Its h vertices span 3h/2 edges, and the counting invariant of compressions gives h + 2N ≤ 2M, so the quotient has at most 2 β₁ vertices (Saturated.card_blocks_le).

The bound. Given η > 0, take the cubic bound with slack ξ = η/2. A quotient on h > N₀ vertices has a layout of width at most (c + ξ) h ≤ (2c + η) β₁, and a quotient on at most N₀ + 1 vertices has at most 3 (N₀ + 1) edges. Expanding the layout of the quotient costs at most 3 log₂ N more edges at each frontier, which is at most η N plus a constant.

Main definitions #

Main results #

source
def Cslib.Circuits.Frontier.CubicLayoutBound (c : ℝ) :
Prop

The cubic layout bound with coefficient c: for every ξ > 0, every large enough cubic graph on h vertices has a layout of width at most (c + ξ) h. A cubic graph is presented as a multigraph without loops or parallel edges in which every vertex has exactly three edges.

Instances For
    source
    theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.ncard_edgeCut_inter_le_one {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {c : G.Compression 3} [Finite E] (hc : c.Saturated) {B B' : ↥c.blocks} (hne : B ≠ B') :
    (G.edgeCut {v : V | v ∈ ↑B} ∩ G.edgeCut {v : V | v ∈ ↑B'}).ncard ≤ 1

    In a saturated compression with budget three, two distinct blocks are joined by at most one edge.

    source
    theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.ncard_edgeCut_eq_three {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {c : G.Compression 3} [Finite E] (hc : c.Saturated) (hG : G.toSimpleGraph.Connected) (two : 1 < Nat.card ↥c.blocks) (B : ↥c.blocks) :
    (G.edgeCut {v : V | v ∈ ↑B}).ncard = 3

    In a saturated compression with budget three of a connected multigraph into at least two blocks, exactly three edges leave each block.

    source
    theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.injective_ends_quotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {c : G.Compression 3} [Finite E] (hc : c.Saturated) :
    Function.Injective c.quotient.ends

    The quotient of a saturated compression with budget three has no parallel edges.

    source
    theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.ncard_incidenceSet_quotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {c : G.Compression 3} [Finite E] (hc : c.Saturated) (hG : G.toSimpleGraph.Connected) (two : 1 < Nat.card ↥c.blocks) (B : ↥c.blocks) :
    (c.quotient.incidenceSet B).ncard = 3

    The quotient of a saturated compression with budget three of a connected multigraph into at least two blocks is cubic.

    source
    theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.card_blocks_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {c : G.Compression 3} [Finite E] (hc : c.Saturated) (hG : G.toSimpleGraph.Connected) (two : 1 < Nat.card ↥c.blocks) :
    Nat.card ↥c.blocks ≤ 2 * G.cycleRank

    The size of the quotient. A saturated compression with budget three of a connected multigraph into at least two blocks has at most 2 β₁ blocks.

    source
    theorem Cslib.Circuits.Frontier.LayoutBound.of_cubic {c : ℝ} (hc : 0 ≤ c) (h : CubicLayoutBound c) :
    LayoutBound 3 (2 * c)

    From cubic graphs to subcubic multigraphs. The cubic layout bound with coefficient c gives the layout hypothesis for maximum degree three with coefficient 2c.