Lax Lean Archive

Lifting type trees through a resolve

Lax185574.ResolveLift · concepts/Lax185574/ResolveLift.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 ∈ ℕ. Given a partial graph G, its distance matrix D_G, colors P, Q, a sign ±, and (tree^G_{k,q}(a) : a ∈ V(G)), one can compute H = resolve^±{P,Q}(G), its distance matrix D_H, and (tree^H{k,q}(a) : a ∈ V(G)) in time

    |G|² · poly_{k,q}(M + T),

    where

    M = max_{a ∈ V(G)} ‖tree^G_{k,q}(a)‖, T = max_{a ∈ V(G)} |{tree^G_{k+i,q−i}(v̄) | 0 ≤ i ≤ q, ℓ ∈ [k+i], v̄ ∈ (Ball^H_{ρ⁺(k,q)}(a))^ℓ}|.

    Each output tree has size poly_{k,q}(T).

    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 48 of this submission's paper
    • page 12 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.TypeTrees
    2import Lax185574.ConstructionSequences
    3import Lax185574.DistanceMatrix
    4import Lax185574.Algorithms
    5
    6/-!
    7---
    8title: Lifting type trees through a resolve
    9type: lemma
    10---
    11Let k ≥ 1 and q ∈ ℕ. Given a partial graph G, its distance matrix D_G,
    12colors P, Q, a sign ±, and (tree^G_{k,q}(a) : a ∈ V(G)), one can compute
    13H = resolve^±_{P,Q}(G), its distance matrix D_H, and
    14(tree^H_{k,q}(a) : a ∈ V(G)) in time
    15
    16 |G|² · poly_{k,q}(M + T),
    17
    18where
    19
    20 M = max_{a ∈ V(G)} ‖tree^G_{k,q}(a)‖,
    21 T = max_{a ∈ V(G)} |{tree^G_{k+i,q−i}(v̄) | 0 ≤ i ≤ q, ℓ ∈ [k+i],
    22 v̄ ∈ (Ball^H_{ρ⁺(k,q)}(a))^ℓ}|.
    23
    24Each output tree has size poly_{k,q}(T).
    25
    26# Formalization notes
    27
    28The algorithm is an algorithm in the sense of `Lax185574.Algorithms`,
    29one for all k and q. Its input is the tuple of G, its distance matrix,
    30P, Q, the sign and the family of type trees, with the encodings of
    31`Lax185574.Encodings`. The sign is a Boolean, `true` for + and `false`
    32for −. The output is the triple of H, its distance matrix and the new
    33family. The partial graph is on `Fin n`, so |G| = n. M is
    34`maxTreeSize G k q`, the time is `O(n² · (M + T + 1)^a)`, and each new
    35tree has an encoding of length at most `c · (T + 1)^a`, where the degree
    36`a` and the constant `c` may depend on k and q. The second factor of
    37the time is increased by one, so that it is positive. The set in the
    38definition of T collects trees of G of tuples from balls in H.
    39-/
    40
    41namespace Lax185574.ResolveLift
    42
    43open Lax185574.Encoding Lax185574.Algorithms
    44open Lax185574.PartialGraphs Lax185574.TypeTrees Lax185574.ConstructionSequences
    45open Lax185574.DistanceMatrix
    46open Lax3.DistFO (rhoMinus rhoPlus)
    47
    48variable {n : ℕ}
    49
    50/-- `resolve^±_{P,Q}(G)`, positive for `true`. -/
    51def resolveBy (G : PartialGraph (Fin n)) (s : Bool) (P Q : ℕ) : PartialGraph (Fin n) :=
    52 if s then resolvePos G P Q else resolveNeg G P Q
    53
    54/-- The parameter `T`: the largest number of type trees in `G` of
    55tuples from a ball of radius `ρ⁺(k, q)` in `H`, over all ranks
    56`(k+i, q−i)` and arities `ℓ ∈ [k+i]`. -/
    57noncomputable def treeCount (G H : PartialGraph (Fin n)) (k q : ℕ) : ℕ :=
    58 Finset.univ.sup fun a : Fin n =>
    59 Set.ncard {τ : TypeTree | ∃ (i ℓ : ℕ) (v : Fin ℓ → Fin n), i ≤ q ∧ 1 ≤ ℓ ∧ ℓ ≤ k + i ∧
    60 (∀ j, v j ∈ H.ball (rhoPlus k q) a) ∧ τ = tree G (k + i) (q - i) v}
    61
    62/-- **Resolve lift.** One algorithm computes the partial graph `H` after
    63a resolve, its distance matrix and the type trees of all vertices in it,
    64from the partial graph `G` before, its distance matrix, `P`, `Q`, the
    65sign and its type trees, in time `O(n² · (M + T + 1)^a)`. Each new tree
    66has size `O((T + 1)^a)`. -/
    67axiom exists_program_resolveLift :
    68 ∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
    69 ∀ (n : ℕ) (G : PartialGraph (Fin n)) (P Q : ℕ) (s : Bool), 1 ≤ k →
    70 let H := resolveBy G s P Q
    71 let T := treeCount G H k q
    72 A.Computes c (G, distMatrix G, P, Q, s, family G k q) (H, distMatrix H, family H k q)
    73 (n ^ 2 * (maxTreeSize G k q + T + 1) ^ a) ∧
    74 ∀ b : Fin n, (encode (tree H k q ![b])).length ≤ c * (T + 1) ^ a
    75
    76end Lax185574.ResolveLift
    77
    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, its distance matrix, P, Q, the sign and the family of type trees, with the encodings of Lax185574.EncodingsLax185574.Encodings. The sign is a Boolean, truetrue for + and falsefalse for −. The output is the triple of H, its distance matrix and the new family. The partial graph is on FinnFin n, so |G| = n. M is maxTreeSizeGkqmaxTreeSize G k q, the time is O(n2⋅(M+T+1)a)O(n² · (M + T + 1)^a), and each new tree has an encoding of length at most c⋅(T+1)ac · (T + 1)^a, where the degree aa and the constant cc may depend on k and q. The second factor of the time is increased by one, so that it is positive. The set in the definition of T collects trees of G of tuples from balls in H.

    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…