Lax Lean Archive

Type trees are distance types

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

    Corollary

    Fix ℓ ≤ k and q, a partial graph G and ā, b̄ ∈ V(G)^ℓ. Then tree_{k,q}(ā) = tree_{k,q}(b̄) if and only if G ⊨ φ(ā) ⇔ φ(b̄) for every distFO formula φ(x̄) of distance rank (k, q) with |x̄| = ℓ.

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

    Lean source view on GitHub

    1import Lax185574.TypeTrees
    2
    3/-!
    4---
    5title: Type trees are distance types
    6type: corollary
    7---
    8Fix ℓ ≤ k and q, a partial graph G and ā, b̄ ∈ V(G)^ℓ. Then
    9tree_{k,q}(ā) = tree_{k,q}(b̄) if and only if G ⊨ φ(ā) ⇔ φ(b̄) for every
    10distFO formula φ(x̄) of distance rank (k, q) with |x̄| = ℓ.
    11
    12# Formalization notes
    13
    14The vertex type is finite, as everywhere in the paper. Equality of type
    15trees is equality of the objects of `Lax185574.TypeTrees`.
    16-/
    17
    18namespace Lax185574.TreeEquivalence
    19
    20open Lax185574.PartialGraphs Lax185574.DistanceLogic Lax185574.DistanceLogic.DistFO
    21open Lax185574.TypeTrees
    22
    23/-- **Type trees are distance types.** Two tuples have the same type
    24tree of rank `(k, q)` exactly when they satisfy the same formulas of
    25distance rank `(k, q)`. -/
    26axiom tree_eq_iff {V : Type*} [Finite V] (G : PartialGraph V) (k q : ℕ) {ℓ : ℕ}
    27 (hℓ : ℓ ≤ k) (a b : Fin ℓ → V) :
    28 tree G k q a = tree G k q b ↔
    29 ∀ φ : DistFO ℓ, DRank k q φ → (Sat G a φ ↔ Sat G b φ)
    30
    31end Lax185574.TreeEquivalence
    32
    Show Proof
    Formalization notes

    The vertex type is finite, as everywhere in the paper. Equality of type trees is equality of the objects of Lax185574.TypeTreesLax185574.TypeTrees.

    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…