Lax Lean Archive

Merge sequences with definable stages from chains

Lax185574.BetterMergeSequences · concepts/Lax185574/BetterMergeSequences.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 every graph G and chain of length ℓ there is a merge sequence (𝒬₁, R₁), …, (𝒬_ℓ, R_ℓ) with the following properties.

    1. For all r ≥ 1, the radius-r width of the merge sequence is bounded by k · π_G(k), where k is the radius-(5r+1) width of the given chain.
    2. For each i ∈ [ℓ], the relations ≡{𝒬_i} and R_i are definable in some expansion G^i of G with two unary predicates, using two fixed first-order formulas φ≡(x, y) and φ_R(x, y) of quantifier rank at most 5.
    3. The merge sequence can be computed in time O(ℓ n³), given G and its chain.

    Here ≡_𝒬 is the equivalence relation on V(G) whose classes are the parts of the partition 𝒬.

    Concept map
    20 concepts; 1 descendant hidden
    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.MergeSequences
    2import Lax185574.Chains
    3import Lax185574.VCDimension
    4import Lax185574.Colorings
    5import Lax185574.FirstOrderTypes
    6import Lax185574.Algorithms
    7
    8/-!
    9---
    10title: Merge sequences with definable stages from chains
    11type: lemma
    12---
    13For every graph G and chain of length ℓ there is a merge sequence
    14(𝒬₁, R₁), …, (𝒬_ℓ, R_ℓ) with the following properties.
    15
    161. For all r ≥ 1, the radius-r width of the merge sequence is bounded by
    17 k · π_G(k), where k is the radius-(5r+1) width of the given chain.
    182. For each i ∈ [ℓ], the relations ≡_{𝒬_i} and R_i are definable in some
    19 expansion G^i of G with two unary predicates, using two fixed
    20 first-order formulas φ_≡(x, y) and φ_R(x, y) of quantifier rank at
    21 most 5.
    223. The merge sequence can be computed in time O(ℓ n³), given G and its
    23 chain.
    24
    25Here ≡_𝒬 is the equivalence relation on V(G) whose classes are the parts
    26of the partition 𝒬.
    27
    28# Formalization notes
    29
    30The two formulas come first, since they are fixed: the same formulas
    31serve every graph, every chain and every stage. Only the expansion G^i
    32depends on the stage. They are formulas of graphs with two colors, in
    33the language of `Lax185574.Colorings`, with the free variables x and y
    34of `Fin 2`. `StagesDefinable` states the second property for given
    35formulas.
    36
    37The merge sequence is produced by a function `M` of the graph and the
    38chain, and the algorithm `A` computes this function, in the sense of
    39`Lax185574.Algorithms`. The algorithm and the constant `c` of the time
    40bound O((ℓ+1) · (n+1)³) come first, so the constant is absolute. The
    41input is the pair (G, S) and the output is the merge sequence, with
    42partitions encoded as in `Lax185574.Partitions`. The merge sequence has
    43length ℓ, the length of the chain. A graph has the vertices `Fin n`,
    44and the notions of merge sequences and chains are applied to its
    45`SimpleGraph`. The neighborhood complexity π_G is
    46`VCDimension.neighborhoodComplexity`.
    47-/
    48
    49namespace Lax185574.BetterMergeSequences
    50
    51open FirstOrder FirstOrder.Language Lax710763.Transductions
    52open Lax185574.Graphs Lax185574.Algorithms
    53open Lax185574.Partitions Lax185574.MergeSequences Lax185574.Chains
    54open Lax185574.VCDimension Lax185574.Colorings Lax185574.FirstOrderTypes
    55
    56universe z
    57
    58variable {V : Type z}
    59
    60/-- The stages of the merge sequence `ms` are definable by the formulas
    61`φeq` and `φR`: for every stage there are two color sets such that, in
    62the expansion of `G` by them, `φeq` defines the equivalence relation of
    63the partition and `φR` defines the relation of the stage. -/
    64def StagesDefinable (G : SimpleGraph V) (ms : List (Setoid V × SimpleGraph V))
    65 (φeq φR : (withColors Language.graph 2).Formula (Fin 2)) : Prop :=
    66 ∀ (t : ℕ) (ht : t < ms.length), ∃ colors : Fin 2 → Set V, ∀ x : Fin 2 → V,
    67 (@Formula.Realize _ V (expansion G colors) _ φeq x ↔ ms[t].1 (x 0) (x 1)) ∧
    68 (@Formula.Realize _ V (expansion G colors) _ φR x ↔ ms[t].2.Adj (x 0) (x 1))
    69
    70/-- **Merge sequences from chains.** Two fixed formulas of quantifier
    71rank at most `5` and one algorithm that computes, from a graph and a
    72chain of length `ℓ`, a merge sequence of length `ℓ` with the following
    73properties. (1) For every `r ≥ 1`, its radius-`r` width is at most
    74`k · π_G(k)` for the radius-`(5r+1)` width `k` of the chain. (2) The two
    75formulas define its stages. (3) The algorithm takes time
    76`O((ℓ+1) · (n+1)³)`. -/
    77axiom exists_mergeSequence_of_chain :
    78 ∃ (φeq φR : (withColors Language.graph 2).Formula (Fin 2)),
    79 quantifierRank φeq ≤ 5 ∧ quantifierRank φR ≤ 5 ∧
    80 ∃ (A : Algorithm) (c : ℕ) (M : (G : Graph) → List (Finset (Fin G.n)) →
    81 List (Setoid (Fin G.n) × SimpleGraph (Fin G.n))),
    82 ∀ (G : Graph) (S : List (Finset (Fin G.n))), IsChain S →
    83 IsMergeSequence G.toSimpleGraph (M G S) ∧ (M G S).length = S.length ∧
    84 (∀ r : ℕ, 1 ≤ r →
    85 mergeWidth r (M G S) ≤ chainWidth G.toSimpleGraph (5 * r + 1) S *
    86 neighborhoodComplexity G.toSimpleGraph (chainWidth G.toSimpleGraph (5 * r + 1) S)) ∧
    87 StagesDefinable G.toSimpleGraph (M G S) φeq φR ∧
    88 A.Computes c (G, S) (M G S) ((S.length + 1) * (G.n + 1) ^ 3)
    89
    90end Lax185574.BetterMergeSequences
    91
    Show Proof
    Formalization notes

    The two formulas come first, since they are fixed: the same formulas serve every graph, every chain and every stage. Only the expansion G^i depends on the stage. They are formulas of graphs with two colors, in the language of Lax185574.ColoringsLax185574.Colorings, with the free variables x and y of Fin2Fin 2. StagesDefinableStagesDefinable states the second property for given formulas.

    The merge sequence is produced by a function MM of the graph and the chain, and the algorithm AA computes this function, in the sense of Lax185574.AlgorithmsLax185574.Algorithms. The algorithm and the constant cc of the time bound O((ℓ+1) · (n+1)³) come first, so the constant is absolute. The input is the pair (G, S) and the output is the merge sequence, with partitions encoded as in Lax185574.PartitionsLax185574.Partitions. The merge sequence has length ℓ, the length of the chain. A graph has the vertices FinnFin n, and the notions of merge sequences and chains are applied to its SimpleGraphSimpleGraph. The neighborhood complexity π_G is VCDimension.neighborhoodComplexityVCDimension.neighborhoodComplexity.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…