Lax Lean Archive

Local definability bounds the width

Lax185574.DefinableToTypes Β· concepts/Lax185574/DefinableToTypes.lean Β· lax-185574

proven

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

    Theorem

    Let q ∈ β„• and h ≔ 7^q. The following holds for every monadically dependent graph class π’ž and all r, c, s, qβ‚€ ∈ β„•. If a construction sequence of a graph G ∈ π’ž is radius-(r+h) definable with c unary predicates, s parameters and rank qβ‚€, then its radius-r depth-q width is at most O_{π’ž,q,qβ‚€,c}(1) Β· poly_{π’ž,q,qβ‚€}(s).

    Concept map
    15 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA β†’ B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 17 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.LocalDefinability
    2import Lax185574.Width
    3import Lax185574.MonadicDependence
    4
    5/-!
    6---
    7title: Local definability bounds the width
    8type: theorem
    9---
    10Let q ∈ β„• and h ≔ 7^q. The following holds for every monadically
    11dependent graph class π’ž and all r, c, s, qβ‚€ ∈ β„•. If a
    12construction sequence of a graph G ∈ π’ž is radius-(r+h) definable with c
    13unary predicates, s parameters and rank qβ‚€, then its radius-r depth-q
    14width is at most O_{π’ž,q,qβ‚€,c}(1) Β· poly_{π’ž,q,qβ‚€}(s).
    15
    16# Formalization notes
    17
    18The bound is spelled out as `F Β· (s + 1)^a`. The exponent `a` depends on
    19the class, `q` and `qβ‚€`, and the factor `F` additionally on `c`. Neither
    20depends on `r` or `s`. The paper says that there is a radius increase
    21h depending on q alone. Its proof takes h = 7^q, the radius of
    22`Lax185574.LocalToGlobal`, and the statement here names this value,
    23because the algorithm of `Lax185574.FewTypes` computes the radius from
    24q.
    25-/
    26
    27namespace Lax185574.DefinableToTypes
    28
    29open Lax185574.Graphs Lax185574.MonadicDependence
    30open Lax185574.ConstructionSequences Lax185574.LocalDefinability Lax185574.PartialGraphs
    31open Lax185574.Width
    32
    33/-- **Local definability bounds the width.** A construction sequence of
    34a member of a monadically dependent class that is radius-`(r + 7^q)`
    35definable with `c` unary predicates, `s` parameters and rank `qβ‚€` has
    36radius-`r` depth-`q` width at most `F Β· (s + 1)^a`. -/
    37axiom width_le_of_isRadiusDefinable (q : β„•) (C : GraphClass) (hC : MonadicallyDependent C)
    38 (qβ‚€ : β„•) :
    39 βˆƒ a : β„•, βˆ€ c : β„•, βˆƒ F : β„•, βˆ€ r s : β„•, βˆ€ G ∈ C,
    40 βˆ€ seq : List (PartialGraph (Fin G.n)), IsConstructionSequence G.toSimpleGraph seq β†’
    41 IsRadiusDefinable G.toSimpleGraph seq (r + 7 ^ q) c s qβ‚€ β†’
    42 width r q seq ≀ F * (s + 1) ^ a
    43
    44end Lax185574.DefinableToTypes
    45
    Show Proof
    Formalization notes

    The bound is spelled out as Fβ‹…(s+1)aF Β· (s + 1)^a. The exponent aa depends on the class, qq and q0qβ‚€, and the factor FF additionally on cc. Neither depends on rr or ss. The paper says that there is a radius increase h depending on q alone. Its proof takes h = 7^q, the radius of Lax185574.LocalToGlobalLax185574.LocalToGlobal, and the statement here names this value, because the algorithm of Lax185574.FewTypesLax185574.FewTypes computes the radius from q.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…