Lax Lean Archive

Rank shift of type trees

Lax185574.RankShift · concepts/Lax185574/RankShift.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 a polynomial-time algorithm which maps tree_{k,q}(ā) to tree_{k+1,q−1}(ā) for all k ∈ ℕ, q ≥ 1, partial graphs G and nonempty ā ∈ V(G)^{≤k}.

    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: Rank shift of type trees
    7type: lemma
    8---
    9There is a polynomial-time algorithm which maps tree_{k,q}(ā) to
    10tree_{k+1,q−1}(ā) for all k ∈ ℕ, q ≥ 1, partial graphs G and nonempty
    11ā ∈ V(G)^{≤k}.
    12
    13# Formalization notes
    14
    15The algorithm is an algorithm in the sense of `Lax185574.Algorithms`,
    16one for all k and q. Polynomial time means time `O((N + 1)^a)` on an
    17input of length `N`, where the degree `a` and the constant `c` may
    18depend on k and q. The paper says polynomial time, with no subscript,
    19so this is weaker than a degree independent of k and q. It suffices,
    20since k and q are fixed in every use. q ≥ 1 is written as q + 1.
    21-/
    22
    23namespace Lax185574.RankShift
    24
    25open Lax185574.Encoding Lax185574.Algorithms
    26open Lax185574.PartialGraphs Lax185574.TypeTrees
    27
    28/-- **Rank shift.** One algorithm computes `tree_{k+1,q}(u)` from
    29`tree_{k,q+1}(u)` in polynomial time. -/
    30axiom exists_program_shift :
    31 ∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
    32 ∀ (n : ℕ) (G : PartialGraph (Fin n)) (ℓ : ℕ) (u : Fin ℓ → Fin n), 1 ≤ ℓ → ℓ ≤ k →
    33 A.Computes c (tree G k (q + 1) u) (tree G (k + 1) q u)
    34 (((encode (tree G k (q + 1) u)).length + 1) ^ a)
    35
    36end Lax185574.RankShift
    37
    Show Proof
    Formalization notes

    The algorithm is an algorithm in the sense of Lax185574.AlgorithmsLax185574.Algorithms, one for all k and q. Polynomial time means time O((N+1)a)O((N + 1)^a) on an input of length NN, 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. q ≥ 1 is written as q + 1.

    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…