Lax Lean Archive

Locality of type trees

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

    Every node at depth j of tree_{k,q}(a) is tree_{k+j,q−j}(v̄) for some tuple v̄ from Ball_{ρ⁺(k,q)}(a), and every color mentioned in the root label of that node intersects this ball.

    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: Locality of type trees
    6type: lemma
    7---
    8Every node at depth j of tree_{k,q}(a) is tree_{k+j,q−j}(v̄) for some
    9tuple v̄ from Ball_{ρ⁺(k,q)}(a), and every color mentioned in the root
    10label of that node intersects this ball.
    11
    12# Formalization notes
    13
    14By the definition of extensions, the nodes at depth j of tree_{k,q}(a)
    15are the trees tree_{k+j,q−j}(v̄) of the tuples v̄ = (v₀, …, v_j) with
    16v₀ = a in which every vᵢ with i ≥ 1 is within distance ρ⁺(k+i, q−i) of
    17an earlier entry. The statement is made for these tuples. The root label
    18of the node is atp_{k+j,q−j}(v̄), which consists of the atoms that hold.
    19An atom mentions the color Y if it is Y(xᵢ) or dist(xᵢ, Y) < r.
    20
    21The paper assumes k ≥ 1, so that the single vertex a has a tree of
    22rank (k, q). The statement about guarded tuples does not need this
    23hypothesis, and it holds for all k.
    24-/
    25
    26namespace Lax185574.TreeLocality
    27
    28open Lax185574.PartialGraphs Lax185574.GaifmanGraph
    29open Lax185574.DistanceLogic Lax185574.DistanceLogic.DistFO Lax185574.TypeTrees
    30open Lax3.DistFO (rhoMinus rhoPlus)
    31
    32/-- The atom mentions the color `Y`. -/
    33def MentionsColor (Y : ℕ) {ℓ : ℕ} : DistFO ℓ → Prop
    34 | .color Y' _ => Y' = Y
    35 | .distColorLt _ Y' _ => Y' = Y
    36 | _ => False
    37
    38/-- **Locality of type trees.** A tuple reached from `v 0` by guarded
    39extensions lies in the ball of radius `ρ⁺(k, q)` around `v 0`, and so
    40does a vertex of every color mentioned in its atomic type. -/
    41axiom ball_of_guarded {V : Type*} (G : PartialGraph V) (k q j : ℕ) (hj : j ≤ q)
    42 (v : Fin (j + 1) → V)
    43 (hv : ∀ i : Fin (j + 1), 0 < i.val → ∃ i' : Fin (j + 1), i'.val < i.val ∧
    44 WithinDist G.resolved (rhoPlus (k + i.val) (q - i.val)) (v i') (v i)) :
    45 (∀ i, v i ∈ G.ball (rhoPlus k q) (v 0)) ∧
    46 ∀ φ ∈ atp G (k + j) (q - j) v, ∀ Y : ℕ, MentionsColor Y φ →
    47 ∃ u ∈ G.ball (rhoPlus k q) (v 0), G.color u = Y
    48
    49end Lax185574.TreeLocality
    50
    Show Proof
    Formalization notes

    By the definition of extensions, the nodes at depth j of tree_{k,q}(a) are the trees tree_{k+j,q−j}(v̄) of the tuples v̄ = (v₀, …, v_j) with v₀ = a in which every vᵢ with i ≥ 1 is within distance ρ⁺(k+i, q−i) of an earlier entry. The statement is made for these tuples. The root label of the node is atp_{k+j,q−j}(v̄), which consists of the atoms that hold. An atom mentions the color Y if it is Y(xᵢ) or dist(xᵢ, Y) < r.

    The paper assumes k ≥ 1, so that the single vertex a has a tree of rank (k, q). The statement about guarded tuples does not need this hypothesis, and it holds for all k.

    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…