Lax Lean Archive

Polynomial bound on the number of types over a parameter set

Lax185574.TypeBound · concepts/Lax185574/TypeBound.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 𝒞 be a monadically dependent graph class and k, q, c ∈ ℕ. For every graph G ∈ 𝒞, every expansion G⁺ of G by c unary predicates and every subset U ⊆ V(G),

    |Types^{G⁺}{k,q}(V(G)/U)| ≤ O{𝒞,q,k,c}(1) · poly_{𝒞,q,k}(|U|).

    The degree of the polynomial does not depend on the number c of unary predicates. Only the constant factor does.

    Concept map
    7 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 4 of this submission's paper
    • page 16 of this submission's paper
    • page 10 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Colorings
    2import Lax185574.FirstOrderTypes
    3import Lax185574.MonadicDependence
    4
    5/-!
    6---
    7title: Polynomial bound on the number of types over a parameter set
    8type: theorem
    9---
    10Let 𝒞 be a monadically dependent graph class and k, q, c ∈ ℕ. For every
    11graph G ∈ 𝒞, every expansion G⁺ of G by c unary predicates and every
    12subset U ⊆ V(G),
    13
    14|Types^{G⁺}_{k,q}(V(G)/U)| ≤ O_{𝒞,q,k,c}(1) · poly_{𝒞,q,k}(|U|).
    15
    16The degree of the polynomial does not depend on the number c of unary
    17predicates. Only the constant factor does.
    18
    19# Formalization notes
    20
    21The bound is spelled out: there is an exponent `a`, depending on the
    22class, `k` and `q`, and for each `c` a factor `F`, such that the count is
    23at most `F · (|U| + 1)^a`. The quantifier order puts `a` before `c`,
    24which is the uniformity in the number of colors that the theorem is
    25about. The paper proves the statement for possibly infinite graphs with
    26finite U. Here it is stated for the finite graphs of a `GraphClass`,
    27which is the case the model-checking theorem uses.
    28-/
    29
    30namespace Lax185574.TypeBound
    31
    32open Lax185574.Graphs Lax185574.MonadicDependence
    33open Lax185574.FirstOrderTypes Lax185574.Colorings
    34
    35/-- **Type bound.** In a monadically dependent class, the number of
    36types of quantifier rank `q` of `k`-tuples over a parameter set `U`, in
    37an expansion by `c` unary predicates, is at most `F · (|U| + 1)^a`. The
    38exponent `a` does not depend on `c`. -/
    39axiom typeCountOver_le (C : GraphClass) (hC : MonadicallyDependent C)
    40 (k q : ℕ) :
    41 ∃ a : ℕ, ∀ c : ℕ, ∃ F : ℕ, ∀ G ∈ C,
    42 ∀ (colors : Fin c → Set (Fin G.n)) (U : Finset (Fin G.n)),
    43 typeCountOver (expansion G.toSimpleGraph colors) k q Set.univ (U : Set (Fin G.n)) ≤
    44 F * (U.card + 1) ^ a
    45
    46end Lax185574.TypeBound
    47
    Show Proof
    Formalization notes

    The bound is spelled out: there is an exponent aa, depending on the class, kk and qq, and for each cc a factor FF, such that the count is at most F⋅(∣U∣+1)aF · (|U| + 1)^a. The quantifier order puts aa before cc, which is the uniformity in the number of colors that the theorem is about. The paper proves the statement for possibly infinite graphs with finite U. Here it is stated for the finite graphs of a GraphClassGraphClass, which is the case the model-checking theorem uses.

    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…