Lax Lean Archive

Few atomic types in balls avoiding a closure

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

    Lemma

    For every monadically dependent graph class π’ž and r, s ∈ β„•, there are some k, t ∈ β„• with the following property. For every G ∈ π’ž and finite set A βŠ† V(G), there is A* βŠ‡ A of size O_{π’ž,r,s}(|A|^k) such that, for every s-definable flip H of G and every vertex v,

    Ball^H_r[v] ∩ A* = βˆ… ⟹ |ATypes^H(Ball^H_r[v]/A)| ≀ t.

    Equivalently, Ball^H_r[v] intersects at most t parts of the partition of V(H) into atomic types over A in H.

    Concept map
    14 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 20 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.AtomicTypes
    2import Lax185574.DefinableFlips
    3import Lax185574.GraphBalls
    4import Lax185574.MonadicDependence
    5
    6/-!
    7---
    8title: Few atomic types in balls avoiding a closure
    9type: lemma
    10---
    11For every monadically dependent graph class π’ž and r, s ∈ β„•, there are
    12some k, t ∈ β„• with the following property. For every G ∈ π’ž and finite
    13set A βŠ† V(G), there is A* βŠ‡ A of size O_{π’ž,r,s}(|A|^k) such that, for
    14every s-definable flip H of G and every vertex v,
    15
    16Ball^H_r[v] ∩ A* = βˆ… ⟹ |ATypes^H(Ball^H_r[v]/A)| ≀ t.
    17
    18Equivalently, Ball^H_r[v] intersects at most t parts of the partition of
    19V(H) into atomic types over A in H.
    20
    21# Formalization notes
    22
    23The bound O_{π’ž,r,s}(|A|^k) is spelled out as a Β· (|A| + 1)^k, with a
    24chosen together with k and t, after π’ž, r and s. The set A* is chosen
    25before the flip H and the vertex v. The atomic types are taken in the
    26flip H, as in the paper. The parameter bound s is an input of the lemma,
    27not an output. The graphs of π’ž are finite, as in `ClosureTheorem`.
    28-/
    29
    30namespace Lax185574.BallTypes
    31
    32open Lax185574.Graphs Lax185574.MonadicDependence
    33open Lax185574.AtomicTypes Lax185574.DefinableFlips Lax185574.GraphBalls
    34
    35/-- **Few types in balls.** Every finite set `A` has a polynomial-size
    36superset `A*` such that, in every `s`-definable flip `H`, each ball of
    37radius `r` that avoids `A*` realizes at most `t` atomic types over `A`
    38in `H`. -/
    39axiom ball_types (C : GraphClass) (hC : MonadicallyDependent C) (r s : β„•) :
    40 βˆƒ k t a : β„•, βˆ€ G ∈ C, βˆ€ A : Finset (Fin G.n), βˆƒ Astar βŠ‡ A,
    41 Astar.card ≀ a * (A.card + 1) ^ k ∧
    42 βˆ€ H : SimpleGraph (Fin G.n), IsDefinableFlip G.toSimpleGraph s H β†’ βˆ€ v : Fin G.n,
    43 Disjoint (graphBall H r {v}) (Astar : Set (Fin G.n)) β†’
    44 atomicTypeCount H (graphBall H r {v}) (A : Set (Fin G.n)) ≀ t
    45
    46end Lax185574.BallTypes
    47
    Show Proof
    Formalization notes

    The bound O_{π’ž,r,s}(|A|^k) is spelled out as a Β· (|A| + 1)^k, with a chosen together with k and t, after π’ž, r and s. The set A* is chosen before the flip H and the vertex v. The atomic types are taken in the flip H, as in the paper. The parameter bound s is an input of the lemma, not an output. The graphs of π’ž are finite, as in ClosureTheoremClosureTheorem.

    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…