Lax Lean Archive

Far composition of type trees

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

    There is an operation ∗ on type trees such that for all k, q ∈ ℕ, partial graphs G and nonempty tuples ā₁, ā₂ with |ā₁ ā₂| ≤ k and dist(ā₁, ā₂) > ρ⁻(k, q),

    tree_{k,q}(ā₁) ∗ tree_{k,q}(ā₂) = tree_{k,q}(ā₁ ā₂).

    Given τ₁ and τ₂ one can compute τ₁ ∗ τ₂ in time poly_{k,q}(‖τ₁‖ + ‖τ₂‖).

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

    Lean source view on GitHub

    1import Lax185574.TypeTrees
    2import Lax185574.Algorithms
    3
    4/-!
    5---
    6title: Far composition of type trees
    7type: lemma
    8---
    9There is an operation ∗ on type trees such that for all k, q ∈ ℕ,
    10partial graphs G and nonempty tuples ā₁, ā₂ with |ā₁ ā₂| ≤ k and
    11dist(ā₁, ā₂) > ρ⁻(k, q),
    12
    13 tree_{k,q}(ā₁) ∗ tree_{k,q}(ā₂) = tree_{k,q}(ā₁ ā₂).
    14
    15Given τ₁ and τ₂ one can compute τ₁ ∗ τ₂ in time poly_{k,q}(‖τ₁‖ + ‖τ₂‖).
    16
    17# Formalization notes
    18
    19The paper adapts Lemma 3.1 of its locality note. The operation is given
    20by one algorithm in the sense of `Lax185574.Algorithms`, for all k and
    21q, whose input is the pair of the two trees. The size ‖τ‖ is the length
    22of the encoding of τ, and the time is `O((‖τ₁‖ + ‖τ₂‖ + 1)^a)`, where the
    23degree `a` and the constant `c` may depend on k and q.
    24dist(ā₁, ā₂) > r means that no entry of ā₁ is within distance r of an
    25entry of ā₂.
    26-/
    27
    28namespace Lax185574.FarComposition
    29
    30open Lax185574.Encoding Lax185574.Algorithms
    31open Lax185574.PartialGraphs Lax185574.GaifmanGraph Lax185574.TypeTrees
    32open Lax3.DistFO (rhoMinus rhoPlus)
    33
    34/-- **Far composition.** One algorithm computes the type tree of the
    35concatenation of two far tuples from their type trees, in time
    36polynomial in their sizes. -/
    37axiom exists_program_compose :
    38 ∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
    39 ∀ (n : ℕ) (G : PartialGraph (Fin n)) (ℓ₁ ℓ₂ : ℕ) (u₁ : Fin ℓ₁ → Fin n)
    40 (u₂ : Fin ℓ₂ → Fin n), 1 ≤ ℓ₁ → 1 ≤ ℓ₂ → ℓ₁ + ℓ₂ ≤ k →
    41 (∀ i j, ¬ WithinDist G.resolved (rhoMinus k q) (u₁ i) (u₂ j)) →
    42 A.Computes c (tree G k q u₁, tree G k q u₂) (tree G k q (Fin.append u₁ u₂))
    43 (((encode (tree G k q u₁)).length + (encode (tree G k q u₂)).length + 1) ^ a)
    44
    45end Lax185574.FarComposition
    46
    Show Proof
    Formalization notes

    The paper adapts Lemma 3.1 of its locality note. The operation is given by one algorithm in the sense of Lax185574.AlgorithmsLax185574.Algorithms, for all k and q, whose input is the pair of the two trees. The size ‖τ‖ is the length of the encoding of τ, and the time is O((‖τ1‖+‖τ2‖+1)a)O((‖τ₁‖ + ‖τ₂‖ + 1)^a), where the degree aa and the constant cc may depend on k and q. dist(ā₁, ā₂) > r means that no entry of ā₁ is within distance r of an entry of ā₂.

    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…