Lax Lean Archive

A definable flip separating a ball one step further

Lax185574.BallFlip · concepts/Lax185574/BallFlip.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 all d, t ∈ ℕ, there is some z ∈ ℕ with the following property.

    For every graph G of VC-dimension at most d, radius r ∈ ℕ, finite set A ⊆ V(G), and arbitrary set C ⊆ V(G) satisfying

    Ball^G_r[C] ∩ A = ∅ and |ATypes^G(Ball^G_r[C]/A)| ≤ t,

    there exists a z-definable flip H of G in which Ball^H_{r+1}[C] ∩ A = ∅.

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

    Lean source view on GitHub

    1import Lax185574.AtomicTypes
    2import Lax185574.DefinableFlips
    3import Lax185574.GraphBalls
    4import Lax185574.VCDimension
    5
    6/-!
    7---
    8title: A definable flip separating a ball one step further
    9type: lemma
    10---
    11For all d, t ∈ ℕ, there is some z ∈ ℕ with the following property.
    12
    13For every graph G of VC-dimension at most d, radius r ∈ ℕ, finite set
    14A ⊆ V(G), and arbitrary set C ⊆ V(G) satisfying
    15
    16Ball^G_r[C] ∩ A = ∅ and |ATypes^G(Ball^G_r[C]/A)| ≤ t,
    17
    18there exists a z-definable flip H of G in which Ball^H_{r+1}[C] ∩ A = ∅.
    19
    20# Formalization notes
    21
    22The number z is chosen after d and t and before the graph and the
    23radius, so it does not depend on r. The graph is finite, so A is finite.
    24The paper also allows infinite graphs with A finite. The lemma is
    25applied in the proof of the closure theorem to flips of graphs of a
    26graph class, which are finite. The atomic types are taken in G.
    27-/
    28
    29namespace Lax185574.BallFlip
    30
    31open Lax185574.AtomicTypes Lax185574.DefinableFlips Lax185574.GraphBalls
    32open Lax185574.VCDimension
    33
    34universe u
    35
    36/-- **Ball flip.** If a ball of radius `r` around `C` avoids `A` and
    37realizes at most `t` atomic types over `A`, then a `z(d, t)`-definable
    38flip moves `A` out of the ball of radius `r + 1` around `C`. -/
    39axiom exists_ball_flip (d t : ℕ) :
    40 ∃ z : ℕ, ∀ (V : Type u) [Finite V] (G : SimpleGraph V), vcDim G ≤ d →
    41 ∀ (r : ℕ) (A C : Set V), Disjoint (graphBall G r C) A →
    42 atomicTypeCount G (graphBall G r C) A ≤ t →
    43 ∃ H : SimpleGraph V, IsDefinableFlip G z H ∧
    44 Disjoint (graphBall H (r + 1) C) A
    45
    46end Lax185574.BallFlip
    47
    Show Proof
    Formalization notes

    The number z is chosen after d and t and before the graph and the radius, so it does not depend on r. The graph is finite, so A is finite. The paper also allows infinite graphs with A finite. The lemma is applied in the proof of the closure theorem to flips of graphs of a graph class, which are finite. The atomic types are taken in G.

    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…