Lax Lean Archive

Merge sequences and their radius-r width

Lax185574.MergeSequences · concepts/Lax185574/MergeSequences.lean · lax-185574

definition

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

    Definition

    A merge sequence of a graph G is a sequence (𝒫₁, R₁), …, (𝒫_m, R_m) such that:

    1. 𝒫₁ is the partition into singletons and 𝒫_m = {V(G)},
    2. 𝒫₁ ≼ ⋯ ≼ 𝒫_m,
    3. R₁ ⊆ ⋯ ⊆ R_m ⊆ (V(G) choose 2), and
    4. for every i ∈ [m] and X, Y ∈ 𝒫_i, the set XY ∖ R_i is contained either in E(G) or in E(Ḡ), that is, the pair X, Y is homogeneous once pairs in R_i are ignored.

    Here XY is the set of pairs xy with x ∈ X, y ∈ Y and x ≠ y. Condition 4 says that 𝒫_i is homogeneous modulo R_i. The radius-r width of the merge sequence is

    max_{2 ≤ i ≤ m} max_{v ∈ V(G)} |Ball^{R_i}r(v)/𝒫{i−1}|.

    The offset in the indices of R_i and 𝒫_{i−1} is intentional.

    Concept map
    9 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 31 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Partitions
    2import Lax185574.GraphBalls
    3import Mathlib.Order.Lattice.Nat
    4
    5/-!
    6---
    7title: Merge sequences and their radius-r width
    8type: definition
    9---
    10A *merge sequence* of a graph G is a sequence (𝒫₁, R₁), …, (𝒫_m, R_m)
    11such that:
    12
    131. 𝒫₁ is the partition into singletons and 𝒫_m = {V(G)},
    142. 𝒫₁ ≼ ⋯ ≼ 𝒫_m,
    153. R₁ ⊆ ⋯ ⊆ R_m ⊆ (V(G) choose 2), and
    164. for every i ∈ [m] and X, Y ∈ 𝒫_i, the set XY ∖ R_i is contained
    17 either in E(G) or in E(Ḡ), that is, the pair X, Y is homogeneous once
    18 pairs in R_i are ignored.
    19
    20Here XY is the set of pairs xy with x ∈ X, y ∈ Y and x ≠ y. Condition 4
    21says that 𝒫_i is *homogeneous modulo R_i*. The *radius-r width* of the
    22merge sequence is
    23
    24max_{2 ≤ i ≤ m} max_{v ∈ V(G)} |Ball^{R_i}_r(v)/𝒫_{i−1}|.
    25
    26The offset in the indices of R_i and 𝒫_{i−1} is intentional.
    27
    28# Formalization notes
    29
    30A merge sequence is a nonempty list of pairs of a partition, as in
    31`Lax185574.Partitions`, and a simple graph on the vertex type, whose
    32edges are the pairs of R_i. So R_i ⊆ (V(G) choose 2) holds by
    33construction, and R_i ⊆ R_{i+1} is the subgraph order. The partition
    34into singletons is `⊥` and the partition with one part is `⊤`.
    35
    36Homogeneity modulo R names the parts X and Y by vertices a and b with
    37X = 𝒫(a) and Y = 𝒫(b), as for flips in `Lax185574.Flips`. The ball
    38Ball^{R_i}_r(v) is the ball in the graph R_i, `GraphBalls.graphBall`.
    39The width is the supremum of a set of natural numbers, finite on a
    40finite vertex type, and the empty maximum (a sequence of length one) is
    410. Algorithms exchange merge sequences as lists of pairs of a partition
    42and a graph, in the encodings of `Lax185574.Encodings` and
    43`Lax185574.Partitions`.
    44-/
    45
    46namespace Lax185574.MergeSequences
    47
    48open Lax185574.Partitions Lax185574.GraphBalls
    49
    50universe z
    51
    52variable {V : Type z}
    53
    54/-- `P` is homogeneous modulo `R`: for every pair of parts `𝒫(a)`,
    55`𝒫(b)`, the pairs of distinct vertices between them that are not in
    56`R` are all edges of `G`, or all non-edges of `G`. -/
    57def HomogeneousModulo (G : SimpleGraph V) (P : Setoid V) (R : SimpleGraph V) : Prop :=
    58 ∀ a b : V,
    59 (∀ x y : V, P x a → P y b → x ≠ y → ¬ R.Adj x y → G.Adj x y) ∨
    60 (∀ x y : V, P x a → P y b → x ≠ y → ¬ R.Adj x y → ¬ G.Adj x y)
    61
    62/-- `ms` is a merge sequence of `G`: it starts with the partition into
    63singletons and ends with the partition with one part, the partitions
    64get coarser and the relations grow, and every partition is homogeneous
    65modulo its relation. -/
    66def IsMergeSequence (G : SimpleGraph V) (ms : List (Setoid V × SimpleGraph V)) : Prop :=
    67 ∃ h : ms ≠ [],
    68 (ms.head h).1 = ⊥ ∧ (ms.getLast h).1 = ⊤ ∧
    69 (∀ (t : ℕ) (ht : t + 1 < ms.length), ms[t].1 ≤ ms[t + 1].1 ∧ ms[t].2 ≤ ms[t + 1].2) ∧
    70 ∀ (t : ℕ) (ht : t < ms.length), HomogeneousModulo G ms[t].1 ms[t].2
    71
    72/-- The radius-`r` width of the merge sequence `ms`: the largest number
    73of parts of `𝒫_t` that meet a ball of radius `r` in `R_{t+1}`. -/
    74noncomputable def mergeWidth (r : ℕ) (ms : List (Setoid V × SimpleGraph V)) : ℕ :=
    75 sSup {K | ∃ (t : ℕ) (ht : t + 1 < ms.length) (v : V),
    76 K = partCount ms[t].1 (graphBall ms[t + 1].2 r {v})}
    77
    78end Lax185574.MergeSequences
    79
    Formalization notes

    A merge sequence is a nonempty list of pairs of a partition, as in Lax185574.PartitionsLax185574.Partitions, and a simple graph on the vertex type, whose edges are the pairs of R_i. So R_i ⊆ (V(G) choose 2) holds by construction, and R_i ⊆ R_{i+1} is the subgraph order. The partition into singletons is ⊥⊥ and the partition with one part is ⊤⊤.

    Homogeneity modulo R names the parts X and Y by vertices a and b with X = 𝒫(a) and Y = 𝒫(b), as for flips in Lax185574.FlipsLax185574.Flips. The ball Ball^{R_i}_r(v) is the ball in the graph R_i, GraphBalls.graphBallGraphBalls.graphBall. The width is the supremum of a set of natural numbers, finite on a finite vertex type, and the empty maximum (a sequence of length one) is 0. Algorithms exchange merge sequences as lists of pairs of a partition and a graph, in the encodings of Lax185574.EncodingsLax185574.Encodings and Lax185574.PartitionsLax185574.Partitions.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…