Lax Lean Archive

Ordered coordinate restriction of type trees

Lax185574.Restriction · concepts/Lax185574/Restriction.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, tuples w̄ ∈ V(G)^ℓ with ℓ ≤ k and ordered lists J of distinct positions in [ℓ],

    tree_{k,q}(w̄) ↾ J = tree_{k,q}(w̄ ↾ J).

    Given τ and J one can compute τ ↾ J in time polynomial in ‖τ‖.

    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 43 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.TypeTrees
    2import Lax185574.Algorithms
    3
    4/-!
    5---
    6title: Ordered coordinate restriction of type trees
    7type: lemma
    8---
    9There is an operation ↾ on type trees such that for all k, q ∈ ℕ,
    10partial graphs G, tuples w̄ ∈ V(G)^ℓ with ℓ ≤ k and ordered lists J of
    11distinct positions in [ℓ],
    12
    13 tree_{k,q}(w̄) ↾ J = tree_{k,q}(w̄ ↾ J).
    14
    15Given τ and J one can compute τ ↾ J in time polynomial in ‖τ‖.
    16
    17# Formalization notes
    18
    19The operation is given by one algorithm in the sense of
    20`Lax185574.Algorithms`, for all k and q. Its input is the pair of the
    21tree and J, a list of positions. Positions are counted from 0. The tuple
    22w̄ ↾ J has the entries w_{j₁}, …, w_{j_p}. The size ‖τ‖ is the length of
    23the encoding of τ, and the time is `O((‖τ‖ + 1)^a)`, where the degree
    24`a` and the constant `c` may depend on k and q. The paper says
    25polynomial time, with no subscript, so this is weaker than a degree
    26independent of k and q. It suffices, since k and q are fixed in every
    27use.
    28-/
    29
    30namespace Lax185574.Restriction
    31
    32open Lax185574.Encoding Lax185574.Algorithms
    33open Lax185574.PartialGraphs Lax185574.TypeTrees
    34
    35/-- **Ordered coordinate restriction.** One algorithm computes
    36`tree_{k,q}(u ↾ J)` from `tree_{k,q}(u)` and `J`, in time polynomial in
    37the size of the tree. -/
    38axiom exists_program_restrict :
    39 ∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
    40 ∀ (n : ℕ) (G : PartialGraph (Fin n)) (ℓ : ℕ) (u : Fin ℓ → Fin n) (J : List (Fin ℓ)),
    41 ℓ ≤ k → J.Nodup →
    42 A.Computes c (tree G k q u, J) (tree G k q (fun i => u (J.get i)))
    43 (((encode (tree G k q u)).length + 1) ^ a)
    44
    45end Lax185574.Restriction
    46
    Show Proof
    Formalization notes

    The operation is given by one algorithm in the sense of Lax185574.AlgorithmsLax185574.Algorithms, for all k and q. Its input is the pair of the tree and J, a list of positions. Positions are counted from 0. The tuple w̄ ↾ J has the entries w_{j₁}, …, w_{j_p}. The size ‖τ‖ is the length of the encoding of τ, and the time is O((‖τ‖+1)a)O((‖τ‖ + 1)^a), where the degree aa and the constant cc may depend on k and q. The paper says polynomial time, with no subscript, so this is weaker than a degree independent of k and q. It suffices, since k and q are fixed in every use.

    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…