Types are determined by types in a neighborhood
Lax185574.LocalToGlobal · concepts/Lax185574/LocalToGlobal.lean · lax-185574
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
For all k, q, α ∈ ℕ there is a number q' = q'(k, q, α) such that with h ≔ 7^q the following holds. Let σ be a relational signature of arity at most α and A a σ-structure. Then, for all ā ∈ V(A)^k and B ⊇ Ball^A_h(ā), the type tp^A_q(ā) depends only on tp^{A[B]}_{q'}(ā).
This is a corollary of Gaifman's locality theorem. The point is that h depends on q alone, and q' does not depend on the signature beyond its arity. The latter matters when the signature has one unary symbol per part of a partition with up to n parts. The paper states that h = h(q) is computable, and its proof takes h = 7^q. The statement here names this value, because algorithms downstream compute the radius from q.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
In the paper
- page 17 of this submission's paper
Lean source view on GitHub
| 1 | import Lax185574.FirstOrderTypes |
| 2 | import Lax185574.GaifmanGraph |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Types are determined by types in a neighborhood |
| 7 | type: theorem |
| 8 | --- |
| 9 | For all k, q, α ∈ ℕ there is a number q' = q'(k, q, α) such that with |
| 10 | h ≔ 7^q the following holds. Let σ be a relational signature of arity at most |
| 11 | α and A a σ-structure. Then, for all ā ∈ V(A)^k and B ⊇ Ball^A_h(ā), |
| 12 | the type tp^A_q(ā) depends only on tp^{A[B]}_{q'}(ā). |
| 13 | |
| 14 | This is a corollary of Gaifman's locality theorem. The point is that h |
| 15 | depends on q alone, and q' does not depend on the signature beyond its |
| 16 | arity. The latter matters when the signature has one unary symbol per |
| 17 | part of a partition with up to n parts. The paper states that h = h(q) |
| 18 | is computable, and its proof takes h = 7^q. The statement here names |
| 19 | this value, because algorithms downstream compute the radius from q. |
| 20 | |
| 21 | # Formalization notes |
| 22 | |
| 23 | "Depends only on" is stated pairwise. If ā with B ⊇ Ball_h(ā) and b̄ with |
| 24 | B' ⊇ Ball_h(b̄) have the same type of rank q' in A[B] and A[B'] |
| 25 | respectively, then they have the same type of rank q in A. The tuples |
| 26 | are given as tuples of B and B', and their images in A are their |
| 27 | coordinates. Types without parameters are compared as sets of formulas |
| 28 | of one fixed language, so types in different substructures are |
| 29 | comparable. |
| 30 | |
| 31 | The paper states the lemma for finite signatures, with h and q' |
| 32 | computable. Here the signature is any relational language with relation |
| 33 | symbols of arity at most α, possibly infinitely many. This is the |
| 34 | generality that the lemma is applied in, as the language of partial |
| 35 | graphs has a unary symbol for every natural number. For an infinite |
| 36 | signature the statement follows from the finite case, applied to the |
| 37 | finitely many symbols of each formula, since q' does not depend on the |
| 38 | signature. The structure is finite. The radius is h = 7^q. The rank q' only exists, as no algorithm |
| 39 | uses it. |
| 40 | -/ |
| 41 | |
| 42 | namespace Lax185574.LocalToGlobal |
| 43 | |
| 44 | open FirstOrder FirstOrder.Language |
| 45 | open Lax185574.FirstOrderTypes Lax185574.GaifmanGraph |
| 46 | |
| 47 | universe u v z |
| 48 | |
| 49 | /-- **Local-to-global types.** For a relational structure of arity at |
| 50 | most `α`, the type of quantifier rank `q` of a `k`-tuple is determined |
| 51 | by its type of quantifier rank `q'` in any induced substructure that |
| 52 | contains its ball of radius `7^q`. -/ |
| 53 | axiom rankType_eq_of_rankType_induced_eq (k q α : ℕ) : |
| 54 | ∃ q' : ℕ, ∀ (L : Language.{u, v}) [L.IsRelational], |
| 55 | (∀ l, α < l → IsEmpty (L.Relations l)) → |
| 56 | ∀ (V : Type z) [Finite V] [L.Structure V] (B B' : Set V) |
| 57 | (a : Fin k → B) (b : Fin k → B'), |
| 58 | ball L (7 ^ q) (Subtype.val ∘ a) ⊆ B → |
| 59 | ball L (7 ^ q) (Subtype.val ∘ b) ⊆ B' → |
| 60 | @rankType L B (induced B) q' k a = @rankType L B' (induced B') q' k b → |
| 61 | rankType (L := L) q (Subtype.val ∘ a) = rankType (L := L) q (Subtype.val ∘ b) |
| 62 | |
| 63 | end Lax185574.LocalToGlobal |
| 64 |
Formalization notes
"Depends only on" is stated pairwise. If ā with B ⊇ Ball_h(ā) and b̄ with B' ⊇ Ball_h(b̄) have the same type of rank q' in A[B] and A[B'] respectively, then they have the same type of rank q in A. The tuples are given as tuples of B and B', and their images in A are their coordinates. Types without parameters are compared as sets of formulas of one fixed language, so types in different substructures are comparable.
The paper states the lemma for finite signatures, with h and q' computable. Here the signature is any relational language with relation symbols of arity at most α, possibly infinitely many. This is the generality that the lemma is applied in, as the language of partial graphs has a unary symbol for every natural number. For an infinite signature the statement follows from the finite case, applied to the finitely many symbols of each formula, since q' does not depend on the signature. The structure is finite. The radius is h = 7^q. The rank q' only exists, as no algorithm uses it.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments