Lax Lean Archive

Converting the flip metric of a partition into a single flip

Lax185574.PartitionMetricConversion Β· concepts/Lax185574/PartitionMetricConversion.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 and let 𝒫 be a partition of V(G). There is a refinement 𝒬 of 𝒫 with |𝒬| ≀ |𝒫| Β· 2^|𝒫| and a 𝒬-flip H of G such that, for every v ∈ V(G) and r ∈ β„•,

    Ball^H_r(v) βŠ† Ball^𝒫_{6r}(v).

    This is Lemma 8 of the cited work on separability properties of monadically dependent graph classes.

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

    Lean source view on GitHub

    1import Lax185574.Flips
    2import Lax185574.GraphBalls
    3
    4/-!
    5---
    6title: Converting the flip metric of a partition into a single flip
    7type: lemma
    8---
    9Let G be a graph and let 𝒫 be a partition of V(G). There is a refinement
    10𝒬 of 𝒫 with |𝒬| ≀ |𝒫| Β· 2^|𝒫| and a 𝒬-flip H of G such that, for every
    11v ∈ V(G) and r ∈ β„•,
    12
    13Ball^H_r(v) βŠ† Ball^𝒫_{6r}(v).
    14
    15This is Lemma 8 of the cited work on separability properties of
    16monadically dependent graph classes.
    17
    18# Formalization notes
    19
    20The graph is finite, so the numbers of parts are natural numbers, the
    21cardinalities of the quotients. The refinement 𝒬 and the flip H are
    22chosen once, before the vertex v and the radius r. The ball Ball^H_r(v)
    23is `GraphBalls.graphBall H r {v}`, and Ball^𝒫_{6r}(v) is the flip-metric
    24ball `Flips.flipBall`.
    25-/
    26
    27namespace Lax185574.PartitionMetricConversion
    28
    29open Lax185574.Flips Lax185574.GraphBalls
    30
    31universe u
    32
    33/-- **Partition-metric conversion.** A refinement `𝒬` of `𝒫` with at
    34most `|𝒫| Β· 2^|𝒫|` parts carries a single flip whose radius-`r` balls lie
    35in the radius-`6r` balls of the flip metric of `𝒫`. -/
    36axiom exists_refinement_flip {V : Type u} [Finite V] (G : SimpleGraph V)
    37 (P : Setoid V) :
    38 βˆƒ Q : Setoid V, Q ≀ P ∧
    39 Nat.card (Quotient Q) ≀ Nat.card (Quotient P) * 2 ^ Nat.card (Quotient P) ∧
    40 βˆƒ H : SimpleGraph V, IsFlip G Q H ∧
    41 βˆ€ (v : V) (r : β„•), graphBall H r {v} βŠ† flipBall G P (6 * r) v
    42
    43end Lax185574.PartitionMetricConversion
    44
    Show Proof
    Formalization notes

    The graph is finite, so the numbers of parts are natural numbers, the cardinalities of the quotients. The refinement 𝒬 and the flip H are chosen once, before the vertex v and the radius r. The ball Ball^H_r(v) is GraphBalls.graphBallHrvGraphBalls.graphBall H r {v}, and Ball^𝒫_{6r}(v) is the flip-metric ball Flips.flipBallFlips.flipBall.

    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…