Lax Lean Archive

Type tree sizes

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

    Let k ≥ 1 and q ∈ ℕ, and put r = ρ⁺(k, q) and d = r + k + q. The following holds for every partial graph G.

    1. |{tree^G_{k+i,q−i}(v̄) | v̄ ∈ X^ℓ}| ≤ |Types^G_{d,d}(X)| for all i ∈ {0, …, q}, ℓ ∈ [k+i] and X ⊆ V(G).
    2. ‖tree^G_{k,q}(a)‖ ≤ poly_{k,q}(|Types^G_{d,d}(Ball^G_r(a))|) for every a ∈ V(G).
    Concept map
    15 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 tree_length_le proven

    2 treeCount_le proven

    In the paper

    • page 52 of this submission's paper
    • page 10 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.TypeTrees
    2import Lax185574.Width
    3
    4/-!
    5---
    6title: Type tree sizes
    7type: lemma
    8---
    9Let k ≥ 1 and q ∈ ℕ, and put r = ρ⁺(k, q) and d = r + k + q. The
    10following holds for every partial graph G.
    11
    121. |{tree^G_{k+i,q−i}(v̄) | v̄ ∈ X^ℓ}| ≤ |Types^G_{d,d}(X)| for all
    13 i ∈ {0, …, q}, ℓ ∈ [k+i] and X ⊆ V(G).
    142. ‖tree^G_{k,q}(a)‖ ≤ poly_{k,q}(|Types^G_{d,d}(Ball^G_r(a))|) for every
    15 a ∈ V(G).
    16
    17# Formalization notes
    18
    19Types^G_{d,d}(X) is counted by `Lax185574.Width.partialTypeCount`, the
    20number of first-order types of quantifier rank d of d-tuples from X in
    21the partial graph G. The vertices are `Fin n`. The polynomial of the
    22second part has a constant and a degree depending on k and q.
    23-/
    24
    25namespace Lax185574.TypeTreeSizes
    26
    27open Lax185574.PartialGraphs Lax185574.Encoding Lax185574.TypeTrees Lax185574.Width
    28open Lax3.DistFO (rhoMinus rhoPlus)
    29
    30/-- **Type tree sizes, counting.** The number of type trees of tuples
    31from `X` is at most the number of `d`-types of `d`-tuples from `X`. -/
    32axiom treeCount_le {n : ℕ} (G : PartialGraph (Fin n)) (k q : ℕ) (hk : 1 ≤ k)
    33 (i ℓ : ℕ) (hi : i ≤ q) (hℓ : 1 ≤ ℓ) (hℓk : ℓ ≤ k + i) (X : Set (Fin n)) :
    34 Set.ncard {τ : TypeTree | ∃ v : Fin ℓ → Fin n, (∀ j, v j ∈ X) ∧ τ = tree G (k + i) (q - i) v} ≤
    35 partialTypeCount G (rhoPlus k q + k + q) (rhoPlus k q + k + q) X
    36
    37/-- **Type tree sizes, size.** The size of the type tree of a vertex is
    38polynomial in the number of `d`-types of `d`-tuples from its ball. -/
    39axiom tree_length_le (k q : ℕ) (hk : 1 ≤ k) :
    40 ∃ c a : ℕ, ∀ (n : ℕ) (G : PartialGraph (Fin n)) (v : Fin n),
    41 wordLength (tree G k q ![v]) ≤
    42 c * (partialTypeCount G (rhoPlus k q + k + q) (rhoPlus k q + k + q)
    43 (G.ball (rhoPlus k q) v) + 1) ^ a
    44
    45end Lax185574.TypeTreeSizes
    46
    Show ProofShow Proof
    Formalization notes

    Types^G_{d,d}(X) is counted by Lax185574.Width.partialTypeCountLax185574.Width.partialTypeCount, the number of first-order types of quantifier rank d of d-tuples from X in the partial graph G. The vertices are FinnFin n. The polynomial of the second part has a constant and a degree depending on k and q.

    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…