Lax Lean Archive

Closure theorem for tuples

Lax185574.ClosureTheoremTuples Β· concepts/Lax185574/ClosureTheoremTuples.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 π’ž, radius r ∈ β„•, and tuple size k ∈ β„•, there are some c, s ∈ β„• with the following property.

    For every G ∈ π’ž and finite set A βŠ† V(G) there is a set β„‹ of O_{π’ž,r,k}(|A|^c) many s-flips of G such that for every tuple vΜ„ ∈ (V(G) βˆ– A)^k there is a 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 20 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Flips
    2import Lax185574.GraphBalls
    3import Lax185574.MonadicDependence
    4
    5/-!
    6---
    7title: Closure theorem for tuples
    8type: theorem
    9---
    10For every monadically dependent graph class π’ž, radius r ∈ β„•, and tuple
    11size k ∈ β„•, there are some c, s ∈ β„• with the following property.
    12
    13For every G ∈ π’ž and finite set A βŠ† V(G) there is a set β„‹ of
    14O_{π’ž,r,k}(|A|^c) many s-flips of G such that for every tuple
    15vΜ„ ∈ (V(G) βˆ– A)^k there is a flip H ∈ β„‹ with
    16
    17dist^H(vΜ„, A) > r.
    18
    19# Formalization notes
    20
    21The bound O_{π’ž,r,k}(|A|^c) is spelled out as a Β· (|A| + 1)^c, with a
    22chosen together with c and s, after π’ž, r and k. The set β„‹ is a finite
    23set of graphs on the vertex set of G, each an s-flip, that is a 𝒫-flip
    24for a partition 𝒫 into at most s parts. The number of parts is the
    25cardinality of the quotient, which is finite as the graph is finite.
    26The flips need not be definable. The condition dist^H(vΜ„, A) > r, for
    27the minimum distance between the entries of vΜ„ and A, is stated as
    28disjointness of A from the ball of radius r around the entries of vΜ„.
    29The graphs of π’ž are finite, as in `ClosureTheorem`.
    30-/
    31
    32namespace Lax185574.ClosureTheoremTuples
    33
    34open Lax185574.Graphs Lax185574.MonadicDependence
    35open Lax185574.Flips Lax185574.GraphBalls
    36
    37/-- **Closure theorem for tuples.** For a monadically dependent class, a
    38radius `r` and a tuple size `k`, every finite parameter set `A` has a
    39polynomial-size family of `s`-flips such that each `k`-tuple outside `A`
    40is at distance more than `r` from `A` in some member. -/
    41axiom closure_theorem_tuples (C : GraphClass) (hC : MonadicallyDependent C)
    42 (r k : β„•) :
    43 βˆƒ c s a : β„•, βˆ€ G ∈ C, βˆ€ A : Finset (Fin G.n),
    44 βˆƒ family : Finset (SimpleGraph (Fin G.n)),
    45 family.card ≀ a * (A.card + 1) ^ c ∧
    46 (βˆ€ H ∈ family, βˆƒ P : Setoid (Fin G.n),
    47 Nat.card (Quotient P) ≀ s ∧ IsFlip G.toSimpleGraph P H) ∧
    48 βˆ€ v : Fin k β†’ Fin G.n, (βˆ€ i, v i βˆ‰ A) β†’
    49 βˆƒ H ∈ family, Disjoint (graphBall H r (Set.range v)) (A : Set (Fin G.n))
    50
    51end Lax185574.ClosureTheoremTuples
    52
    Show Proof
    Formalization notes

    The bound O_{π’ž,r,k}(|A|^c) is spelled out as a Β· (|A| + 1)^c, with a chosen together with c and s, after π’ž, r and k. The set β„‹ is a finite set of graphs on the vertex set of G, each an s-flip, that is a 𝒫-flip for a partition 𝒫 into at most s parts. The number of parts is the cardinality of the quotient, which is finite as the graph is finite. The flips need not be definable. The condition dist^H(vΜ„, A) > r, for the minimum distance between the entries of vΜ„ and A, is stated as disjointness of A from the ball of radius r around the entries of vΜ„. 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…