Lax Lean Archive

Splitting by a transversal keeps few parts in flip-metric balls

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

    Let G be a graph, 𝒫 ≼ 𝒬 partitions of V(G), and T a transversal of 𝒫. Suppose |Ball^𝒬_{r+1}(v)/𝒫| ≤ k for every v ∈ V(G). Then for every v ∈ V(G),

    |Ball^𝒬_r(v)/(𝒫 ∧ T)| ≤ k · π_G(k).

    This is Corollary 5.4 of Drabik, Dumas, Geniet, Nowakowski, Pilipczuk and Toruńczyk, Variants of merge-width and applications (2026).

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

    Lean source view on GitHub

    1import Lax185574.TypeSplitting
    2import Lax185574.Flips
    3import Lax185574.VCDimension
    4
    5/-!
    6---
    7title: Splitting by a transversal keeps few parts in flip-metric balls
    8type: lemma
    9---
    10Let G be a graph, 𝒫 ≼ 𝒬 partitions of V(G), and T a transversal of 𝒫.
    11Suppose |Ball^𝒬_{r+1}(v)/𝒫| ≤ k for every v ∈ V(G). Then for every
    12v ∈ V(G),
    13
    14|Ball^𝒬_r(v)/(𝒫 ∧ T)| ≤ k · π_G(k).
    15
    16This is Corollary 5.4 of Drabik, Dumas, Geniet, Nowakowski, Pilipczuk and
    17Toruńczyk, *Variants of merge-width and applications* (2026).
    18
    19# Formalization notes
    20
    21The balls are those of the 𝒬-flip metric, `Flips.flipBall`, and 𝒫 ∧ T
    22is `TypeSplitting.split`. The neighborhood complexity π_G is
    23`VCDimension.neighborhoodComplexity`. The graph is finite, so that the
    24counts of parts are exact. The radius r and the bound k are arbitrary
    25natural numbers.
    26-/
    27
    28namespace Lax185574.SplitBalls
    29
    30open Lax185574.Partitions Lax185574.Flips Lax185574.TypeSplitting Lax185574.VCDimension
    31
    32universe z
    33
    34/-- **Splitting along a transversal.** If every radius-`(r+1)` ball of
    35the `𝒬`-flip metric meets at most `k` parts of `𝒫 ≼ 𝒬`, then every
    36radius-`r` ball meets at most `k · π_G(k)` parts of `𝒫 ∧ T`. -/
    37axiom partCount_split_le {V : Type z} [Finite V] (G : SimpleGraph V) (P Q : Setoid V)
    38 (T : Set V) (r k : ℕ) (hPQ : P ≤ Q) (hT : IsTransversal P T)
    39 (hk : ∀ v : V, partCount P (flipBall G Q (r + 1) v) ≤ k) (v : V) :
    40 partCount (split G P T) (flipBall G Q r v) ≤ k * neighborhoodComplexity G k
    41
    42end Lax185574.SplitBalls
    43
    Show Proof
    Formalization notes

    The balls are those of the 𝒬-flip metric, Flips.flipBallFlips.flipBall, and 𝒫 ∧ T is TypeSplitting.splitTypeSplitting.split. The neighborhood complexity π_G is VCDimension.neighborhoodComplexityVCDimension.neighborhoodComplexity. The graph is finite, so that the counts of parts are exact. The radius r and the bound k are arbitrary natural numbers.

    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…