Lax Lean Archive

(φ, ψ)-patterns

Lax185574.PhiPsiPatterns · concepts/Lax185574/PhiPsiPatterns.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

    Fix first-order formulas φ(x̄, z) and ψ(ȳ, z). A (φ, ψ)-pattern of order s × t in a graph G consists of tuples ā₁, …, ā_s ∈ V(G)^{|x̄|}, b̄₁, …, b̄t ∈ V(G)^{|ȳ|}, and vertices (c{i,j} : i ∈ [s], j ∈ [t]) such that the following holds for all i, i' ∈ [s] and j, j' ∈ [t]:

    1. G ⊨ φ(āᵢ, c_{i,j}), and G ⊭ φ(ā_{i'}, c_{i,j}) if i' > i,
    2. G ⊨ ψ(b̄ⱼ, c_{i,j}), and G ⊭ ψ(b̄_{j'}, c_{i,j}) if j' > j.

    The set { c_{i,j} : i ∈ [s], j ∈ [t] } is the set of grid-points of the pattern, and s is its height.

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

    In the paper

    • page 22 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Graph
    2import Mathlib.ModelTheory.Semantics
    3
    4/-!
    5---
    6title: (φ, ψ)-patterns
    7type: definition
    8---
    9Fix first-order formulas φ(x̄, z) and ψ(ȳ, z). A *(φ, ψ)-pattern* of
    10order s × t in a graph G consists of tuples ā₁, …, ā_s ∈ V(G)^{|x̄|},
    11b̄₁, …, b̄_t ∈ V(G)^{|ȳ|}, and vertices (c_{i,j} : i ∈ [s], j ∈ [t])
    12such that the following holds for all i, i' ∈ [s] and j, j' ∈ [t]:
    13
    141. G ⊨ φ(āᵢ, c_{i,j}), and G ⊭ φ(ā_{i'}, c_{i,j}) if i' > i,
    152. G ⊨ ψ(b̄ⱼ, c_{i,j}), and G ⊭ ψ(b̄_{j'}, c_{i,j}) if j' > j.
    16
    17The set { c_{i,j} : i ∈ [s], j ∈ [t] } is the set of *grid-points* of
    18the pattern, and s is its *height*.
    19
    20# Formalization notes
    21
    22Formulas are mathlib's first-order formulas in the language of graphs,
    23evaluated in the structure of the graph G. A formula φ(x̄, z) has the
    24free variables `Fin p ⊕ Fin 1`: the left summand is the tuple x̄ of
    25length p, and the right summand is the single variable z. This is the
    26convention of `IndependenceProperty` for formulas φ(x̄, ȳ). Rows and
    27columns are indexed by `Fin s` and `Fin t` with their usual order. The
    28grid-points and the tuples need not be distinct.
    29-/
    30
    31namespace Lax185574.PhiPsiPatterns
    32
    33open FirstOrder FirstOrder.Language
    34
    35universe u
    36
    37variable {V : Type u}
    38
    39/-- `G ⊨ φ(ā, c)` for a formula `φ(x̄, z)` of the language of graphs. -/
    40def Holds (G : SimpleGraph V) {p : ℕ}
    41 (φ : Language.graph.Formula (Fin p ⊕ Fin 1)) (a : Fin p → V) (c : V) :
    42 Prop :=
    43 @Formula.Realize Language.graph V G.structure _ φ (Sum.elim a ![c])
    44
    45/-- The tuples `a i`, `b j` and the vertices `c i j` form a
    46`(φ, ψ)`-pattern of order `s × t` in `G`. -/
    47def IsPattern (G : SimpleGraph V) {p p' : ℕ}
    48 (φ : Language.graph.Formula (Fin p ⊕ Fin 1))
    49 (ψ : Language.graph.Formula (Fin p' ⊕ Fin 1)) {s t : ℕ}
    50 (a : Fin s → Fin p → V) (b : Fin t → Fin p' → V) (c : Fin s → Fin t → V) :
    51 Prop :=
    52 ∀ i j,
    53 (Holds G φ (a i) (c i j) ∧ ∀ i', i < i' → ¬ Holds G φ (a i') (c i j)) ∧
    54 (Holds G ψ (b j) (c i j) ∧ ∀ j', j < j' → ¬ Holds G ψ (b j') (c i j))
    55
    56/-- `G` contains a `(φ, ψ)`-pattern of order `s × t`. -/
    57def HasPattern (G : SimpleGraph V) {p p' : ℕ}
    58 (φ : Language.graph.Formula (Fin p ⊕ Fin 1))
    59 (ψ : Language.graph.Formula (Fin p' ⊕ Fin 1)) (s t : ℕ) : Prop :=
    60 ∃ (a : Fin s → Fin p → V) (b : Fin t → Fin p' → V) (c : Fin s → Fin t → V),
    61 IsPattern G φ ψ a b c
    62
    63end Lax185574.PhiPsiPatterns
    64
    Formalization notes

    Formulas are mathlib's first-order formulas in the language of graphs, evaluated in the structure of the graph G. A formula φ(x̄, z) has the free variables Finp⊕Fin1Fin p ⊕ Fin 1: the left summand is the tuple x̄ of length p, and the right summand is the single variable z. This is the convention of IndependencePropertyIndependenceProperty for formulas φ(x̄, ȳ). Rows and columns are indexed by FinsFin s and FintFin t with their usual order. The grid-points and the tuples need not be distinct.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…