Lax Lean Archive

Closure theorem

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

    For every monadically dependent graph class π’ž and radius r ∈ β„• there are some c, s ∈ β„• with the following property.

    For every G ∈ π’ž and finite set A βŠ† V(G) there is a set A* βŠ† V(G) of size O_{π’ž,r}(|A|^c) such that for every vertex v βˆ‰ A there is a set S(v) βŠ† A* of size at most s and an S(v)-definable flip H with

    dist^H(v, A) > r.

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

    Lean source view on GitHub

    1import Lax185574.Flips
    2import Lax185574.GraphBalls
    3import Lax185574.Partitions
    4import Lax185574.MonadicDependence
    5
    6/-!
    7---
    8title: Closure theorem
    9type: theorem
    10---
    11For every monadically dependent graph class π’ž and radius r ∈ β„• there are
    12some c, s ∈ β„• with the following property.
    13
    14For every G ∈ π’ž and finite set A βŠ† V(G) there is a set A* βŠ† V(G) of size
    15O_{π’ž,r}(|A|^c) such that for every vertex v βˆ‰ A there is a set
    16S(v) βŠ† A* of size at most s and an S(v)-definable flip H with
    17
    18dist^H(v, A) > r.
    19
    20# Formalization notes
    21
    22The bound O_{π’ž,r}(|A|^c) is spelled out as a Β· (|A| + 1)^c, with a
    23chosen together with c and s, after π’ž and r. Since c is existentially
    24quantified, this is equivalent to the paper's aΒ·|A|^c + b. An
    25S(v)-definable flip is an S(v)-flip, that is a flip for the partition
    26`Partitions.atomicTypes` of G into atomic types over S(v). These are
    27the flips G βŠ• (pΜ„, R) for the tuples pΜ„ listing S(v). The condition
    28dist^H(v, A) > r is stated as Ball^H_r[v] ∩ A = βˆ….
    29
    30The set A* need not contain A, as in the paper. The paper proves the
    31theorem for finite or infinite graphs. Here π’ž is a `GraphClass`, so its
    32members are finite, which is the case used in the model-checking
    33theorem. Monadic dependence is that of `Lax185574.MonadicDependence`,
    34by transductions, as in the paper.
    35-/
    36
    37namespace Lax185574.ClosureTheorem
    38
    39open Lax185574.Graphs Lax185574.MonadicDependence
    40open Lax185574.Flips Lax185574.GraphBalls Lax185574.Partitions
    41
    42/-- **Closure theorem.** For a monadically dependent class and a radius
    43`r`, every finite parameter set `A` has a polynomial-size closure `A*`
    44such that each vertex outside `A` is separated from `A` at distance more
    45than `r` by a flip over at most `s` vertices of `A*`. -/
    46axiom closure_theorem (C : GraphClass) (hC : MonadicallyDependent C) (r : β„•) :
    47 βˆƒ c s a : β„•, βˆ€ G ∈ C, βˆ€ A : Finset (Fin G.n), βˆƒ Astar : Finset (Fin G.n),
    48 Astar.card ≀ a * (A.card + 1) ^ c ∧
    49 βˆ€ v βˆ‰ A, βˆƒ S βŠ† Astar, S.card ≀ s ∧ βˆƒ H : SimpleGraph (Fin G.n),
    50 IsFlip G.toSimpleGraph (atomicTypes G.toSimpleGraph (S : Set (Fin G.n))) H ∧
    51 Disjoint (graphBall H r {v}) (A : Set (Fin G.n))
    52
    53end Lax185574.ClosureTheorem
    54
    Show Proof
    Formalization notes

    The bound O_{π’ž,r}(|A|^c) is spelled out as a Β· (|A| + 1)^c, with a chosen together with c and s, after π’ž and r. Since c is existentially quantified, this is equivalent to the paper's aΒ·|A|^c + b. An S(v)-definable flip is an S(v)-flip, that is a flip for the partition Partitions.atomicTypesPartitions.atomicTypes of G into atomic types over S(v). These are the flips G βŠ• (pΜ„, R) for the tuples pΜ„ listing S(v). The condition dist^H(v, A) > r is stated as Ball^H_r[v] ∩ A = βˆ….

    The set A* need not contain A, as in the paper. The paper proves the theorem for finite or infinite graphs. Here π’ž is a GraphClassGraphClass, so its members are finite, which is the case used in the model-checking theorem. Monadic dependence is that of Lax185574.MonadicDependenceLax185574.MonadicDependence, by transductions, as in the paper.

    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…