Lax Lean Archive

The pair relation of atomic types is definable

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

    Suppose G is a graph and 𝒫 is the partition of V(G) into atomic types over some set S ⊆ V(G). Then the relation R ≔ R(G, 𝒫) is definable in G expanded with one unary predicate marking S, using a fixed first-order formula φ_R(x, y) of quantifier rank at most 5.

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

    Lean source view on GitHub

    1import Lax185574.PairRelation
    2import Lax185574.Colorings
    3import Lax185574.FirstOrderTypes
    4
    5/-!
    6---
    7title: The pair relation of atomic types is definable
    8type: lemma
    9---
    10Suppose G is a graph and 𝒫 is the partition of V(G) into atomic types
    11over some set S ⊆ V(G). Then the relation R ≔ R(G, 𝒫) is definable in G
    12expanded with one unary predicate marking S, using a fixed first-order
    13formula φ_R(x, y) of quantifier rank at most 5.
    14
    15# Formalization notes
    16
    17"Fixed" means that one formula serves all graphs and all sets S, so the
    18formula is chosen first. It is a formula of graphs with one color, in
    19the language of `Lax185574.Colorings`, with the two free variables x
    20and y of `Fin 2`. The expansion interprets the color by S. The graph may
    21be infinite.
    22-/
    23
    24namespace Lax185574.PairRelationDefinable
    25
    26open FirstOrder FirstOrder.Language Lax710763.Transductions
    27open Lax185574.Partitions Lax185574.PairRelation Lax185574.Colorings
    28open Lax185574.FirstOrderTypes
    29
    30universe z
    31
    32/-- **Definability of the pair relation.** One formula of quantifier
    33rank at most `5`, with one color marking `S`, defines `R(G, 𝒫_S)` in
    34every graph `G`. -/
    35axiom exists_formula_pairRelation :
    36 ∃ φ : (withColors Language.graph 1).Formula (Fin 2), quantifierRank φ ≤ 5 ∧
    37 ∀ {V : Type z} (G : SimpleGraph V) (S : Set V) (x : Fin 2 → V),
    38 @Formula.Realize _ V (expansion G fun _ => S) _ φ x ↔
    39 (pairRelation G (atomicTypes G S)).Adj (x 0) (x 1)
    40
    41end Lax185574.PairRelationDefinable
    42
    Show Proof
    Formalization notes

    "Fixed" means that one formula serves all graphs and all sets S, so the formula is chosen first. It is a formula of graphs with one color, in the language of Lax185574.ColoringsLax185574.Colorings, with the two free variables x and y of Fin2Fin 2. The expansion interprets the color by S. The graph may be infinite.

    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…