Lax Lean Archive

Radius-r depth-q width of a construction sequence

Lax185574.Width · concepts/Lax185574/Width.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

    For r, q ∈ ℕ, the radius-r depth-q width of a construction sequence G₁, …, G_λ is

    max_{t ∈ [λ−1]} max_{v ∈ V(G)} |Types^{G_t}{q,q}(Ball^{G{t+1}}_r(v))|.

    It measures a construction sequence by the number of types of q-tuples realized near each vertex. Types are taken in G_t, and balls in G_{t+1}.

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

    In the paper

    • page 14 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.ConstructionSequences
    2import Lax185574.FirstOrderTypes
    3import Mathlib.Order.ConditionallyCompleteLattice.Basic
    4import Mathlib.Data.Nat.Lattice
    5
    6/-!
    7---
    8title: Radius-r depth-q width of a construction sequence
    9type: definition
    10---
    11For r, q ∈ ℕ, the *radius-r depth-q width* of a construction sequence
    12G₁, …, G_λ is
    13
    14max_{t ∈ [λ−1]} max_{v ∈ V(G)} |Types^{G_t}_{q,q}(Ball^{G_{t+1}}_r(v))|.
    15
    16It measures a construction sequence by the number of types of q-tuples
    17realized near each vertex. Types are taken in G_t, and balls in G_{t+1}.
    18
    19# Formalization notes
    20
    21The partial graph `G_t` is the relational structure of
    22`Lax185574.PartialGraphs`, with edges, non-edges and one unary relation
    23per color. The types are those of `Lax185574.FirstOrderTypes`, without
    24parameters, `typeCount`. The maximum is the supremum of a set of natural numbers.
    25That set is finite when the vertex type is finite, which is the case in
    26every statement that uses the width. The empty maximum, for a sequence
    27of length one, is 0.
    28-/
    29
    30namespace Lax185574.Width
    31
    32open Lax185574.PartialGraphs Lax185574.FirstOrderTypes
    33
    34universe z
    35
    36variable {V : Type z}
    37
    38/-- The number of types of `q`-tuples of quantifier rank `q`, in the
    39partial graph `G`, realized by tuples from the set `X`. -/
    40noncomputable def partialTypeCount (G : PartialGraph V) (k q : ℕ) (X : Set V) : ℕ :=
    41 @typeCount language V G.structure k q X
    42
    43/-- The radius-`r` depth-`q` width of the sequence `s`: the largest
    44number of types of `q`-tuples of quantifier rank `q` in `s[t]` realized
    45by tuples from a ball of radius `r` in `s[t+1]`. -/
    46noncomputable def width (r q : ℕ) (s : List (PartialGraph V)) : ℕ :=
    47 sSup {K | ∃ (t : ℕ) (ht : t + 1 < s.length) (v : V),
    48 K = partialTypeCount s[t] q q (s[t + 1].ball r v)}
    49
    50end Lax185574.Width
    51
    Formalization notes

    The partial graph GtG_t is the relational structure of Lax185574.PartialGraphsLax185574.PartialGraphs, with edges, non-edges and one unary relation per color. The types are those of Lax185574.FirstOrderTypesLax185574.FirstOrderTypes, without parameters, typeCounttypeCount. The maximum is the supremum of a set of natural numbers. That set is finite when the vertex type is finite, which is the case in every statement that uses the width. The empty maximum, for a sequence of length one, is 0.

    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…