Lax Lean Archive

Few types far from a parameter set, with a fixed tuple of parameters

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

    For every q, k, c ∈ ℕ there are numbers r = r(q) and T = T(q, k, c) with the following property. Let H be a graph expanded by at most c unary predicates and U ⊆ V(H). Fix a tuple ū of vertices of U of finite length. Let F ≔ { a ∈ V(H) : dist^H(a, U) > r }. Then

    |{ tp^H_q(ā ū/U) : ā ∈ F^k }| ≤ T(q, k, c).

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

    Lean source view on GitHub

    1import Lax185574.Colorings
    2import Lax185574.FirstOrderTypes
    3import Lax185574.GraphBalls
    4
    5/-!
    6---
    7title: Few types far from a parameter set, with a fixed tuple of parameters
    8type: lemma
    9---
    10For every q, k, c ∈ ℕ there are numbers r = r(q) and T = T(q, k, c)
    11with the following property. Let H be a graph expanded by at most c
    12unary predicates and U ⊆ V(H). Fix a tuple ū of vertices of U of finite
    13length. Let F ≔ { a ∈ V(H) : dist^H(a, U) > r }. Then
    14
    15 |{ tp^H_q(ā ū/U) : ā ∈ F^k }| ≤ T(q, k, c).
    16
    17# Formalization notes
    18
    19The quantifier order is that of `SeparatingTypes`: r depends on q only,
    20and T on q, k and c only. In particular T does not depend on the length
    21m of ū. The tuple ā ū is the concatenation `Fin.append ā ū` of length
    22k + m. The far set F is the complement of the ball Ball^H_r[U] of
    23`GraphBalls.graphBall`. As in `SeparatingTypes`, the graph
    24is finite and its expansion has exactly c, possibly empty, color sets.
    25-/
    26
    27namespace Lax185574.SeparatingTypesTuples
    28
    29open FirstOrder FirstOrder.Language Lax710763.Transductions
    30open Lax185574.FirstOrderTypes Lax185574.Colorings Lax185574.GraphBalls
    31
    32universe z
    33
    34/-- **Few types far from a parameter set, with fixed parameters.** For a
    35fixed tuple `ū` from `U`, the tuples `ā ū` with `ā` a `k`-tuple far from
    36`U` realize at most `T(q, k, c)` types of quantifier rank `q` over `U`,
    37independently of the length of `ū`. -/
    38axiom ncard_rankTypeOver_append_le (q : ℕ) :
    39 ∃ r : ℕ, ∀ k c : ℕ, ∃ T : ℕ,
    40 ∀ (V : Type z) [Finite V] (G : SimpleGraph V) (colors : Fin c → Set V)
    41 (U : Set V) (m : ℕ) (u : Fin m → V), (∀ i, u i ∈ U) →
    42 ((fun a : Fin k → V =>
    43 @rankTypeOver (withColors Language.graph c) V (expansion G colors) q U
    44 (k + m) (Fin.append a u)) ''
    45 {a | ∀ i, a i ∉ graphBall G r U}).ncard ≤ T
    46
    47end Lax185574.SeparatingTypesTuples
    48
    Show Proof
    Formalization notes

    The quantifier order is that of SeparatingTypesSeparatingTypes: r depends on q only, and T on q, k and c only. In particular T does not depend on the length m of ū. The tuple ā ū is the concatenation Fin.append ā ū of length k + m. The far set F is the complement of the ball Ball^H_r[U] of GraphBalls.graphBallGraphBalls.graphBall. As in SeparatingTypesSeparatingTypes, the graph is finite and its expansion has exactly c, possibly empty, color sets.

    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…