Lax Lean Archive

Radius-r width of a construction sequence

Lax185574.ConstructionWidth · concepts/Lax185574/ConstructionWidth.lean · lax-185574

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Partial graphs, construction sequences and their radius-r width are defined in the technical overview of the paper. A construction sequence of a graph G with vertex set V is a sequence G₁, …, G_λ of partial graphs with vertex set V. Its radius-r width is the maximum, over all t ∈ [λ] and v ∈ V, of the number of parts of G_t that intersect Ball^{G_t}_r(v). The ball is taken in the Gaifman graph (V, R(G_t)) of G_t, whose edges are the resolved pairs E(G_t) ∪ N(G_t). The radius-r merge-width of G is the minimum radius-r width over all construction sequences of G.

    For a partial graph H with partition 𝒫 and a set W ⊆ V(H), the induced partial graph H[W] has vertex set W, edges E(H) ∩ (W choose 2), non-edges N(H) ∩ (W choose 2), and partition { P ∩ W : P ∈ 𝒫 } ∖ {∅}.

    Concept map
    8 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 8 of this submission's paper
    • page 14 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.PartialGraphs
    2import Mathlib.Order.Lattice.Nat
    3
    4/-!
    5---
    6title: Radius-r width of a construction sequence
    7type: definition
    8---
    9Partial graphs, construction sequences and their radius-r width are
    10defined in the technical overview of the paper. A construction sequence
    11of a graph G with vertex set V is a sequence G₁, …, G_λ of partial
    12graphs with vertex set V. Its *radius-r width* is the maximum, over all
    13t ∈ [λ] and v ∈ V, of the number of parts of G_t that intersect
    14Ball^{G_t}_r(v). The ball is taken in the Gaifman graph (V, R(G_t)) of
    15G_t, whose edges are the resolved pairs E(G_t) ∪ N(G_t). The radius-r
    16merge-width of G is the minimum radius-r width over all construction
    17sequences of G.
    18
    19For a partial graph H with partition 𝒫 and a set W ⊆ V(H), the induced
    20partial graph H[W] has vertex set W, edges E(H) ∩ (W choose 2),
    21non-edges N(H) ∩ (W choose 2), and partition { P ∩ W : P ∈ 𝒫 } ∖ {∅}.
    22
    23# Formalization notes
    24
    25A construction sequence is a list of partial graphs, as in
    26`Lax185574.ConstructionSequences`. The Gaifman graph (V, R(G_t)) is the
    27graph of resolved pairs, so the ball is `PartialGraph.ball`. The
    28parts of a partial graph are its nonempty color classes, so the parts
    29meeting a set B correspond to the colors of the vertices of B, and their
    30number is the number of these colors. The maximum is the supremum of a
    31set of natural numbers, which is finite when the vertex type is finite.
    32The empty maximum is 0.
    33
    34This width counts parts. It is not the radius-r depth-q width of
    35`Lax185574.Width`, which counts types. The merge-width of a graph is not
    36needed and is not defined here.
    37
    38The induced partial graph H[W] is the induced substructure of
    39`Lax185574.GaifmanGraph` on the structure of H, see
    40`Lax185574.PartialGraphs`. Its colors are those of H restricted to W, so
    41its parts are the nonempty sets P ∩ W.
    42-/
    43
    44namespace Lax185574.ConstructionWidth
    45
    46open Lax185574.PartialGraphs
    47
    48universe z
    49
    50variable {V : Type z}
    51
    52/-- The radius-`r` width of the sequence `s`: the largest number of
    53parts of `s[t]` that meet a ball of radius `r` in the resolved pairs of
    54`s[t]`. -/
    55noncomputable def constructionWidth (r : ℕ) (s : List (PartialGraph V)) : ℕ :=
    56 sSup {K | ∃ (t : ℕ) (ht : t < s.length) (v : V),
    57 K = ((s[t]).color '' (s[t]).ball r v).ncard}
    58
    59end Lax185574.ConstructionWidth
    60
    Formalization notes

    A construction sequence is a list of partial graphs, as in Lax185574.ConstructionSequencesLax185574.ConstructionSequences. The Gaifman graph (V, R(G_t)) is the graph of resolved pairs, so the ball is PartialGraph.ballPartialGraph.ball. The parts of a partial graph are its nonempty color classes, so the parts meeting a set B correspond to the colors of the vertices of B, and their number is the number of these colors. The maximum is the supremum of a set of natural numbers, which is finite when the vertex type is finite. The empty maximum is 0.

    This width counts parts. It is not the radius-r depth-q width of Lax185574.WidthLax185574.Width, which counts types. The merge-width of a graph is not needed and is not defined here.

    The induced partial graph H[W] is the induced substructure of Lax185574.GaifmanGraphLax185574.GaifmanGraph on the structure of H, see Lax185574.PartialGraphsLax185574.PartialGraphs. Its colors are those of H restricted to W, so its parts are the nonempty sets P ∩ W.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…