Lax Lean Archive

A four-part flip of a bipartite graph with short edges in both polarities

Lax185574.BipartiteFlip · concepts/Lax185574/BipartiteFlip.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 B = (X, Y, E) be a bipartite graph with bipartite complement B̄, and pick arbitrary vertices x ∈ X and y ∈ Y. Partition X according to adjacency to y, that is, X = X₊ ⊎ X₋ with X₊ = N(y) and X₋ = X ∖ N(y), and similarly Y = Y₊ ⊎ Y₋ according to x. Then there is a bipartite graph B′ = (X, Y, E′), obtained from B by some {X₊, X₋, Y₊, Y₋}-flip, satisfying

    for all uv ∈ E′, dist^B(u, v) ≤ 5 and dist^{B̄}(u, v) ≤ 5.

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

    Concept map
    3 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.BipartiteGraphs
    2import Lax185574.GaifmanGraph
    3
    4/-!
    5---
    6title: A four-part flip of a bipartite graph with short edges in both polarities
    7type: lemma
    8---
    9Let B = (X, Y, E) be a bipartite graph with bipartite complement B̄, and
    10pick arbitrary vertices x ∈ X and y ∈ Y. Partition X according to
    11adjacency to y, that is, X = X₊ ⊎ X₋ with X₊ = N(y) and X₋ = X ∖ N(y),
    12and similarly Y = Y₊ ⊎ Y₋ according to x. Then there is a bipartite
    13graph B′ = (X, Y, E′), obtained from B by some {X₊, X₋, Y₊, Y₋}-flip,
    14satisfying
    15
    16for all uv ∈ E′, dist^B(u, v) ≤ 5 and dist^{B̄}(u, v) ≤ 5.
    17
    18This is Lemma A.3 of Drabik, Dumas, Geniet, Nowakowski, Pilipczuk and
    19Toruńczyk, *Variants of merge-width and applications* (2026).
    20
    21# Formalization notes
    22
    23The parts X and Y are types, and the bipartite graphs B and B̄ are
    24`bipartiteGraph E` and `bipartiteGraph` of the negated relation, from
    25`Lax185574.BipartiteGraphs`. Distances are measured by walks from the
    26copy of u in X to the copy of v in Y.
    27
    28B′ is again bipartite with parts X and Y, so the flip changes adjacency
    29only between X and Y, and it is given by its edge relation E′. That B′
    30is obtained by a {X₊, X₋, Y₊, Y₋}-flip says that for each of the four
    31pairs of a part of X and a part of Y, either E′ agrees with E on all of
    32its pairs, or with the negation of E on all of them. The statement
    33expresses this as: whether E′ agrees with E on a pair uv depends only on
    34whether u ∈ X₊ and whether v ∈ Y₊.
    35
    36The cited lemma bounds the distances by 6, and the paper states 5,
    37noting that the two statements are equivalent. Every walk in a
    38bipartite graph between a vertex of X and a vertex of Y has odd
    39length, so a distance at most 6 is at most 5. The statement uses the
    40bound 5 of the paper.
    41-/
    42
    43namespace Lax185574.BipartiteFlip
    44
    45open Lax185574.BipartiteGraphs Lax185574.GaifmanGraph
    46
    47universe u w
    48
    49/-- **Four-part flip of a bipartite graph.** For representatives `x`
    50and `y`, some flip of `E` on the four parts given by adjacency to `y`
    51and to `x` keeps only edges `uv` with `dist^B(u, v) ≤ 5` and
    52`dist^{B̄}(u, v) ≤ 5`. -/
    53axiom exists_flip_close {X : Type u} {Y : Type w} (E : X → Y → Prop) (x : X) (y : Y) :
    54 ∃ E' : X → Y → Prop,
    55 (∀ (u u' : X) (v v' : Y), (E u y ↔ E u' y) → (E x v ↔ E x v') →
    56 ((E' u v ↔ E u v) ↔ (E' u' v' ↔ E u' v'))) ∧
    57 ∀ (u : X) (v : Y), E' u v →
    58 WithinDist (bipartiteGraph E) 5 (.inl u) (.inr v) ∧
    59 WithinDist (bipartiteGraph fun a b => ¬ E a b) 5 (.inl u) (.inr v)
    60
    61end Lax185574.BipartiteFlip
    62
    Show Proof
    Formalization notes

    The parts X and Y are types, and the bipartite graphs B and B̄ are bipartiteGraphEbipartiteGraph E and bipartiteGraphbipartiteGraph of the negated relation, from Lax185574.BipartiteGraphsLax185574.BipartiteGraphs. Distances are measured by walks from the copy of u in X to the copy of v in Y.

    B′ is again bipartite with parts X and Y, so the flip changes adjacency only between X and Y, and it is given by its edge relation E′. That B′ is obtained by a {X₊, X₋, Y₊, Y₋}-flip says that for each of the four pairs of a part of X and a part of Y, either E′ agrees with E on all of its pairs, or with the negation of E on all of them. The statement expresses this as: whether E′ agrees with E on a pair uv depends only on whether u ∈ X₊ and whether v ∈ Y₊.

    The cited lemma bounds the distances by 6, and the paper states 5, noting that the two statements are equivalent. Every walk in a bipartite graph between a vertex of X and a vertex of Y has odd length, so a distance at most 6 is at most 5. The statement uses the bound 5 of 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…