Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Gaifman distance and local formulas

Lax512892.Locality · concepts/Lax512892/Locality.lean · lax-512892

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

    Two distinct elements of a relational structure are Gaifman-adjacent when they occur together in a tuple belonging to an interpreted relation. The predicate distanceAtMostArabdistanceAtMost A r a b says that the Gaifman graph has a walk of length at most rr from aa to bb.

    An rr-local formula around a tuple of anchor variables is represented by a syntax in which every quantifier is explicitly restricted to the union of the radius-rr balls around those anchors. Its atomic terms may refer to anchors, locally bound variables, and vocabulary constants. This is the syntactic notion of locality used by Gaifman's normal-form theorem, not merely a semantic invariance property.

    Concept map
    3 concepts; 1 descendant hidden
    100%
    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax512892.FirstOrder
    2
    3/-!
    4---
    5title: Gaifman distance and local formulas
    6type: definition
    7---
    8Two distinct elements of a relational structure are Gaifman-adjacent when they
    9occur together in a tuple belonging to an interpreted relation. The predicate
    10`distanceAtMost A r a b` says that the Gaifman graph has a walk of length at
    11most `r` from `a` to `b`.
    12
    13An `r`-local formula around a tuple of anchor variables is represented by a
    14syntax in which every quantifier is explicitly restricted to the union of the
    15radius-`r` balls around those anchors. Its atomic terms may refer to anchors,
    16locally bound variables, and vocabulary constants. This is the syntactic notion
    17of locality used by Gaifman's normal-form theorem, not merely a semantic
    18invariance property.
    19
    20# Formalization notes
    21
    22Anchor variables and locally bound variables have separate types. This prevents
    23a newly quantified variable from silently becoming an additional centre of the
    24neighbourhood. The semantics of the local existential constructor chooses an
    25element in the ball around one of the original anchors and extends only the
    26bound-variable environment. Negation supplies restricted universal
    27quantification in the usual way.
    28
    29Distance is defined by bounded walks instead of a minimum taking the value
    30infinity. At radius zero it is equality; the successor clause either uses a
    31shorter walk or takes one Gaifman edge followed by a shorter walk.
    32-/
    33
    34namespace Lax512892.Locality
    35
    36open Lax512892.RelationalStructures Lax512892.FirstOrder
    37
    38/-- Adjacency in the Gaifman graph of a relational structure. -/
    39def gaifmanAdjacent {σ : Vocabulary} {M : Type*} (A : Structure σ M) (a b : M) : Prop :=
    40 a ≠ b ∧
    41 ∃ (R : σ.Relation) (tuple : Fin (σ.arity R) → M),
    42 A.relation R tuple ∧
    43 ∃ i j : Fin (σ.arity R), i ≠ j ∧ tuple i = a ∧ tuple j = b
    44
    45/-- `distanceAtMost A r a b` holds when a walk of at most `r` Gaifman edges
    46joins `a` to `b`. -/
    47def distanceAtMost {σ : Vocabulary} {M : Type*} (A : Structure σ M) :
    48 ℕ → M → M → Prop
    49 | 0, a, b => a = b
    50 | r + 1, a, b =>
    51 distanceAtMost A r a b ∨
    52 ∃ c : M, gaifmanAdjacent A a c ∧ distanceAtMost A r c b
    53
    54/-- Membership in the union of the radius-`r` balls around the tuple `anchors`. -/
    55def inBallAround {σ : Vocabulary} {M : Type*} (A : Structure σ M)
    56 (r : ℕ) {k : ℕ} (anchors : Fin k → M) (x : M) : Prop :=
    57 ∃ i : Fin k, distanceAtMost A r (anchors i) x
    58
    59/-- A term in a local formula, distinguishing the fixed anchor variables from
    60variables introduced by restricted quantifiers. -/
    61inductive LocalTerm (σ : Vocabulary) (anchorCount boundCount : ℕ) : Type
    62 /-- One of the fixed variables around which locality is measured. -/
    63 | anchor (i : Fin anchorCount)
    64 /-- A variable introduced by a restricted quantifier. -/
    65 | bound (i : Fin boundCount)
    66 /-- A constant of the vocabulary. -/
    67 | const (c : σ.Constant)
    68
    69/-- Formulas whose quantifiers are all restricted to the radius-`r` ball around
    70the original `anchorCount` variables. -/
    71inductive LocalFormula (σ : Vocabulary) (anchorCount r : ℕ) : ℕ → Type
    72 /-- A relation atom. -/
    73 | rel {boundCount : ℕ} (R : σ.Relation)
    74 (args : Fin (σ.arity R) → LocalTerm σ anchorCount boundCount) :
    75 LocalFormula σ anchorCount r boundCount
    76 /-- Equality of local terms. -/
    77 | eq {boundCount : ℕ} (left right : LocalTerm σ anchorCount boundCount) :
    78 LocalFormula σ anchorCount r boundCount
    79 /-- Negation. -/
    80 | not {boundCount : ℕ} (φ : LocalFormula σ anchorCount r boundCount) :
    81 LocalFormula σ anchorCount r boundCount
    82 /-- Disjunction. -/
    83 | or {boundCount : ℕ} (φ ψ : LocalFormula σ anchorCount r boundCount) :
    84 LocalFormula σ anchorCount r boundCount
    85 /-- Existential quantification restricted to the radius-`r` ball around the
    86 original anchors. -/
    87 | ex {boundCount : ℕ} (φ : LocalFormula σ anchorCount r (boundCount + 1)) :
    88 LocalFormula σ anchorCount r boundCount
    89
    90namespace LocalTerm
    91
    92/-- Interpretation of a term occurring in a local formula. -/
    93def eval {σ : Vocabulary} {M : Type*} {anchorCount boundCount : ℕ}
    94 (A : Structure σ M)
    95 (anchors : Fin anchorCount → M) (bound : Fin boundCount → M) :
    96 LocalTerm σ anchorCount boundCount → M
    97 | .anchor i => anchors i
    98 | .bound i => bound i
    99 | .const c => A.constant c
    100
    101end LocalTerm
    102
    103namespace LocalFormula
    104
    105/-- Satisfaction for a syntactically local formula. Every existential witness
    106is required to lie in the fixed neighbourhood of the anchor tuple. -/
    107def Sat {σ : Vocabulary} {M : Type*} {anchorCount r : ℕ}
    108 (A : Structure σ M)
    109 (anchors : Fin anchorCount → M) :
    110 {boundCount : ℕ} → LocalFormula σ anchorCount r boundCount →
    111 (Fin boundCount → M) → Prop
    112 | _, .rel R args, bound =>
    113 A.relation R (fun i => (args i).eval A anchors bound)
    114 | _, .eq left right, bound =>
    115 left.eval A anchors bound = right.eval A anchors bound
    116 | _, .not φ, bound => ¬ Sat A anchors φ bound
    117 | _, .or φ ψ, bound => Sat A anchors φ bound ∨ Sat A anchors ψ bound
    118 | _, .ex φ, bound =>
    119 ∃ x : M, inBallAround A r anchors x ∧ Sat A anchors φ (Fin.snoc bound x)
    120
    121end LocalFormula
    122
    123end Lax512892.Locality
    124
    Formalization notes

    Anchor variables and locally bound variables have separate types. This prevents a newly quantified variable from silently becoming an additional centre of the neighbourhood. The semantics of the local existential constructor chooses an element in the ball around one of the original anchors and extends only the bound-variable environment. Negation supplies restricted universal quantification in the usual way.

    Distance is defined by bounded walks instead of a minimum taking the value infinity. At radius zero it is equality; the successor clause either uses a shorter walk or takes one Gaifman edge followed by a shorter walk.

    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…