Lax Lean Archive

Computing the scatter type

Lax185574.ComputeScatterType · concepts/Lax185574/ComputeScatterType.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 algorithm which, given a nonempty partial graph G, numbers k ≥ 1 and q ∈ ℕ, its distance matrix D_G, and the family (tree_{k,q}(a) : a ∈ V(G)), computes stp^G_{k,q} in time

    |G|² · poly_{k,q}(max_{a ∈ V(G)} ‖tree_{k,q}(a)‖).

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

    Lean source view on GitHub

    1import Lax185574.ScatterTypes
    2import Lax185574.DistanceMatrix
    3import Lax185574.Algorithms
    4
    5/-!
    6---
    7title: Computing the scatter type
    8type: lemma
    9---
    10There is an algorithm which, given a nonempty partial graph G, numbers
    11k ≥ 1 and q ∈ ℕ, its distance matrix D_G, and the family
    12(tree_{k,q}(a) : a ∈ V(G)), computes stp^G_{k,q} in time
    13
    14 |G|² · poly_{k,q}(max_{a ∈ V(G)} ‖tree_{k,q}(a)‖).
    15
    16# Formalization notes
    17
    18The algorithm is an algorithm in the sense of `Lax185574.Algorithms`,
    19one for all k and q. Its input is the tuple of G, k, q, the distance
    20matrix and the family of type trees, with the encodings of
    21`Lax185574.Encodings`. The partial graph is on `Fin n`, so |G| = n, and
    22it is nonempty when 1 ≤ n. The output is the scatter type, a finite set
    23as in `Lax185574.ScatterTypes`. The largest size of a tree of the
    24family is `maxTreeSize G k q`, and the time is
    25`O(n² · (maxTreeSize G k q + 1)^a)`, where the degree `a` and the
    26constant `c` may depend on k and q. The second factor is increased by
    27one, so that it is positive.
    28-/
    29
    30namespace Lax185574.ComputeScatterType
    31
    32open Lax185574.Encoding Lax185574.Algorithms
    33open Lax185574.PartialGraphs Lax185574.ScatterTypes Lax185574.TypeTrees
    34open Lax185574.DistanceMatrix
    35
    36/-- **Computing the scatter type.** One algorithm computes `stp^G_{k,q}`
    37from `G`, `k`, `q`, the distance matrix `D_G` and the type trees of all
    38vertices, in time quadratic in `n` and polynomial in the largest size of
    39a tree. -/
    40axiom exists_program_stp :
    41 ∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
    42 ∀ (n : ℕ) (G : PartialGraph (Fin n)), 1 ≤ k → 1 ≤ n →
    43 A.Computes c (G, k, q, distMatrix G, family G k q) (stp G k q)
    44 (n ^ 2 * (maxTreeSize G k q + 1) ^ a)
    45
    46end Lax185574.ComputeScatterType
    47
    Show Proof
    Formalization notes

    The algorithm is an algorithm in the sense of Lax185574.AlgorithmsLax185574.Algorithms, one for all k and q. Its input is the tuple of G, k, q, the distance matrix and the family of type trees, with the encodings of Lax185574.EncodingsLax185574.Encodings. The partial graph is on FinnFin n, so |G| = n, and it is nonempty when 1 ≤ n. The output is the scatter type, a finite set as in Lax185574.ScatterTypesLax185574.ScatterTypes. The largest size of a tree of the family is maxTreeSizeGkqmaxTreeSize G k q, and the time is O(n2⋅(maxTreeSizeGkq+1)a)O(n² · (maxTreeSize G k q + 1)^a), where the degree aa and the constant cc may depend on k and q. The second factor is increased by one, so that it is positive.

    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…