Lax Lean Archive

Monadically dependent classes exclude large (φ, ψ)-patterns

Lax185574.ForbiddenPhiPsiPatterns · concepts/Lax185574/ForbiddenPhiPsiPatterns.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 monadically dependent graph class 𝒞 and formulas φ(x̄, z), ψ(ȳ, z), there is some t ∈ ℕ such that no graph G ∈ 𝒞 contains a (φ, ψ)-pattern of order t × t.

    This is a corollary of Lemma C.1 of the cited work on ordered twin-width. The paper includes a self-contained proof.

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

    Lean source view on GitHub

    1import Lax185574.PhiPsiPatterns
    2import Lax185574.MonadicDependence
    3
    4/-!
    5---
    6title: Monadically dependent classes exclude large (φ, ψ)-patterns
    7type: lemma
    8---
    9For every monadically dependent graph class 𝒞 and formulas φ(x̄, z),
    10ψ(ȳ, z), there is some t ∈ ℕ such that no graph G ∈ 𝒞 contains a
    11(φ, ψ)-pattern of order t × t.
    12
    13This is a corollary of Lemma C.1 of the cited work on ordered
    14twin-width. The paper includes a self-contained proof.
    15
    16# Formalization notes
    17
    18The paper allows infinite graphs in this part. Here the graphs are
    19those of a `GraphClass`, which are finite, as in every use.
    20
    21The formulas are formulas of the language of graphs, without colors,
    22with free variables as in `PhiPsiPatterns`. The number t is chosen after
    23𝒞, φ and ψ, so it depends on these only. Monadic dependence is that of
    24`Lax185574.MonadicDependence`, by transductions. The proof in the paper
    25uses the tuple form of the independence property,
    26`IndependenceProperty`.
    27-/
    28
    29namespace Lax185574.ForbiddenPhiPsiPatterns
    30
    31open FirstOrder FirstOrder.Language
    32open Lax185574.Graphs Lax185574.MonadicDependence Lax185574.PhiPsiPatterns
    33
    34/-- **Forbidden `(φ, ψ)`-patterns.** No graph of a monadically
    35dependent class contains a `(φ, ψ)`-pattern of order `t × t`, for some
    36`t` depending on the class, `φ` and `ψ`. -/
    37axiom forbidden_phiPsi_patterns (C : GraphClass) (hC : MonadicallyDependent C)
    38 {p p' : ℕ} (φ : Language.graph.Formula (Fin p ⊕ Fin 1))
    39 (ψ : Language.graph.Formula (Fin p' ⊕ Fin 1)) :
    40 ∃ t : ℕ, ∀ G ∈ C, ¬ HasPattern G.toSimpleGraph φ ψ t t
    41
    42end Lax185574.ForbiddenPhiPsiPatterns
    43
    Show Proof
    Formalization notes

    The paper allows infinite graphs in this part. Here the graphs are those of a GraphClassGraphClass, which are finite, as in every use.

    The formulas are formulas of the language of graphs, without colors, with free variables as in PhiPsiPatternsPhiPsiPatterns. The number t is chosen after 𝒞, φ and ψ, so it depends on these only. Monadic dependence is that of Lax185574.MonadicDependenceLax185574.MonadicDependence, by transductions. The proof in the paper uses the tuple form of the independence property, IndependencePropertyIndependenceProperty.

    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…