Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Tree decompositions from recursive balanced separators

Lax263307.SeparatorDecompositions · concepts/Lax263307/SeparatorDecompositions.lean · lax-263307

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

    Theorem

    Attach the decompositions of the parts below a new root bag containing the separator, and add the separator to every child bag. The resulting bags have size at most the separator size plus the largest child bag. Recursing on balanced parts costs at most one separator bound per recursion level.

    Concept map
    9 concepts; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 glue_bound proven

    2 recursive_bag_bound proven

    Lean source view on GitHub

    1import Lax263307.SeparatorComponents
    2import Lax263307.EdgeSublinearSeparators
    3import Lax263307.RecursionDepth
    4import Lax228581.Treewidth
    5
    6/-!
    7---
    8title: Tree decompositions from recursive balanced separators
    9type: theorem
    10---
    11Attach the decompositions of the parts below a new root bag containing the
    12separator, and add the separator to every child bag. The resulting bags have
    13size at most the separator size plus the largest child bag. Recursing on
    14balanced parts costs at most one separator bound per recursion level.
    15
    16# Formalization notes
    17
    18The component trees may have different finite node types. The joining tree
    19uses a disjoint dependent sum of these types and one additional root. The
    20recursive bound keeps its logarithmic depth explicit; conversion to an
    21edge-only sublinear bound is a separate step.
    22-/
    23
    24namespace Lax263307.SeparatorDecompositions
    25
    26open GraphClasses EdgeSublinearSeparators SeparatorComponents Lax228581.Treewidth
    27
    28/-- Join the component decompositions below a separator root. -/
    29axiom glue_bound {n : ℕ} (G : SimpleGraph (Fin n)) (S : Finset (Fin n))
    30 {ι : Type} [Fintype ι] (P : Partition G S ι)
    31 (D : ∀ i, TreeDecomposition (G.induce (↑(P.vertices i) : Set (Fin n))))
    32 (B : ℕ) (bound : ∀ i j, ((D i).bag j).card ≤ B) :
    33 ∃ E : TreeDecomposition G, ∀ j, (E.bag j).card ≤ S.card + B
    34
    35/-- Balanced recursive separators give a logarithmic depth bag bound. -/
    36axiom recursive_bag_bound (C : GraphClass) (hereditary : IsHereditary C)
    37 (B : ℕ → ℕ) (monotone : Monotone B) (positive : ∀ m, 1 ≤ B m)
    38 (separators : ∀ n (G : SimpleGraph (Fin n)), G ∈ C n →
    39 ∃ S : Finset (Fin n), IsBalancedSeparator G S ∧ S.card ≤ B G.edgeSet.ncard)
    40 {n : ℕ} (G : SimpleGraph (Fin n)) (member : G ∈ C n) :
    41 ∃ D : TreeDecomposition G, ∀ j,
    42 (D.bag j).card ≤ B G.edgeSet.ncard * (RecursionDepth.depth n + 1)
    43
    44end Lax263307.SeparatorDecompositions
    45
    Show ProofShow Proof
    Formalization notes

    The component trees may have different finite node types. The joining tree uses a disjoint dependent sum of these types and one additional root. The recursive bound keeps its logarithmic depth explicit; conversion to an edge-only sublinear bound is a separate step.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…