Documentation

Complexity.Computability.Circuit.Frontier.Layouts.General

The layout hypothesis in every degree, from spanning trees #

A tree of maximum degree d on N vertices has a layout of width at most d log₂ N: in a compression of a tree with the fewest blocks, some block has at most one edge leaving it, so it merges with a neighbour unless it is the only block, and then the expansion of the trivial layout of the quotient is the layout (exists_width_le_of_card_add_one_eq).

A connected multigraph has a spanning tree, obtained from one of its underlying simple graph (exists_spanningTree). Laying out the spanning tree and putting back the β₁ edges outside it costs at most β₁ edges at each frontier (exists_width_le_cycleRank_add). So every fixed maximum degree has layout coefficient one (layoutBound_one), which yields unconditional circuit lower bounds for every fan-in (the module Complexity.Computability.Circuit.Frontier.Unconditional).

Main definitions #

Main results #

source
def Cslib.Circuits.Frontier.Multigraph.edgeRestrict {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (F : Set E) :
Multigraph V ↑F

The multigraph keeping the edges in F, and all the vertices.

Instances For
    source
    theorem Cslib.Circuits.Frontier.Multigraph.MaxDegreeLE.edgeRestrict {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite E] {d : ℕ} (hd : G.MaxDegreeLE d) (F : Set E) :
    (G.edgeRestrict F).MaxDegreeLE d

    Removing edges does not increase degrees.

    source
    theorem Cslib.Circuits.Frontier.Multigraph.exists_spanningTree {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite V] (hG : G.toSimpleGraph.Connected) :
    ∃ (F : Set E), (G.edgeRestrict F).toSimpleGraph.Connected ∧ Nat.card ↑F + 1 = Nat.card V

    Spanning trees. A finite connected multigraph has a set of |V| - 1 edges that still connects it. The edges are chosen along a spanning tree of the underlying simple graph.

    source
    theorem Cslib.Circuits.Frontier.Multigraph.exists_width_le_of_card_add_one_eq {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite V] [Finite E] {d : ℕ} (hG : G.toSimpleGraph.Connected) (hcard : Nat.card E + 1 = Nat.card V) (hd : G.MaxDegreeLE d) :
    ∃ (π : Layout V), G.width π ≤ d * Nat.log 2 (Nat.card V)

    Trees have logarithmic width. A finite connected multigraph of maximum degree d with one edge fewer than vertices has a layout of width at most d log₂ |V|.

    source
    theorem Cslib.Circuits.Frontier.Multigraph.exists_width_le_cycleRank_add {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite V] [Finite E] {d : ℕ} (hG : G.toSimpleGraph.Connected) (hd : G.MaxDegreeLE d) :
    ∃ (π : Layout V), G.width π ≤ G.cycleRank + d * Nat.log 2 (Nat.card V)

    Layouts from spanning trees. A finite connected multigraph of maximum degree d has a layout of width at most β₁ + d log₂ |V|, where β₁ is its cycle rank: lay out a spanning tree, and put back the β₁ edges outside it.

    source
    theorem Cslib.Circuits.Frontier.layoutBound_one (d : ℕ) :
    LayoutBound d 1

    The layout hypothesis with coefficient one, in every degree: connected multigraphs of maximum degree d have layouts of width at most β₁ + d log₂ |V|.